src/HOL/Meson.thy
changeset 39953 aa54f347e5e2
parent 39950 f3c4849868b8
child 40620 7a9278de19ad
     1.1 --- a/src/HOL/Meson.thy	Tue Oct 05 11:14:56 2010 +0200
     1.2 +++ b/src/HOL/Meson.thy	Tue Oct 05 11:45:10 2010 +0200
     1.3 @@ -18,22 +18,22 @@
     1.4  
     1.5  text {* de Morgan laws *}
     1.6  
     1.7 -lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q"
     1.8 -  and meson_not_disjD: "~(P|Q) ==> ~P & ~Q"
     1.9 -  and meson_not_notD: "~~P ==> P"
    1.10 -  and meson_not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
    1.11 -  and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
    1.12 +lemma not_conjD: "~(P&Q) ==> ~P | ~Q"
    1.13 +  and not_disjD: "~(P|Q) ==> ~P & ~Q"
    1.14 +  and not_notD: "~~P ==> P"
    1.15 +  and not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
    1.16 +  and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
    1.17    by fast+
    1.18  
    1.19  text {* Removal of @{text "-->"} and @{text "<->"} (positive and
    1.20  negative occurrences) *}
    1.21  
    1.22 -lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q"
    1.23 -  and meson_not_impD: "~(P-->Q) ==> P & ~Q"
    1.24 -  and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
    1.25 -  and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
    1.26 +lemma imp_to_disjD: "P-->Q ==> ~P | Q"
    1.27 +  and not_impD: "~(P-->Q) ==> P & ~Q"
    1.28 +  and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
    1.29 +  and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
    1.30      -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
    1.31 -  and meson_not_refl_disj_D: "x ~= x | P ==> P"
    1.32 +  and not_refl_disj_D: "x ~= x | P ==> P"
    1.33    by fast+
    1.34  
    1.35  
    1.36 @@ -41,24 +41,24 @@
    1.37  
    1.38  text {* Conjunction *}
    1.39  
    1.40 -lemma meson_conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
    1.41 -  and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
    1.42 +lemma conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
    1.43 +  and conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
    1.44    by fast+
    1.45  
    1.46  
    1.47  text {* Disjunction *}
    1.48  
    1.49 -lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
    1.50 +lemma disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
    1.51    -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *}
    1.52    -- {* With ex-Skolemization, makes fewer Skolem constants *}
    1.53 -  and meson_disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
    1.54 -  and meson_disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
    1.55 +  and disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
    1.56 +  and disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
    1.57    by fast+
    1.58  
    1.59 -lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)"
    1.60 -  and meson_disj_comm: "P|Q ==> Q|P"
    1.61 -  and meson_disj_FalseD1: "False|P ==> P"
    1.62 -  and meson_disj_FalseD2: "P|False ==> P"
    1.63 +lemma disj_assoc: "(P|Q)|R ==> P|(Q|R)"
    1.64 +  and disj_comm: "P|Q ==> Q|P"
    1.65 +  and disj_FalseD1: "False|P ==> P"
    1.66 +  and disj_FalseD2: "P|False ==> P"
    1.67    by fast+
    1.68  
    1.69  
    1.70 @@ -197,4 +197,11 @@
    1.71    #> Meson_Tactic.setup
    1.72  *}
    1.73  
    1.74 +hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
    1.75 +hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
    1.76 +    not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
    1.77 +    disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
    1.78 +    COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C
    1.79 +    abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
    1.80 +
    1.81  end