split_paired_all.ML: turn surjective pairing into split rule;

--- a/src/Provers/README	Tue Oct 20 11:27:06 1998 +0200
+++ b/src/Provers/README	Tue Oct 20 16:18:18 1998 +0200
@@ -14,6 +14,7 @@
   quantifier1.ML	simplification procedures for "1 point rules"
   simp.ML               powerful but slow simplifier
   simplifier.ML         fast simplifier
+  split_paired_all.ML	turn surjective pairing into split rule
   splitter.ML           performs case splits for simplifier.ML
   typedsimp.ML          basic simplifier for explicitly typed logics
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/split_paired_all.ML	Tue Oct 20 16:18:18 1998 +0200
@@ -0,0 +1,67 @@
+(*  Title:      Provers/split_paired_all.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Derived rule for turning meta-level surjective pairing into split rule:
+
+           p == (fst p, snd p)
+ --------------------------------------
+  !!a b. PROP (a, b) == !! x. PROP P x
+
+*)
+
+signature SPLIT_PAIRED_ALL =
+sig
+  val rule: thm -> thm
+end;
+
+structure SplitPairedAll: SPLIT_PAIRED_ALL =
+struct
+
+
+fun all x T t = Term.all T $ Abs (x, T, t);
+
+infixr ==>;
+val op ==> = Logic.mk_implies;
+
+
+fun rule raw_surj_pair =
+  let
+    val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
+
+    val surj_pair = Drule.unvarify 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) ==> PROP P x"*)
+   val lem2 = prove_goalw_cterm [lem1]
+     (ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> P $ x))
+     (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)))
+     (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)))))
+     (fn prems => [resolve_tac prems 1]);
+  in standard (Thm.equal_intr lem4 lem3) end;
+
+
+end;