--- a/src/Provers/split_paired_all.ML Tue Oct 20 18:04:23 1998 +0200
+++ b/src/Provers/split_paired_all.ML Wed Oct 21 11:10:38 1998 +0200
@@ -29,37 +29,31 @@
let
val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
- val surj_pair = Drule.unvarify raw_surj_pair;
+ val surj_pair = Drule.unvarify (standard raw_surj_pair);
val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []);
val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair));
val pT as Type (_, [aT, bT]) = fastype_of p;
-
val P = Free (variant used "P", pT --> propT);
- val x_name = variant used "x";
- val x = Free (x_name, pT);
- val a = variant used "a";
- val b = variant used "b";
- (*"P x == P (fst x, snd x)"*)
- val lem1 =
- Thm.combination (Thm.reflexive (ct P)) surj_pair
- |> Thm.forall_intr (ct p)
- |> Thm.forall_elim (ct x);
+ (*"!!a b. PROP (a, b)"*)
+ val all_a_b = all "a" aT (all "b" bT (P $ (con $ Bound 1 $ Bound 0)));
+ (*"!!x. PROP P x"*)
+ val all_x = all "x" pT (P $ Bound 0);
- (*"!!a b. PROP (a, b) ==> PROP P x"*)
- val lem2 = prove_goalw_cterm [lem1]
- (ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> P $ x))
+ (*lemma "P p == P (fst p, snd p)"*)
+ val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
+
+ (*lemma "!!a b. PROP (a, b) ==> PROP P p"*)
+ val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
(fn prems => [resolve_tac prems 1]);
- (*"!!a b. PROP (a, b) ==> !! x. PROP P x"*)
- val lem3 = prove_goalw_cterm []
- (ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> all x_name pT (P $ Bound 0)))
+ (*lemma "!!a b. PROP (a, b) ==> !!x. PROP P x"*)
+ val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
(fn prems => [rtac lem2 1, resolve_tac prems 1]);
- (*"!! x. PROP P x ==> !!a b. PROP (a, b)"*)
- val lem4 = prove_goalw_cterm []
- (ct (all x_name pT (P $ Bound 0) ==> all a aT (all a bT (P $ (con $ Bound 1 $ Bound 0)))))
+ (*lemma "!!x. PROP P x ==> !!a b. PROP (a, b)"*)
+ val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
(fn prems => [resolve_tac prems 1]);
in standard (Thm.equal_intr lem4 lem3) end;