Email Gateway (Aug 18 2022 at 12:27): Email Gateway (Aug 18 2022 at 12:27):From: Randy Pollack <rpollack@inf.ed.ac.uk>
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
Email Gateway (Aug 18 2022 at 12:27):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 08:18 UTC