Email Gateway (Aug 18 2022 at 10:54): Email Gateway (Aug 18 2022 at 10:54):From: Andreas Lochbihler <lochbihl@infosun.fim.uni-passau.de>
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
Email Gateway (Aug 18 2022 at 10:54):From: Makarius <makarius@sketis.net>
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" beginlemma liftI: "(!!a b. as b = Some a ==> P a) ==> lift as"
apply(clarsimp simp: lift_def)
by(case_tac "as b", auto)(* ... *)
endAlso, 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
likelemma "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
Last updated: May 03 2024 at 08:18 UTC