Re: [isabelle] bug?



On Thu, 25 Sep 2008, Randy Pollack wrote:

>  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

The confusion originates from two sources:

  * The names of theory "Hoare" and const "Hoare" coincide, which causes 
    slightly odd name space accesses of Hoare.induct both via the global 
    theory prefix and the local specification prefix.  The second 
    inductive definition then overrides "Hoare.induct" via the theory 
    prefix, rendering the access via the previous const prefix 
    inaccesible.

    The usual convention is to keep theory names separate from anything 
    else, to prevent this kind of behaviour.

  * The inductive package is a bit simplistic in producing unqualified 
    accesses for the "induct" rule in the first place.  In the next round 
    of tuning the internal local theory interfaces we will include a way 
    to enforce qualification via the const prefix.


	Makarius





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