*To*: Fritz Lehmann <fritz.random.lehmann at googlemail.com>*Subject*: Re: [isabelle] elim resolution with allE*From*: Makarius <makarius at sketis.net>*Date*: Wed, 26 Mar 2008 15:05:05 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <8f1520400803251606o639687a3hb6fd8b5992dec14d@mail.gmail.com>*References*: <8f1520400803251606o639687a3hb6fd8b5992dec14d@mail.gmail.com>

On Wed, 26 Mar 2008, Fritz Lehmann wrote: > in the following proof I try to understand the elim resolution with allE: > 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) > > 1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> ALL z. ?P2(x,z) > 2. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a); ?P2(x,?z1(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.: > 1. !!x. [| P(?a); ~ (ALL x. P(?z1(x)) --> P(x)) |] ==> P(x) > > Looks similar to: > 1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x) > > but where comes the xa from (lifting over parameters?) and could you > find other errors in the step by step calculation? 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

**References**:**[isabelle] elim resolution with allE***From:*Fritz Lehmann

- Previous by Date: [isabelle] elim resolution with allE
- Next by Date: Re: [isabelle] Trouble selecting maximum element of locally linear relation
- Previous by Thread: [isabelle] elim resolution with allE
- Next by Thread: [isabelle] Intro, elim, dest modifiers
- Cl-isabelle-users March 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list