tuned proofs;
authorwenzelm
Sat Apr 01 19:16:19 2017 +0200 (2017-04-01)
changeset 653430a8e30a7b10e
parent 65342 e32eb488c3a3
child 65344 b99283eed13c
tuned proofs;
src/HOL/Library/Boolean_Algebra.thy
     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Sat Apr 01 18:50:26 2017 +0200
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Sat Apr 01 19:16:19 2017 +0200
     1.3 @@ -9,21 +9,21 @@
     1.4  begin
     1.5  
     1.6  locale boolean =
     1.7 -  fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70)
     1.8 -  fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65)
     1.9 -  fixes compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80)
    1.10 -  fixes zero :: "'a" ("\<zero>")
    1.11 -  fixes one  :: "'a" ("\<one>")
    1.12 +  fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<sqinter>" 70)
    1.13 +    and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<squnion>" 65)
    1.14 +    and compl :: "'a \<Rightarrow> 'a"  ("\<sim> _" [81] 80)
    1.15 +    and zero :: "'a"  ("\<zero>")
    1.16 +    and one  :: "'a"  ("\<one>")
    1.17    assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    1.18 -  assumes disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    1.19 -  assumes conj_commute: "x \<sqinter> y = y \<sqinter> x"
    1.20 -  assumes disj_commute: "x \<squnion> y = y \<squnion> x"
    1.21 -  assumes conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.22 -  assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.23 -  assumes conj_one_right [simp]: "x \<sqinter> \<one> = x"
    1.24 -  assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
    1.25 -  assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
    1.26 -  assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
    1.27 +    and disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    1.28 +    and conj_commute: "x \<sqinter> y = y \<sqinter> x"
    1.29 +    and disj_commute: "x \<squnion> y = y \<squnion> x"
    1.30 +    and conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.31 +    and disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.32 +    and conj_one_right [simp]: "x \<sqinter> \<one> = x"
    1.33 +    and disj_zero_right [simp]: "x \<squnion> \<zero> = x"
    1.34 +    and conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
    1.35 +    and disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
    1.36  begin
    1.37  
    1.38  sublocale conj: abel_semigroup conj
    1.39 @@ -33,7 +33,6 @@
    1.40    by standard (fact disj_assoc disj_commute)+
    1.41  
    1.42  lemmas conj_left_commute = conj.left_commute
    1.43 -
    1.44  lemmas disj_left_commute = disj.left_commute
    1.45  
    1.46  lemmas conj_ac = conj.assoc conj.commute conj.left_commute
    1.47 @@ -41,15 +40,15 @@
    1.48  
    1.49  lemma dual: "boolean disj conj compl one zero"
    1.50    apply (rule boolean.intro)
    1.51 -  apply (rule disj_assoc)
    1.52 -  apply (rule conj_assoc)
    1.53 -  apply (rule disj_commute)
    1.54 -  apply (rule conj_commute)
    1.55 -  apply (rule disj_conj_distrib)
    1.56 -  apply (rule conj_disj_distrib)
    1.57 -  apply (rule disj_zero_right)
    1.58 -  apply (rule conj_one_right)
    1.59 -  apply (rule disj_cancel_right)
    1.60 +           apply (rule disj_assoc)
    1.61 +          apply (rule conj_assoc)
    1.62 +         apply (rule disj_commute)
    1.63 +        apply (rule conj_commute)
    1.64 +       apply (rule disj_conj_distrib)
    1.65 +      apply (rule conj_disj_distrib)
    1.66 +     apply (rule disj_zero_right)
    1.67 +    apply (rule conj_one_right)
    1.68 +   apply (rule disj_cancel_right)
    1.69    apply (rule conj_cancel_right)
    1.70    done
    1.71  
    1.72 @@ -63,16 +62,16 @@
    1.73    assumes 4: "a \<squnion> y = \<one>"
    1.74    shows "x = y"
    1.75  proof -
    1.76 -  have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)"
    1.77 -    using 1 3 by simp
    1.78 +  from 1 3 have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)"
    1.79 +    by simp
    1.80    then have "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)"
    1.81 -    using conj_commute by simp
    1.82 +    by (simp add: conj_commute)
    1.83    then have "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)"
    1.84 -    using conj_disj_distrib by simp
    1.85 -  then have "x \<sqinter> \<one> = y \<sqinter> \<one>"
    1.86 -    using 2 4 by simp
    1.87 +    by (simp add: conj_disj_distrib)
    1.88 +  with 2 4 have "x \<sqinter> \<one> = y \<sqinter> \<one>"
    1.89 +    by simp
    1.90    then show "x = y"
    1.91 -    using conj_one_right by simp
    1.92 +    by simp
    1.93  qed
    1.94  
    1.95  lemma compl_unique: "x \<sqinter> y = \<zero> \<Longrightarrow> x \<squnion> y = \<one> \<Longrightarrow> \<sim> x = y"
    1.96 @@ -80,10 +79,10 @@
    1.97  
    1.98  lemma double_compl [simp]: "\<sim> (\<sim> x) = x"
    1.99  proof (rule compl_unique)
   1.100 -  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>"
   1.101 -    by (simp only: conj_commute)
   1.102 -  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>"
   1.103 -    by (simp only: disj_commute)
   1.104 +  show "\<sim> x \<sqinter> x = \<zero>"
   1.105 +    by (simp only: conj_cancel_right conj_commute)
   1.106 +  show "\<sim> x \<squnion> x = \<one>"
   1.107 +    by (simp only: disj_cancel_right disj_commute)
   1.108  qed
   1.109  
   1.110  lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y"
   1.111 @@ -95,28 +94,28 @@
   1.112  lemma conj_absorb [simp]: "x \<sqinter> x = x"
   1.113  proof -
   1.114    have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>"
   1.115 -    using disj_zero_right by simp
   1.116 -  also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)"
   1.117 -    using conj_cancel_right by simp
   1.118 -  also have "... = x \<sqinter> (x \<squnion> \<sim> x)"
   1.119 -    using conj_disj_distrib by (simp only:)
   1.120 -  also have "... = x \<sqinter> \<one>"
   1.121 -    using disj_cancel_right by simp
   1.122 -  also have "... = x"
   1.123 -    using conj_one_right by simp
   1.124 +    by simp
   1.125 +  also have "\<dots> = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)"
   1.126 +    by simp
   1.127 +  also have "\<dots> = x \<sqinter> (x \<squnion> \<sim> x)"
   1.128 +    by (simp only: conj_disj_distrib)
   1.129 +  also have "\<dots> = x \<sqinter> \<one>"
   1.130 +    by simp
   1.131 +  also have "\<dots> = x"
   1.132 +    by simp
   1.133    finally show ?thesis .
   1.134  qed
   1.135  
   1.136  lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>"
   1.137  proof -
   1.138 -  have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)"
   1.139 -    using conj_cancel_right by simp
   1.140 -  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x"
   1.141 -    using conj_assoc by (simp only:)
   1.142 -  also have "... = x \<sqinter> \<sim> x"
   1.143 -    using conj_absorb by simp
   1.144 -  also have "... = \<zero>"
   1.145 -    using conj_cancel_right by simp
   1.146 +  from conj_cancel_right have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)"
   1.147 +    by simp
   1.148 +  also from conj_assoc have "\<dots> = (x \<sqinter> x) \<sqinter> \<sim> x"
   1.149 +    by (simp only:)
   1.150 +  also from conj_absorb have "\<dots> = x \<sqinter> \<sim> x"
   1.151 +    by simp
   1.152 +  also have "\<dots> = \<zero>"
   1.153 +    by simp
   1.154    finally show ?thesis .
   1.155  qed
   1.156  
   1.157 @@ -176,14 +175,14 @@
   1.158  proof (rule compl_unique)
   1.159    have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)"
   1.160      by (rule conj_disj_distrib)
   1.161 -  also have "... = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))"
   1.162 +  also have "\<dots> = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))"
   1.163      by (simp only: conj_ac)
   1.164    finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>"
   1.165      by (simp only: conj_cancel_right conj_zero_right disj_zero_right)
   1.166  next
   1.167    have "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = (x \<squnion> (\<sim> x \<squnion> \<sim> y)) \<sqinter> (y \<squnion> (\<sim> x \<squnion> \<sim> y))"
   1.168      by (rule disj_conj_distrib2)
   1.169 -  also have "... = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))"
   1.170 +  also have "\<dots> = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))"
   1.171      by (simp only: disj_ac)
   1.172    finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>"
   1.173      by (simp only: disj_cancel_right disj_one_right conj_one_right)
   1.174 @@ -205,15 +204,12 @@
   1.175  sublocale xor: abel_semigroup xor
   1.176  proof
   1.177    fix x y z :: 'a
   1.178 -  let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
   1.179 -            (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
   1.180 -  have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
   1.181 -        ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"
   1.182 +  let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
   1.183 +  have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) = ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"
   1.184      by (simp only: conj_cancel_right conj_zero_right)
   1.185    then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   1.186 -    apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   1.187 -    apply (simp only: conj_disj_distribs conj_ac disj_ac)
   1.188 -    done
   1.189 +    by (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   1.190 +      (simp only: conj_disj_distribs conj_ac disj_ac)
   1.191    show "x \<oplus> y = y \<oplus> x"
   1.192      by (simp only: xor_def conj_commute disj_commute)
   1.193  qed