# 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.*