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