[isabelle] elim resolution with allE



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)
 1. !!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)
 1. !!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)

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?

Kind regards,

Fritz.





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