[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.