src/FOL/simpdata.ML
changeset 3835 9a5a4e123859
parent 3610 7e5300420b03
child 3910 1cc9b8ab161c
     1.1 --- a/src/FOL/simpdata.ML	Fri Oct 10 15:51:38 1997 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Oct 10 15:52:12 1997 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
     1.5  
     1.6  val quant_simps = map int_prove_fun
     1.7 - ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
     1.8 + ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
     1.9  
    1.10  (*These are NOT supplied by default!*)
    1.11  val distrib_simps  = map int_prove_fun
    1.12 @@ -103,23 +103,23 @@
    1.13  val ex_simps = map prove_fun 
    1.14                  ["(EX x. x=t & P(x)) <-> P(t)",
    1.15                   "(EX x. t=x & P(x)) <-> P(t)",
    1.16 -                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
    1.17 -                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
    1.18 -                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
    1.19 -                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
    1.20 -                 "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
    1.21 -                 "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
    1.22 +                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
    1.23 +                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
    1.24 +                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
    1.25 +                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
    1.26 +                 "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
    1.27 +                 "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
    1.28  
    1.29  (*Miniscoping: pushing in universal quantifiers*)
    1.30  val all_simps = map prove_fun
    1.31                  ["(ALL x. x=t --> P(x)) <-> P(t)",
    1.32                   "(ALL x. t=x --> P(x)) <-> P(t)",
    1.33 -                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
    1.34 -                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
    1.35 -                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
    1.36 -                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
    1.37 -                 "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
    1.38 -                 "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
    1.39 +                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
    1.40 +                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
    1.41 +                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
    1.42 +                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
    1.43 +                 "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
    1.44 +                 "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
    1.45  
    1.46  fun int_prove nm thm  = qed_goal nm IFOL.thy thm
    1.47      (fn prems => [ (cut_facts_tac prems 1), 
    1.48 @@ -150,9 +150,9 @@
    1.49  
    1.50  prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
    1.51  
    1.52 -prove     "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
    1.53 -prove     "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
    1.54 -int_prove "not_ex"  "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
    1.55 +prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
    1.56 +prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
    1.57 +int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
    1.58  int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
    1.59  
    1.60  int_prove "ex_disj_distrib"