boolean algebras as locales and numbers as types by Brian Huffman
authorkleing
Mon Aug 20 00:22:18 2007 +0200 (2007-08-20)
changeset 24332e3a2b75b1cf9
parent 24331 76f7a8c6e842
child 24333 e77ea0ea7f2c
boolean algebras as locales and numbers as types by Brian Huffman
CONTRIBUTORS
src/HOL/IsaMakefile
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Library.thy
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/CONTRIBUTORS	Sun Aug 19 21:21:37 2007 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Aug 20 00:22:18 2007 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  Contributions to Isabelle 2007
     1.5  ------------------------------
     1.6  
     1.7 +* August 2007: Brian Huffman, PSU
     1.8 +  HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type
     1.9 +
    1.10  * June 2007: Amine Chaieb, TUM
    1.11    Semiring normalization and Groebner Bases
    1.12  
     2.1 --- a/src/HOL/IsaMakefile	Sun Aug 19 21:21:37 2007 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Aug 20 00:22:18 2007 +0200
     2.3 @@ -226,8 +226,10 @@
     2.4    Library/SCT_Interpretation.thy \
     2.5    Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
     2.6    Library/SCT_Examples.thy Library/sct.ML \
     2.7 -  Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy Library/Pretty_Int.thy \
     2.8 -  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy
     2.9 +  Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
    2.10 +  Library/Pretty_Int.thy \
    2.11 +  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy\
    2.12 +  Library/Numeral_Type.thy Library/Boolean_Algebra.thy
    2.13  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    2.14  
    2.15  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Aug 20 00:22:18 2007 +0200
     3.3 @@ -0,0 +1,276 @@
     3.4 +(* 
     3.5 +  ID:     $Id$
     3.6 +  Author: Brian Huffman
     3.7 +
     3.8 +  Boolean algebras as locales.
     3.9 +*)
    3.10 +
    3.11 +header {* Boolean Algebras *}
    3.12 +
    3.13 +theory Boolean_Algebra
    3.14 +imports Main
    3.15 +begin
    3.16 +
    3.17 +locale boolean =
    3.18 +  fixes conj :: "'a => 'a => 'a" (infixr "\<sqinter>" 70)
    3.19 +  fixes disj :: "'a => 'a => 'a" (infixr "\<squnion>" 65)
    3.20 +  fixes compl :: "'a => 'a" ("\<sim> _" [81] 80)
    3.21 +  fixes zero :: "'a" ("\<zero>")
    3.22 +  fixes one  :: "'a" ("\<one>")
    3.23 +  assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    3.24 +  assumes disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
    3.25 +  assumes conj_commute: "x \<sqinter> y = y \<sqinter> x"
    3.26 +  assumes disj_commute: "x \<squnion> y = y \<squnion> x"
    3.27 +  assumes conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    3.28 +  assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    3.29 +  assumes conj_one_right: "x \<sqinter> \<one> = x"
    3.30 +  assumes disj_zero_right: "x \<squnion> \<zero> = x"
    3.31 +  assumes conj_cancel_right: "x \<sqinter> \<sim> x = \<zero>"
    3.32 +  assumes disj_cancel_right: "x \<squnion> \<sim> x = \<one>"
    3.33 +begin
    3.34 +
    3.35 +lemmas disj_ac =
    3.36 +  disj_assoc disj_commute
    3.37 +  mk_left_commute [of "disj", OF disj_assoc disj_commute]
    3.38 +
    3.39 +lemmas conj_ac =
    3.40 +  conj_assoc conj_commute
    3.41 +  mk_left_commute [of "conj", OF conj_assoc conj_commute]
    3.42 +
    3.43 +lemma dual: "boolean disj conj compl one zero"
    3.44 +apply (rule boolean.intro)
    3.45 +apply (rule disj_assoc)
    3.46 +apply (rule conj_assoc)
    3.47 +apply (rule disj_commute)
    3.48 +apply (rule conj_commute)
    3.49 +apply (rule disj_conj_distrib)
    3.50 +apply (rule conj_disj_distrib)
    3.51 +apply (rule disj_zero_right)
    3.52 +apply (rule conj_one_right)
    3.53 +apply (rule disj_cancel_right)
    3.54 +apply (rule conj_cancel_right)
    3.55 +done
    3.56 +
    3.57 +text {* Complement *}
    3.58 +
    3.59 +lemma complement_unique:
    3.60 +  assumes 1: "a \<sqinter> x = \<zero>"
    3.61 +  assumes 2: "a \<squnion> x = \<one>"
    3.62 +  assumes 3: "a \<sqinter> y = \<zero>"
    3.63 +  assumes 4: "a \<squnion> y = \<one>"
    3.64 +  shows "x = y"
    3.65 +proof -
    3.66 +  have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)" using 1 3 by simp
    3.67 +  hence "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)" using conj_commute by simp
    3.68 +  hence "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)" using conj_disj_distrib by simp
    3.69 +  hence "x \<sqinter> \<one> = y \<sqinter> \<one>" using 2 4 by simp
    3.70 +  thus "x = y" using conj_one_right by simp
    3.71 +qed
    3.72 +
    3.73 +lemma compl_unique: "[| x \<sqinter> y = \<zero>; x \<squnion> y = \<one> |] ==> \<sim> x = y"
    3.74 +by (rule complement_unique [OF conj_cancel_right disj_cancel_right])
    3.75 +
    3.76 +lemma double_compl [simp]: "\<sim> (\<sim> x) = x"
    3.77 +proof (rule compl_unique)
    3.78 +  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>" by (simp add: conj_commute)
    3.79 +  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>" by (simp add: disj_commute)
    3.80 +qed
    3.81 +
    3.82 +lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
    3.83 +by (rule inj_eq [OF inj_on_inverseI], rule double_compl)
    3.84 +
    3.85 +text {* Conjunction *}
    3.86 +
    3.87 +lemma conj_absorb: "x \<sqinter> x = x"
    3.88 +proof -
    3.89 +  have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" using disj_zero_right by simp
    3.90 +  also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
    3.91 +  also have "... = x \<sqinter> (x \<squnion> \<sim> x)" using conj_disj_distrib by simp
    3.92 +  also have "... = x \<sqinter> \<one>" using disj_cancel_right by simp
    3.93 +  also have "... = x" using conj_one_right by simp
    3.94 +  finally show ?thesis .
    3.95 +qed
    3.96 +
    3.97 +lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>"
    3.98 +proof -
    3.99 +  have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
   3.100 +  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" using conj_assoc by simp
   3.101 +  also have "... = x \<sqinter> \<sim> x" using conj_absorb by simp
   3.102 +  also have "... = \<zero>" using conj_cancel_right by simp
   3.103 +  finally show ?thesis .
   3.104 +qed
   3.105 +
   3.106 +lemma compl_one [simp]: "\<sim> \<one> = \<zero>"
   3.107 +by (rule compl_unique [OF conj_zero_right disj_zero_right])
   3.108 +
   3.109 +lemma conj_zero_left [simp]: "\<zero> \<sqinter> x = \<zero>"
   3.110 +by (subst conj_commute) (rule conj_zero_right)
   3.111 +
   3.112 +lemma conj_one_left [simp]: "\<one> \<sqinter> x = x"
   3.113 +by (subst conj_commute) (rule conj_one_right)
   3.114 +
   3.115 +lemma conj_cancel_left [simp]: "\<sim> x \<sqinter> x = \<zero>"
   3.116 +by (subst conj_commute) (rule conj_cancel_right)
   3.117 +
   3.118 +lemma conj_left_absorb [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   3.119 +by (simp add: conj_assoc [symmetric] conj_absorb)
   3.120 +
   3.121 +lemma conj_disj_distrib2:
   3.122 +  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
   3.123 +by (simp add: conj_commute conj_disj_distrib)
   3.124 +
   3.125 +lemmas conj_disj_distribs =
   3.126 +   conj_disj_distrib conj_disj_distrib2
   3.127 +
   3.128 +text {* Disjunction *}
   3.129 +
   3.130 +lemma disj_absorb [simp]: "x \<squnion> x = x"
   3.131 +by (rule boolean.conj_absorb [OF dual])
   3.132 +
   3.133 +lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>"
   3.134 +by (rule boolean.conj_zero_right [OF dual])
   3.135 +
   3.136 +lemma compl_zero [simp]: "\<sim> \<zero> = \<one>"
   3.137 +by (rule boolean.compl_one [OF dual])
   3.138 +
   3.139 +lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x"
   3.140 +by (rule boolean.conj_one_left [OF dual])
   3.141 +
   3.142 +lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>"
   3.143 +by (rule boolean.conj_zero_left [OF dual])
   3.144 +
   3.145 +lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>"
   3.146 +by (rule boolean.conj_cancel_left [OF dual])
   3.147 +
   3.148 +lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   3.149 +by (rule boolean.conj_left_absorb [OF dual])
   3.150 +
   3.151 +lemma disj_conj_distrib2:
   3.152 +  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   3.153 +by (rule boolean.conj_disj_distrib2 [OF dual])
   3.154 +
   3.155 +lemmas disj_conj_distribs =
   3.156 +   disj_conj_distrib disj_conj_distrib2
   3.157 +
   3.158 +text {* De Morgan's Laws *}
   3.159 +
   3.160 +lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
   3.161 +proof (rule compl_unique)
   3.162 +  have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)"
   3.163 +    by (rule conj_disj_distrib)
   3.164 +  also have "... = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))"
   3.165 +    by (simp add: conj_ac)
   3.166 +  finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>"
   3.167 +    by (simp add: conj_cancel_right conj_zero_right disj_zero_right)
   3.168 +next
   3.169 +  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))"
   3.170 +    by (rule disj_conj_distrib2)
   3.171 +  also have "... = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))"
   3.172 +    by (simp add: disj_ac)
   3.173 +  finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>"
   3.174 +    by (simp add: disj_cancel_right disj_one_right conj_one_right)
   3.175 +qed
   3.176 +
   3.177 +lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
   3.178 +by (rule boolean.de_Morgan_conj [OF dual])
   3.179 +
   3.180 +end
   3.181 +
   3.182 +text {* Symmetric Difference *}
   3.183 +
   3.184 +locale boolean_xor = boolean +
   3.185 +  fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
   3.186 +  assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
   3.187 +begin
   3.188 +
   3.189 +lemma xor_def2:
   3.190 +  "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
   3.191 +by (simp add: xor_def conj_disj_distribs
   3.192 +              disj_ac conj_ac conj_cancel_right disj_zero_left)
   3.193 +
   3.194 +lemma xor_commute: "x \<oplus> y = y \<oplus> x"
   3.195 +by (simp add: xor_def conj_commute disj_commute)
   3.196 +
   3.197 +lemma xor_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   3.198 +proof -
   3.199 +  let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
   3.200 +            (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
   3.201 +  have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
   3.202 +        ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"
   3.203 +    by (simp add: conj_cancel_right conj_zero_right)
   3.204 +  thus "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   3.205 +    apply (simp add: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   3.206 +    apply (simp add: conj_disj_distribs conj_ac disj_ac)
   3.207 +    done
   3.208 +qed
   3.209 +
   3.210 +lemmas xor_ac =
   3.211 +  xor_assoc xor_commute
   3.212 +  mk_left_commute [of "xor", OF xor_assoc xor_commute]
   3.213 +
   3.214 +lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
   3.215 +by (simp add: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
   3.216 +
   3.217 +lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x"
   3.218 +by (subst xor_commute) (rule xor_zero_right)
   3.219 +
   3.220 +lemma xor_one_right [simp]: "x \<oplus> \<one> = \<sim> x"
   3.221 +by (simp add: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)
   3.222 +
   3.223 +lemma xor_one_left [simp]: "\<one> \<oplus> x = \<sim> x"
   3.224 +by (subst xor_commute) (rule xor_one_right)
   3.225 +
   3.226 +lemma xor_self [simp]: "x \<oplus> x = \<zero>"
   3.227 +by (simp add: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
   3.228 +
   3.229 +lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
   3.230 +by (simp add: xor_assoc [symmetric] xor_self xor_zero_left)
   3.231 +
   3.232 +lemma xor_compl_left: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
   3.233 +apply (simp add: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   3.234 +apply (simp add: conj_disj_distribs)
   3.235 +apply (simp add: conj_cancel_right conj_cancel_left)
   3.236 +apply (simp add: disj_zero_left disj_zero_right)
   3.237 +apply (simp add: disj_ac conj_ac)
   3.238 +done
   3.239 +
   3.240 +lemma xor_compl_right: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
   3.241 +apply (simp add: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   3.242 +apply (simp add: conj_disj_distribs)
   3.243 +apply (simp add: conj_cancel_right conj_cancel_left)
   3.244 +apply (simp add: disj_zero_left disj_zero_right)
   3.245 +apply (simp add: disj_ac conj_ac)
   3.246 +done
   3.247 +
   3.248 +lemma xor_cancel_right [simp]: "x \<oplus> \<sim> x = \<one>"
   3.249 +by (simp add: xor_compl_right xor_self compl_zero)
   3.250 +
   3.251 +lemma xor_cancel_left [simp]: "\<sim> x \<oplus> x = \<one>"
   3.252 +by (subst xor_commute) (rule xor_cancel_right)
   3.253 +
   3.254 +lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   3.255 +proof -
   3.256 +  have "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
   3.257 +        (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)"
   3.258 +    by (simp add: conj_cancel_right conj_zero_right disj_zero_left)
   3.259 +  thus "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   3.260 +    by (simp (no_asm_use) add:
   3.261 +        xor_def de_Morgan_disj de_Morgan_conj double_compl
   3.262 +        conj_disj_distribs conj_ac disj_ac)
   3.263 +qed
   3.264 +
   3.265 +lemma conj_xor_distrib2:
   3.266 +  "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
   3.267 +proof -
   3.268 +  have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   3.269 +    by (rule conj_xor_distrib)
   3.270 +  thus "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
   3.271 +    by (simp add: conj_commute)
   3.272 +qed
   3.273 +
   3.274 +lemmas conj_xor_distribs =
   3.275 +   conj_xor_distrib conj_xor_distrib2
   3.276 +
   3.277 +end
   3.278 +
   3.279 +end
     4.1 --- a/src/HOL/Library/Library.thy	Sun Aug 19 21:21:37 2007 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Mon Aug 20 00:22:18 2007 +0200
     4.3 @@ -6,6 +6,7 @@
     4.4    AssocList
     4.5    BigO
     4.6    Binomial
     4.7 +  Boolean_Algebra
     4.8    Char_ord
     4.9    Coinductive_List
    4.10    Commutative_Ring
    4.11 @@ -24,6 +25,7 @@
    4.12    NatPair
    4.13    Nat_Infinity
    4.14    Nested_Environment
    4.15 +  Numeral_Type
    4.16    OptionalSugar
    4.17    Parity
    4.18    Permutation
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Aug 20 00:22:18 2007 +0200
     5.3 @@ -0,0 +1,238 @@
     5.4 +(*
     5.5 +  ID:     $Id$
     5.6 +  Author: Brian Huffman
     5.7 +
     5.8 +  Numeral Syntax for Types
     5.9 +*)
    5.10 +
    5.11 +header "Numeral Syntax for Types"
    5.12 +
    5.13 +theory Numeral_Type
    5.14 +  imports Infinite_Set
    5.15 +begin
    5.16 +
    5.17 +subsection {* Preliminary lemmas *}
    5.18 +(* These should be moved elsewhere *)
    5.19 +
    5.20 +lemma inj_Inl [simp]: "inj_on Inl A"
    5.21 +  by (rule inj_onI, simp)
    5.22 +
    5.23 +lemma inj_Inr [simp]: "inj_on Inr A"
    5.24 +  by (rule inj_onI, simp)
    5.25 +
    5.26 +lemma inj_Some [simp]: "inj_on Some A"
    5.27 +  by (rule inj_onI, simp)
    5.28 +
    5.29 +lemma card_Plus:
    5.30 +  "[| finite A; finite B |] ==> card (A <+> B) = card A + card B"
    5.31 +  unfolding Plus_def
    5.32 +  apply (subgoal_tac "Inl ` A \<inter> Inr ` B = {}")
    5.33 +  apply (simp add: card_Un_disjoint card_image)
    5.34 +  apply fast
    5.35 +  done
    5.36 +
    5.37 +lemma (in type_definition) univ:
    5.38 +  "UNIV = Abs ` A"
    5.39 +proof
    5.40 +  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
    5.41 +  show "UNIV \<subseteq> Abs ` A"
    5.42 +  proof
    5.43 +    fix x :: 'b
    5.44 +    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
    5.45 +    moreover have "Rep x \<in> A" by (rule Rep)
    5.46 +    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
    5.47 +  qed
    5.48 +qed
    5.49 +
    5.50 +lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
    5.51 +  by (simp add: univ card_image inj_on_def Abs_inject)
    5.52 +
    5.53 +
    5.54 +subsection {* Cardinalities of types *}
    5.55 +
    5.56 +syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    5.57 +
    5.58 +translations "CARD(t)" => "card (UNIV::t set)"
    5.59 +
    5.60 +lemma card_unit: "CARD(unit) = 1"
    5.61 +  unfolding univ_unit by simp
    5.62 +
    5.63 +lemma card_bool: "CARD(bool) = 2"
    5.64 +  unfolding univ_bool by simp
    5.65 +
    5.66 +lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
    5.67 +  unfolding univ_prod by (simp only: card_cartesian_product)
    5.68 +
    5.69 +lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
    5.70 +  unfolding univ_sum by (simp only: finite card_Plus)
    5.71 +
    5.72 +lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
    5.73 +  unfolding univ_option
    5.74 +  apply (subgoal_tac "(None::'a option) \<notin> range Some")
    5.75 +  apply (simp add: finite card_image)
    5.76 +  apply fast
    5.77 +  done
    5.78 +
    5.79 +lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
    5.80 +  unfolding univ_set
    5.81 +  by (simp only: card_Pow finite numeral_2_eq_2)
    5.82 +
    5.83 +subsection {* Numeral Types *}
    5.84 +
    5.85 +typedef (open) pls = "UNIV :: nat set" ..
    5.86 +typedef (open) num1 = "UNIV :: unit set" ..
    5.87 +typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
    5.88 +typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
    5.89 +
    5.90 +instance num1 :: finite
    5.91 +proof
    5.92 +  show "finite (UNIV::num1 set)"
    5.93 +    unfolding type_definition.univ [OF type_definition_num1]
    5.94 +    using finite by (rule finite_imageI)
    5.95 +qed
    5.96 +
    5.97 +instance bit0 :: (finite) finite
    5.98 +proof
    5.99 +  show "finite (UNIV::'a bit0 set)"
   5.100 +    unfolding type_definition.univ [OF type_definition_bit0]
   5.101 +    using finite by (rule finite_imageI)
   5.102 +qed
   5.103 +
   5.104 +instance bit1 :: (finite) finite
   5.105 +proof
   5.106 +  show "finite (UNIV::'a bit1 set)"
   5.107 +    unfolding type_definition.univ [OF type_definition_bit1]
   5.108 +    using finite by (rule finite_imageI)
   5.109 +qed
   5.110 +
   5.111 +lemma card_num1: "CARD(num1) = 1"
   5.112 +  unfolding type_definition.card [OF type_definition_num1]
   5.113 +  by (simp only: card_unit)
   5.114 +
   5.115 +lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
   5.116 +  unfolding type_definition.card [OF type_definition_bit0]
   5.117 +  by (simp only: card_prod card_bool)
   5.118 +
   5.119 +lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
   5.120 +  unfolding type_definition.card [OF type_definition_bit1]
   5.121 +  by (simp only: card_prod card_option card_bool)
   5.122 +
   5.123 +lemma card_pls: "CARD (pls) = 0"
   5.124 +  by (simp add: type_definition.card [OF type_definition_pls])
   5.125 +
   5.126 +lemmas card_univ_simps [simp] =
   5.127 +  card_unit
   5.128 +  card_bool
   5.129 +  card_prod
   5.130 +  card_sum
   5.131 +  card_option
   5.132 +  card_set
   5.133 +  card_num1
   5.134 +  card_bit0
   5.135 +  card_bit1
   5.136 +  card_pls
   5.137 +
   5.138 +subsection {* Syntax *}
   5.139 +
   5.140 +
   5.141 +syntax
   5.142 +  "_NumeralType" :: "num_const => type"  ("_")
   5.143 +  "_NumeralType0" :: type ("0")
   5.144 +  "_NumeralType1" :: type ("1")
   5.145 +
   5.146 +translations
   5.147 +  "_NumeralType1" == (type) "num1"
   5.148 +  "_NumeralType0" == (type) "pls"
   5.149 +
   5.150 +parse_translation {*
   5.151 +let
   5.152 +
   5.153 +val num1_const = Syntax.const "Numeral_Type.num1";
   5.154 +val pls_const = Syntax.const "Numeral_Type.pls";
   5.155 +val B0_const = Syntax.const "Numeral_Type.bit0";
   5.156 +val B1_const = Syntax.const "Numeral_Type.bit1";
   5.157 +
   5.158 +fun mk_bintype n =
   5.159 +  let
   5.160 +    fun mk_bit n = if n = 0 then B0_const else B1_const;
   5.161 +    fun bin_of n =
   5.162 +      if n = 1 then num1_const
   5.163 +      else if n = 0 then pls_const
   5.164 +      else if n = ~1 then raise TERM ("negative type numeral", [])
   5.165 +      else
   5.166 +        let val (q, r) = IntInf.divMod (n, 2);
   5.167 +        in mk_bit r $ bin_of q end;
   5.168 +  in bin_of n end;
   5.169 +
   5.170 +fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
   5.171 +      mk_bintype (valOf (IntInf.fromString str))
   5.172 +  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
   5.173 +
   5.174 +in [("_NumeralType", numeral_tr)] end;
   5.175 +*}
   5.176 +
   5.177 +print_translation {*
   5.178 +let
   5.179 +fun int_of [] = 0
   5.180 +  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
   5.181 +
   5.182 +fun bin_of (Const ("pls", _)) = []
   5.183 +  | bin_of (Const ("num1", _)) = [1]
   5.184 +  | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
   5.185 +  | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
   5.186 +  | bin_of t = raise TERM("bin_of", [t]);
   5.187 +
   5.188 +fun bit_tr' b [t] =
   5.189 +  let
   5.190 +    val rev_digs = b :: bin_of t handle TERM _ => raise Match
   5.191 +    val i = int_of rev_digs;
   5.192 +    val num = IntInf.toString (IntInf.abs i);
   5.193 +  in
   5.194 +    Syntax.const "_NumeralType" $ Syntax.free num
   5.195 +  end
   5.196 +  | bit_tr' b _ = raise Match;
   5.197 +
   5.198 +in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
   5.199 +*}
   5.200 +
   5.201 +
   5.202 +subsection {* Classes with at values least 1 and 2  *}
   5.203 +
   5.204 +text {* Class finite already captures "at least 1" *}
   5.205 +
   5.206 +lemma zero_less_card_finite:
   5.207 +  "0 < CARD('a::finite)"
   5.208 +proof (cases "CARD('a::finite) = 0")
   5.209 +  case False thus ?thesis by (simp del: card_0_eq)
   5.210 +next
   5.211 +  case True
   5.212 +  thus ?thesis by (simp add: finite)
   5.213 +qed
   5.214 +
   5.215 +lemma one_le_card_finite:
   5.216 +  "Suc 0 <= CARD('a::finite)"
   5.217 +  by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
   5.218 +
   5.219 +
   5.220 +text {* Class for cardinality "at least 2" *}
   5.221 +
   5.222 +class card2 = finite + 
   5.223 +  assumes two_le_card: "2 <= CARD('a)"
   5.224 +
   5.225 +lemma one_less_card: "Suc 0 < CARD('a::card2)"
   5.226 +  using two_le_card [where 'a='a] by simp
   5.227 +
   5.228 +instance bit0 :: (finite) card2
   5.229 +  by intro_classes (simp add: one_le_card_finite)
   5.230 +
   5.231 +instance bit1 :: (finite) card2
   5.232 +  by intro_classes (simp add: one_le_card_finite)
   5.233 +
   5.234 +subsection {* Examples *}
   5.235 +
   5.236 +term "TYPE(10)"
   5.237 +
   5.238 +lemma "CARD(0) = 0" by simp
   5.239 +lemma "CARD(17) = 17" by simp
   5.240 +  
   5.241 +end