# HG changeset patch
# User paulson
# Date 877078668 -7200
# Node ID 1cc9b8ab161c5b57730e70b54d5f8d45497a953a
# Parent  e48e2fb8b8953b623b641b9700b1b5b796cb47b4
New simprules imp_disj1,2 and some comments

diff -r e48e2fb8b895 -r 1cc9b8ab161c src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Oct 17 09:04:02 1997 +0200
+++ b/src/FOL/simpdata.ML	Fri Oct 17 10:57:48 1997 +0200
@@ -125,7 +125,7 @@
     (fn prems => [ (cut_facts_tac prems 1), 
                    (IntPr.fast_tac 1) ]);
 
-fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);
+fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
 
 int_prove "conj_commute" "P&Q <-> Q&P";
 int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
@@ -145,6 +145,9 @@
 int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
 int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
 
+prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)";
+prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)";
+
 int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
 prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
 
@@ -210,22 +213,26 @@
 fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
 				 eq_assume_tac, ematch_tac [FalseE]];
 
+(*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
 			    setSSolver   safe_solver
 			    setSolver  unsafe_solver
 			    setmksimps (map mk_meta_eq o atomize o gen_all);
 
+(*intuitionistic simprules only*)
 val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
 			   addcongs [imp_cong];
 
 val cla_simps = 
-    [de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] @
+    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
+     not_all, not_ex, cases_simp] @
     map prove_fun
      ["~(P&Q)  <-> ~P | ~Q",
       "P | ~P",             "~P | P",
       "~ ~ P <-> P",        "(~P --> P) <-> P",
       "(~P <-> ~Q) <-> (P<->Q)"];
 
+(*classical simprules too*)
 val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);