FOL_basic_ss: simprocs moved to FOL_ss;
authorwenzelm
Fri Nov 10 19:01:33 2000 +0100 (2000-11-10 ago)
changeset 10431bb67f704d631
parent 10430 d3f780c3af0c
child 10432 3dfbc913d184
FOL_basic_ss: simprocs moved to FOL_ss;
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Fri Nov 10 19:00:51 2000 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Nov 10 19:01:33 2000 +0100
     1.3 @@ -18,10 +18,10 @@
     1.4  
     1.5  (*** Rewrite rules ***)
     1.6  
     1.7 -fun int_prove_fun s = 
     1.8 - (writeln s;  
     1.9 +fun int_prove_fun s =
    1.10 + (writeln s;
    1.11    prove_goal IFOL.thy s
    1.12 -   (fn prems => [ (cut_facts_tac prems 1), 
    1.13 +   (fn prems => [ (cut_facts_tac prems 1),
    1.14                    (IntPr.fast_tac 1) ]));
    1.15  
    1.16  val conj_simps = map int_prove_fun
    1.17 @@ -43,7 +43,7 @@
    1.18  
    1.19  val imp_simps = map int_prove_fun
    1.20   ["(P --> False) <-> ~P",       "(P --> True) <-> True",
    1.21 -  "(False --> P) <-> True",     "(True --> P) <-> P", 
    1.22 +  "(False --> P) <-> True",     "(True --> P) <-> P",
    1.23    "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
    1.24  
    1.25  val iff_simps = map int_prove_fun
    1.26 @@ -53,16 +53,16 @@
    1.27  
    1.28  (*The x=t versions are needed for the simplification procedures*)
    1.29  val quant_simps = map int_prove_fun
    1.30 - ["(ALL x. P) <-> P",   
    1.31 + ["(ALL x. P) <-> P",
    1.32    "(ALL x. x=t --> P(x)) <-> P(t)",
    1.33    "(ALL x. t=x --> P(x)) <-> P(t)",
    1.34    "(EX x. P) <-> P",
    1.35 -  "(EX x. x=t & P(x)) <-> P(t)", 
    1.36 +  "(EX x. x=t & P(x)) <-> P(t)",
    1.37    "(EX x. t=x & P(x)) <-> P(t)"];
    1.38  
    1.39  (*These are NOT supplied by default!*)
    1.40  val distrib_simps  = map int_prove_fun
    1.41 - ["P & (Q | R) <-> P&Q | P&R", 
    1.42 + ["P & (Q | R) <-> P&Q | P&R",
    1.43    "(Q | R) & P <-> Q&P | R&P",
    1.44    "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
    1.45  
    1.46 @@ -81,7 +81,7 @@
    1.47  fun mk_meta_eq th = case concl_of th of
    1.48      _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
    1.49    | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
    1.50 -  | _                           => 
    1.51 +  | _                           =>
    1.52    error("conclusion must be a =-equality or <->");;
    1.53  
    1.54  fun mk_eq th = case concl_of th of
    1.55 @@ -92,8 +92,8 @@
    1.56    | _                           => th RS iff_reflection_T;
    1.57  
    1.58  (*Replace premises x=y, X<->Y by X==Y*)
    1.59 -val mk_meta_prems = 
    1.60 -    rule_by_tactic 
    1.61 +val mk_meta_prems =
    1.62 +    rule_by_tactic
    1.63        (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
    1.64  
    1.65  (*Congruence rules for = or <-> (instead of ==)*)
    1.66 @@ -127,32 +127,32 @@
    1.67  
    1.68  (*** Classical laws ***)
    1.69  
    1.70 -fun prove_fun s = 
    1.71 - (writeln s;  
    1.72 +fun prove_fun s =
    1.73 + (writeln s;
    1.74    prove_goal (the_context ()) s
    1.75 -   (fn prems => [ (cut_facts_tac prems 1), 
    1.76 +   (fn prems => [ (cut_facts_tac prems 1),
    1.77                    (Cla.fast_tac FOL_cs 1) ]));
    1.78  
    1.79 -(*Avoids duplication of subgoals after expand_if, when the true and false 
    1.80 -  cases boil down to the same thing.*) 
    1.81 +(*Avoids duplication of subgoals after expand_if, when the true and false
    1.82 +  cases boil down to the same thing.*)
    1.83  val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
    1.84  
    1.85  
    1.86  (*** Miniscoping: pushing quantifiers in
    1.87       We do NOT distribute of ALL over &, or dually that of EX over |
    1.88 -     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
    1.89 +     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
    1.90       show that this step can increase proof length!
    1.91  ***)
    1.92  
    1.93  (*existential miniscoping*)
    1.94 -val int_ex_simps = map int_prove_fun 
    1.95 +val int_ex_simps = map int_prove_fun
    1.96                       ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    1.97                        "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    1.98                        "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    1.99                        "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
   1.100  
   1.101  (*classical rules*)
   1.102 -val cla_ex_simps = map prove_fun 
   1.103 +val cla_ex_simps = map prove_fun
   1.104                       ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
   1.105                        "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
   1.106  
   1.107 @@ -176,7 +176,7 @@
   1.108  (*** Named rewrite rules proved for IFOL ***)
   1.109  
   1.110  fun int_prove nm thm  = qed_goal nm IFOL.thy thm
   1.111 -    (fn prems => [ (cut_facts_tac prems 1), 
   1.112 +    (fn prems => [ (cut_facts_tac prems 1),
   1.113                     (IntPr.fast_tac 1) ]);
   1.114  
   1.115  fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]);
   1.116 @@ -301,7 +301,7 @@
   1.117      True_implies_equals];  (* prune asms `True' *)
   1.118  
   1.119  val IFOL_simps =
   1.120 -    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
   1.121 +    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @
   1.122      imp_simps @ iff_simps @ quant_simps;
   1.123  
   1.124  val notFalseI = int_prove_fun "~False";
   1.125 @@ -314,20 +314,19 @@
   1.126                                   eq_assume_tac, ematch_tac [FalseE]];
   1.127  
   1.128  (*No simprules, but basic infastructure for simplification*)
   1.129 -val FOL_basic_ss =
   1.130 -  empty_ss setsubgoaler asm_simp_tac
   1.131 -    addsimprocs [defALL_regroup, defEX_regroup]
   1.132 -    setSSolver (mk_solver "FOL safe" safe_solver)
   1.133 -    setSolver (mk_solver "FOL unsafe" unsafe_solver)
   1.134 -    setmksimps (mksimps mksimps_pairs)
   1.135 -    setmkcong mk_meta_cong;
   1.136 +val FOL_basic_ss = empty_ss
   1.137 +  setsubgoaler asm_simp_tac
   1.138 +  setSSolver (mk_solver "FOL safe" safe_solver)
   1.139 +  setSolver (mk_solver "FOL unsafe" unsafe_solver)
   1.140 +  setmksimps (mksimps mksimps_pairs)
   1.141 +  setmkcong mk_meta_cong;
   1.142  
   1.143  
   1.144  (*intuitionistic simprules only*)
   1.145 -val IFOL_ss =
   1.146 -    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @
   1.147 -                           int_ex_simps @ int_all_simps)
   1.148 -                 addcongs [imp_cong];
   1.149 +val IFOL_ss = FOL_basic_ss
   1.150 +  addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps)
   1.151 +  addsimprocs [defALL_regroup, defEX_regroup]    
   1.152 +  addcongs [imp_cong];
   1.153  
   1.154  val cla_simps =
   1.155      [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,