Replaced several occurrences of "blast" by "rules".
authorberghofe
Mon Dec 10 15:16:49 2001 +0100 (2001-12-10)
changeset 12436a2df07fefed7
parent 12435 a42be4b09cc3
child 12437 6d4e02b6dd43
Replaced several occurrences of "blast" by "rules".
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Mon Dec 10 13:30:14 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Dec 10 15:16:49 2001 +0100
     1.3 @@ -310,9 +310,12 @@
     1.4  
     1.5  lemma simp_thms:
     1.6    (not_not: "(~ ~ P) = P" and
     1.7 +    "(P ~= Q) = (P = (~Q))"
     1.8 +    "(P | ~P) = True"    "(~P | P) = True"
     1.9 +    "((~P) = (~Q)) = (P=Q)"
    1.10      "(x = x) = True"
    1.11      "(~True) = False"  "(~False) = True"
    1.12 -    "(~P) ~= P"  "P ~= (~P)"  "(P ~= Q) = (P = (~Q))"
    1.13 +    "(~P) ~= P"  "P ~= (~P)"
    1.14      "(True=P) = P"  "(P=True) = P"  "(False=P) = (~P)"  "(P=False) = (~P)"
    1.15      "(True --> P) = P"  "(False --> P) = True"
    1.16      "(P --> True) = True"  "(P --> P) = True"
    1.17 @@ -323,9 +326,7 @@
    1.18      "(P & ~P) = False"    "(~P & P) = False"
    1.19      "(P | True) = True"  "(True | P) = True"
    1.20      "(P | False) = P"  "(False | P) = P"
    1.21 -    "(P | P) = P"  "(P | (P | Q)) = (P | Q)"
    1.22 -    "(P | ~P) = True"    "(~P | P) = True"
    1.23 -    "((~P) = (~Q)) = (P=Q)" and
    1.24 +    "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and
    1.25      "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
    1.26      -- {* needed for the one-point-rule quantifier simplification procs *}
    1.27      -- {* essential for termination!! *} and
    1.28 @@ -333,8 +334,8 @@
    1.29      "!!P. (EX x. t=x & P(x)) = P(t)"
    1.30      "!!P. (ALL x. x=t --> P(x)) = P(t)"
    1.31      "!!P. (ALL x. t=x --> P(x)) = P(t)")
    1.32 -  by blast+
    1.33 -
    1.34 +  by (blast, blast, blast, blast, blast, rules+)
    1.35 + 
    1.36  lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
    1.37    by rules
    1.38  
    1.39 @@ -346,7 +347,7 @@
    1.40    "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
    1.41    "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
    1.42    -- {* Miniscoping: pushing in existential quantifiers. *}
    1.43 -  by blast+
    1.44 +  by (rules | blast)+
    1.45  
    1.46  lemma all_simps:
    1.47    "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
    1.48 @@ -356,33 +357,33 @@
    1.49    "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
    1.50    "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
    1.51    -- {* Miniscoping: pushing in universal quantifiers. *}
    1.52 -  by blast+
    1.53 +  by (rules | blast)+
    1.54  
    1.55  lemma eq_ac:
    1.56   (eq_commute: "(a=b) = (b=a)" and
    1.57    eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
    1.58 -  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by blast+
    1.59 -lemma neq_commute: "(a~=b) = (b~=a)" by blast
    1.60 +  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by (rules, blast+)
    1.61 +lemma neq_commute: "(a~=b) = (b~=a)" by rules
    1.62  
    1.63  lemma conj_comms:
    1.64   (conj_commute: "(P&Q) = (Q&P)" and
    1.65 -  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by blast+
    1.66 -lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by blast
    1.67 +  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by rules+
    1.68 +lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
    1.69  
    1.70  lemma disj_comms:
    1.71   (disj_commute: "(P|Q) = (Q|P)" and
    1.72 -  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by blast+
    1.73 -lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by blast
    1.74 +  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by rules+
    1.75 +lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
    1.76  
    1.77 -lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by blast
    1.78 -lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by blast
    1.79 +lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
    1.80 +lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by rules
    1.81  
    1.82 -lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by blast
    1.83 -lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by blast
    1.84 +lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by rules
    1.85 +lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by rules
    1.86  
    1.87 -lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by blast
    1.88 -lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by blast
    1.89 -lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by blast
    1.90 +lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by rules
    1.91 +lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by rules
    1.92 +lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by rules
    1.93  
    1.94  text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
    1.95  lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
    1.96 @@ -391,7 +392,7 @@
    1.97  lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
    1.98  lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
    1.99  
   1.100 -lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by blast
   1.101 +lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by rules
   1.102  lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
   1.103  lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
   1.104  lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
   1.105 @@ -400,7 +401,7 @@
   1.106    by blast
   1.107  lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
   1.108  
   1.109 -lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by blast
   1.110 +lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by rules
   1.111  
   1.112  
   1.113  lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
   1.114 @@ -410,11 +411,11 @@
   1.115  
   1.116  lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
   1.117  lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
   1.118 -lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by blast
   1.119 -lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by blast
   1.120 +lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by rules
   1.121 +lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by rules
   1.122  
   1.123 -lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by blast
   1.124 -lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by blast
   1.125 +lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by rules
   1.126 +lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by rules
   1.127  
   1.128  text {*
   1.129    \medskip The @{text "&"} congruence rule: not included by default!
   1.130 @@ -489,8 +490,8 @@
   1.131    apply blast
   1.132    done
   1.133  
   1.134 -lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) blast
   1.135 -lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) blast
   1.136 +lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
   1.137 +lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
   1.138  
   1.139  use "simpdata.ML"
   1.140  setup Simplifier.setup