src/HOL/Tools/cnf.ML
changeset 60759 36d9f215c982
parent 60696 8304fb4fb823
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/cnf.ML	Sat Jul 18 22:58:50 2015 +0200
     1.2 +++ b/src/HOL/Tools/cnf.ML	Sun Jul 19 00:03:10 2015 +0200
     1.3 @@ -54,41 +54,41 @@
     1.4  structure CNF : CNF =
     1.5  struct
     1.6  
     1.7 -val clause2raw_notE      = @{lemma "[| P; ~P |] ==> False" by auto};
     1.8 -val clause2raw_not_disj  = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
     1.9 -val clause2raw_not_not   = @{lemma "P ==> ~~P" by auto};
    1.10 +val clause2raw_notE      = @{lemma "\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> False" by auto};
    1.11 +val clause2raw_not_disj  = @{lemma "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<or> Q)" by auto};
    1.12 +val clause2raw_not_not   = @{lemma "P \<Longrightarrow> \<not>\<not> P" by auto};
    1.13  
    1.14  val iff_refl             = @{lemma "(P::bool) = P" by auto};
    1.15  val iff_trans            = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
    1.16 -val conj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
    1.17 -val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
    1.18 +val conj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P \<and> Q) = (P' \<and> Q')" by auto};
    1.19 +val disj_cong            = @{lemma "[| P = P'; Q = Q' |] ==> (P \<or> Q) = (P' \<or> Q')" by auto};
    1.20  
    1.21 -val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
    1.22 -val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
    1.23 +val make_nnf_imp         = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P \<longrightarrow> Q) = (P' \<or> Q')" by auto};
    1.24 +val make_nnf_iff         = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' \<or> NQ) \<and> (NP \<or> Q'))" by auto};
    1.25  val make_nnf_not_false   = @{lemma "(~False) = True" by auto};
    1.26  val make_nnf_not_true    = @{lemma "(~True) = False" by auto};
    1.27 -val make_nnf_not_conj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
    1.28 -val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
    1.29 -val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
    1.30 -val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
    1.31 +val make_nnf_not_conj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \<and> Q)) = (P' \<or> Q')" by auto};
    1.32 +val make_nnf_not_disj    = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \<or> Q)) = (P' \<and> Q')" by auto};
    1.33 +val make_nnf_not_imp     = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P \<longrightarrow> Q)) = (P' \<and> Q')" by auto};
    1.34 +val make_nnf_not_iff     = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' \<or> Q') \<and> (NP \<or> NQ))" by auto};
    1.35  val make_nnf_not_not     = @{lemma "P = P' ==> (~~P) = P'" by auto};
    1.36  
    1.37 -val simp_TF_conj_True_l  = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
    1.38 -val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
    1.39 -val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
    1.40 -val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
    1.41 -val simp_TF_disj_True_l  = @{lemma "P = True ==> (P | Q) = True" by auto};
    1.42 -val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P | Q) = True" by auto};
    1.43 -val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
    1.44 -val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
    1.45 +val simp_TF_conj_True_l  = @{lemma "[| P = True; Q = Q' |] ==> (P \<and> Q) = Q'" by auto};
    1.46 +val simp_TF_conj_True_r  = @{lemma "[| P = P'; Q = True |] ==> (P \<and> Q) = P'" by auto};
    1.47 +val simp_TF_conj_False_l = @{lemma "P = False ==> (P \<and> Q) = False" by auto};
    1.48 +val simp_TF_conj_False_r = @{lemma "Q = False ==> (P \<and> Q) = False" by auto};
    1.49 +val simp_TF_disj_True_l  = @{lemma "P = True ==> (P \<or> Q) = True" by auto};
    1.50 +val simp_TF_disj_True_r  = @{lemma "Q = True ==> (P \<or> Q) = True" by auto};
    1.51 +val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P \<or> Q) = Q'" by auto};
    1.52 +val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P \<or> Q) = P'" by auto};
    1.53  
    1.54 -val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
    1.55 -val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
    1.56 +val make_cnf_disj_conj_l = @{lemma "[| (P \<or> R) = PR; (Q \<or> R) = QR |] ==> ((P \<and> Q) \<or> R) = (PR \<and> QR)" by auto};
    1.57 +val make_cnf_disj_conj_r = @{lemma "[| (P \<or> Q) = PQ; (P \<or> R) = PR |] ==> (P \<or> (Q \<and> R)) = (PQ \<and> PR)" by auto};
    1.58  
    1.59 -val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
    1.60 -val make_cnfx_disj_ex_r  = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
    1.61 -val make_cnfx_newlit     = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
    1.62 -val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
    1.63 +val make_cnfx_disj_ex_l  = @{lemma "((EX (x::bool). P x) \<or> Q) = (EX x. P x \<or> Q)" by auto};
    1.64 +val make_cnfx_disj_ex_r  = @{lemma "(P \<or> (EX (x::bool). Q x)) = (EX x. P \<or> Q x)" by auto};
    1.65 +val make_cnfx_newlit     = @{lemma "(P \<or> Q) = (EX x. (P \<or> x) \<and> (Q \<or> ~x))" by auto};
    1.66 +val make_cnfx_ex_cong    = @{lemma "(ALL (x::bool). P x = Q x) \<Longrightarrow> (EX x. P x) = (EX x. Q x)" by auto};
    1.67  
    1.68  val weakening_thm        = @{lemma "[| P; Q |] ==> Q" by auto};
    1.69