Email Gateway (Aug 18 2022 at 11:36): Email Gateway (Aug 18 2022 at 11:36):From: Fritz Lehmann <fritz.random.lehmann@googlemail.com>
Hi,
in the following proof I try to understand the elim resolution with allE:
--
Goal "EX y. ALL x. (P(y) --> P(x))";
br exCI 1;
br allI 1;
br impI 1;
Level 3 (1 subgoal)
EX y. ALL x. P(y) --> P(x)
!!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
val it = () : unit
be allE 1;
Level 4 (1 subgoal)
EX y. ALL x. P(y) --> P(x)
!!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
val it = () : unit
be (allI RSN (2,swap)) 1;
br impI 1;
be notE 1;
ba 1;
--
but I'm not sure about the several steps.
allE: [| ALL x. ?P(x); ?P(?x) ==> ?R |] ==> ?R
Don't care about name clashes:
[| ALL z. ?P1(z); ?P1(?z) ==> ?R1 |] ==> ?R1
Lifting over parameters:
[| !!x. ALL z. ?P2(x,z); !!x. ?P2(x,?z1(x)) ==> ?R2(x) |] ==> !!x. ?R2(x)
Lifting over assumptions:
[| !!x. ?K ==> ALL z. ?P2(x,z); !!x. ?K ==> (?P2(x,?z1(x)) ==> ?R2(x))
|] ==> !!x. ?K ==> ?R2(x)
(Elim-)Resolution with !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a)
|] ==> P(x):
?K := [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |]
?R2 := %x. P(x)
By assumption 1 (because of elim):
z := y
?P2 := %x z. ~(ALL x. P(z) --> P(x))
Remove 1., remove "ALL y. ~ (ALL x. P(y) --> P(x));" from 2.:
Looks similar to:
but where comes the xa from (lifting over parameters?) and could you
find other errors in the step by step calculation?
Kind regards,
Fritz.
Email Gateway (Aug 18 2022 at 11:36):From: Makarius <makarius@sketis.net>
Applying ?P2 to the local x and ?z1(x) results in beta reduction, i.e.
capture-avoiding substitution: the proper result is ~ (ALL xa. P(?y3(x))
--> P(xa)). In the first version ~ (ALL x. P(?z1(x)) --> P(x)) the x in
?z1(x) got captured by the inner ALL x quantifier.
BTW, your script uses rather ancient ML interfaces of Isabelle, which are
essentially obsolete (it seems you have studied the old Introduction to
Isabelle Manual). Here is a version using contempory Isabelle/Isar
syntax, also in HOL which is more convenient to write, with less
parentheses:
theory Scratch
imports Main
begin
lemma all_elim: "ALL z. B z ==> (B b ==> C) ==> C" by blast
lemma "EX y. ALL x. P y --> P x"
apply (rule exCI)
apply (rule allI)
apply (rule impI)
ML {* bind_thm ("r", Thm.lift_rule (Thm.cprem_of (#2 (Isar.goal ())) 1) @{thm all_elim}) *}
thm r
apply (erule allE)
apply (erule allI [THEN [2] swap])
apply (rule impI)
apply (erule notE)
apply assumption
done
end
By using distinctive variables from the very beginning, there is less
confusion with implicit renaming in the example. Moreover, I've asked the
system to do the lifting directly, cf. rule r.
Also note that your ?K in lifting over assumptions needs to mention the
local x in general, but your goal premises were independent of that by
accident.
If you really want to see how lifting works, here is the ML implementation
from Isabelle/src/Pure/logic.ML:
fun lift_all inc =
let
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
| lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
| lift Ts _ t = incr_indexes (rev Ts, inc) t;
in lift [] end;
This means the ==> and !! structure of the first term (from the subgoal)
is imposed on the second one (from the rule). The incr_indexes function is
defined in the same file. In Isabelle/src/Pure/thm.ML all of this will be
wrapped into the Thm.lift_rule inference.
Makarius
Last updated: May 03 2024 at 08:18 UTC