--- a/src/Sequents/simpdata.ML Tue Aug 29 00:54:22 2000 +0200
+++ b/src/Sequents/simpdata.ML Tue Aug 29 00:55:31 2000 +0200
@@ -10,10 +10,10 @@
(*** Rewrite rules ***)
-fun prove_fun s =
- (writeln s;
+fun prove_fun s =
+ (writeln s;
prove_goal LK.thy s
- (fn prems => [ (cut_facts_tac prems 1),
+ (fn prems => [ (cut_facts_tac prems 1),
(fast_tac (pack() add_safes [subst]) 1) ]));
val conj_simps = map prove_fun
@@ -34,7 +34,7 @@
val imp_simps = map prove_fun
["|- (P --> False) <-> ~P", "|- (P --> True) <-> True",
- "|- (False --> P) <-> True", "|- (True --> P) <-> P",
+ "|- (False --> P) <-> True", "|- (True --> P) <-> P",
"|- (P --> P) <-> True", "|- (P --> ~P) <-> ~P"];
val iff_simps = map prove_fun
@@ -44,40 +44,40 @@
val quant_simps = map prove_fun
- ["|- (ALL x. P) <-> P",
+ ["|- (ALL x. P) <-> P",
"|- (ALL x. x=t --> P(x)) <-> P(t)",
"|- (ALL x. t=x --> P(x)) <-> P(t)",
"|- (EX x. P) <-> P",
- "|- (EX x. x=t & P(x)) <-> P(t)",
+ "|- (EX x. x=t & P(x)) <-> P(t)",
"|- (EX x. t=x & P(x)) <-> P(t)"];
(*** Miniscoping: pushing quantifiers in
We do NOT distribute of ALL over &, or dually that of EX over |
- Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
+ Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
show that this step can increase proof length!
***)
(*existential miniscoping*)
-val ex_simps = map prove_fun
+val ex_simps = map prove_fun
["|- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
- "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
- "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
- "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
- "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
- "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
+ "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
+ "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
+ "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
+ "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
+ "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
(*universal miniscoping*)
val all_simps = map prove_fun
["|- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
- "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
- "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
- "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
- "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
- "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
+ "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
+ "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
+ "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
+ "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
+ "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
(*These are NOT supplied by default!*)
val distrib_simps = map prove_fun
- ["|- P & (Q | R) <-> P&Q | P&R",
+ ["|- P & (Q | R) <-> P&Q | P&R",
"|- (Q | R) & P <-> Q&P | R&P",
"|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
@@ -91,29 +91,29 @@
case concl_of r of
Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (forms_of_seq a, forms_of_seq c) of
- ([], [p]) =>
- (case p of
- Const("op -->",_)$_$_ => atomize(r RS mp_R)
- | Const("op &",_)$_$_ => atomize(r RS conjunct1) @
- atomize(r RS conjunct2)
- | Const("All",_)$_ => atomize(r RS spec)
- | Const("True",_) => [] (*True is DELETED*)
- | Const("False",_) => [] (*should False do something?*)
- | _ => [r])
+ ([], [p]) =>
+ (case p of
+ Const("op -->",_)$_$_ => atomize(r RS mp_R)
+ | Const("op &",_)$_$_ => atomize(r RS conjunct1) @
+ atomize(r RS conjunct2)
+ | Const("All",_)$_ => atomize(r RS spec)
+ | Const("True",_) => [] (*True is DELETED*)
+ | Const("False",_) => [] (*should False do something?*)
+ | _ => [r])
| _ => []) (*ignore theorem unless it has precisely one conclusion*)
| _ => [r];
Goal "|- ~P ==> |- (P <-> False)";
by (etac (thinR RS cut) 1);
-by (Fast_tac 1);
+by (Fast_tac 1);
qed "P_iff_F";
val iff_reflection_F = P_iff_F RS iff_reflection;
Goal "|- P ==> |- (P <-> True)";
by (etac (thinR RS cut) 1);
-by (Fast_tac 1);
+by (Fast_tac 1);
qed "P_iff_T";
val iff_reflection_T = P_iff_T RS iff_reflection;
@@ -122,22 +122,23 @@
fun mk_meta_eq th = case concl_of th of
Const("==",_)$_$_ => th
| Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
- (case (forms_of_seq a, forms_of_seq c) of
- ([], [p]) =>
- (case p of
- (Const("op =",_)$_$_) => th RS eq_reflection
- | (Const("op <->",_)$_$_) => th RS iff_reflection
- | (Const("Not",_)$_) => th RS iff_reflection_F
- | _ => th RS iff_reflection_T)
- | _ => error ("addsimps: unable to use theorem\n" ^
- string_of_thm th));
+ (case (forms_of_seq a, forms_of_seq c) of
+ ([], [p]) =>
+ (case p of
+ (Const("op =",_)$_$_) => th RS eq_reflection
+ | (Const("op <->",_)$_$_) => th RS iff_reflection
+ | (Const("Not",_)$_) => th RS iff_reflection_F
+ | _ => th RS iff_reflection_T)
+ | _ => error ("addsimps: unable to use theorem\n" ^
+ string_of_thm th));
(*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
- rule_by_tactic
+val mk_meta_prems =
+ rule_by_tactic
(REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
+(*Congruence rules for = or <-> (instead of ==)*)
fun mk_meta_cong rl =
standard(mk_meta_eq (mk_meta_prems rl))
handle THM _ =>
@@ -147,7 +148,7 @@
(*** Named rewrite rules ***)
fun prove nm thm = qed_goal nm LK.thy thm
- (fn prems => [ (cut_facts_tac prems 1),
+ (fn prems => [ (cut_facts_tac prems 1),
(fast_tac LK_pack 1) ]);
prove "conj_commute" "|- P&Q <-> Q&P";
@@ -177,26 +178,26 @@
prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
-val [p1,p2] = Goal
+val [p1,p2] = Goal
"[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
by (lemma_tac p1 1);
by (Safe_tac 1);
-by (REPEAT (rtac cut 1
- THEN
- DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
- THEN
- Safe_tac 1));
+by (REPEAT (rtac cut 1
+ THEN
+ DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
+ THEN
+ Safe_tac 1));
qed "imp_cong";
-val [p1,p2] = Goal
+val [p1,p2] = Goal
"[| |- P <-> P'; |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
by (lemma_tac p1 1);
by (Safe_tac 1);
-by (REPEAT (rtac cut 1
- THEN
- DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
- THEN
- Safe_tac 1));
+by (REPEAT (rtac cut 1
+ THEN
+ DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
+ THEN
+ Safe_tac 1));
qed "conj_cong";
Goal "|- (x=y) <-> (y=x)";
@@ -229,32 +230,26 @@
(*** Standard simpsets ***)
-(*Add congruence rules for = or <-> (instead of ==) *)
-infix 4 addcongs delcongs;
-fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
-fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
-
-fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
-fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
-
val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
- assume_tac];
+ assume_tac];
(*No premature instantiation of variables during simplification*)
fun safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
- eq_assume_tac];
+ eq_assume_tac];
(*No simprules, but basic infrastructure for simplification*)
-val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
- setSSolver (mk_solver "safe" safe_solver)
- setSolver (mk_solver "unsafe" unsafe_solver)
- setmksimps (map mk_meta_eq o atomize o gen_all);
+val LK_basic_ss =
+ empty_ss setsubgoaler asm_simp_tac
+ setSSolver (mk_solver "safe" safe_solver)
+ setSolver (mk_solver "unsafe" unsafe_solver)
+ setmksimps (map mk_meta_eq o atomize o gen_all)
+ setmkcong mk_meta_cong;
val LK_simps =
[triv_forall_equality, (* prunes params *)
- refl RS P_iff_T] @
- conj_simps @ disj_simps @ not_simps @
+ refl RS P_iff_T] @
+ conj_simps @ disj_simps @ not_simps @
imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
map prove_fun
@@ -262,8 +257,10 @@
"|- ~ ~ P <-> P", "|- (~P --> P) <-> P",
"|- (~P <-> ~Q) <-> (P<->Q)"];
-val LK_ss = LK_basic_ss addsimps LK_simps addeqcongs [left_cong]
- addcongs [imp_cong];
+val LK_ss =
+ LK_basic_ss addsimps LK_simps
+ addeqcongs [left_cong]
+ addcongs [imp_cong];
simpset_ref() := LK_ss;