# [isabelle] Multiple simultaneous interpretations of a locale

Hello all,
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.
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"
Is there any syntax to write this or is it just impossible to refer to
different interpretations of a locale in a single lemma? Is there
another concept in Isabelle which would serve my purposes better?
Regards,
Andreas Lochbihler

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