[isabelle-dev] auto raises a TYPE exception

[Stefan Berghofer]

On 04/12/2013 02:18 PM, Makarius wrote:
> 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.

Hi Markus,

it is not particularly surprising that the attached example leads to a TYPE exception. A
closer look at the disagreement pairs

> [("\<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)")];

reveals that the variable ?n6 indeed appears with two distinct types: In lines 2 and 8, it has type
"nat => 'a => nat", whereas in lines 5 and 10, it has type "?'b10 => 'a => nat". This is clearly an
error, and therefore the exception is justified. An interesting question is why Thm.bicompose_aux
supplies these ill-formed disagreement pairs to Unify.unifiers in the first place.

Note that before the "reforms" mentioned above, most of the substitution functions used in unify.ML
simply ignored types and therefore were likely to produce ill-formed terms when applied to terms
containing variables with same name but different types.

Greetings,
Stefan