cleaned up; declared more simp rules
authorhuffman
Mon Aug 20 20:38:32 2007 +0200 (2007-08-20)
changeset 24357d42cf77da51f
parent 24356 65fd09a7243f
child 24358 d75af3e90e82
cleaned up; declared more simp rules
src/HOL/Library/Boolean_Algebra.thy
     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.185 -apply (simp add: conj_disj_distribs)
   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.198 -apply (simp add: conj_disj_distribs)
   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 =