1.1 --- a/src/HOL/IsaMakefile	Wed Aug 30 08:30:09 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Aug 30 08:34:45 2006 +0200
     1.3 @@ -640,7 +640,7 @@
     1.4  
     1.5  $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
     1.6    ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
     1.7 -  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
     1.8 +  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
     1.9    ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
    1.10    ex/CodeOperationalEquality.thy ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
    1.11    ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/CodeCollections.thy	Wed Aug 30 08:34:45 2006 +0200
     2.3 @@ -0,0 +1,417 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Florian Haftmann, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* Collection classes as examples for code generation *}
     2.9 +
    2.10 +theory CodeCollections
    2.11 +imports CodeOperationalEquality
    2.12 +begin
    2.13 +
    2.14 +section {* Collection classes as examples for code generation *}
    2.15 +
    2.16 +class ordered = eq +
    2.17 +  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.18 +  fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<=" 65)
    2.19 +  fixes lt :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<" 65)
    2.20 +  assumes order_refl: "x \<^loc><<= x"
    2.21 +  assumes order_trans: "x \<^loc><<= y ==> y \<^loc><<= z ==> x \<^loc><<= z"
    2.22 +  assumes order_antisym: "x \<^loc><<= y ==> y \<^loc><<= x ==> x = y"
    2.23 +
    2.24 +declare order_refl [simp, intro]
    2.25 +
    2.26 +defs
    2.27 +  lt_def: "x << y == (x <<= y \<and> x \<noteq> y)"
    2.28 +
    2.29 +lemma lt_intro [intro]:
    2.30 +  assumes "x <<= y" and "x \<noteq> y"
    2.31 +  shows "x << y"
    2.32 +unfolding lt_def ..
    2.33 +
    2.34 +lemma lt_elim [elim]:
    2.35 +  assumes "(x::'a::ordered) << y"
    2.36 +  and Q: "!!x y::'a::ordered. x <<= y \<Longrightarrow> x \<noteq> y \<Longrightarrow> P"
    2.37 +  shows P
    2.38 +proof -
    2.39 +  from prems have R1: "x <<= y" and R2: "x \<noteq> y" by (simp_all add: lt_def)
    2.40 +  show P by (rule Q [OF R1 R2])
    2.41 +qed
    2.42 +
    2.43 +lemma lt_trans:
    2.44 +  assumes "x << y" and "y << z"
    2.45 +  shows "x << z"
    2.46 +proof
    2.47 +  from prems lt_def have prems': "x <<= y" "y <<= z" by auto
    2.48 +  show "x <<= z" by (rule order_trans, auto intro: prems')
    2.49 +next
    2.50 +  show "x \<noteq> z"
    2.51 +  proof
    2.52 +    from prems lt_def have prems': "x <<= y" "y <<= z" "x \<noteq> y" by auto
    2.53 +    assume "x = z"
    2.54 +    with prems' have "x <<= y" and "y <<= x" by auto
    2.55 +    with order_antisym have "x = y" .
    2.56 +    with prems' show False by auto
    2.57 +  qed
    2.58 +qed
    2.59 +
    2.60 +definition (in ordered)
    2.61 +  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.62 +  "min x y = (if x \<^loc><<= y then x else y)"
    2.63 +  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.64 +  "max x y = (if x \<^loc><<= y then y else x)"
    2.65 +
    2.66 +definition
    2.67 +  min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
    2.68 +  "min x y = (if x <<= y then x else y)"
    2.69 +  max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
    2.70 +  "max x y = (if x <<= y then y else x)"
    2.71 +
    2.72 +consts
    2.73 +  abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    2.74 +
    2.75 +function
    2.76 +  "abs_sorted cmp [] = True"
    2.77 +  "abs_sorted cmp [x] = True"
    2.78 +  "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
    2.79 +by pat_completeness simp_all
    2.80 +termination by (auto_term "measure (length o snd)")
    2.81 +
    2.82 +abbreviation (in ordered)
    2.83 +  "sorted \<equiv> abs_sorted le"
    2.84 +
    2.85 +abbreviation
    2.86 +  "sorted \<equiv> abs_sorted le"
    2.87 +
    2.88 +lemma (in ordered) sorted_weakening:
    2.89 +  assumes "sorted (x # xs)"
    2.90 +  shows "sorted xs"
    2.91 +using prems proof (induct xs)
    2.92 +  case Nil show ?case by simp 
    2.93 +next
    2.94 +  case (Cons x' xs)
    2.95 +  from this(5) have "sorted (x # x' # xs)" .
    2.96 +  then show "sorted (x' # xs)" by auto
    2.97 +qed
    2.98 +
    2.99 +instance bool :: ordered
   2.100 +  "p <<= q == (p --> q)"
   2.101 +  by default (unfold ordered_bool_def, blast+)
   2.102 +
   2.103 +instance nat :: ordered
   2.104 +  "m <<= n == m <= n"
   2.105 +  by default (simp_all add: ordered_nat_def)
   2.106 +
   2.107 +instance int :: ordered
   2.108 +  "k <<= l == k <= l"
   2.109 +  by default (simp_all add: ordered_int_def)
   2.110 +
   2.111 +instance unit :: ordered
   2.112 +  "u <<= v == True"
   2.113 +  by default (simp_all add:  ordered_unit_def)
   2.114 +
   2.115 +consts
   2.116 +  le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
   2.117 +
   2.118 +function
   2.119 +  "le_option' None y = True"
   2.120 +  "le_option' (Some x) None = False"
   2.121 +  "le_option' (Some x) (Some y) = x <<= y"
   2.122 +  by pat_completeness simp_all
   2.123 +termination by (auto_term "{}")
   2.124 +
   2.125 +instance (ordered) option :: ordered
   2.126 +  "x <<= y == le_option' x y"
   2.127 +proof (default, unfold ordered_option_def)
   2.128 +  fix x
   2.129 +  show "le_option' x x" by (cases x) simp_all
   2.130 +next
   2.131 +  fix x y z
   2.132 +  assume "le_option' x y" "le_option' y z"
   2.133 +  then show "le_option' x z"
   2.134 +    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
   2.135 +    (erule order_trans, assumption)
   2.136 +next
   2.137 +  fix x y
   2.138 +  assume "le_option' x y" "le_option' y x"
   2.139 +  then show "x = y"
   2.140 +    by (cases x, simp_all, cases y, simp_all, cases y, simp_all)
   2.141 +    (erule order_antisym, assumption)
   2.142 +qed
   2.143 +
   2.144 +lemma [simp, code]:
   2.145 +  "None <<= y = True"
   2.146 +  "Some x <<= None = False"
   2.147 +  "Some v <<= Some w = v <<= w"
   2.148 +  unfolding ordered_option_def le_option'.simps by rule+
   2.149 +
   2.150 +consts
   2.151 +  le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   2.152 +
   2.153 +function
   2.154 +  "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
   2.155 +  by pat_completeness simp_all
   2.156 +termination by (auto_term "{}")
   2.157 +
   2.158 +instance (ordered, ordered) * :: ordered
   2.159 +  "x <<= y == le_pair' x y"
   2.160 +apply (default, unfold "ordered_*_def", unfold split_paired_all)
   2.161 +apply simp_all
   2.162 +apply (auto intro: lt_trans order_trans)[1]
   2.163 +unfolding lt_def apply (auto intro: order_antisym)[1]
   2.164 +done
   2.165 +
   2.166 +lemma [simp, code]:
   2.167 +  "(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
   2.168 +  unfolding "ordered_*_def" le_pair'.simps ..
   2.169 +
   2.170 +(* consts
   2.171 +  le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
   2.172 +
   2.173 +function
   2.174 +  "le_list' [] ys = True"
   2.175 +  "le_list' (x#xs) [] = False"
   2.176 +  "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
   2.177 +    by pat_completeness simp_all
   2.178 +termination by (auto_term "measure (length o fst)")
   2.179 +
   2.180 +instance (ordered) list :: ordered
   2.181 +  "xs <<= ys == le_list' xs ys"
   2.182 +proof (default, unfold "ordered_list_def")
   2.183 +  fix xs
   2.184 +  show "le_list' xs xs" by (induct xs) simp_all
   2.185 +next
   2.186 +  fix xs ys zs
   2.187 +  assume "le_list' xs ys" and "le_list' ys zs"
   2.188 +  then show "le_list' xs zs"
   2.189 +  apply (induct xs zs rule: le_list'.induct)
   2.190 +  apply simp_all
   2.191 +  apply (cases ys) apply simp_all
   2.192 +  
   2.193 +  apply (induct ys) apply simp_all
   2.194 +  apply (induct ys)
   2.195 +  apply simp_all
   2.196 +  apply (induct zs)
   2.197 +  apply simp_all
   2.198 +next
   2.199 +  fix xs ys
   2.200 +  assume "le_list' xs ys" and "le_list' ys xs"
   2.201 +  show "xs = ys" sorry
   2.202 +qed
   2.203 +
   2.204 +lemma [simp, code]:
   2.205 +  "[] <<= ys = True"
   2.206 +  "(x#xs) <<= [] = False"
   2.207 +  "(x#xs) <<= (y#ys) = (x << y \<or> x = y \<and> xs <<= ys)"
   2.208 +  unfolding "ordered_list_def" le_list'.simps by rule+*)
   2.209 +
   2.210 +class infimum = ordered +
   2.211 +  fixes inf
   2.212 +  assumes inf: "inf \<^loc><<= x"
   2.213 +
   2.214 +lemma (in infimum)
   2.215 +  assumes prem: "a \<^loc><<= inf"
   2.216 +  shows no_smaller: "a = inf"
   2.217 +using prem inf by (rule order_antisym)
   2.218 +
   2.219 +consts
   2.220 +  abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
   2.221 +
   2.222 +ML {* set quick_and_dirty *}
   2.223 +function
   2.224 +  "abs_max_of cmp inff [] = inff"
   2.225 +  "abs_max_of cmp inff [x] = x"
   2.226 +  "abs_max_of cmp inff (x#xs) =
   2.227 +     ordered.max cmp x (abs_max_of cmp inff xs)"
   2.228 +apply pat_completeness sorry
   2.229 +
   2.230 +abbreviation (in infimum)
   2.231 +  "max_of xs \<equiv> abs_max_of le inf"
   2.232 +
   2.233 +abbreviation
   2.234 +  "max_of xs \<equiv> abs_max_of le inf"
   2.235 +
   2.236 +instance bool :: infimum
   2.237 +  "inf == False"
   2.238 +  by default (simp add: infimum_bool_def)
   2.239 +
   2.240 +instance nat :: infimum
   2.241 +  "inf == 0"
   2.242 +  by default (simp add: infimum_nat_def)
   2.243 +
   2.244 +instance unit :: infimum
   2.245 +  "inf == ()"
   2.246 +  by default (simp add: infimum_unit_def)
   2.247 +
   2.248 +instance (ordered) option :: infimum
   2.249 +  "inf == None"
   2.250 +  by default (simp add: infimum_option_def)
   2.251 +
   2.252 +instance (infimum, infimum) * :: infimum
   2.253 +  "inf == (inf, inf)"
   2.254 +  by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf)
   2.255 +
   2.256 +class enum = ordered +
   2.257 +  fixes enum :: "'a list"
   2.258 +  assumes member_enum: "x \<in> set enum"
   2.259 +  and ordered_enum: "abs_sorted le enum"
   2.260 +
   2.261 +(*
   2.262 +FIXME:
   2.263 +- abbreviations must be propagated before locale introduction
   2.264 +- then also now shadowing may occur
   2.265 +*)
   2.266 +(*abbreviation (in enum)
   2.267 +  "local.sorted \<equiv> abs_sorted le"*)
   2.268 +
   2.269 +instance bool :: enum
   2.270 +  (* FIXME: better name handling of definitions *)
   2.271 +  "_1": "enum == [False, True]"
   2.272 +  by default (simp_all add: enum_bool_def)
   2.273 +
   2.274 +instance unit :: enum
   2.275 +  "_2": "enum == [()]"
   2.276 +  by default (simp_all add: enum_unit_def)
   2.277 +
   2.278 +(*consts
   2.279 +  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
   2.280 +
   2.281 +primrec
   2.282 +  "product [] ys = []"
   2.283 +  "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   2.284 +
   2.285 +lemma product_all:
   2.286 +  assumes "x \<in> set xs" "y \<in> set ys"
   2.287 +  shows "(x, y) \<in> set (product xs ys)"
   2.288 +using prems proof (induct xs)
   2.289 +  case Nil
   2.290 +  then have False by auto
   2.291 +  then show ?case ..
   2.292 +next
   2.293 +  case (Cons z xs)
   2.294 +  then show ?case
   2.295 +  proof (cases "x = z")
   2.296 +    case True
   2.297 +    with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
   2.298 +    with True show ?thesis by simp
   2.299 +  next
   2.300 +    case False
   2.301 +    with Cons have "x \<in> set xs" by auto
   2.302 +    with Cons have "(x, y) \<in> set (product xs ys)" by auto
   2.303 +    then show "(x, y) \<in> set (product (z#xs) ys)" by auto
   2.304 +  qed
   2.305 +qed
   2.306 +
   2.307 +lemma product_sorted:
   2.308 +  assumes "sorted xs" "sorted ys"
   2.309 +  shows "sorted (product xs ys)"
   2.310 +using prems proof (induct xs)
   2.311 +  case Nil
   2.312 +  then show ?case by simp
   2.313 +next
   2.314 +  case (Cons x xs)
   2.315 +  from Cons ordered.sorted_weakening have "sorted xs" by auto
   2.316 +  with Cons have "sorted (product xs ys)" by auto
   2.317 +  then show ?case apply simp
   2.318 +  proof -
   2.319 +    assume 
   2.320 +apply simp
   2.321 +  
   2.322 +  proof (cases "x = z")
   2.323 +    case True
   2.324 +    with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
   2.325 +    with True show ?thesis by simp
   2.326 +  next
   2.327 +    case False
   2.328 +    with Cons have "x \<in> set xs" by auto
   2.329 +    with Cons have "(x, y) \<in> set (product xs ys)" by auto
   2.330 +    then show "(x, y) \<in> set (product (z#xs) ys)" by auto
   2.331 +  qed
   2.332 +qed
   2.333 +
   2.334 +instance (enum, enum) * :: enum
   2.335 +  "_3": "enum == product enum enum"
   2.336 +apply default
   2.337 +apply (simp_all add: "enum_*_def")
   2.338 +apply (unfold split_paired_all)
   2.339 +apply (rule product_all)
   2.340 +apply (rule member_enum)+
   2.341 +sorry*)
   2.342 +
   2.343 +instance (enum) option :: enum
   2.344 +  "_4": "enum == None # map Some enum"
   2.345 +proof (default, unfold enum_option_def)
   2.346 +  fix x :: "'a::enum option"
   2.347 +  show "x \<in> set (None # map Some enum)"
   2.348 +  proof (cases x)
   2.349 +    case None then show ?thesis by auto
   2.350 +  next
   2.351 +    case (Some x) then show ?thesis by (auto intro: member_enum)
   2.352 +  qed
   2.353 +next
   2.354 +  show "sorted (None # map Some (enum :: ('a::enum) list))"
   2.355 +  sorry
   2.356 +  (*proof (cases "enum :: 'a list")
   2.357 +    case Nil then show ?thesis by simp
   2.358 +  next
   2.359 +   case (Cons x xs)
   2.360 +   then have "sorted (None # map Some (x # xs))" sorry
   2.361 +   then show ?thesis apply simp
   2.362 +  apply simp_all
   2.363 +  apply auto*)
   2.364 +qed
   2.365 +
   2.366 +ML {* reset quick_and_dirty *}
   2.367 +
   2.368 +consts
   2.369 +  get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option"
   2.370 +
   2.371 +primrec
   2.372 +  "get_first p [] = None"
   2.373 +  "get_first p (x#xs) = (if p x then Some x else get_first p xs)"
   2.374 +
   2.375 +consts
   2.376 +  get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option"
   2.377 +
   2.378 +primrec
   2.379 +  "get_index p n [] = None"
   2.380 +  "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)"
   2.381 +
   2.382 +definition
   2.383 +  between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option"
   2.384 +  "between x y = get_first (\<lambda>z. x << z & z << y) enum"
   2.385 +
   2.386 +definition
   2.387 +  index :: "'a::enum \<Rightarrow> nat"
   2.388 +  "index x = the (get_index (\<lambda>y. y = x) 0 enum)"
   2.389 +
   2.390 +definition
   2.391 +  add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a"
   2.392 +  "add x y =
   2.393 +    (let
   2.394 +      enm = enum
   2.395 +    in enm ! ((index x + index y) mod length enm))"
   2.396 +
   2.397 +consts
   2.398 +  sum :: "'a::{enum, infimum} list \<Rightarrow> 'a"
   2.399 +
   2.400 +primrec
   2.401 +  "sum [] = inf"
   2.402 +  "sum (x#xs) = add x (sum xs)"
   2.403 +
   2.404 +definition
   2.405 +  "test1 = sum [None, Some True, None, Some False]"
   2.406 +  "test2 = (inf :: nat \<times> unit)"
   2.407 +
   2.408 +code_generate eq
   2.409 +code_generate "op <<="
   2.410 +code_generate "op <<"
   2.411 +code_generate inf
   2.412 +code_generate between
   2.413 +code_generate index
   2.414 +code_generate sum
   2.415 +code_generate test1
   2.416 +code_generate test2
   2.417 +
   2.418 +code_serialize ml (-)
   2.419 +
   2.420 +end
   2.421 \ No newline at end of file

     3.1 --- a/src/HOL/ex/ROOT.ML	Wed Aug 30 08:30:09 2006 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Wed Aug 30 08:34:45 2006 +0200
     3.3 @@ -7,6 +7,7 @@
     3.4  no_document time_use_thy "Classpackage";
     3.5  no_document time_use_thy "Codegenerator";
     3.6  no_document time_use_thy "CodeOperationalEquality";
     3.7 +no_document time_use_thy "CodeCollections";
     3.8  no_document time_use_thy "CodeEval";
     3.9  no_document time_use_thy "CodeRandom";
    3.10