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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
