src/FOL/simpdata.ML
changeset 3910 1cc9b8ab161c
parent 3835 9a5a4e123859
child 4094 9e501199ec01
     1.1 --- a/src/FOL/simpdata.ML	Fri Oct 17 09:04:02 1997 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Oct 17 10:57:48 1997 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4      (fn prems => [ (cut_facts_tac prems 1), 
     1.5                     (IntPr.fast_tac 1) ]);
     1.6  
     1.7 -fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);
     1.8 +fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
     1.9  
    1.10  int_prove "conj_commute" "P&Q <-> Q&P";
    1.11  int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
    1.12 @@ -145,6 +145,9 @@
    1.13  int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
    1.14  int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
    1.15  
    1.16 +prove "imp_disj1" "(P-->Q) | R <-> (P-->Q | R)";
    1.17 +prove "imp_disj2" "Q | (P-->R) <-> (P-->Q | R)";
    1.18 +
    1.19  int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
    1.20  prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
    1.21  
    1.22 @@ -210,22 +213,26 @@
    1.23  fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
    1.24  				 eq_assume_tac, ematch_tac [FalseE]];
    1.25  
    1.26 +(*No simprules, but basic infastructure for simplification*)
    1.27  val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    1.28  			    setSSolver   safe_solver
    1.29  			    setSolver  unsafe_solver
    1.30  			    setmksimps (map mk_meta_eq o atomize o gen_all);
    1.31  
    1.32 +(*intuitionistic simprules only*)
    1.33  val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
    1.34  			   addcongs [imp_cong];
    1.35  
    1.36  val cla_simps = 
    1.37 -    [de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] @
    1.38 +    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
    1.39 +     not_all, not_ex, cases_simp] @
    1.40      map prove_fun
    1.41       ["~(P&Q)  <-> ~P | ~Q",
    1.42        "P | ~P",             "~P | P",
    1.43        "~ ~ P <-> P",        "(~P --> P) <-> P",
    1.44        "(~P <-> ~Q) <-> (P<->Q)"];
    1.45  
    1.46 +(*classical simprules too*)
    1.47  val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
    1.48  
    1.49