src/FOL/simpdata.ML
changeset 4349 50403e5a44c0
parent 4325 e72cba5af6c5
child 4477 b3e5857d8d99
     1.1 --- a/src/FOL/simpdata.ML	Wed Dec 03 10:47:13 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Dec 03 10:48:16 1997 +0100
     1.3 @@ -41,8 +41,14 @@
     1.4    "(P <-> P) <-> True",
     1.5    "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
     1.6  
     1.7 +(*The x=t versions are needed for the simplification procedures*)
     1.8  val quant_simps = map int_prove_fun
     1.9 - ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
    1.10 + ["(ALL x. P) <-> P",   
    1.11 +  "(ALL x. x=t --> P(x)) <-> P(t)",
    1.12 +  "(ALL x. t=x --> P(x)) <-> P(t)",
    1.13 +  "(EX x. P) <-> P",
    1.14 +  "(EX x. x=t & P(x)) <-> P(t)", 
    1.15 +  "(EX x. t=x & P(x)) <-> P(t)"];
    1.16  
    1.17  (*These are NOT supplied by default!*)
    1.18  val distrib_simps  = map int_prove_fun
    1.19 @@ -96,30 +102,43 @@
    1.20    cases boil down to the same thing.*) 
    1.21  val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
    1.22  
    1.23 -(*At present, miniscoping is for classical logic only.  We do NOT include
    1.24 -  distribution of ALL over &, or dually that of EX over |.*)
    1.25 +
    1.26 +(*** Miniscoping: pushing quantifiers in
    1.27 +     We do NOT distribute of ALL over &, or dually that of EX over |
    1.28 +     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
    1.29 +     show that this step can increase proof length!
    1.30 +***)
    1.31 +
    1.32 +(*existential miniscoping*)
    1.33 +val int_ex_simps = map int_prove_fun 
    1.34 +		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    1.35 +		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    1.36 +		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    1.37 +		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
    1.38 +
    1.39 +(*classical rules*)
    1.40 +val cla_ex_simps = map prove_fun 
    1.41 +                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    1.42 +		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    1.43  
    1.44 -(*Miniscoping: pushing in existential quantifiers*)
    1.45 -val ex_simps = map prove_fun 
    1.46 -                ["(EX x. x=t & P(x)) <-> P(t)",
    1.47 -                 "(EX x. t=x & P(x)) <-> P(t)",
    1.48 -                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    1.49 -                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    1.50 -                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    1.51 -                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
    1.52 -                 "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    1.53 -                 "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    1.54 +val ex_simps = int_ex_simps @ cla_ex_simps;
    1.55 +
    1.56 +(*universal miniscoping*)
    1.57 +val int_all_simps = map int_prove_fun
    1.58 +		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    1.59 +		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    1.60 +		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    1.61 +		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    1.62  
    1.63 -(*Miniscoping: pushing in universal quantifiers*)
    1.64 -val all_simps = map prove_fun
    1.65 -                ["(ALL x. x=t --> P(x)) <-> P(t)",
    1.66 -                 "(ALL x. t=x --> P(x)) <-> P(t)",
    1.67 -                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    1.68 -                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    1.69 -                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    1.70 -                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
    1.71 -                 "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    1.72 -                 "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    1.73 +(*classical rules*)
    1.74 +val cla_all_simps = map prove_fun
    1.75 +                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    1.76 +		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
    1.77 +
    1.78 +val all_simps = int_all_simps @ cla_all_simps;
    1.79 +
    1.80 +
    1.81 +(*** Named rewrite rules proved for IFOL ***)
    1.82  
    1.83  fun int_prove nm thm  = qed_goal nm IFOL.thy thm
    1.84      (fn prems => [ (cut_facts_tac prems 1), 
    1.85 @@ -168,7 +187,50 @@
    1.86  val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
    1.87    (fn [prem] => [rewtac prem, rtac refl 1]);
    1.88  
    1.89 -(*** case splitting ***)
    1.90 +
    1.91 +open Simplifier;
    1.92 +
    1.93 +(** make simplification procedures for quantifier elimination **)
    1.94 +structure Quantifier1 = Quantifier1Fun(
    1.95 +struct
    1.96 +  (*abstract syntax*)
    1.97 +  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
    1.98 +    | dest_eq _ = None;
    1.99 +  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
   1.100 +    | dest_conj _ = None;
   1.101 +  val conj = FOLogic.conj
   1.102 +  val imp  = FOLogic.imp
   1.103 +  (*rules*)
   1.104 +  val iff_reflection = iff_reflection
   1.105 +  val iffI = iffI
   1.106 +  val sym  = sym
   1.107 +  val conjI= conjI
   1.108 +  val conjE= conjE
   1.109 +  val impI = impI
   1.110 +  val impE = impE
   1.111 +  val mp   = mp
   1.112 +  val exI  = exI
   1.113 +  val exE  = exE
   1.114 +  val allI = allI
   1.115 +  val allE = allE
   1.116 +end);
   1.117 +
   1.118 +local
   1.119 +val ex_pattern =
   1.120 +  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
   1.121 +
   1.122 +val all_pattern =
   1.123 +  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
   1.124 +
   1.125 +in
   1.126 +val defEX_regroup =
   1.127 +  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
   1.128 +val defALL_regroup =
   1.129 +  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
   1.130 +end;
   1.131 +
   1.132 +
   1.133 +(*** Case splitting ***)
   1.134  
   1.135  qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
   1.136          (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
   1.137 @@ -192,7 +254,7 @@
   1.138  
   1.139  structure Induction = InductionFun(struct val spec=IFOL.spec end);
   1.140  
   1.141 -open Simplifier Induction;
   1.142 +open Induction;
   1.143  
   1.144  (*Add congruence rules for = or <-> (instead of ==) *)
   1.145  infix 4 addcongs delcongs;
   1.146 @@ -222,12 +284,13 @@
   1.147  
   1.148  (*No simprules, but basic infastructure for simplification*)
   1.149  val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   1.150 +                            addsimprocs [defALL_regroup,defEX_regroup]
   1.151  			    setSSolver   safe_solver
   1.152  			    setSolver  unsafe_solver
   1.153  			    setmksimps (map mk_meta_eq o atomize o gen_all);
   1.154  
   1.155  (*intuitionistic simprules only*)
   1.156 -val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
   1.157 +val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
   1.158  			   addcongs [imp_cong];
   1.159  
   1.160  val cla_simps = 
   1.161 @@ -240,7 +303,7 @@
   1.162        "(~P <-> ~Q) <-> (P<->Q)"];
   1.163  
   1.164  (*classical simprules too*)
   1.165 -val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
   1.166 +val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
   1.167  
   1.168  simpset_ref() := FOL_ss;
   1.169