src/HOL/Library/Boolean_Algebra.thy
 changeset 24357 d42cf77da51f parent 24332 e3a2b75b1cf9 child 24393 b9718519f3d2
```     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Aug 20 20:36:19 2007 +0200
1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Aug 20 20:38:32 2007 +0200
1.3 @@ -12,9 +12,9 @@
1.4  begin
1.5
1.6  locale boolean =
1.7 -  fixes conj :: "'a => 'a => 'a" (infixr "\<sqinter>" 70)
1.8 -  fixes disj :: "'a => 'a => 'a" (infixr "\<squnion>" 65)
1.9 -  fixes compl :: "'a => 'a" ("\<sim> _" [81] 80)
1.10 +  fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70)
1.11 +  fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65)
1.12 +  fixes compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80)
1.13    fixes zero :: "'a" ("\<zero>")
1.14    fixes one  :: "'a" ("\<one>")
1.15    assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
1.16 @@ -23,10 +23,10 @@
1.17    assumes disj_commute: "x \<squnion> y = y \<squnion> x"
1.18    assumes conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
1.19    assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
1.20 -  assumes conj_one_right: "x \<sqinter> \<one> = x"
1.21 -  assumes disj_zero_right: "x \<squnion> \<zero> = x"
1.22 -  assumes conj_cancel_right: "x \<sqinter> \<sim> x = \<zero>"
1.23 -  assumes disj_cancel_right: "x \<squnion> \<sim> x = \<one>"
1.24 +  assumes conj_one_right [simp]: "x \<sqinter> \<one> = x"
1.25 +  assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
1.26 +  assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
1.27 +  assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
1.28  begin
1.29
1.30  lemmas disj_ac =
1.31 @@ -51,7 +51,7 @@
1.32  apply (rule conj_cancel_right)
1.33  done
1.34
1.35 -text {* Complement *}
1.36 +subsection {* Complement *}
1.37
1.38  lemma complement_unique:
1.39    assumes 1: "a \<sqinter> x = \<zero>"
1.40 @@ -67,25 +67,25 @@
1.41    thus "x = y" using conj_one_right by simp
1.42  qed
1.43
1.44 -lemma compl_unique: "[| x \<sqinter> y = \<zero>; x \<squnion> y = \<one> |] ==> \<sim> x = y"
1.45 +lemma compl_unique: "\<lbrakk>x \<sqinter> y = \<zero>; x \<squnion> y = \<one>\<rbrakk> \<Longrightarrow> \<sim> x = y"
1.46  by (rule complement_unique [OF conj_cancel_right disj_cancel_right])
1.47
1.48  lemma double_compl [simp]: "\<sim> (\<sim> x) = x"
1.49  proof (rule compl_unique)
1.50 -  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>" by (simp add: conj_commute)
1.51 -  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>" by (simp add: disj_commute)
1.52 +  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>" by (simp only: conj_commute)
1.53 +  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>" by (simp only: disj_commute)
1.54  qed
1.55
1.56  lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
1.57  by (rule inj_eq [OF inj_on_inverseI], rule double_compl)
1.58
1.59 -text {* Conjunction *}
1.60 +subsection {* Conjunction *}
1.61
1.62  lemma conj_absorb: "x \<sqinter> x = x"
1.63  proof -
1.64    have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" using disj_zero_right by simp
1.65    also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
1.66 -  also have "... = x \<sqinter> (x \<squnion> \<sim> x)" using conj_disj_distrib by simp
1.67 +  also have "... = x \<sqinter> (x \<squnion> \<sim> x)" using conj_disj_distrib by (simp only:)
1.68    also have "... = x \<sqinter> \<one>" using disj_cancel_right by simp
1.69    also have "... = x" using conj_one_right by simp
1.70    finally show ?thesis .
1.71 @@ -113,16 +113,16 @@
1.72  by (subst conj_commute) (rule conj_cancel_right)
1.73
1.74  lemma conj_left_absorb [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
1.75 -by (simp add: conj_assoc [symmetric] conj_absorb)
1.76 +by (simp only: conj_assoc [symmetric] conj_absorb)
1.77
1.78  lemma conj_disj_distrib2:
1.79    "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
1.80 -by (simp add: conj_commute conj_disj_distrib)
1.81 +by (simp only: conj_commute conj_disj_distrib)
1.82
1.83  lemmas conj_disj_distribs =
1.84     conj_disj_distrib conj_disj_distrib2
1.85
1.86 -text {* Disjunction *}
1.87 +subsection {* Disjunction *}
1.88
1.89  lemma disj_absorb [simp]: "x \<squnion> x = x"
1.90  by (rule boolean.conj_absorb [OF dual])
1.91 @@ -152,23 +152,23 @@
1.92  lemmas disj_conj_distribs =
1.93     disj_conj_distrib disj_conj_distrib2
1.94
1.95 -text {* De Morgan's Laws *}
1.96 +subsection {* De Morgan's Laws *}
1.97
1.98  lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
1.99  proof (rule compl_unique)
1.100    have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)"
1.101      by (rule conj_disj_distrib)
1.102    also have "... = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))"
1.103 -    by (simp add: conj_ac)
1.104 +    by (simp only: conj_ac)
1.105    finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>"
1.106 -    by (simp add: conj_cancel_right conj_zero_right disj_zero_right)
1.107 +    by (simp only: conj_cancel_right conj_zero_right disj_zero_right)
1.108  next
1.109    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.110      by (rule disj_conj_distrib2)
1.111    also have "... = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))"
1.112 -    by (simp add: disj_ac)
1.113 +    by (simp only: disj_ac)
1.114    finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>"
1.115 -    by (simp add: disj_cancel_right disj_one_right conj_one_right)
1.116 +    by (simp only: disj_cancel_right disj_one_right conj_one_right)
1.117  qed
1.118
1.119  lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
1.120 @@ -176,7 +176,7 @@
1.121
1.122  end
1.123
1.124 -text {* Symmetric Difference *}
1.125 +subsection {* Symmetric Difference *}
1.126
1.127  locale boolean_xor = boolean +
1.128    fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
1.129 @@ -185,11 +185,11 @@
1.130
1.131  lemma xor_def2:
1.132    "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
1.133 -by (simp add: xor_def conj_disj_distribs
1.134 -              disj_ac conj_ac conj_cancel_right disj_zero_left)
1.135 +by (simp only: xor_def conj_disj_distribs
1.136 +               disj_ac conj_ac conj_cancel_right disj_zero_left)
1.137
1.138  lemma xor_commute: "x \<oplus> y = y \<oplus> x"
1.139 -by (simp add: xor_def conj_commute disj_commute)
1.140 +by (simp only: xor_def conj_commute disj_commute)
1.141
1.142  lemma xor_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
1.143  proof -
1.144 @@ -197,10 +197,10 @@
1.145              (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
1.146    have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
1.147          ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"
1.148 -    by (simp add: conj_cancel_right conj_zero_right)
1.149 +    by (simp only: conj_cancel_right conj_zero_right)
1.150    thus "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
1.151 -    apply (simp add: xor_def de_Morgan_disj de_Morgan_conj double_compl)
1.152 -    apply (simp add: conj_disj_distribs conj_ac disj_ac)
1.153 +    apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
1.154 +    apply (simp only: conj_disj_distribs conj_ac disj_ac)
1.155      done
1.156  qed
1.157
1.158 @@ -209,41 +209,41 @@
1.159    mk_left_commute [of "xor", OF xor_assoc xor_commute]
1.160
1.161  lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
1.162 -by (simp add: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
1.163 +by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
1.164
1.165  lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x"
1.166  by (subst xor_commute) (rule xor_zero_right)
1.167
1.168  lemma xor_one_right [simp]: "x \<oplus> \<one> = \<sim> x"
1.169 -by (simp add: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)
1.170 +by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)
1.171
1.172  lemma xor_one_left [simp]: "\<one> \<oplus> x = \<sim> x"
1.173  by (subst xor_commute) (rule xor_one_right)
1.174
1.175  lemma xor_self [simp]: "x \<oplus> x = \<zero>"
1.176 -by (simp add: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
1.177 +by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
1.178
1.179  lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
1.180 -by (simp add: xor_assoc [symmetric] xor_self xor_zero_left)
1.181 +by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
1.182
1.183  lemma xor_compl_left: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
1.184 -apply (simp add: xor_def de_Morgan_disj de_Morgan_conj double_compl)
1.186 -apply (simp add: conj_cancel_right conj_cancel_left)
1.187 -apply (simp add: disj_zero_left disj_zero_right)
1.188 -apply (simp add: disj_ac conj_ac)
1.189 +apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
1.190 +apply (simp only: conj_disj_distribs)
1.191 +apply (simp only: conj_cancel_right conj_cancel_left)
1.192 +apply (simp only: disj_zero_left disj_zero_right)
1.193 +apply (simp only: disj_ac conj_ac)
1.194  done
1.195
1.196  lemma xor_compl_right: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
1.197 -apply (simp add: xor_def de_Morgan_disj de_Morgan_conj double_compl)
1.199 -apply (simp add: conj_cancel_right conj_cancel_left)
1.200 -apply (simp add: disj_zero_left disj_zero_right)
1.201 -apply (simp add: disj_ac conj_ac)
1.202 +apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
1.203 +apply (simp only: conj_disj_distribs)
1.204 +apply (simp only: conj_cancel_right conj_cancel_left)
1.205 +apply (simp only: disj_zero_left disj_zero_right)
1.206 +apply (simp only: disj_ac conj_ac)
1.207  done
1.208
1.209  lemma xor_cancel_right [simp]: "x \<oplus> \<sim> x = \<one>"
1.210 -by (simp add: xor_compl_right xor_self compl_zero)
1.211 +by (simp only: xor_compl_right xor_self compl_zero)
1.212
1.213  lemma xor_cancel_left [simp]: "\<sim> x \<oplus> x = \<one>"
1.214  by (subst xor_commute) (rule xor_cancel_right)
1.215 @@ -252,9 +252,9 @@
1.216  proof -
1.217    have "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
1.218          (y \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z)"
1.219 -    by (simp add: conj_cancel_right conj_zero_right disj_zero_left)
1.220 +    by (simp only: conj_cancel_right conj_zero_right disj_zero_left)
1.221    thus "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
1.222 -    by (simp (no_asm_use) add:
1.223 +    by (simp (no_asm_use) only:
1.224          xor_def de_Morgan_disj de_Morgan_conj double_compl
1.225          conj_disj_distribs conj_ac disj_ac)
1.226  qed
1.227 @@ -265,7 +265,7 @@
1.228    have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
1.229      by (rule conj_xor_distrib)
1.230    thus "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
1.231 -    by (simp add: conj_commute)
1.232 +    by (simp only: conj_commute)
1.233  qed
1.234
1.235  lemmas conj_xor_distribs =
```