src/HOL/Library/Boolean_Algebra.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63462 c1fe30f2bc32
child 65343 0a8e30a7b10e
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29629
5111ce425e7a tuned header
haftmann
parents: 27368
diff changeset
     1
(*  Title:      HOL/Library/Boolean_Algebra.thy
5111ce425e7a tuned header
haftmann
parents: 27368
diff changeset
     2
    Author:     Brian Huffman
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
     3
*)
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Boolean Algebras\<close>
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
     6
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
     7
theory Boolean_Algebra
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
     8
  imports Main
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
     9
begin
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    10
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    11
locale boolean =
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    12
  fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70)
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    13
  fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65)
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    14
  fixes compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    15
  fixes zero :: "'a" ("\<zero>")
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    16
  fixes one  :: "'a" ("\<one>")
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    17
  assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    18
  assumes disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    19
  assumes conj_commute: "x \<sqinter> y = y \<sqinter> x"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    20
  assumes disj_commute: "x \<squnion> y = y \<squnion> x"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    21
  assumes conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    22
  assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    23
  assumes conj_one_right [simp]: "x \<sqinter> \<one> = x"
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    24
  assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    25
  assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
    26
  assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
54868
bab6cade3cc5 prefer target-style syntaxx for sublocale
haftmann
parents: 34973
diff changeset
    27
begin
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    28
61605
1bf7b186542e qualifier is mandatory by default;
wenzelm
parents: 60855
diff changeset
    29
sublocale conj: abel_semigroup conj
60855
wenzelm
parents: 60500
diff changeset
    30
  by standard (fact conj_assoc conj_commute)+
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    31
61605
1bf7b186542e qualifier is mandatory by default;
wenzelm
parents: 60855
diff changeset
    32
sublocale disj: abel_semigroup disj
60855
wenzelm
parents: 60500
diff changeset
    33
  by standard (fact disj_assoc disj_commute)+
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    34
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    35
lemmas conj_left_commute = conj.left_commute
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    36
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    37
lemmas disj_left_commute = disj.left_commute
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    38
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    39
lemmas conj_ac = conj.assoc conj.commute conj.left_commute
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
    40
lemmas disj_ac = disj.assoc disj.commute disj.left_commute
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    41
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    42
lemma dual: "boolean disj conj compl one zero"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    43
  apply (rule boolean.intro)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    44
  apply (rule disj_assoc)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    45
  apply (rule conj_assoc)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    46
  apply (rule disj_commute)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    47
  apply (rule conj_commute)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    48
  apply (rule disj_conj_distrib)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    49
  apply (rule conj_disj_distrib)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    50
  apply (rule disj_zero_right)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    51
  apply (rule conj_one_right)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    52
  apply (rule disj_cancel_right)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    53
  apply (rule conj_cancel_right)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    54
  done
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    55
60855
wenzelm
parents: 60500
diff changeset
    56
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    57
subsection \<open>Complement\<close>
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    58
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    59
lemma complement_unique:
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    60
  assumes 1: "a \<sqinter> x = \<zero>"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    61
  assumes 2: "a \<squnion> x = \<one>"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    62
  assumes 3: "a \<sqinter> y = \<zero>"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    63
  assumes 4: "a \<squnion> y = \<one>"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    64
  shows "x = y"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    65
proof -
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    66
  have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    67
    using 1 3 by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    68
  then have "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    69
    using conj_commute by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    70
  then have "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    71
    using conj_disj_distrib by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    72
  then have "x \<sqinter> \<one> = y \<sqinter> \<one>"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    73
    using 2 4 by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    74
  then show "x = y"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    75
    using conj_one_right by simp
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    76
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    77
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    78
lemma compl_unique: "x \<sqinter> y = \<zero> \<Longrightarrow> x \<squnion> y = \<one> \<Longrightarrow> \<sim> x = y"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    79
  by (rule complement_unique [OF conj_cancel_right disj_cancel_right])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    80
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    81
lemma double_compl [simp]: "\<sim> (\<sim> x) = x"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    82
proof (rule compl_unique)
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    83
  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    84
    by (simp only: conj_commute)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    85
  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    86
    by (simp only: disj_commute)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    87
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    88
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    89
lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    90
  by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    91
