cong setup now part of Simplifier;
authorwenzelm
Tue Aug 29 00:55:31 2000 +0200 (2000-08-29)
changeset 97132c5b42311eb0
parent 9712 e33422a2eb9c
child 9714 79db0e5b7824
cong setup now part of Simplifier;
src/FOL/FOL.thy
src/FOL/simpdata.ML
src/HOL/HOL.thy
src/HOL/simpdata.ML
src/Sequents/simpdata.ML
     1.1 --- a/src/FOL/FOL.thy	Tue Aug 29 00:54:22 2000 +0200
     1.2 +++ b/src/FOL/FOL.thy	Tue Aug 29 00:55:31 2000 +0200
     1.3 @@ -55,7 +55,6 @@
     1.4  
     1.5  use "simpdata.ML"
     1.6  setup simpsetup
     1.7 -setup cong_attrib_setup
     1.8  setup "Simplifier.method_setup Splitter.split_modifiers"
     1.9  setup Splitter.setup
    1.10  setup Clasimp.setup
     2.1 --- a/src/FOL/simpdata.ML	Tue Aug 29 00:54:22 2000 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Tue Aug 29 00:55:31 2000 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  Simplification data for FOL
     2.5  *)
     2.6  
     2.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
     2.8 +(*** Addition of rules to simpsets and clasets simultaneously ***)      (* FIXME move to Provers/clasimp.ML? *)
     2.9  
    2.10  infix 4 addIffs delIffs;
    2.11  
    2.12 @@ -30,15 +30,15 @@
    2.13  
    2.14    fun delIff ((cla, simp), th) = 
    2.15        (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
    2.16 -	   (Const ("Not", _) $ A) =>
    2.17 -	       cla delrules [zero_var_indexes (th RS notE)]
    2.18 -	 | (Const("op <->", _) $ _ $ _) =>
    2.19 -	       cla delrules [zero_var_indexes (th RS iffD2),
    2.20 -			     cla_make_elim (zero_var_indexes (th RS iffD1))]
    2.21 -	 | _ => cla delrules [th],
    2.22 +           (Const ("Not", _) $ A) =>
    2.23 +               cla delrules [zero_var_indexes (th RS notE)]
    2.24 +         | (Const("op <->", _) $ _ $ _) =>
    2.25 +               cla delrules [zero_var_indexes (th RS iffD2),
    2.26 +                             cla_make_elim (zero_var_indexes (th RS iffD1))]
    2.27 +         | _ => cla delrules [th],
    2.28         simp delsimps [th])
    2.29        handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    2.30 -				string_of_thm th); (cla, simp));
    2.31 +                                string_of_thm th); (cla, simp));
    2.32  
    2.33    fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    2.34  in
    2.35 @@ -139,6 +139,7 @@
    2.36      rule_by_tactic 
    2.37        (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
    2.38  
    2.39 +(*Congruence rules for = or <-> (instead of ==)*)
    2.40  fun mk_meta_cong rl =
    2.41    standard(mk_meta_eq (mk_meta_prems rl))
    2.42    handle THM _ =>
    2.43 @@ -188,29 +189,29 @@
    2.44  
    2.45  (*existential miniscoping*)
    2.46  val int_ex_simps = map int_prove_fun 
    2.47 -		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    2.48 -		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    2.49 -		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    2.50 -		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
    2.51 +                     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    2.52 +                      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    2.53 +                      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    2.54 +                      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
    2.55  
    2.56  (*classical rules*)
    2.57  val cla_ex_simps = map prove_fun 
    2.58                       ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    2.59 -		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    2.60 +                      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    2.61  
    2.62  val ex_simps = int_ex_simps @ cla_ex_simps;
    2.63  
    2.64  (*universal miniscoping*)
    2.65  val int_all_simps = map int_prove_fun
    2.66 -		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    2.67 -		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    2.68 -		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    2.69 -		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    2.70 +                      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    2.71 +                       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    2.72 +                       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    2.73 +                       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    2.74  
    2.75  (*classical rules*)
    2.76  val cla_all_simps = map prove_fun
    2.77                        ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    2.78 -		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    2.79 +                       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    2.80  
    2.81  val all_simps = int_all_simps @ cla_all_simps;
    2.82  
    2.83 @@ -338,28 +339,6 @@
    2.84  open Induction;
    2.85  
    2.86  
    2.87 -(* Add congruence rules for = or <-> (instead of ==) *)
    2.88 -
    2.89 -(* ###FIXME: Move to simplifier, 
    2.90 -   taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *)
    2.91 -infix 4 addcongs delcongs;
    2.92 -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
    2.93 -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
    2.94 -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    2.95 -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    2.96 -
    2.97 -val cong_add_global = Simplifier.change_global_ss (op addcongs);
    2.98 -val cong_del_global = Simplifier.change_global_ss (op delcongs);
    2.99 -val cong_add_local = Simplifier.change_local_ss (op addcongs);
   2.100 -val cong_del_local = Simplifier.change_local_ss (op delcongs);
   2.101 -
   2.102 -val cong_attrib_setup =
   2.103 - [Attrib.add_attributes [("cong",
   2.104 -   (Attrib.add_del_args cong_add_global cong_del_global,
   2.105 -    Attrib.add_del_args cong_add_local cong_del_local),
   2.106 -    "declare Simplifier congruence rules")]];
   2.107 -
   2.108 -
   2.109  val meta_simps =
   2.110     [triv_forall_equality,  (* prunes params *)
   2.111      True_implies_equals];  (* prune asms `True' *)
   2.112 @@ -372,27 +351,28 @@
   2.113  val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
   2.114  
   2.115  fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
   2.116 -				 atac, etac FalseE];
   2.117 +                                 atac, etac FalseE];
   2.118  (*No premature instantiation of variables during simplification*)
   2.119  fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
   2.120 -				 eq_assume_tac, ematch_tac [FalseE]];
   2.121 +                                 eq_assume_tac, ematch_tac [FalseE]];
   2.122  
   2.123  (*No simprules, but basic infastructure for simplification*)
   2.124 -val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   2.125 -                            addsimprocs [defALL_regroup,defEX_regroup]
   2.126 -			    setSSolver  (mk_solver "FOL safe" safe_solver)
   2.127 -			    setSolver  (mk_solver "FOL unsafe" unsafe_solver)
   2.128 -			    setmksimps (mksimps mksimps_pairs);
   2.129 -
   2.130 +val FOL_basic_ss =
   2.131 +  empty_ss setsubgoaler asm_simp_tac
   2.132 +    addsimprocs [defALL_regroup, defEX_regroup]
   2.133 +    setSSolver (mk_solver "FOL safe" safe_solver)
   2.134 +    setSolver (mk_solver "FOL unsafe" unsafe_solver)
   2.135 +    setmksimps (mksimps mksimps_pairs)
   2.136 +    setmkcong mk_meta_cong;
   2.137  
   2.138  
   2.139  (*intuitionistic simprules only*)
   2.140 -val IFOL_ss = 
   2.141 -    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ 
   2.142 -			   int_ex_simps @ int_all_simps)
   2.143 +val IFOL_ss =
   2.144 +    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @
   2.145 +                           int_ex_simps @ int_all_simps)
   2.146                   addcongs [imp_cong];
   2.147  
   2.148 -val cla_simps = 
   2.149 +val cla_simps =
   2.150      [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
   2.151       not_all, not_ex, cases_simp] @
   2.152      map prove_fun
     3.1 --- a/src/HOL/HOL.thy	Tue Aug 29 00:54:22 2000 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Aug 29 00:55:31 2000 +0200
     3.3 @@ -217,8 +217,7 @@
     3.4  
     3.5  use "blastdata.ML"	setup Blast.setup
     3.6  use "simpdata.ML"	setup Simplifier.setup
     3.7 -			setup "Simplifier.method_setup Splitter.split_modifiers"
     3.8 -			setup simpsetup setup cong_attrib_setup
     3.9 +			setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    3.10                          setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup
    3.11  
    3.12  
     4.1 --- a/src/HOL/simpdata.ML	Tue Aug 29 00:54:22 2000 +0200
     4.2 +++ b/src/HOL/simpdata.ML	Tue Aug 29 00:55:31 2000 +0200
     4.3 @@ -8,46 +8,46 @@
     4.4  
     4.5  section "Simplifier";
     4.6  
     4.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
     4.8 +(*** Addition of rules to simpsets and clasets simultaneously ***)      (* FIXME move to Provers/clasimp.ML? *)
     4.9  
    4.10  infix 4 addIffs delIffs;
    4.11  
    4.12 -(*Takes UNCONDITIONAL theorems of the form A<->B to 
    4.13 -        the Safe Intr     rule B==>A and 
    4.14 +(*Takes UNCONDITIONAL theorems of the form A<->B to
    4.15 +        the Safe Intr     rule B==>A and
    4.16          the Safe Destruct rule A==>B.
    4.17    Also ~A goes to the Safe Elim rule A ==> ?R
    4.18    Failing other cases, A is added as a Safe Intr rule*)
    4.19  local
    4.20    val iff_const = HOLogic.eq_const HOLogic.boolT;
    4.21  
    4.22 -  fun addIff ((cla, simp), th) = 
    4.23 +  fun addIff ((cla, simp), th) =
    4.24        (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
    4.25                  (Const("Not", _) $ A) =>
    4.26                      cla addSEs [zero_var_indexes (th RS notE)]
    4.27                | (con $ _ $ _) =>
    4.28                      if con = iff_const
    4.29 -                    then cla addSIs [zero_var_indexes (th RS iffD2)]  
    4.30 +                    then cla addSIs [zero_var_indexes (th RS iffD2)]
    4.31                                addSDs [zero_var_indexes (th RS iffD1)]
    4.32                      else  cla addSIs [th]
    4.33                | _ => cla addSIs [th],
    4.34         simp addsimps [th])
    4.35 -      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    4.36 +      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^
    4.37                           string_of_thm th);
    4.38  
    4.39 -  fun delIff ((cla, simp), th) = 
    4.40 +  fun delIff ((cla, simp), th) =
    4.41        (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
    4.42 -	   (Const ("Not", _) $ A) =>
    4.43 -	       cla delrules [zero_var_indexes (th RS notE)]
    4.44 -	 | (con $ _ $ _) =>
    4.45 -	       if con = iff_const
    4.46 -	       then cla delrules 
    4.47 -		        [zero_var_indexes (th RS iffD2),
    4.48 -			 cla_make_elim (zero_var_indexes (th RS iffD1))]
    4.49 -	       else cla delrules [th]
    4.50 -	 | _ => cla delrules [th],
    4.51 +           (Const ("Not", _) $ A) =>
    4.52 +               cla delrules [zero_var_indexes (th RS notE)]
    4.53 +         | (con $ _ $ _) =>
    4.54 +               if con = iff_const
    4.55 +               then cla delrules
    4.56 +                        [zero_var_indexes (th RS iffD2),
    4.57 +                         cla_make_elim (zero_var_indexes (th RS iffD1))]
    4.58 +               else cla delrules [th]
    4.59 +         | _ => cla delrules [th],
    4.60         simp delsimps [th])
    4.61 -      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    4.62 -				string_of_thm th); (cla, simp));
    4.63 +      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^
    4.64 +                                string_of_thm th); (cla, simp));
    4.65  
    4.66    fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    4.67  in
    4.68 @@ -89,6 +89,7 @@
    4.69  
    4.70  fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);
    4.71  
    4.72 +(*Congruence rules for = (instead of ==)*)
    4.73  fun mk_meta_cong rl =
    4.74    standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    4.75    handle THM _ =>
    4.76 @@ -101,45 +102,23 @@
    4.77     "(~True) = False", "(~False) = True",
    4.78     "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    4.79     "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    4.80 -   "(True --> P) = P", "(False --> P) = True", 
    4.81 +   "(True --> P) = P", "(False --> P) = True",
    4.82     "(P --> True) = True", "(P --> P) = True",
    4.83     "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    4.84 -   "(P & True) = P", "(True & P) = P", 
    4.85 +   "(P & True) = P", "(True & P) = P",
    4.86     "(P & False) = False", "(False & P) = False",
    4.87     "(P & P) = P", "(P & (P & Q)) = (P & Q)",
    4.88     "(P & ~P) = False",    "(~P & P) = False",
    4.89 -   "(P | True) = True", "(True | P) = True", 
    4.90 +   "(P | True) = True", "(True | P) = True",
    4.91     "(P | False) = P", "(False | P) = P",
    4.92     "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    4.93     "(P | ~P) = True",    "(~P | P) = True",
    4.94     "((~P) = (~Q)) = (P=Q)",
    4.95 -   "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
    4.96 +   "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
    4.97  (*two needed for the one-point-rule quantifier simplification procs*)
    4.98 -   "(? x. x=t & P(x)) = P(t)",		(*essential for termination!!*)
    4.99 +   "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
   4.100     "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
   4.101  
   4.102 -(* Add congruence rules for = (instead of ==) *)
   4.103 -
   4.104 -(* ###FIXME: Move to simplifier, 
   4.105 -   taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *)
   4.106 -infix 4 addcongs delcongs;
   4.107 -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
   4.108 -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
   4.109 -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
   4.110 -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
   4.111 -
   4.112 -val cong_add_global = Simplifier.change_global_ss (op addcongs);
   4.113 -val cong_del_global = Simplifier.change_global_ss (op delcongs);
   4.114 -val cong_add_local = Simplifier.change_local_ss (op addcongs);
   4.115 -val cong_del_local = Simplifier.change_local_ss (op delcongs);
   4.116 -
   4.117 -val cong_attrib_setup =
   4.118 - [Attrib.add_attributes [("cong",
   4.119 -   (Attrib.add_del_args cong_add_global cong_del_global,
   4.120 -    Attrib.add_del_args cong_add_local cong_del_local),
   4.121 -    "declare Simplifier congruence rules")]];
   4.122 -
   4.123 -
   4.124  val imp_cong = impI RSN
   4.125      (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   4.126          (fn _=> [(Blast_tac 1)]) RS mp RS mp);
   4.127 @@ -235,8 +214,8 @@
   4.128  prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))";
   4.129  
   4.130  
   4.131 -(*Avoids duplication of subgoals after split_if, when the true and false 
   4.132 -  cases boil down to the same thing.*) 
   4.133 +(*Avoids duplication of subgoals after split_if, when the true and false
   4.134 +  cases boil down to the same thing.*)
   4.135  prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
   4.136  
   4.137  prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))";
   4.138 @@ -250,19 +229,19 @@
   4.139  (* '&' congruence rule: not included by default!
   4.140     May slow rewrite proofs down by as much as 50% *)
   4.141  
   4.142 -let val th = prove_goal (the_context ()) 
   4.143 +let val th = prove_goal (the_context ())
   4.144                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   4.145                  (fn _=> [(Blast_tac 1)])
   4.146  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   4.147  
   4.148 -let val th = prove_goal (the_context ()) 
   4.149 +let val th = prove_goal (the_context ())
   4.150                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   4.151                  (fn _=> [(Blast_tac 1)])
   4.152  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   4.153  
   4.154  (* '|' congruence rule: not included by default! *)
   4.155  
   4.156 -let val th = prove_goal (the_context ()) 
   4.157 +let val th = prove_goal (the_context ())
   4.158                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   4.159                  (fn _=> [(Blast_tac 1)])
   4.160  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   4.161 @@ -393,7 +372,7 @@
   4.162  
   4.163  (*In general it seems wrong to add distributive laws by default: they
   4.164    might cause exponential blow-up.  But imp_disjL has been in for a while
   4.165 -  and cannot be removed without affecting existing proofs.  Moreover, 
   4.166 +  and cannot be removed without affecting existing proofs.  Moreover,
   4.167    rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   4.168    grounds that it allows simplification of R in the two cases.*)
   4.169  
   4.170 @@ -433,14 +412,16 @@
   4.171           eq_assume_tac, ematch_tac [FalseE]];
   4.172  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   4.173  
   4.174 -val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   4.175 -			    setSSolver safe_solver
   4.176 -			    setSolver  unsafe_solver
   4.177 -			    setmksimps (mksimps mksimps_pairs)
   4.178 -			    setmkeqTrue mk_eq_True;
   4.179 +val HOL_basic_ss =
   4.180 +  empty_ss setsubgoaler asm_simp_tac
   4.181 +    setSSolver safe_solver
   4.182 +    setSolver unsafe_solver
   4.183 +    setmksimps (mksimps mksimps_pairs)
   4.184 +    setmkeqTrue mk_eq_True
   4.185 +    setmkcong mk_meta_cong;
   4.186  
   4.187 -val HOL_ss = 
   4.188 -    HOL_basic_ss addsimps 
   4.189 +val HOL_ss =
   4.190 +    HOL_basic_ss addsimps
   4.191       ([triv_forall_equality, (* prunes params *)
   4.192         True_implies_equals, (* prune asms `True' *)
   4.193         eta_contract_eq, (* prunes eta-expansions *)
   4.194 @@ -486,7 +467,7 @@
   4.195    during unification.*)
   4.196  fun expand_case_tac P i =
   4.197      res_inst_tac [("P",P)] expand_case i THEN
   4.198 -    Simp_tac (i+1) THEN 
   4.199 +    Simp_tac (i+1) THEN
   4.200      Simp_tac i;
   4.201  
   4.202  (*This lemma restricts the effect of the rewrite rule u=v to the left-hand
   4.203 @@ -496,9 +477,8 @@
   4.204  qed "restrict_to_left";
   4.205  
   4.206  (* default simpset *)
   4.207 -val simpsetup = 
   4.208 -    [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; 
   4.209 -		thy)];
   4.210 +val simpsetup =
   4.211 +  [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
   4.212  
   4.213  
   4.214  (*** integration of simplifier with classical reasoner ***)
   4.215 @@ -523,7 +503,7 @@
   4.216  
   4.217  
   4.218  (*** A general refutation procedure ***)
   4.219 - 
   4.220 +
   4.221  (* Parameters:
   4.222  
   4.223     test: term -> bool
     5.1 --- a/src/Sequents/simpdata.ML	Tue Aug 29 00:54:22 2000 +0200
     5.2 +++ b/src/Sequents/simpdata.ML	Tue Aug 29 00:55:31 2000 +0200
     5.3 @@ -10,10 +10,10 @@
     5.4  
     5.5  (*** Rewrite rules ***)
     5.6  
     5.7 -fun prove_fun s = 
     5.8 - (writeln s;  
     5.9 +fun prove_fun s =
    5.10 + (writeln s;
    5.11    prove_goal LK.thy s
    5.12 -   (fn prems => [ (cut_facts_tac prems 1), 
    5.13 +   (fn prems => [ (cut_facts_tac prems 1),
    5.14                    (fast_tac (pack() add_safes [subst]) 1) ]));
    5.15  
    5.16  val conj_simps = map prove_fun
    5.17 @@ -34,7 +34,7 @@
    5.18  
    5.19  val imp_simps = map prove_fun
    5.20   ["|- (P --> False) <-> ~P",       "|- (P --> True) <-> True",
    5.21 -  "|- (False --> P) <-> True",     "|- (True --> P) <-> P", 
    5.22 +  "|- (False --> P) <-> True",     "|- (True --> P) <-> P",
    5.23    "|- (P --> P) <-> True",         "|- (P --> ~P) <-> ~P"];
    5.24  
    5.25  val iff_simps = map prove_fun
    5.26 @@ -44,40 +44,40 @@
    5.27  
    5.28  
    5.29  val quant_simps = map prove_fun
    5.30 - ["|- (ALL x. P) <-> P",   
    5.31 + ["|- (ALL x. P) <-> P",
    5.32    "|- (ALL x. x=t --> P(x)) <-> P(t)",
    5.33    "|- (ALL x. t=x --> P(x)) <-> P(t)",
    5.34    "|- (EX x. P) <-> P",
    5.35 -  "|- (EX x. x=t & P(x)) <-> P(t)", 
    5.36 +  "|- (EX x. x=t & P(x)) <-> P(t)",
    5.37    "|- (EX x. t=x & P(x)) <-> P(t)"];
    5.38  
    5.39  (*** Miniscoping: pushing quantifiers in
    5.40       We do NOT distribute of ALL over &, or dually that of EX over |
    5.41 -     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
    5.42 +     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
    5.43       show that this step can increase proof length!
    5.44  ***)
    5.45  
    5.46  (*existential miniscoping*)
    5.47 -val ex_simps = map prove_fun 
    5.48 +val ex_simps = map prove_fun
    5.49                     ["|- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    5.50 -		    "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    5.51 -		    "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    5.52 -		    "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
    5.53 -		    "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    5.54 -		    "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    5.55 +                    "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    5.56 +                    "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    5.57 +                    "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
    5.58 +                    "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    5.59 +                    "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    5.60  
    5.61  (*universal miniscoping*)
    5.62  val all_simps = map prove_fun
    5.63                      ["|- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    5.64 -		     "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    5.65 -		     "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    5.66 -		     "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
    5.67 -		     "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    5.68 -		     "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    5.69 +                     "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    5.70 +                     "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    5.71 +                     "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
    5.72 +                     "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    5.73 +                     "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    5.74  
    5.75  (*These are NOT supplied by default!*)
    5.76  val distrib_simps  = map prove_fun
    5.77 - ["|- P & (Q | R) <-> P&Q | P&R", 
    5.78 + ["|- P & (Q | R) <-> P&Q | P&R",
    5.79    "|- (Q | R) & P <-> Q&P | R&P",
    5.80    "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
    5.81  
    5.82 @@ -91,29 +91,29 @@
    5.83   case concl_of r of
    5.84     Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
    5.85       (case (forms_of_seq a, forms_of_seq c) of
    5.86 -	([], [p]) =>
    5.87 -	  (case p of
    5.88 -	       Const("op -->",_)$_$_ => atomize(r RS mp_R)
    5.89 -	     | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    5.90 -		   atomize(r RS conjunct2)
    5.91 -	     | Const("All",_)$_      => atomize(r RS spec)
    5.92 -	     | Const("True",_)       => []    (*True is DELETED*)
    5.93 -	     | Const("False",_)      => []    (*should False do something?*)
    5.94 -	     | _                     => [r])
    5.95 +        ([], [p]) =>
    5.96 +          (case p of
    5.97 +               Const("op -->",_)$_$_ => atomize(r RS mp_R)
    5.98 +             | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    5.99 +                   atomize(r RS conjunct2)
   5.100 +             | Const("All",_)$_      => atomize(r RS spec)
   5.101 +             | Const("True",_)       => []    (*True is DELETED*)
   5.102 +             | Const("False",_)      => []    (*should False do something?*)
   5.103 +             | _                     => [r])
   5.104        | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
   5.105   | _ => [r];
   5.106  
   5.107  
   5.108  Goal "|- ~P ==> |- (P <-> False)";
   5.109  by (etac (thinR RS cut) 1);
   5.110 -by (Fast_tac 1);		
   5.111 +by (Fast_tac 1);
   5.112  qed "P_iff_F";
   5.113  
   5.114  val iff_reflection_F = P_iff_F RS iff_reflection;
   5.115  
   5.116  Goal "|- P ==> |- (P <-> True)";
   5.117  by (etac (thinR RS cut) 1);
   5.118 -by (Fast_tac 1);		
   5.119 +by (Fast_tac 1);
   5.120  qed "P_iff_T";
   5.121  
   5.122  val iff_reflection_T = P_iff_T RS iff_reflection;
   5.123 @@ -122,22 +122,23 @@
   5.124  fun mk_meta_eq th = case concl_of th of
   5.125      Const("==",_)$_$_           => th
   5.126    | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
   5.127 -	(case (forms_of_seq a, forms_of_seq c) of
   5.128 -	     ([], [p]) => 
   5.129 -		 (case p of
   5.130 -		      (Const("op =",_)$_$_)   => th RS eq_reflection
   5.131 -		    | (Const("op <->",_)$_$_) => th RS iff_reflection
   5.132 -		    | (Const("Not",_)$_)      => th RS iff_reflection_F
   5.133 -		    | _                       => th RS iff_reflection_T)
   5.134 -	   | _ => error ("addsimps: unable to use theorem\n" ^
   5.135 -			 string_of_thm th));
   5.136 +        (case (forms_of_seq a, forms_of_seq c) of
   5.137 +             ([], [p]) =>
   5.138 +                 (case p of
   5.139 +                      (Const("op =",_)$_$_)   => th RS eq_reflection
   5.140 +                    | (Const("op <->",_)$_$_) => th RS iff_reflection
   5.141 +                    | (Const("Not",_)$_)      => th RS iff_reflection_F
   5.142 +                    | _                       => th RS iff_reflection_T)
   5.143 +           | _ => error ("addsimps: unable to use theorem\n" ^
   5.144 +                         string_of_thm th));
   5.145  
   5.146  
   5.147  (*Replace premises x=y, X<->Y by X==Y*)
   5.148 -val mk_meta_prems = 
   5.149 -    rule_by_tactic 
   5.150 +val mk_meta_prems =
   5.151 +    rule_by_tactic
   5.152        (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
   5.153  
   5.154 +(*Congruence rules for = or <-> (instead of ==)*)
   5.155  fun mk_meta_cong rl =
   5.156    standard(mk_meta_eq (mk_meta_prems rl))
   5.157    handle THM _ =>
   5.158 @@ -147,7 +148,7 @@
   5.159  (*** Named rewrite rules ***)
   5.160  
   5.161  fun prove nm thm  = qed_goal nm LK.thy thm
   5.162 -    (fn prems => [ (cut_facts_tac prems 1), 
   5.163 +    (fn prems => [ (cut_facts_tac prems 1),
   5.164                     (fast_tac LK_pack 1) ]);
   5.165  
   5.166  prove "conj_commute" "|- P&Q <-> Q&P";
   5.167 @@ -177,26 +178,26 @@
   5.168  prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
   5.169  
   5.170  
   5.171 -val [p1,p2] = Goal 
   5.172 +val [p1,p2] = Goal
   5.173      "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
   5.174  by (lemma_tac p1 1);
   5.175  by (Safe_tac 1);
   5.176 -by (REPEAT (rtac cut 1 
   5.177 -	    THEN
   5.178 -	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   5.179 -	    THEN
   5.180 -	    Safe_tac 1));
   5.181 +by (REPEAT (rtac cut 1
   5.182 +            THEN
   5.183 +            DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   5.184 +            THEN
   5.185 +            Safe_tac 1));
   5.186  qed "imp_cong";
   5.187  
   5.188 -val [p1,p2] = Goal 
   5.189 +val [p1,p2] = Goal
   5.190      "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
   5.191  by (lemma_tac p1 1);
   5.192  by (Safe_tac 1);
   5.193 -by (REPEAT (rtac cut 1 
   5.194 -	    THEN
   5.195 -	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   5.196 -	    THEN
   5.197 -	    Safe_tac 1));
   5.198 +by (REPEAT (rtac cut 1
   5.199 +            THEN
   5.200 +            DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   5.201 +            THEN
   5.202 +            Safe_tac 1));
   5.203  qed "conj_cong";
   5.204  
   5.205  Goal "|- (x=y) <-> (y=x)";
   5.206 @@ -229,32 +230,26 @@
   5.207  
   5.208  (*** Standard simpsets ***)
   5.209  
   5.210 -(*Add congruence rules for = or <-> (instead of ==) *)
   5.211 -infix 4 addcongs delcongs;
   5.212 -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
   5.213 -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
   5.214 -
   5.215 -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
   5.216 -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
   5.217 -
   5.218  val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
   5.219  
   5.220  fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
   5.221 -				 assume_tac];
   5.222 +                                 assume_tac];
   5.223  (*No premature instantiation of variables during simplification*)
   5.224  fun   safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
   5.225 -				 eq_assume_tac];
   5.226 +                                 eq_assume_tac];
   5.227  
   5.228  (*No simprules, but basic infrastructure for simplification*)
   5.229 -val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
   5.230 -			   setSSolver   (mk_solver "safe" safe_solver)
   5.231 -			   setSolver    (mk_solver "unsafe" unsafe_solver)
   5.232 -			   setmksimps   (map mk_meta_eq o atomize o gen_all);
   5.233 +val LK_basic_ss =
   5.234 +  empty_ss setsubgoaler asm_simp_tac
   5.235 +    setSSolver (mk_solver "safe" safe_solver)
   5.236 +    setSolver (mk_solver "unsafe" unsafe_solver)
   5.237 +    setmksimps (map mk_meta_eq o atomize o gen_all)
   5.238 +    setmkcong mk_meta_cong;
   5.239  
   5.240  val LK_simps =
   5.241     [triv_forall_equality, (* prunes params *)
   5.242 -    refl RS P_iff_T] @ 
   5.243 -    conj_simps @ disj_simps @ not_simps @ 
   5.244 +    refl RS P_iff_T] @
   5.245 +    conj_simps @ disj_simps @ not_simps @
   5.246      imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
   5.247      [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
   5.248      map prove_fun
   5.249 @@ -262,8 +257,10 @@
   5.250        "|- ~ ~ P <-> P",        "|- (~P --> P) <-> P",
   5.251        "|- (~P <-> ~Q) <-> (P<->Q)"];
   5.252  
   5.253 -val LK_ss = LK_basic_ss addsimps LK_simps addeqcongs [left_cong]
   5.254 -					  addcongs [imp_cong];
   5.255 +val LK_ss =
   5.256 +  LK_basic_ss addsimps LK_simps
   5.257 +  addeqcongs [left_cong]
   5.258 +  addcongs [imp_cong];
   5.259  
   5.260  simpset_ref() := LK_ss;
   5.261