*To*: lochbihl at fim.uni-passau.de*Subject*: Re: [isabelle] Multiple simultaneous interpretations of a locale*From*: Makarius <makarius at sketis.net>*Date*: Sat, 20 Oct 2007 21:45:35 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <471874A7.90005@infosun.fim.uni-passau.de>*References*: <471874A7.90005@infosun.fim.uni-passau.de>

On Fri, 19 Oct 2007, Andreas Lochbihler wrote: > I'm working with a development snapshot of Isabelle (15 Oct 2007) and > got stuck when trying to employ locales with definitions inside. > My problem is how to refer to different interpretations of a single > locale in one lemma. > > The following example, which heavily simplifies the situation in my > theory, illustrates my problem: > > Suppose, I have a locale a which fixes a parameter function P and > defines a lift operator to lift the predicate to maps. > > locale a = > fixes P :: "'a => bool" > fixes lift :: "('b => 'a option) => bool" > defines lift_def: "lift as == !b. case as b of None => True | Some a > => P a" begin > > lemma liftI: "(!!a b. as b = Some a ==> P a) ==> lift as" > apply(clarsimp simp: lift_def) > by(case_tac "as b", auto) > > (* ... *) > end > > Also, there is predicate P, e.g. > > definition P :: "nat => bool" > where "P n == n > 0" > > which we want to lift: > > interpretation a [P] . > > Then, there is another predicate, say Q, which also must be lifted. > > definition Q :: "nat => bool" > where "Q n == n = 0" > > interpretation a [Q] . > Strangely, Isabelle issues a warning at this point, saying that it > replaces oly copies of the theorems Xpl.P_lift.lift_def and > Xpl.P_lift.liftI, i.e. if I refer to theorems generated by the > interpretation of a with parameter P, this now gives those for parameter > Q. This works by using separate name prefixes each interpretations. Moreover, local definitions are better expressed as definitions within the locale context, not as "defines" which are slightly outdated. Here is my version of the above: locale a = fixes P :: "'a => bool" begin definition lift :: "('b => 'a option) => bool" where "lift as <-> (ALL b. case as b of None => True | Some a => P a)" lemma liftI: "(!!a b. as b = Some a ==> P a) ==> lift as" unfolding lift_def by (auto split: option.splits) end definition P :: "nat => bool" where "P = (%n. n > 0)" interpretation P: a [P] . definition Q :: "nat => bool" where "Q = (%n. n = 0)" interpretation Q: a [Q] . > Now I want to prove that if Q lifted to a map as holds, then P does not > hold when lifted to the same map, i.e. I would like to write something > like > > lemma "Q.lift as ==> ~P.lift as" You can now write this, but cannot prove it. In fact the following holds: lemma "as = empty ==> Q.lift as <-> P.lift as" unfolding P.lift_def Q.lift_def by auto Makarius

**References**:**[isabelle] Multiple simultaneous interpretations of a locale***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Isabelle help
- Next by Date: Re: [isabelle] Isabelle help
- Previous by Thread: [isabelle] Multiple simultaneous interpretations of a locale
- Next by Thread: [isabelle] Simplifier question
- Cl-isabelle-users October 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list