Re: [isabelle] Multiple simultaneous interpretations of a locale



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





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