Introduction of miniscoping for FOL
authorpaulson
Thu Sep 05 18:28:01 1996 +0200 (1996-09-05)
changeset 1953832ccc1dba95
parent 1952 4acc84e5831f
child 1954 4b5b2d04782c
Introduction of miniscoping for FOL
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu Sep 05 10:30:42 1996 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Sep 05 18:28:01 1996 +0200
     1.3 @@ -14,38 +14,38 @@
     1.4     (fn prems => [ (cut_facts_tac prems 1), 
     1.5                    (Int.fast_tac 1) ]));
     1.6  
     1.7 -val conj_rews = map int_prove_fun
     1.8 +val conj_simps = map int_prove_fun
     1.9   ["P & True <-> P",      "True & P <-> P",
    1.10    "P & False <-> False", "False & P <-> False",
    1.11    "P & P <-> P",
    1.12    "P & ~P <-> False",    "~P & P <-> False",
    1.13    "(P & Q) & R <-> P & (Q & R)"];
    1.14  
    1.15 -val disj_rews = map int_prove_fun
    1.16 +val disj_simps = map int_prove_fun
    1.17   ["P | True <-> True",  "True | P <-> True",
    1.18    "P | False <-> P",    "False | P <-> P",
    1.19    "P | P <-> P",
    1.20    "(P | Q) | R <-> P | (Q | R)"];
    1.21  
    1.22 -val not_rews = map int_prove_fun
    1.23 +val not_simps = map int_prove_fun
    1.24   ["~(P|Q)  <-> ~P & ~Q",
    1.25    "~ False <-> True",   "~ True <-> False"];
    1.26  
    1.27 -val imp_rews = map int_prove_fun
    1.28 +val imp_simps = map int_prove_fun
    1.29   ["(P --> False) <-> ~P",       "(P --> True) <-> True",
    1.30    "(False --> P) <-> True",     "(True --> P) <-> P", 
    1.31    "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
    1.32  
    1.33 -val iff_rews = map int_prove_fun
    1.34 +val iff_simps = map int_prove_fun
    1.35   ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    1.36    "(P <-> P) <-> True",
    1.37    "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    1.38  
    1.39 -val quant_rews = map int_prove_fun
    1.40 +val quant_simps = map int_prove_fun
    1.41   ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
    1.42  
    1.43  (*These are NOT supplied by default!*)
    1.44 -val distrib_rews  = map int_prove_fun
    1.45 +val distrib_simps  = map int_prove_fun
    1.46   ["P & (Q | R) <-> P&Q | P&R", 
    1.47    "(Q | R) & P <-> Q&P | R&P",
    1.48    "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
    1.49 @@ -97,9 +97,9 @@
    1.50  fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
    1.51  
    1.52  
    1.53 -val IFOL_rews =
    1.54 -   [refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
    1.55 -    imp_rews @ iff_rews @ quant_rews;
    1.56 +val IFOL_simps =
    1.57 +   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.58 +    imp_simps @ iff_simps @ quant_simps;
    1.59  
    1.60  val notFalseI = int_prove_fun "~False";
    1.61  val triv_rls = [TrueI,refl,iff_refl,notFalseI];
    1.62 @@ -111,7 +111,7 @@
    1.63                            ORELSE' assume_tac
    1.64                            ORELSE' etac FalseE)
    1.65    setsubgoaler asm_simp_tac
    1.66 -  addsimps IFOL_rews
    1.67 +  addsimps IFOL_simps
    1.68    addcongs [imp_cong];
    1.69  
    1.70  (*Classical version...*)
    1.71 @@ -121,12 +121,42 @@
    1.72     (fn prems => [ (cut_facts_tac prems 1), 
    1.73                    (Cla.fast_tac FOL_cs 1) ]));
    1.74  
    1.75 -val cla_rews = map prove_fun
    1.76 - ["~(P&Q)  <-> ~P | ~Q",
    1.77 -  "P | ~P",             "~P | P",
    1.78 -  "~ ~ P <-> P",        "(~P --> P) <-> P"];
    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 +val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
    1.82 +
    1.83 +val cla_simps = 
    1.84 +    cases_simp::
    1.85 +    map prove_fun
    1.86 +     ["~(P&Q)  <-> ~P | ~Q",
    1.87 +      "P | ~P",             "~P | P",
    1.88 +      "~ ~ P <-> P",        "(~P --> P) <-> P",
    1.89 +      "(~P <-> ~Q) <-> (P<->Q)"];
    1.90 +
    1.91 +(*At present, miniscoping is for classical logic only.  We do NOT include
    1.92 +  distribution of ALL over &, or dually that of EX over |.*)
    1.93  
    1.94 -val FOL_ss = IFOL_ss addsimps cla_rews;
    1.95 +(*Miniscoping: pushing in existential quantifiers*)
    1.96 +val ex_simps = map prove_fun 
    1.97 +                ["(EX x. P) <-> P",
    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 +                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
   1.101 +                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
   1.102 +                 "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
   1.103 +                 "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
   1.104 +
   1.105 +(*Miniscoping: pushing in universal quantifiers*)
   1.106 +val all_simps = map prove_fun
   1.107 +                ["(ALL x. P) <-> P",
   1.108 +                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
   1.109 +                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
   1.110 +                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
   1.111 +                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
   1.112 +                 "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
   1.113 +                 "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
   1.114 +
   1.115 +val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
   1.116  
   1.117  fun int_prove nm thm  = qed_goal nm IFOL.thy thm
   1.118      (fn prems => [ (cut_facts_tac prems 1),