split_paired_all.ML;
authorwenzelm
Tue Oct 20 16:39:14 1998 +0200 (1998-10-20)
changeset 56995b9a359e083c
parent 5698 2b5d9bdec5af
child 5700 491944c2fb12
split_paired_all.ML;
src/HOL/IsaMakefile
src/HOL/Prod.ML
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 20 16:38:37 1998 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 20 16:39:14 1998 +0200
     1.3 @@ -30,33 +30,32 @@
     1.4  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.5  
     1.6  $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
     1.7 -  $(SRC)/Provers/Arith/nat_transitive.ML \
     1.8 +  $(SRC)/Provers/Arith/nat_transitive.ML	\
     1.9    $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
    1.10    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    1.11    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    1.12 -  $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \
    1.13 -  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \
    1.14 -  $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \
    1.15 -  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
    1.16 -  $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
    1.17 -  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
    1.18 -  Arith.ML Arith.thy Datatype.thy \
    1.19 -  Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy \
    1.20 -  Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy \
    1.21 -  Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy \
    1.22 -  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
    1.23 -  Integ/simproc.ML \
    1.24 -  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \
    1.25 -  Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    1.26 -  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
    1.27 +  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
    1.28 +  $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \
    1.29 +  $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig \
    1.30 +  $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
    1.31 +  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
    1.32 +  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
    1.33 +  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
    1.34 +  Datatype.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
    1.35 +  Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
    1.36 +  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML \
    1.37 +  Integ/IntDef.thy Integ/Int.ML Integ/Int.thy Integ/simproc.ML Lfp.ML \
    1.38 +  Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy \
    1.39 +  NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
    1.40 +  Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
    1.41    RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    1.42 -  String.thy Sum.ML Sum.thy \
    1.43 -  Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    1.44 +  String.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    1.45 +  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    1.46    Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    1.47 -  Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
    1.48 -  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.49 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
    1.50 -  WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
    1.51 +  Tools/inductive_package.ML Tools/primrec_package.ML \
    1.52 +  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
    1.53 +  Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    1.54 +  WF_Rel.ML WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
    1.55    equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
    1.56    subset.thy thy_syntax.ML
    1.57  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
     2.1 --- a/src/HOL/Prod.ML	Tue Oct 20 16:38:37 1998 +0200
     2.2 +++ b/src/HOL/Prod.ML	Tue Oct 20 16:39:14 1998 +0200
     2.3 @@ -67,25 +67,9 @@
     2.4  	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
     2.5  Addsimps [surj_pair];
     2.6  
     2.7 -(* lemmas for splitting paired `!!' *)
     2.8 -local 
     2.9 -    val lemma1 = prove_goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))" 
    2.10 -		 (fn prems => [resolve_tac prems 1]);
    2.11  
    2.12 -    val psig = sign_of Prod.thy;
    2.13 -    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
    2.14 -    val PeqP = reflexive(read_cterm psig ("P", pT));
    2.15 -    val psplit = zero_var_indexes(read_instantiate [("p","x")]
    2.16 -                                  surjective_pairing RS eq_reflection);
    2.17 -    val adhoc = combination PeqP psplit;
    2.18 -    val lemma = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x" 
    2.19 -		(fn prems => [rewtac adhoc, resolve_tac prems 1]);
    2.20 -    val lemma2 = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)"
    2.21 -		(fn prems => [rtac lemma 1, resolve_tac prems 1]);
    2.22 -in
    2.23 -  val split_paired_all = equal_intr lemma1 lemma2
    2.24 -end;
    2.25 -bind_thm("split_paired_all", split_paired_all);
    2.26 +bind_thm ("split_paired_all",
    2.27 +  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
    2.28  (*
    2.29  Addsimps [split_paired_all] does not work with simplifier 
    2.30  because it also affects premises in congrence rules, 
     3.1 --- a/src/HOL/ROOT.ML	Tue Oct 20 16:38:37 1998 +0200
     3.2 +++ b/src/HOL/ROOT.ML	Tue Oct 20 16:39:14 1998 +0200
     3.3 @@ -17,6 +17,7 @@
     3.4  use "thy_syntax.ML";
     3.5  
     3.6  use "$ISABELLE_HOME/src/Provers/simplifier.ML";
     3.7 +use "$ISABELLE_HOME/src/Provers/split_paired_all.ML";
     3.8  use "$ISABELLE_HOME/src/Provers/splitter.ML";
     3.9  use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    3.10  use "$ISABELLE_HOME/src/Provers/classical.ML";
    3.11 @@ -39,9 +40,6 @@
    3.12  use_thy "Sum";
    3.13  use_thy "Gfp";
    3.14  
    3.15 -use "Tools/record_package.ML";
    3.16 -use_thy "Record";
    3.17 -
    3.18  use_thy "NatDef";
    3.19  
    3.20  use "Tools/inductive_package.ML";
    3.21 @@ -55,6 +53,9 @@
    3.22  use "Tools/primrec_package.ML";
    3.23  use_thy "Datatype";
    3.24  
    3.25 +use "Tools/record_package.ML";
    3.26 +use_thy "Record";
    3.27 +
    3.28  use_thy "Arith";
    3.29  use "arith_data.ML";
    3.30