improved meson setup;
authorwenzelm
Tue Sep 05 21:06:01 2000 +0200 (2000-09-05)
changeset 986995dca9f991f2
parent 9868 580c50fc6559
child 9870 2374ba026fc6
improved meson setup;
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/IsaMakefile
src/HOL/Tools/meson.ML
src/HOL/meson_lemmas.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 05 18:59:22 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 05 21:06:01 2000 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  *)
     1.5  
     1.6  theory HOL = CPure
     1.7 -files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") 
     1.8 -      ("Tools/meson.ML"):
     1.9 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    1.10 +  ("meson_lemmas.ML") ("Tools/meson.ML"):
    1.11  
    1.12  
    1.13  (** Core syntax **)
    1.14 @@ -54,7 +54,7 @@
    1.15  
    1.16  (* Overloaded Constants *)
    1.17  
    1.18 -axclass zero  < "term" 
    1.19 +axclass zero  < "term"
    1.20  axclass plus  < "term"
    1.21  axclass minus < "term"
    1.22  axclass times < "term"
    1.23 @@ -65,7 +65,7 @@
    1.24    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    1.25    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    1.26    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    1.27 -  abs		:: "('a::minus) => 'a"
    1.28 +  abs           :: "('a::minus) => 'a"
    1.29    *             :: "['a::times, 'a] => 'a"          (infixl 70)
    1.30    (*See Nat.thy for "^"*)
    1.31  
    1.32 @@ -193,7 +193,11 @@
    1.33  (* theory and package setup *)
    1.34  
    1.35  use "HOL_lemmas.ML"
    1.36 -use "cladata.ML"	setup hypsubst_setup setup Classical.setup setup clasetup
    1.37 +
    1.38 +use "cladata.ML"
    1.39 +setup hypsubst_setup
    1.40 +setup Classical.setup
    1.41 +setup clasetup
    1.42  
    1.43  lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
    1.44  proof (rule equal_intr_rule)
    1.45 @@ -216,12 +220,17 @@
    1.46  
    1.47  lemmas atomize = all_eq imp_eq
    1.48  
    1.49 -use "blastdata.ML"	setup Blast.setup
    1.50 -use "simpdata.ML"	setup Simplifier.setup
    1.51 -			setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    1.52 -                        setup Splitter.setup setup Clasimp.setup
    1.53 -			setup rulify_attrib_setup
    1.54 +use "blastdata.ML"
    1.55 +setup Blast.setup
    1.56  
    1.57 +use "simpdata.ML"
    1.58 +setup Simplifier.setup
    1.59 +setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    1.60 +setup Splitter.setup setup Clasimp.setup
    1.61 +setup rulify_attrib_setup
    1.62 +
    1.63 +use "meson_lemmas.ML"
    1.64  use "Tools/meson.ML"
    1.65 +setup meson_setup
    1.66  
    1.67  end
     2.1 --- a/src/HOL/HOL_lemmas.ML	Tue Sep 05 18:59:22 2000 +0200
     2.2 +++ b/src/HOL/HOL_lemmas.ML	Tue Sep 05 21:06:01 2000 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4  by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
     2.5  qed "allE";
     2.6  
     2.7 -val prems = goal (the_context ()) 
     2.8 +val prems = goal (the_context ())
     2.9      "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
    2.10  by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
    2.11  qed "all_dupE";
    2.12 @@ -224,7 +224,7 @@
    2.13  by (etac selectI 1) ;
    2.14  qed "exI";
    2.15  
    2.16 -val [major,minor] = 
    2.17 +val [major,minor] =
    2.18  Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
    2.19  by (rtac (major RS minor) 1);
    2.20  qed "exE";
    2.21 @@ -451,8 +451,8 @@
    2.22  val major::prems = Goal
    2.23      "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
    2.24  by (rtac (major RS iffE) 1);
    2.25 -by (REPEAT (DEPTH_SOLVE_1 
    2.26 -	    (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
    2.27 +by (REPEAT (DEPTH_SOLVE_1
    2.28 +            (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
    2.29  qed "iffCE";
    2.30  
    2.31  val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";
    2.32 @@ -471,9 +471,9 @@
    2.33  by (rtac (thm"plus_ac0.zero") 1);
    2.34  qed "plus_ac0_zero_right";
    2.35  
    2.36 -bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute", 
    2.37 -			plus_ac0_left_commute,
    2.38 -			thm"plus_ac0.zero", plus_ac0_zero_right]);
    2.39 +bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute",
    2.40 +                        plus_ac0_left_commute,
    2.41 +                        thm"plus_ac0.zero", plus_ac0_zero_right]);
    2.42  
    2.43  (* case distinction *)
    2.44  
    2.45 @@ -488,7 +488,7 @@
    2.46  
    2.47  (** Standard abbreviations **)
    2.48  
    2.49 -(* combination of (spec RS spec RS ...(j times) ... spec RS mp *) 
    2.50 +(* combination of (spec RS spec RS ...(j times) ... spec RS mp *)
    2.51  local
    2.52    fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
    2.53    |   wrong_prem (Bound _) = true
    2.54 @@ -500,4 +500,4 @@
    2.55  end;
    2.56  
    2.57  
    2.58 -fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
    2.59 +fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
     3.1 --- a/src/HOL/IsaMakefile	Tue Sep 05 18:59:22 2000 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Sep 05 21:06:01 2000 +0200
     3.3 @@ -33,45 +33,43 @@
     3.4  Pure:
     3.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     3.6  
     3.7 -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
     3.8 -  $(SRC)/Provers/Arith/cancel_sums.ML					\
     3.9 -  $(SRC)/Provers/Arith/assoc_fold.ML					\
    3.10 -  $(SRC)/Provers/Arith/combine_numerals.ML				\
    3.11 -  $(SRC)/Provers/Arith/cancel_numerals.ML				\
    3.12 -  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
    3.13 -  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML			\
    3.14 -  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML		\
    3.15 -  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML	\
    3.16 -  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml	\
    3.17 -  $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig		\
    3.18 -  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml		\
    3.19 -  $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig	\
    3.20 -  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml	\
    3.21 -  Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML		\
    3.22 -  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy	\
    3.23 -  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy \
    3.24 -  Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy \
    3.25 -  Integ/IntArith.ML Integ/IntArith.thy \
    3.26 -  Integ/IntPower.ML Integ/IntPower.thy \
    3.27 -  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML	\
    3.28 -  Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
    3.29 -  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
    3.30 -  Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
    3.31 -  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
    3.32 -  Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML  \
    3.33 -  Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML       \
    3.34 -  Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy   \
    3.35 -  Set.ML Set.thy SetInterval.ML	SetInterval.thy String.thy              \
    3.36 -  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML     \
    3.37 -  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML Tools/datatype_prop.ML	\
    3.38 -  Tools/datatype_rep_proofs.ML Tools/induct_method.ML			\
    3.39 -  Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML     \
    3.40 -  Tools/primrec_package.ML Tools/recdef_package.ML			\
    3.41 -  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML	\
    3.42 -  Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML	\
    3.43 -  WF.thy WF_Rel.ML WF_Rel.thy While.ML While.thy arith_data.ML blastdata.ML \
    3.44 -  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy   \
    3.45 -  simpdata.ML subset.ML subset.thy thy_syntax.ML
    3.46 +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		 \
    3.47 +  $(SRC)/Provers/Arith/cancel_sums.ML		\
    3.48 +  $(SRC)/Provers/Arith/assoc_fold.ML		\
    3.49 +  $(SRC)/Provers/Arith/combine_numerals.ML	\
    3.50 +  $(SRC)/Provers/Arith/cancel_numerals.ML	\
    3.51 +  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    3.52 +  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML \
    3.53 +  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \
    3.54 +  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML \
    3.55 +  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
    3.56 +  $(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
    3.57 +  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
    3.58 +  Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \
    3.59 +  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
    3.60 +  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
    3.61 +  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
    3.62 +  Integ/IntArith.thy Integ/IntPower.ML Integ/IntPower.thy \
    3.63 +  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
    3.64 +  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
    3.65 +  Integ/NatSimprocs.thy Integ/NatSimprocs.ML Integ/int_arith1.ML \
    3.66 +  Integ/int_arith2.ML Integ/nat_simprocs.ML Lfp.ML Lfp.thy List.ML \
    3.67 +  List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
    3.68 +  NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
    3.69 +  Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy \
    3.70 +  RelPow.ML RelPow.thy Relation.ML Relation.thy Set.ML Set.thy \
    3.71 +  SetInterval.ML SetInterval.thy String.thy SVC_Oracle.ML \
    3.72 +  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    3.73 +  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    3.74 +  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    3.75 +  Tools/induct_method.ML Tools/inductive_package.ML Tools/meson.ML \
    3.76 +  Tools/numeral_syntax.ML Tools/primrec_package.ML \
    3.77 +  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
    3.78 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    3.79 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy While.ML \
    3.80 +  While.thy arith_data.ML blastdata.ML cladata.ML equalities.ML \
    3.81 +  equalities.thy hologic.ML meson_lemmas.ML mono.ML mono.thy simpdata.ML \
    3.82 +  subset.ML subset.thy thy_syntax.ML
    3.83  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    3.84  
    3.85  
     4.1 --- a/src/HOL/Tools/meson.ML	Tue Sep 05 18:59:22 2000 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Tue Sep 05 21:06:01 2000 +0200
     4.3 @@ -1,9 +1,9 @@
     4.4 -(*  Title:      HOL/ex/meson
     4.5 +(*  Title:      HOL/Tools/meson.ML
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1992  University of Cambridge
     4.9  
    4.10 -The MESON resolution proof procedure for HOL
    4.11 +The MESON resolution proof procedure for HOL.
    4.12  
    4.13  When making clauses, avoids using the rewriter -- instead uses RS recursively
    4.14  
    4.15 @@ -11,100 +11,12 @@
    4.16  FUNCTION nodups -- if done to goal clauses too!
    4.17  *)
    4.18  
    4.19 -
    4.20 -(**** LEMMAS : outside the "local" block ****)
    4.21 -
    4.22 -(** "Axiom" of Choice, proved using the description operator **)
    4.23 -
    4.24 -Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    4.25 -by (fast_tac (claset() addEs [selectI]) 1);
    4.26 -qed "choice";
    4.27 -
    4.28 -(*** Generation of contrapositives ***)
    4.29 -
    4.30 -(*Inserts negated disjunct after removing the negation; P is a literal*)
    4.31 -val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
    4.32 -by (rtac (major RS disjE) 1);
    4.33 -by (rtac notE 1);
    4.34 -by (etac minor 2);
    4.35 -by (ALLGOALS assume_tac);
    4.36 -qed "make_neg_rule";
    4.37 -
    4.38 -(*For Plaisted's "Postive refinement" of the MESON procedure*)
    4.39 -Goal "~P|Q ==> (P ==> Q)";
    4.40 -by (Blast_tac 1);
    4.41 -qed "make_refined_neg_rule";
    4.42 -
    4.43 -(*P should be a literal*)
    4.44 -val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";
    4.45 -by (rtac (major RS disjE) 1);
    4.46 -by (rtac notE 1);
    4.47 -by (etac minor 1);
    4.48 -by (ALLGOALS assume_tac);
    4.49 -qed "make_pos_rule";
    4.50 -
    4.51 -(*** Generation of a goal clause -- put away the final literal ***)
    4.52 -
    4.53 -val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";
    4.54 -by (rtac notE 1);
    4.55 -by (rtac minor 2);
    4.56 -by (ALLGOALS (rtac major));
    4.57 -qed "make_neg_goal";
    4.58 -
    4.59 -val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";
    4.60 -by (rtac notE 1);
    4.61 -by (rtac minor 1);
    4.62 -by (ALLGOALS (rtac major));
    4.63 -qed "make_pos_goal";
    4.64 -
    4.65 -
    4.66 -(**** Lemmas for forward proof (like congruence rules) ****)
    4.67 -
    4.68 -(*NOTE: could handle conjunctions (faster?) by
    4.69 -    nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
    4.70 -val major::prems = Goal
    4.71 -    "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q";
    4.72 -by (rtac (major RS conjE) 1);
    4.73 -by (rtac conjI 1);
    4.74 -by (ALLGOALS (eresolve_tac prems));
    4.75 -qed "conj_forward";
    4.76 -
    4.77 -val major::prems = Goal
    4.78 -    "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q";
    4.79 -by (rtac (major RS disjE) 1);
    4.80 -by (ALLGOALS (dresolve_tac prems));
    4.81 -by (ALLGOALS (eresolve_tac [disjI1,disjI2]));
    4.82 -qed "disj_forward";
    4.83 -
    4.84 -(*Version for removal of duplicate literals*)
    4.85 -val major::prems = Goal
    4.86 -    "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q";
    4.87 -by (cut_facts_tac [major] 1);
    4.88 -by (blast_tac (claset() addIs prems) 1); 
    4.89 -qed "disj_forward2";
    4.90 -
    4.91 -val major::prems = Goal
    4.92 -    "[| ALL x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)";
    4.93 -by (rtac allI 1);
    4.94 -by (resolve_tac prems 1);
    4.95 -by (rtac (major RS spec) 1);
    4.96 -qed "all_forward";
    4.97 -
    4.98 -val major::prems = Goal
    4.99 -    "[| EX x. P'(x);  !!x. P'(x) ==> P(x) |] ==> EX x. P(x)";
   4.100 -by (rtac (major RS exE) 1);
   4.101 -by (rtac exI 1);
   4.102 -by (eresolve_tac prems 1);
   4.103 -qed "ex_forward";
   4.104 -
   4.105 -(**** END OF LEMMAS ****)
   4.106 -
   4.107  local
   4.108  
   4.109   (*Prove theorems using fast_tac*)
   4.110 - fun prove_fun s = 
   4.111 + fun prove_fun s =
   4.112       prove_goal (the_context ()) s
   4.113 -	  (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
   4.114 +          (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
   4.115  
   4.116   (**** Negation Normal Form ****)
   4.117  
   4.118 @@ -174,11 +86,11 @@
   4.119  
   4.120  
   4.121   (*Are any of the constants in "bs" present in the term?*)
   4.122 - fun has_consts bs = 
   4.123 + fun has_consts bs =
   4.124     let fun has (Const(a,_)) = a mem bs
   4.125 -	 | has (f$u) = has f orelse has u
   4.126 -	 | has (Abs(_,_,t)) = has t
   4.127 -	 | has _ = false
   4.128 +         | has (f$u) = has f orelse has u
   4.129 +         | has (Abs(_,_,t)) = has t
   4.130 +         | has _ = false
   4.131     in  has  end;
   4.132  
   4.133  
   4.134 @@ -197,12 +109,12 @@
   4.135     | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts;
   4.136  
   4.137   (*Include False as a literal: an occurrence of ~False is a tautology*)
   4.138 - fun is_taut th = taut_lits ((true, HOLogic.false_const) :: 
   4.139 -			     literals (prop_of th));
   4.140 + fun is_taut th = taut_lits ((true, HOLogic.false_const) ::
   4.141 +                             literals (prop_of th));
   4.142  
   4.143   (*Generation of unique names -- maxidx cannot be relied upon to increase!
   4.144     Cannot rely on "variant", since variables might coincide when literals
   4.145 -   are joined to make a clause... 
   4.146 +   are joined to make a clause...
   4.147     19 chooses "U" as the first variable name*)
   4.148   val name_ref = ref 19;
   4.149  
   4.150 @@ -211,31 +123,31 @@
   4.151   fun freeze_spec th =
   4.152     let val sth = th RS spec
   4.153         val newname = (name_ref := !name_ref + 1;
   4.154 -		      radixstring(26, "A", !name_ref))
   4.155 +                      radixstring(26, "A", !name_ref))
   4.156     in  read_instantiate [("x", newname)] sth  end;
   4.157  
   4.158   fun resop nf [prem] = resolve_tac (nf prem) 1;
   4.159  
   4.160   (*Conjunctive normal form, detecting tautologies early.
   4.161     Strips universal quantifiers and breaks up conjunctions. *)
   4.162 - fun cnf_aux seen (th,ths) = 
   4.163 + fun cnf_aux seen (th,ths) =
   4.164     if taut_lits (literals(prop_of th) @ seen)  then ths
   4.165     else if not (has_consts ["All","op &"] (prop_of th))  then th::ths
   4.166     else (*conjunction?*)
   4.167 -	 cnf_aux seen (th RS conjunct1, 
   4.168 -		       cnf_aux seen (th RS conjunct2, ths))
   4.169 +         cnf_aux seen (th RS conjunct1,
   4.170 +                       cnf_aux seen (th RS conjunct2, ths))
   4.171     handle THM _ => (*universal quant?*)
   4.172 -	 cnf_aux  seen (freeze_spec th,  ths)
   4.173 +         cnf_aux  seen (freeze_spec th,  ths)
   4.174     handle THM _ => (*disjunction?*)
   4.175 -     let val tac = 
   4.176 -	 (METAHYPS (resop (cnf_nil seen)) 1) THEN
   4.177 -	 (fn st' => st' |>
   4.178 -		 METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
   4.179 +     let val tac =
   4.180 +         (METAHYPS (resop (cnf_nil seen)) 1) THEN
   4.181 +         (fn st' => st' |>
   4.182 +                 METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
   4.183       in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
   4.184   and cnf_nil seen th = cnf_aux seen (th,[]);
   4.185  
   4.186   (*Top-level call to cnf -- it's safe to reset name_ref*)
   4.187 - fun cnf (th,ths) = 
   4.188 + fun cnf (th,ths) =
   4.189      (name_ref := 19;  cnf (th RS conjunct1, cnf (th RS conjunct2, ths))
   4.190       handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths));
   4.191  
   4.192 @@ -244,9 +156,9 @@
   4.193   (*Forward proof, passing extra assumptions as theorems to the tactic*)
   4.194   fun forward_res2 nf hyps st =
   4.195     case Seq.pull
   4.196 -	 (REPEAT 
   4.197 -	  (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
   4.198 -	  st)
   4.199 +         (REPEAT
   4.200 +          (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   4.201 +          st)
   4.202     of Some(th,_) => th
   4.203      | None => raise THM("forward_res2", 0, [st]);
   4.204  
   4.205 @@ -255,7 +167,7 @@
   4.206   fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   4.207       handle THM _ => tryres(th,rls)
   4.208       handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   4.209 -			    [disj_FalseD1, disj_FalseD2, asm_rl])
   4.210 +                            [disj_FalseD1, disj_FalseD2, asm_rl])
   4.211       handle THM _ => th;
   4.212  
   4.213   (*Remove duplicate literals, if there are any*)
   4.214 @@ -268,7 +180,7 @@
   4.215  
   4.216   (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   4.217   fun assoc_right th = assoc_right (th RS disj_assoc)
   4.218 -	 handle THM _ => th;
   4.219 +         handle THM _ => th;
   4.220  
   4.221   (*Must check for negative literal first!*)
   4.222   val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   4.223 @@ -278,7 +190,7 @@
   4.224  
   4.225   (*Create a goal or support clause, conclusing False*)
   4.226   fun make_goal th =   (*Must check for negative literal first!*)
   4.227 -     make_goal (tryres(th, clause_rules)) 
   4.228 +     make_goal (tryres(th, clause_rules))
   4.229     handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   4.230  
   4.231   (*Sort clauses by number of literals*)
   4.232 @@ -291,23 +203,23 @@
   4.233   fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
   4.234  
   4.235   (*Create a meta-level Horn clause*)
   4.236 - fun make_horn crules th = make_horn crules (tryres(th,crules)) 
   4.237 -			   handle THM _ => th;
   4.238 + fun make_horn crules th = make_horn crules (tryres(th,crules))
   4.239 +                           handle THM _ => th;
   4.240  
   4.241   (*Generate Horn clauses for all contrapositives of a clause*)
   4.242 - fun add_contras crules (th,hcs) = 
   4.243 + fun add_contras crules (th,hcs) =
   4.244     let fun rots (0,th) = hcs
   4.245 -	 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
   4.246 -			 rots(k-1, assoc_right (th RS disj_comm))
   4.247 +         | rots (k,th) = zero_var_indexes (make_horn crules th) ::
   4.248 +                         rots(k-1, assoc_right (th RS disj_comm))
   4.249     in case nliterals(prop_of th) of
   4.250 -	 1 => th::hcs
   4.251 +         1 => th::hcs
   4.252         | n => rots(n, assoc_right th)
   4.253     end;
   4.254  
   4.255   (*Use "theorem naming" to label the clauses*)
   4.256 - fun name_thms label = 
   4.257 + fun name_thms label =
   4.258       let fun name1 (th, (k,ths)) =
   4.259 -	   (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   4.260 +           (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   4.261  
   4.262       in  fn ths => #2 (foldr name1 (ths, (length ths, [])))  end;
   4.263  
   4.264 @@ -320,7 +232,7 @@
   4.265   (***** MESON PROOF PROCEDURE *****)
   4.266  
   4.267   fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   4.268 -	    As) = rhyps(phi, A::As)
   4.269 +            As) = rhyps(phi, A::As)
   4.270     | rhyps (_, As) = As;
   4.271  
   4.272   (** Detecting repeated assumptions in a subgoal **)
   4.273 @@ -333,23 +245,23 @@
   4.274     | has_reps [_] = false
   4.275     | has_reps [t,u] = (t aconv u)
   4.276     | has_reps ts = (foldl ins_term (Net.empty, ts);  false)
   4.277 -		   handle INSERT => true; 
   4.278 +                   handle INSERT => true;
   4.279  
   4.280   (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   4.281   fun TRYALL_eq_assume_tac 0 st = Seq.single st
   4.282 -   | TRYALL_eq_assume_tac i st = 
   4.283 -	TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
   4.284 -	handle THM _ => TRYALL_eq_assume_tac (i-1) st;
   4.285 +   | TRYALL_eq_assume_tac i st =
   4.286 +        TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
   4.287 +        handle THM _ => TRYALL_eq_assume_tac (i-1) st;
   4.288  
   4.289   (*Loop checking: FAIL if trying to prove the same thing twice
   4.290     -- if *ANY* subgoal has repeated literals*)
   4.291 - fun check_tac st = 
   4.292 + fun check_tac st =
   4.293     if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   4.294     then  Seq.empty  else  Seq.single st;
   4.295  
   4.296  
   4.297   (* net_resolve_tac actually made it slower... *)
   4.298 - fun prolog_step_tac horns i = 
   4.299 + fun prolog_step_tac horns i =
   4.300       (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   4.301       TRYALL eq_assume_tac;
   4.302  
   4.303 @@ -365,48 +277,48 @@
   4.304  
   4.305  (*Negation Normal Form*)
   4.306  val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   4.307 -	       not_impD, not_iffD, not_allD, not_exD, not_notD];
   4.308 +               not_impD, not_iffD, not_allD, not_exD, not_notD];
   4.309  fun make_nnf th = make_nnf (tryres(th, nnf_rls))
   4.310 -    handle THM _ => 
   4.311 -	forward_res make_nnf
   4.312 -	   (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   4.313 +    handle THM _ =>
   4.314 +        forward_res make_nnf
   4.315 +           (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   4.316      handle THM _ => th;
   4.317  
   4.318  (*Pull existential quantifiers (Skolemization)*)
   4.319 -fun skolemize th = 
   4.320 +fun skolemize th =
   4.321    if not (has_consts ["Ex"] (prop_of th)) then th
   4.322    else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   4.323 -			      disj_exD, disj_exD1, disj_exD2]))
   4.324 -    handle THM _ => 
   4.325 -	skolemize (forward_res skolemize
   4.326 -		   (tryres (th, [conj_forward, disj_forward, all_forward])))
   4.327 +                              disj_exD, disj_exD1, disj_exD2]))
   4.328 +    handle THM _ =>
   4.329 +        skolemize (forward_res skolemize
   4.330 +                   (tryres (th, [conj_forward, disj_forward, all_forward])))
   4.331      handle THM _ => forward_res skolemize (th RS ex_forward);
   4.332  
   4.333  
   4.334  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   4.335    The resulting clauses are HOL disjunctions.*)
   4.336 -fun make_clauses ths = 
   4.337 +fun make_clauses ths =
   4.338      sort_clauses (map (generalize o nodups) (foldr cnf (ths,[])));
   4.339  
   4.340  (*Convert a list of clauses to (contrapositive) Horn clauses*)
   4.341 -fun make_horns ths = 
   4.342 +fun make_horns ths =
   4.343      name_thms "Horn#"
   4.344        (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
   4.345  
   4.346  (*Could simply use nprems_of, which would count remaining subgoals -- no
   4.347    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   4.348  
   4.349 -fun best_prolog_tac sizef horns = 
   4.350 +fun best_prolog_tac sizef horns =
   4.351      BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   4.352  
   4.353 -fun depth_prolog_tac horns = 
   4.354 +fun depth_prolog_tac horns =
   4.355      DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   4.356  
   4.357  (*Return all negative clauses, as possible goal clauses*)
   4.358  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   4.359  
   4.360  
   4.361 -fun skolemize_tac prems = 
   4.362 +fun skolemize_tac prems =
   4.363      cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   4.364      REPEAT o (etac exE);
   4.365  
   4.366 @@ -419,21 +331,21 @@
   4.367  
   4.368  (** Best-first search versions **)
   4.369  
   4.370 -fun best_meson_tac sizef = 
   4.371 -  MESON (fn cls => 
   4.372 +fun best_meson_tac sizef =
   4.373 +  MESON (fn cls =>
   4.374           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   4.375                           (has_fewer_prems 1, sizef)
   4.376                           (prolog_step_tac (make_horns cls) 1));
   4.377  
   4.378  (*First, breaks the goal into independent units*)
   4.379  val safe_best_meson_tac =
   4.380 -     SELECT_GOAL (TRY Safe_tac THEN 
   4.381 +     SELECT_GOAL (TRY Safe_tac THEN
   4.382                    TRYALL (best_meson_tac size_of_subgoals));
   4.383  
   4.384  (** Depth-first search version **)
   4.385  
   4.386  val depth_meson_tac =
   4.387 -     MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, 
   4.388 +     MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   4.389                               depth_prolog_tac (make_horns cls)]);
   4.390  
   4.391  
   4.392 @@ -442,7 +354,7 @@
   4.393  
   4.394  (*This version does only one inference per call;
   4.395    having only one eq_assume_tac speeds it up!*)
   4.396 -fun prolog_step_tac' horns = 
   4.397 +fun prolog_step_tac' horns =
   4.398      let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   4.399              take_prefix Thm.no_prems horns
   4.400          val nrtac = net_resolve_tac horns
   4.401 @@ -451,17 +363,34 @@
   4.402                  ((assume_tac i APPEND nrtac i) THEN check_tac)
   4.403      end;
   4.404  
   4.405 -fun iter_deepen_prolog_tac horns = 
   4.406 +fun iter_deepen_prolog_tac horns =
   4.407      ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   4.408  
   4.409 -val iter_deepen_meson_tac = 
   4.410 -  MESON (fn cls => 
   4.411 +val iter_deepen_meson_tac =
   4.412 +  MESON (fn cls =>
   4.413           (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
   4.414                             (has_fewer_prems 1)
   4.415                             (prolog_step_tac' (make_horns cls))));
   4.416  
   4.417 -val meson_tac =
   4.418 -     SELECT_GOAL (TRY Safe_tac THEN 
   4.419 -                  TRYALL (iter_deepen_meson_tac));
   4.420 +fun meson_claset_tac cs =
   4.421 +  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac);
   4.422 +
   4.423 +val meson_tac = CLASET' meson_claset_tac;
   4.424 +
   4.425 +
   4.426 +(* proof method setup *)
   4.427 +
   4.428 +local
   4.429 +
   4.430 +fun meson_meth ctxt =
   4.431 +  Method.SIMPLE_METHOD' HEADGOAL (CHANGED o meson_claset_tac (Classical.get_local_claset ctxt));
   4.432 +
   4.433 +in
   4.434 +
   4.435 +val meson_setup =
   4.436 + [Method.add_methods
   4.437 +  [("meson", Method.ctxt_args meson_meth, "The MESON resolution proof procedure")]];
   4.438  
   4.439  end;
   4.440 +
   4.441 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/meson_lemmas.ML	Tue Sep 05 21:06:01 2000 +0200
     5.3 @@ -0,0 +1,92 @@
     5.4 +(*  Title:      HOL/meson_lemmas.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1992  University of Cambridge
     5.8 +
     5.9 +Lemmas for Meson.
    5.10 +*)
    5.11 +
    5.12 +(* "Axiom" of Choice, proved using the description operator *)
    5.13 +
    5.14 +Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    5.15 +by (fast_tac (claset() addEs [selectI]) 1);
    5.16 +qed "choice";
    5.17 +
    5.18 +
    5.19 +(* Generation of contrapositives *)
    5.20 +
    5.21 +(*Inserts negated disjunct after removing the negation; P is a literal*)
    5.22 +val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
    5.23 +by (rtac (major RS disjE) 1);
    5.24 +by (rtac notE 1);
    5.25 +by (etac minor 2);
    5.26 +by (ALLGOALS assume_tac);
    5.27 +qed "make_neg_rule";
    5.28 +
    5.29 +(*For Plaisted's "Postive refinement" of the MESON procedure*)
    5.30 +Goal "~P|Q ==> (P ==> Q)";
    5.31 +by (Blast_tac 1);
    5.32 +qed "make_refined_neg_rule";
    5.33 +
    5.34 +(*P should be a literal*)
    5.35 +val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";
    5.36 +by (rtac (major RS disjE) 1);
    5.37 +by (rtac notE 1);
    5.38 +by (etac minor 1);
    5.39 +by (ALLGOALS assume_tac);
    5.40 +qed "make_pos_rule";
    5.41 +
    5.42 +
    5.43 +(* Generation of a goal clause -- put away the final literal *)
    5.44 +
    5.45 +val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";
    5.46 +by (rtac notE 1);
    5.47 +by (rtac minor 2);
    5.48 +by (ALLGOALS (rtac major));
    5.49 +qed "make_neg_goal";
    5.50 +
    5.51 +val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";
    5.52 +by (rtac notE 1);
    5.53 +by (rtac minor 1);
    5.54 +by (ALLGOALS (rtac major));
    5.55 +qed "make_pos_goal";
    5.56 +
    5.57 +
    5.58 +(* Lemmas for forward proof (like congruence rules) *)
    5.59 +
    5.60 +(*NOTE: could handle conjunctions (faster?) by
    5.61 +    nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
    5.62 +val major::prems = Goal
    5.63 +    "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q";
    5.64 +by (rtac (major RS conjE) 1);
    5.65 +by (rtac conjI 1);
    5.66 +by (ALLGOALS (eresolve_tac prems));
    5.67 +qed "conj_forward";
    5.68 +
    5.69 +val major::prems = Goal
    5.70 +    "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q";
    5.71 +by (rtac (major RS disjE) 1);
    5.72 +by (ALLGOALS (dresolve_tac prems));
    5.73 +by (ALLGOALS (eresolve_tac [disjI1,disjI2]));
    5.74 +qed "disj_forward";
    5.75 +
    5.76 +(*Version for removal of duplicate literals*)
    5.77 +val major::prems = Goal
    5.78 +    "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q";
    5.79 +by (cut_facts_tac [major] 1);
    5.80 +by (blast_tac (claset() addIs prems) 1);
    5.81 +qed "disj_forward2";
    5.82 +
    5.83 +val major::prems = Goal
    5.84 +    "[| ALL x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)";
    5.85 +by (rtac allI 1);
    5.86 +by (resolve_tac prems 1);
    5.87 +by (rtac (major RS spec) 1);
    5.88 +qed "all_forward";
    5.89 +
    5.90 +val major::prems = Goal
    5.91 +    "[| EX x. P'(x);  !!x. P'(x) ==> P(x) |] ==> EX x. P(x)";
    5.92 +by (rtac (major RS exE) 1);
    5.93 +by (rtac exI 1);
    5.94 +by (eresolve_tac prems 1);
    5.95 +qed "ex_forward";