refined internal structure of Enum.thy
authorhaftmann
Sat Oct 20 10:00:21 2012 +0200 (2012-10-20)
changeset 49949be3dd2e602e8
parent 49948 744934b818c7
child 49950 cd882d53ba6b
refined internal structure of Enum.thy
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Sat Oct 20 09:12:16 2012 +0200
     1.2 +++ b/src/HOL/Enum.thy	Sat Oct 20 10:00:21 2012 +0200
     1.3 @@ -37,7 +37,71 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* Equality and order on functions *}
     1.8 +subsection {* Implementations using @{class enum} *}
     1.9 +
    1.10 +subsubsection {* Unbounded operations and quantifiers *}
    1.11 +
    1.12 +lemma Collect_code [code]:
    1.13 +  "Collect P = set (filter P enum)"
    1.14 +  by (auto simp add: enum_UNIV)
    1.15 +
    1.16 +definition card_UNIV :: "'a itself \<Rightarrow> nat"
    1.17 +where
    1.18 +  [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"
    1.19 +
    1.20 +lemma [code]:
    1.21 +  "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
    1.22 +  by (simp only: card_UNIV_def enum_UNIV)
    1.23 +
    1.24 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
    1.25 +  by (simp add: enum_all)
    1.26 +
    1.27 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
    1.28 +  by (simp add: enum_ex)
    1.29 +
    1.30 +lemma exists1_code [code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
    1.31 +  by (auto simp add: enum_UNIV list_ex1_iff)
    1.32 +
    1.33 +
    1.34 +subsubsection {* An executable choice operator *}
    1.35 +
    1.36 +definition
    1.37 +  [code del]: "enum_the = The"
    1.38 +
    1.39 +lemma [code]:
    1.40 +  "The P = (case filter P enum of [x] => x | _ => enum_the P)"
    1.41 +proof -
    1.42 +  {
    1.43 +    fix a
    1.44 +    assume filter_enum: "filter P enum = [a]"
    1.45 +    have "The P = a"
    1.46 +    proof (rule the_equality)
    1.47 +      fix x
    1.48 +      assume "P x"
    1.49 +      show "x = a"
    1.50 +      proof (rule ccontr)
    1.51 +        assume "x \<noteq> a"
    1.52 +        from filter_enum obtain us vs
    1.53 +          where enum_eq: "enum = us @ [a] @ vs"
    1.54 +          and "\<forall> x \<in> set us. \<not> P x"
    1.55 +          and "\<forall> x \<in> set vs. \<not> P x"
    1.56 +          and "P a"
    1.57 +          by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
    1.58 +        with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
    1.59 +      qed
    1.60 +    next
    1.61 +      from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
    1.62 +    qed
    1.63 +  }
    1.64 +  from this show ?thesis
    1.65 +    unfolding enum_the_def by (auto split: list.split)
    1.66 +qed
    1.67 +
    1.68 +code_abort enum_the
    1.69 +code_const enum_the (Eval "(fn p => raise Match)")
    1.70 +
    1.71 +
    1.72 +subsubsection {* Equality and order on functions *}
    1.73  
    1.74  instantiation "fun" :: (enum, equal) equal
    1.75  begin
    1.76 @@ -65,19 +129,43 @@
    1.77    by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le)
    1.78  
    1.79  
    1.80 -subsection {* Quantifiers *}
    1.81 +subsubsection {* Operations on relations *}
    1.82 +
    1.83 +lemma [code]:
    1.84 +  "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
    1.85 +  by (auto intro: imageI in_enum)
    1.86  
    1.87 -lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
    1.88 -  by (simp add: enum_all)
    1.89 +lemma tranclp_unfold [code, no_atp]:
    1.90 +  "tranclp r a b \<longleftrightarrow> (a, b) \<in> trancl {(x, y). r x y}"
    1.91 +  by (simp add: trancl_def)
    1.92 +
    1.93 +lemma rtranclp_rtrancl_eq [code, no_atp]:
    1.94 +  "rtranclp r x y \<longleftrightarrow> (x, y) \<in> rtrancl {(x, y). r x y}"
    1.95 +  by (simp add: rtrancl_def)
    1.96  
    1.97 -lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
    1.98 -  by (simp add: enum_ex)
    1.99 +lemma max_ext_eq [code]:
   1.100 +  "max_ext R = {(X, Y). finite X \<and> finite Y \<and> Y \<noteq> {} \<and> (\<forall>x. x \<in> X \<longrightarrow> (\<exists>xa \<in> Y. (x, xa) \<in> R))}"
   1.101 +  by (auto simp add: max_ext.simps)
   1.102 +
   1.103 +lemma max_extp_eq [code]:
   1.104 +  "max_extp r x y \<longleftrightarrow> (x, y) \<in> max_ext {(x, y). r x y}"
   1.105 +  by (simp add: max_ext_def)
   1.106  
   1.107 -lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
   1.108 -  by (auto simp add: enum_UNIV list_ex1_iff)
   1.109 +lemma mlex_eq [code]:
   1.110 +  "f <*mlex*> R = {(x, y). f x < f y \<or> (f x \<le> f y \<and> (x, y) \<in> R)}"
   1.111 +  by (auto simp add: mlex_prod_def)
   1.112 +
   1.113 +lemma [code]:
   1.114 +  fixes xs :: "('a::finite \<times> 'a) list"
   1.115 +  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
   1.116 +  by (simp add: card_UNIV_def acc_bacc_eq)
   1.117 +
   1.118 +lemma [code]:
   1.119 +  "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
   1.120 +  by (simp add: acc_def)
   1.121  
   1.122  
   1.123 -subsection {* Default instances *}
   1.124 +subsection {* Default instances for @{class enum} *}
   1.125  
   1.126  lemma map_of_zip_enum_is_Some:
   1.127    assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   1.128 @@ -651,91 +739,6 @@
   1.129  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   1.130  
   1.131  
   1.132 -subsection {* An executable THE operator on finite types *}
   1.133 -
   1.134 -definition
   1.135 -  [code del]: "enum_the = The"
   1.136 -
   1.137 -lemma [code]:
   1.138 -  "The P = (case filter P enum of [x] => x | _ => enum_the P)"
   1.139 -proof -
   1.140 -  {
   1.141 -    fix a
   1.142 -    assume filter_enum: "filter P enum = [a]"
   1.143 -    have "The P = a"
   1.144 -    proof (rule the_equality)
   1.145 -      fix x
   1.146 -      assume "P x"
   1.147 -      show "x = a"
   1.148 -      proof (rule ccontr)
   1.149 -        assume "x \<noteq> a"
   1.150 -        from filter_enum obtain us vs
   1.151 -          where enum_eq: "enum = us @ [a] @ vs"
   1.152 -          and "\<forall> x \<in> set us. \<not> P x"
   1.153 -          and "\<forall> x \<in> set vs. \<not> P x"
   1.154 -          and "P a"
   1.155 -          by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
   1.156 -        with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
   1.157 -      qed
   1.158 -    next
   1.159 -      from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
   1.160 -    qed
   1.161 -  }
   1.162 -  from this show ?thesis
   1.163 -    unfolding enum_the_def by (auto split: list.split)
   1.164 -qed
   1.165 -
   1.166 -code_abort enum_the
   1.167 -code_const enum_the (Eval "(fn p => raise Match)")
   1.168 -
   1.169 -
   1.170 -subsection {* Further operations on finite types *}
   1.171 -
   1.172 -lemma Collect_code [code]:
   1.173 -  "Collect P = set (filter P enum)"
   1.174 -by (auto simp add: enum_UNIV)
   1.175 -
   1.176 -lemma [code]:
   1.177 -  "Id = image (%x. (x, x)) (set Enum.enum)"
   1.178 -by (auto intro: imageI in_enum)
   1.179 -
   1.180 -lemma tranclp_unfold [code, no_atp]:
   1.181 -  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
   1.182 -by (simp add: trancl_def)
   1.183 -
   1.184 -lemma rtranclp_rtrancl_eq [code, no_atp]:
   1.185 -  "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
   1.186 -unfolding rtrancl_def by auto
   1.187 -
   1.188 -lemma max_ext_eq [code]:
   1.189 -  "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
   1.190 -by (auto simp add: max_ext.simps)
   1.191 -
   1.192 -lemma max_extp_eq[code]:
   1.193 -  "max_extp r x y = ((x, y) : max_ext {(x, y). r x y})"
   1.194 -unfolding max_ext_def by auto
   1.195 -
   1.196 -lemma mlex_eq[code]:
   1.197 -  "f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}"
   1.198 -unfolding mlex_prod_def by auto
   1.199 -
   1.200 -subsection {* Executable accessible part *}
   1.201 -
   1.202 -definition 
   1.203 -  [code del]: "card_UNIV = card UNIV"
   1.204 -
   1.205 -lemma [code]:
   1.206 -  "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
   1.207 -  unfolding card_UNIV_def enum_UNIV ..
   1.208 -
   1.209 -lemma [code]:
   1.210 -  fixes xs :: "('a::finite \<times> 'a) list"
   1.211 -  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
   1.212 -  by (simp add: card_UNIV_def acc_bacc_eq)
   1.213 -
   1.214 -lemma [code_unfold]: "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
   1.215 -  unfolding acc_def by simp
   1.216 -
   1.217  subsection {* Closing up *}
   1.218  
   1.219  hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5