src/HOL/simpdata.ML
changeset 2082 8659e3063a30
parent 2054 bf3891343aa5
child 2097 076a8d2f972b
     1.1 --- a/src/HOL/simpdata.ML	Thu Oct 10 10:45:20 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Oct 10 10:46:14 1996 +0200
     1.3 @@ -106,24 +106,24 @@
     1.4  
     1.5    fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
     1.6  
     1.7 -  val simp_thms = map prover
     1.8 -   [ "(x=x) = True",
     1.9 -     "(~True) = False", "(~False) = True", "(~ ~ P) = P",
    1.10 -     "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    1.11 -     "(True=P) = P", "(P=True) = P",
    1.12 -     "(True --> P) = P", "(False --> P) = True", 
    1.13 -     "(P --> True) = True", "(P --> P) = True",
    1.14 -     "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    1.15 -     "(P & True) = P", "(True & P) = P", 
    1.16 -     "(P & False) = False", "(False & P) = False", "(P & P) = P",
    1.17 -     "(P | True) = True", "(True | P) = True", 
    1.18 -     "(P | False) = P", "(False | P) = P", "(P | P) = P",
    1.19 -     "((~P) = (~Q)) = (P=Q)",
    1.20 -     "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
    1.21 -     "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
    1.22 -     "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
    1.23 +in
    1.24  
    1.25 -in
    1.26 +val simp_thms = map prover
    1.27 + [ "(x=x) = True",
    1.28 +   "(~True) = False", "(~False) = True", "(~ ~ P) = P",
    1.29 +   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    1.30 +   "(True=P) = P", "(P=True) = P",
    1.31 +   "(True --> P) = P", "(False --> P) = True", 
    1.32 +   "(P --> True) = True", "(P --> P) = True",
    1.33 +   "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    1.34 +   "(P & True) = P", "(True & P) = P", 
    1.35 +   "(P & False) = False", "(False & P) = False", "(P & P) = P",
    1.36 +   "(P | True) = True", "(True | P) = True", 
    1.37 +   "(P | False) = P", "(False | P) = P", "(P | P) = P",
    1.38 +   "((~P) = (~Q)) = (P=Q)",
    1.39 +   "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
    1.40 +   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
    1.41 +   "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
    1.42  
    1.43  val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"
    1.44    (fn [prem] => [rewtac prem, rtac refl 1]);
    1.45 @@ -201,17 +201,6 @@
    1.46                   "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
    1.47                   "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
    1.48  
    1.49 -val HOL_ss = empty_ss
    1.50 -      setmksimps (mksimps mksimps_pairs)
    1.51 -      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
    1.52 -                             ORELSE' etac FalseE)
    1.53 -      setsubgoaler asm_simp_tac
    1.54 -      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
    1.55 -                 cases_simp]
    1.56 -        @ ex_simps @ all_simps @ simp_thms)
    1.57 -      addcongs [imp_cong];
    1.58 -
    1.59 -
    1.60  (*In general it seems wrong to add distributive laws by default: they
    1.61    might cause exponential blow-up.  But imp_disj has been in for a while
    1.62    and cannot be removed without affecting existing proofs.  Moreover, 
    1.63 @@ -318,6 +307,17 @@
    1.64  prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
    1.65  
    1.66  
    1.67 +val HOL_ss = empty_ss
    1.68 +      setmksimps (mksimps mksimps_pairs)
    1.69 +      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
    1.70 +                             ORELSE' etac FalseE)
    1.71 +      setsubgoaler asm_simp_tac
    1.72 +      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
    1.73 +                 de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
    1.74 +        @ ex_simps @ all_simps @ simp_thms)
    1.75 +      addcongs [imp_cong];
    1.76 +
    1.77 +
    1.78  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.79    (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    1.80