src/HOL/Tools/SMT/conj_disj_perm.ML
changeset 67091 1393c2340eec
parent 60752 b48830b670a1
child 67149 e61557884799
     1.1 --- a/src/HOL/Tools/SMT/conj_disj_perm.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/SMT/conj_disj_perm.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4  
     1.5  fun add_lit thm = Termtab.update (HOLogic.dest_Trueprop (Thm.prop_of thm), thm)
     1.6  
     1.7 -val ndisj1_rule = @{lemma "~(P | Q) ==> ~P" by auto}
     1.8 -val ndisj2_rule = @{lemma "~(P | Q) ==> ~Q" by auto}
     1.9 +val ndisj1_rule = @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>P" by auto}
    1.10 +val ndisj2_rule = @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>Q" by auto}
    1.11  
    1.12  fun explode_thm thm =
    1.13    (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
    1.14 @@ -33,7 +33,7 @@
    1.15  and explode_conj_thm rule1 rule2 thm lits =
    1.16    explode_thm (thm RS rule1) (explode_thm (thm RS rule2) (add_lit thm lits))
    1.17  
    1.18 -val not_false_rule = @{lemma "~False" by auto}
    1.19 +val not_false_rule = @{lemma "\<not>False" by auto}
    1.20  fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty))
    1.21  
    1.22  fun find_dual_lit lits (@{const HOL.Not} $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm)
    1.23 @@ -41,8 +41,8 @@
    1.24  
    1.25  fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits
    1.26  
    1.27 -val not_not_rule = @{lemma "P ==> ~~P" by auto}
    1.28 -val ndisj_rule = @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto}
    1.29 +val not_not_rule = @{lemma "P \<Longrightarrow> \<not>\<not>P" by auto}
    1.30 +val ndisj_rule = @{lemma "\<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> \<not>(P \<or> Q)" by auto}
    1.31  
    1.32  fun join lits t =
    1.33    (case Termtab.lookup lits t of
    1.34 @@ -63,8 +63,8 @@
    1.35      val thm2 = prove_conj_disj_imp crhs clhs
    1.36    in eq_from_impls thm1 thm2 end
    1.37  
    1.38 -val not_not_false_rule = @{lemma "~~False ==> P" by auto}
    1.39 -val not_true_rule = @{lemma "~True ==> P" by auto}
    1.40 +val not_not_false_rule = @{lemma "\<not>\<not>False \<Longrightarrow> P" by auto}
    1.41 +val not_true_rule = @{lemma "\<not>True \<Longrightarrow> P" by auto}
    1.42  
    1.43  fun prove_any_imp ct =
    1.44    (case Thm.term_of ct of
    1.45 @@ -94,7 +94,7 @@
    1.46      val thm2 = if to_right then prove_any_imp crhs else prove_contradiction_imp crhs
    1.47    in eq_from_impls thm1 thm2 end
    1.48  
    1.49 -val contrapos_rule = @{lemma "(~P) = (~Q) ==> P = Q" by auto}
    1.50 +val contrapos_rule = @{lemma "(\<not>P) = (\<not>Q) \<Longrightarrow> P = Q" by auto}
    1.51  fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply @{cterm HOL.Not}) cp)]
    1.52  
    1.53  datatype kind = True | False | Conj | Disj | Other