Re: [isabelle] elim resolution with allE



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






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