got rid of Provers/split_paired_all.ML;
authorwenzelm
Fri Oct 19 22:00:08 2001 +0200 (2001-10-19)
changeset 11837b2a9853ec6dd
parent 11836 805b0c13607e
child 11838 02d75712061d
got rid of Provers/split_paired_all.ML;
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/Provers/split_paired_all.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 19 21:59:33 2001 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 19 22:00:08 2001 +0200
     1.3 @@ -74,8 +74,7 @@
     1.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     1.5    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
     1.6    $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
     1.7 -  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
     1.8 -  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
     1.9 +  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
    1.10    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    1.11    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
    1.12    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
    1.13 @@ -92,7 +91,7 @@
    1.14    Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
    1.15    Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
    1.16    Option.ML Option.thy Power.ML Power.thy PreList.thy \
    1.17 -  Product_Type_lemmas.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
    1.18 +  Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
    1.19    Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
    1.20    SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
    1.21    SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
     2.1 --- a/src/HOL/ROOT.ML	Fri Oct 19 21:59:33 2001 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Fri Oct 19 22:00:08 2001 +0200
     2.3 @@ -17,7 +17,6 @@
     2.4  use "hologic.ML";
     2.5  
     2.6  use "~~/src/Provers/simplifier.ML";
     2.7 -use "~~/src/Provers/split_paired_all.ML";
     2.8  use "~~/src/Provers/splitter.ML";
     2.9  use "~~/src/Provers/hypsubst.ML";
    2.10  use "~~/src/Provers/induct_method.ML";
     3.1 --- a/src/Provers/split_paired_all.ML	Fri Oct 19 21:59:33 2001 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,64 +0,0 @@
     3.4 -(*  Title:      Provers/split_paired_all.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Markus Wenzel, TU Muenchen
     3.7 -
     3.8 -Derived rule for turning meta-level surjective pairing into split rule:
     3.9 -
    3.10 -           p == (fst p, snd p)
    3.11 - --------------------------------------
    3.12 -  !!a b. PROP (a, b) == !! x. PROP P x
    3.13 -
    3.14 -*)
    3.15 -
    3.16 -signature SPLIT_PAIRED_ALL =
    3.17 -sig
    3.18 -  val rule_params: string -> string -> thm -> thm
    3.19 -  val rule: thm -> thm
    3.20 -end;
    3.21 -
    3.22 -structure SplitPairedAll: SPLIT_PAIRED_ALL =
    3.23 -struct
    3.24 -
    3.25 -
    3.26 -fun all x T t = Term.all T $ Abs (x, T, t);
    3.27 -
    3.28 -infixr ==>;
    3.29 -val op ==> = Logic.mk_implies;
    3.30 -
    3.31 -
    3.32 -fun rule_params a b raw_surj_pair =
    3.33 -  let
    3.34 -    val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
    3.35 -
    3.36 -    val surj_pair = Drule.unvarify (standard raw_surj_pair);
    3.37 -    val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []);
    3.38 -
    3.39 -    val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair));
    3.40 -    val pT as Type (_, [aT, bT]) = fastype_of p;
    3.41 -    val P = Free (variant used "P", pT --> propT);
    3.42 -
    3.43 -   (*"!!a b. PROP (a, b)"*)
    3.44 -   val all_a_b = all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0)));
    3.45 -   (*"!!x. PROP P x"*)
    3.46 -   val all_x = all "x" pT (P $ Bound 0);
    3.47 -
    3.48 -   (*lemma "P p == P (fst p, snd p)"*)
    3.49 -   val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
    3.50 -
    3.51 -   (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
    3.52 -   val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
    3.53 -     (fn prems => [resolve_tac prems 1]);
    3.54 -
    3.55 -   (*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*)
    3.56 -   val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
    3.57 -     (fn prems => [rtac lem2 1, resolve_tac prems 1]);
    3.58 -
    3.59 -   (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*)
    3.60 -   val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
    3.61 -     (fn prems => [resolve_tac prems 1]);
    3.62 -  in standard (Thm.equal_intr lem4 lem3) end;
    3.63 -
    3.64 -val rule = rule_params "a" "b";
    3.65 -
    3.66 -
    3.67 -end;