60855
wenzelm
parents: 60500
diff changeset
    92
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    93
subsection \<open>Conjunction\<close>
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    94
24393
b9718519f3d2 declare conj_absorb [simp]
huffman
parents: 24357
diff changeset
    95
lemma conj_absorb [simp]: "x \<sqinter> x = x"
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
    96
proof -
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    97
  have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    98
    using disj_zero_right by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
    99
  also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   100
    using conj_cancel_right by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   101
  also have "... = x \<sqinter> (x \<squnion> \<sim> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   102
    using conj_disj_distrib by (simp only:)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   103
  also have "... = x \<sqinter> \<one>"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   104
    using disj_cancel_right by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   105
  also have "... = x"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   106
    using conj_one_right by simp
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   107
  finally show ?thesis .
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   108
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   109
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   110
lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   111
proof -
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   112
  have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   113
    using conj_cancel_right by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   114
  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   115
    using conj_assoc by (simp only:)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   116
  also have "... = x \<sqinter> \<sim> x"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   117
    using conj_absorb by simp
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   118
  also have "... = \<zero>"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   119
    using conj_cancel_right by simp
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   120
  finally show ?thesis .
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   121
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   122
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   123
lemma compl_one [simp]: "\<sim> \<one> = \<zero>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   124
  by (rule compl_unique [OF conj_zero_right disj_zero_right])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   125
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   126
lemma conj_zero_left [simp]: "\<zero> \<sqinter> x = \<zero>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   127
  by (subst conj_commute) (rule conj_zero_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   128
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   129
lemma conj_one_left [simp]: "\<one> \<sqinter> x = x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   130
  by (subst conj_commute) (rule conj_one_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   131
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   132
lemma conj_cancel_left [simp]: "\<sim> x \<sqinter> x = \<zero>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   133
  by (subst conj_commute) (rule conj_cancel_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   134
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   135
lemma conj_left_absorb [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   136
  by (simp only: conj_assoc [symmetric] conj_absorb)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   137
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   138
lemma conj_disj_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   139
  by (simp only: conj_commute conj_disj_distrib)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   140
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   141
lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   142
60855
wenzelm
parents: 60500
diff changeset
   143
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   144
subsection \<open>Disjunction\<close>
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   145
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   146
lemma disj_absorb [simp]: "x \<squnion> x = x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   147
  by (rule boolean.conj_absorb [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   148
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   149
lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   150
  by (rule boolean.conj_zero_right [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   151
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   152
lemma compl_zero [simp]: "\<sim> \<zero> = \<one>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   153
  by (rule boolean.compl_one [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   154
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   155
lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   156
  by (rule boolean.conj_one_left [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   157
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   158
lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   159
  by (rule boolean.conj_zero_left [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   160
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   161
lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   162
  by (rule boolean.conj_cancel_left [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   163
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   164
lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   165
  by (rule boolean.conj_left_absorb [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   166
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   167
lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   168
  by (rule boolean.conj_disj_distrib2 [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   169
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   170
lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   171
60855
wenzelm
parents: 60500
diff changeset
   172
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   173
subsection \<open>De Morgan's Laws\<close>
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   174
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   175
lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   176
proof (rule compl_unique)
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   177
  have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   178
    by (rule conj_disj_distrib)
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   179
  also have "... = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   180
    by (simp only: conj_ac)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   181
  finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   182
    by (simp only: conj_cancel_right conj_zero_right disj_zero_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   183
next
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   184
  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))"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   185
    by (rule disj_conj_distrib2)
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   186
  also have "... = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   187
    by (simp only: disj_ac)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   188
  finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   189
    by (simp only: disj_cancel_right disj_one_right conj_one_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   190
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   191
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   192
lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   193
  by (rule boolean.de_Morgan_conj [OF dual])
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   194
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   195
end
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   196
60855
wenzelm
parents: 60500
diff changeset
   197
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   198
subsection \<open>Symmetric Difference\<close>
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   199
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   200
locale boolean_xor = boolean +
60855
wenzelm
parents: 60500
diff changeset
   201
  fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<oplus>" 65)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   202
  assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
54868
bab6cade3cc5 prefer target-style syntaxx for sublocale
haftmann
parents: 34973
diff changeset
   203
begin
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   204
61605
1bf7b186542e qualifier is mandatory by default;
wenzelm
parents: 60855
diff changeset
   205
sublocale xor: abel_semigroup xor
60855
wenzelm
parents: 60500
diff changeset
   206
proof
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   207
  fix x y z :: 'a
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   208
  let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   209
            (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   210
  have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   211
        ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   212
    by (simp only: conj_cancel_right conj_zero_right)
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   213
  then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   214
    apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   215
    apply (simp only: conj_disj_distribs conj_ac disj_ac)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   216
    done
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   217
  show "x \<oplus> y = y \<oplus> x"
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   218
    by (simp only: xor_def conj_commute disj_commute)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   219
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   220
34973
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   221
lemmas xor_assoc = xor.assoc
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   222
lemmas xor_commute = xor.commute
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   223
lemmas xor_left_commute = xor.left_commute
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   224
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   225
lemmas xor_ac = xor.assoc xor.commute xor.left_commute
ae634fad947e dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents: 30663
diff changeset
   226
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   227
lemma xor_def2: "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   228
  by (simp only: xor_def conj_disj_distribs disj_ac conj_ac conj_cancel_right disj_zero_left)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   229
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   230
lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   231
  by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   232
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   233
lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   234
  by (subst xor_commute) (rule xor_zero_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   235
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   236
lemma xor_one_right [simp]: "x \<oplus> \<one> = \<sim> x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   237
  by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   238
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   239
lemma xor_one_left [simp]: "\<one> \<oplus> x = \<sim> x"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   240
  by (subst xor_commute) (rule xor_one_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   241
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   242
lemma xor_self [simp]: "x \<oplus> x = \<zero>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   243
  by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   244
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   245
lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   246
  by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   247
29996
c09f348ca88a declare xor_compl_{left,right} [simp]
huffman
parents: 29629
diff changeset
   248
lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   249
  apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   250
  apply (simp only: conj_disj_distribs)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   251
  apply (simp only: conj_cancel_right conj_cancel_left)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   252
  apply (simp only: disj_zero_left disj_zero_right)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   253
  apply (simp only: disj_ac conj_ac)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   254
  done
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   255
29996
c09f348ca88a declare xor_compl_{left,right} [simp]
huffman
parents: 29629
diff changeset
   256
lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   257
  apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   258
  apply (simp only: conj_disj_distribs)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   259
  apply (simp only: conj_cancel_right conj_cancel_left)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   260
  apply (simp only: disj_zero_left disj_zero_right)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   261
  apply (simp only: disj_ac conj_ac)
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   262
  done
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   263
29996
c09f348ca88a declare xor_compl_{left,right} [simp]
huffman
parents: 29629
diff changeset
   264
lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   265
  by (simp only: xor_compl_right xor_self compl_zero)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   266
29996
c09f348ca88a declare xor_compl_{left,right} [simp]
huffman
parents: 29629
diff changeset
   267
lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   268
  by (simp only: xor_compl_left xor_self compl_zero)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   269
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   270
lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   271
proof -
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   272
  have *: "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   273
        (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)"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   274
    by (simp only: conj_cancel_right conj_zero_right disj_zero_left)
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   275
  then show "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   276
    by (simp (no_asm_use) only:
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   277
        xor_def de_Morgan_disj de_Morgan_conj double_compl
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   278
        conj_disj_distribs conj_ac disj_ac)
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   279
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   280
60855
wenzelm
parents: 60500
diff changeset
   281
lemma conj_xor_distrib2: "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   282
proof -
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   283
  have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   284
    by (rule conj_xor_distrib)
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 61605
diff changeset
   285
  then show "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
24357
d42cf77da51f cleaned up; declared more simp rules
huffman
parents: 24332
diff changeset
   286
    by (simp only: conj_commute)
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   287
qed
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   288
60855
wenzelm
parents: 60500
diff changeset
   289
lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   290
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   291
end
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   292
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff changeset
   293
end