[isabelle] bug?



Consider the following two theory files:

-------  file LangExec.thy ---------
 theory LangExec imports Main begin

 typedecl state
 datatype com = Do "(state =>state set)"

 end
--------- file Hoare.thy ---------
 theory Hoare imports LangExec begin

 types
   'a pred = "'a => state => bool"
   'a cntxt = "('a pred \<times> com \<times> 'a pred)set"

 inductive
   Hoare :: "'a cntxt => 'a pred => com => 'a pred => bool"
			   ("_ \<stileturn>/ ({(1_)}/ (_)/ {(1_)})" 50)
 where
    HDo: "C \<stileturn> {%z s. \<forall>t \<in> f s . P z t} Do f {P}"

 thm Hoare.induct 

 inductive
   xxxx :: "'a cntxt => nat => 'a pred => com => 'a pred => bool"
			   ("_ \<stileturn>_, {_} _ {_}" 50)
 where
    xx1: "C \<stileturn>0, {%z s. \<forall>t \<in> f s . P z t} Do f {P}"

 thm Hoare.induct
------------------------------

Stepping through Hoare.thy in Isabelle2008, you will see that the last
inductive definition, xxxx, changes what is bound to Hoare.induct,
which seems like a bug.

Further, combining these two files into one file, the apparent bug
doesn't occur.

Best,
Randy

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.