--- a/src/HOL/IsaMakefile Fri Oct 19 21:59:33 2001 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 19 22:00:08 2001 +0200
@@ -74,8 +74,7 @@
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
$(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
- $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
+ $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
$(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
$(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
@@ -92,7 +91,7 @@
Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
Option.ML Option.thy Power.ML Power.thy PreList.thy \
- Product_Type_lemmas.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+ Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
--- a/src/HOL/ROOT.ML Fri Oct 19 21:59:33 2001 +0200
+++ b/src/HOL/ROOT.ML Fri Oct 19 22:00:08 2001 +0200
@@ -17,7 +17,6 @@
use "hologic.ML";
use "~~/src/Provers/simplifier.ML";
-use "~~/src/Provers/split_paired_all.ML";
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/hypsubst.ML";
use "~~/src/Provers/induct_method.ML";
--- a/src/Provers/split_paired_all.ML Fri Oct 19 21:59:33 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(* 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_params: string -> string -> thm -> thm
- 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_params a b raw_surj_pair =
- let
- val ct = Thm.cterm_of (Thm.sign_of_thm 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);
-
- (*"!!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);
-
- (*lemma "P p == P (fst p, snd p)"*)
- val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
-
- (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
- val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
- (fn prems => [resolve_tac prems 1]);
-
- (*lemma "(!!a b. PROP P (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]);
-
- (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (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;
-
-val rule = rule_params "a" "b";
-
-
-end;