[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Wed, 10 Apr 2013, Makarius wrote:

> On Wed, 10 Apr 2013, Johannes Hölzl wrote:
>
>> Unfortunately, as you mentioned the excpetion_trace output is not very 
>> helpful, all I see is Seq.make / .copy / .append. The inner functions which 
>> call Envir.var_clash is not shown.
>
> It is relatively easy to instrument the main Seq.make abstraction itself. 
> Doing this, it points to Thm.bicompose_aux and Unify.unifiers, which is the 
> very core of "Isabelle" in the sense of the 1989 version.

Just for completeness, I am posting here a self-contained example to 
expose the problem.

It looks like I need to discuss it further with Stefan Berghofer, because 
he made some reforms there in 2005 that now seem to crash on us.


 	Makarius
-------------- next part --------------
theory Bad
imports "~~/src/HOL/Nat"
begin

ML {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}

ML "print_depth 1000"
ML {*
val dpairs =
  map (pairself (Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_schematic @{context})))
  [("\<And>xa\<Colon>'a. xa \<in> {a\<Colon>'a. (?j12\<Colon>'a \<Rightarrow> nat) xa + Suc ((?n13\<Colon>'a \<Rightarrow> nat) xa) \
    \ < Suc ((?n6\<Colon>nat \<Rightarrow> 'a \<Rightarrow> nat) (?j12 xa + Suc (?n13 xa)) a)} \<Longrightarrow> \
    \          (Q\<Colon>'b \<Rightarrow> bool) ((f\<Colon>'a \<Rightarrow> 'b) xa)",
    "\<And>xa\<Colon>'a. xa \<in> {a\<Colon>'a. (?n7\<Colon>?'b10 \<Rightarrow> 'a \<Rightarrow> nat) ((?a10\<Colon>'a \<Rightarrow> ?'b10) xa) a \
    \                      < Suc ((?n6\<Colon>?'b10 \<Rightarrow> 'a \<Rightarrow> nat) (?a10 xa) a)} \<Longrightarrow> \
    \          (Q\<Colon>'b \<Rightarrow> bool) ((f\<Colon>'a \<Rightarrow> 'b) xa)"),
   ("?n13\<Colon>'a \<Rightarrow> nat",
    "\<lambda>xa\<Colon>'a. (?n6\<Colon>nat \<Rightarrow> 'a \<Rightarrow> nat) ((?j12\<Colon>'a \<Rightarrow> nat) xa + Suc ((?n13\<Colon>'a \<Rightarrow> nat) xa)) xa"),
   ("\<lambda>xa\<Colon>?'b10. (?n7\<Colon>?'b10 \<Rightarrow> 'a \<Rightarrow> nat) xa (x\<Colon>'a)",
    "\<lambda>xa\<Colon>?'b10. (?n6\<Colon>?'b10 \<Rightarrow> 'a \<Rightarrow> nat) xa (x\<Colon>'a)")];
*}

ML {*
  Seq.pull (Unify.unifiers (@{theory}, Envir.empty 15, take 2 dpairs));
*}

ML {*
  Seq.pull (Unify.unifiers (@{theory}, Envir.empty 15, dpairs));
*}

end