src/FOL/simpdata.ML
changeset 1914 86b095835de9
parent 1722 bb326972ede6
child 1953 832ccc1dba95
     1.1 --- a/src/FOL/simpdata.ML	Mon Aug 19 11:19:55 1996 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Mon Aug 19 11:20:37 1996 +0200
     1.3 @@ -50,9 +50,6 @@
     1.4    "(Q | R) & P <-> Q&P | R&P",
     1.5    "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
     1.6  
     1.7 -bind_thm("conj_commute", int_prove_fun "P&Q <-> Q&P");
     1.8 -bind_thm("disj_commute", int_prove_fun "P|Q <-> Q|P");
     1.9 -
    1.10  (** Conversion into rewrite rules **)
    1.11  
    1.12  fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    1.13 @@ -131,6 +128,46 @@
    1.14  
    1.15  val FOL_ss = IFOL_ss addsimps cla_rews;
    1.16  
    1.17 +fun int_prove nm thm  = qed_goal nm IFOL.thy thm
    1.18 +    (fn prems => [ (cut_facts_tac prems 1), 
    1.19 +                   (Int.fast_tac 1) ]);
    1.20 +
    1.21 +fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);
    1.22 +
    1.23 +int_prove "conj_commute" "P&Q <-> Q&P";
    1.24 +int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
    1.25 +val conj_comms = [conj_commute, conj_left_commute];
    1.26 +
    1.27 +int_prove "disj_commute" "P|Q <-> Q|P";
    1.28 +int_prove "disj_left_commute" "P|(Q|R) <-> Q|(P|R)";
    1.29 +val disj_comms = [disj_commute, disj_left_commute];
    1.30 +
    1.31 +int_prove "conj_disj_distribL" "P&(Q|R) <-> (P&Q | P&R)";
    1.32 +int_prove "conj_disj_distribR" "(P|Q)&R <-> (P&R | Q&R)";
    1.33 +
    1.34 +int_prove "disj_conj_distribL" "P|(Q&R) <-> (P|Q) & (P|R)";
    1.35 +int_prove "disj_conj_distribR" "(P&Q)|R <-> (P|R) & (Q|R)";
    1.36 +
    1.37 +int_prove "imp_conj_distrib" "(P --> (Q&R)) <-> (P-->Q) & (P-->R)";
    1.38 +int_prove "imp_conj"         "((P&Q)-->R)   <-> (P --> (Q --> R))";
    1.39 +int_prove "imp_disj"         "(P|Q --> R)   <-> (P-->R) & (Q-->R)";
    1.40 +
    1.41 +int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
    1.42 +prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
    1.43 +
    1.44 +prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
    1.45 +
    1.46 +prove     "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
    1.47 +prove     "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
    1.48 +int_prove "not_ex"  "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
    1.49 +int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
    1.50 +
    1.51 +int_prove "ex_disj_distrib"
    1.52 +    "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
    1.53 +int_prove "all_conj_distrib"
    1.54 +    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
    1.55 +
    1.56 +
    1.57  (*Used in ZF, perhaps elsewhere?*)
    1.58  val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
    1.59    (fn [prem] => [rewtac prem, rtac refl 1]);