--- a/src/HOL/simpdata.ML Thu Oct 10 10:45:20 1996 +0200
+++ b/src/HOL/simpdata.ML Thu Oct 10 10:46:14 1996 +0200
@@ -106,24 +106,24 @@
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
- val simp_thms = map prover
- [ "(x=x) = True",
- "(~True) = False", "(~False) = True", "(~ ~ P) = P",
- "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
- "(True=P) = P", "(P=True) = P",
- "(True --> P) = P", "(False --> P) = True",
- "(P --> True) = True", "(P --> P) = True",
- "(P --> False) = (~P)", "(P --> ~P) = (~P)",
- "(P & True) = P", "(True & P) = P",
- "(P & False) = False", "(False & P) = False", "(P & P) = P",
- "(P | True) = True", "(True | P) = True",
- "(P | False) = P", "(False | P) = P", "(P | P) = P",
- "((~P) = (~Q)) = (P=Q)",
- "(!x.P) = P", "(? x.P) = P", "? x. x=t",
- "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
- "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
+in
-in
+val simp_thms = map prover
+ [ "(x=x) = True",
+ "(~True) = False", "(~False) = True", "(~ ~ P) = P",
+ "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
+ "(True=P) = P", "(P=True) = P",
+ "(True --> P) = P", "(False --> P) = True",
+ "(P --> True) = True", "(P --> P) = True",
+ "(P --> False) = (~P)", "(P --> ~P) = (~P)",
+ "(P & True) = P", "(True & P) = P",
+ "(P & False) = False", "(False & P) = False", "(P & P) = P",
+ "(P | True) = True", "(True | P) = True",
+ "(P | False) = P", "(False | P) = P", "(P | P) = P",
+ "((~P) = (~Q)) = (P=Q)",
+ "(!x.P) = P", "(? x.P) = P", "? x. x=t",
+ "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
+ "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"
(fn [prem] => [rewtac prem, rtac refl 1]);
@@ -201,17 +201,6 @@
"(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
"(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
-val HOL_ss = empty_ss
- setmksimps (mksimps mksimps_pairs)
- setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
- ORELSE' etac FalseE)
- setsubgoaler asm_simp_tac
- addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
- cases_simp]
- @ ex_simps @ all_simps @ simp_thms)
- addcongs [imp_cong];
-
-
(*In general it seems wrong to add distributive laws by default: they
might cause exponential blow-up. But imp_disj has been in for a while
and cannot be removed without affecting existing proofs. Moreover,
@@ -318,6 +307,17 @@
prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
+val HOL_ss = empty_ss
+ setmksimps (mksimps mksimps_pairs)
+ setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
+ ORELSE' etac FalseE)
+ setsubgoaler asm_simp_tac
+ addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
+ de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
+ @ ex_simps @ all_simps @ simp_thms)
+ addcongs [imp_cong];
+
+
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);