src/FOL/simpdata.ML
changeset 9713 2c5b42311eb0
parent 9300 ee5c9672d208
child 9851 e22db9397e17
     1.1 --- a/src/FOL/simpdata.ML	Tue Aug 29 00:54:22 2000 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Aug 29 00:55:31 2000 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Simplification data for FOL
     1.5  *)
     1.6  
     1.7 -(*** Addition of rules to simpsets and clasets simultaneously ***)	(* FIXME move to Provers/clasimp.ML? *)
     1.8 +(*** Addition of rules to simpsets and clasets simultaneously ***)      (* FIXME move to Provers/clasimp.ML? *)
     1.9  
    1.10  infix 4 addIffs delIffs;
    1.11  
    1.12 @@ -30,15 +30,15 @@
    1.13  
    1.14    fun delIff ((cla, simp), th) = 
    1.15        (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
    1.16 -	   (Const ("Not", _) $ A) =>
    1.17 -	       cla delrules [zero_var_indexes (th RS notE)]
    1.18 -	 | (Const("op <->", _) $ _ $ _) =>
    1.19 -	       cla delrules [zero_var_indexes (th RS iffD2),
    1.20 -			     cla_make_elim (zero_var_indexes (th RS iffD1))]
    1.21 -	 | _ => cla delrules [th],
    1.22 +           (Const ("Not", _) $ A) =>
    1.23 +               cla delrules [zero_var_indexes (th RS notE)]
    1.24 +         | (Const("op <->", _) $ _ $ _) =>
    1.25 +               cla delrules [zero_var_indexes (th RS iffD2),
    1.26 +                             cla_make_elim (zero_var_indexes (th RS iffD1))]
    1.27 +         | _ => cla delrules [th],
    1.28         simp delsimps [th])
    1.29        handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.30 -				string_of_thm th); (cla, simp));
    1.31 +                                string_of_thm th); (cla, simp));
    1.32  
    1.33    fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    1.34  in
    1.35 @@ -139,6 +139,7 @@
    1.36      rule_by_tactic 
    1.37        (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
    1.38  
    1.39 +(*Congruence rules for = or <-> (instead of ==)*)
    1.40  fun mk_meta_cong rl =
    1.41    standard(mk_meta_eq (mk_meta_prems rl))
    1.42    handle THM _ =>
    1.43 @@ -188,29 +189,29 @@
    1.44  
    1.45  (*existential miniscoping*)
    1.46  val int_ex_simps = map int_prove_fun 
    1.47 -		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    1.48 -		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    1.49 -		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    1.50 -		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
    1.51 +                     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    1.52 +                      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    1.53 +                      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    1.54 +                      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
    1.55  
    1.56  (*classical rules*)
    1.57  val cla_ex_simps = map prove_fun 
    1.58                       ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    1.59 -		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    1.60 +                      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    1.61  
    1.62  val ex_simps = int_ex_simps @ cla_ex_simps;
    1.63  
    1.64  (*universal miniscoping*)
    1.65  val int_all_simps = map int_prove_fun
    1.66 -		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    1.67 -		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    1.68 -		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    1.69 -		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    1.70 +                      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    1.71 +                       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    1.72 +                       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    1.73 +                       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    1.74  
    1.75  (*classical rules*)
    1.76  val cla_all_simps = map prove_fun
    1.77                        ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    1.78 -		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    1.79 +                       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    1.80  
    1.81  val all_simps = int_all_simps @ cla_all_simps;
    1.82  
    1.83 @@ -338,28 +339,6 @@
    1.84  open Induction;
    1.85  
    1.86  
    1.87 -(* Add congruence rules for = or <-> (instead of ==) *)
    1.88 -
    1.89 -(* ###FIXME: Move to simplifier, 
    1.90 -   taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *)
    1.91 -infix 4 addcongs delcongs;
    1.92 -fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
    1.93 -fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
    1.94 -fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.95 -fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.96 -
    1.97 -val cong_add_global = Simplifier.change_global_ss (op addcongs);
    1.98 -val cong_del_global = Simplifier.change_global_ss (op delcongs);
    1.99 -val cong_add_local = Simplifier.change_local_ss (op addcongs);
   1.100 -val cong_del_local = Simplifier.change_local_ss (op delcongs);
   1.101 -
   1.102 -val cong_attrib_setup =
   1.103 - [Attrib.add_attributes [("cong",
   1.104 -   (Attrib.add_del_args cong_add_global cong_del_global,
   1.105 -    Attrib.add_del_args cong_add_local cong_del_local),
   1.106 -    "declare Simplifier congruence rules")]];
   1.107 -
   1.108 -
   1.109  val meta_simps =
   1.110     [triv_forall_equality,  (* prunes params *)
   1.111      True_implies_equals];  (* prune asms `True' *)
   1.112 @@ -372,27 +351,28 @@
   1.113  val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
   1.114  
   1.115  fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
   1.116 -				 atac, etac FalseE];
   1.117 +                                 atac, etac FalseE];
   1.118  (*No premature instantiation of variables during simplification*)
   1.119  fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
   1.120 -				 eq_assume_tac, ematch_tac [FalseE]];
   1.121 +                                 eq_assume_tac, ematch_tac [FalseE]];
   1.122  
   1.123  (*No simprules, but basic infastructure for simplification*)
   1.124 -val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   1.125 -                            addsimprocs [defALL_regroup,defEX_regroup]
   1.126 -			    setSSolver  (mk_solver "FOL safe" safe_solver)
   1.127 -			    setSolver  (mk_solver "FOL unsafe" unsafe_solver)
   1.128 -			    setmksimps (mksimps mksimps_pairs);
   1.129 -
   1.130 +val FOL_basic_ss =
   1.131 +  empty_ss setsubgoaler asm_simp_tac
   1.132 +    addsimprocs [defALL_regroup, defEX_regroup]
   1.133 +    setSSolver (mk_solver "FOL safe" safe_solver)
   1.134 +    setSolver (mk_solver "FOL unsafe" unsafe_solver)
   1.135 +    setmksimps (mksimps mksimps_pairs)
   1.136 +    setmkcong mk_meta_cong;
   1.137  
   1.138  
   1.139  (*intuitionistic simprules only*)
   1.140 -val IFOL_ss = 
   1.141 -    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ 
   1.142 -			   int_ex_simps @ int_all_simps)
   1.143 +val IFOL_ss =
   1.144 +    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @
   1.145 +                           int_ex_simps @ int_all_simps)
   1.146                   addcongs [imp_cong];
   1.147  
   1.148 -val cla_simps = 
   1.149 +val cla_simps =
   1.150      [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
   1.151       not_all, not_ex, cases_simp] @
   1.152      map prove_fun