# 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  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.