# HG changeset patch
# User haftmann
# Date 1156919685 -7200
# Node ID 0af8655ab0bb33edcf842f389bdb41d08fbfee3e
# Parent  d2a30fed7596d637b191ba79c855f8d5f07125f1
added yet another code generator example

diff -r d2a30fed7596 -r 0af8655ab0bb src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 30 08:30:09 2006 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 30 08:34:45 2006 +0200
@@ -640,7 +640,7 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
   ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
-  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
+  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
   ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
   ex/CodeOperationalEquality.thy ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
   ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
diff -r d2a30fed7596 -r 0af8655ab0bb src/HOL/ex/CodeCollections.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeCollections.thy	Wed Aug 30 08:34:45 2006 +0200
@@ -0,0 +1,417 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Collection classes as examples for code generation *}
+
+theory CodeCollections
+imports CodeOperationalEquality
+begin
+
+section {* Collection classes as examples for code generation *}
+
+class ordered = eq +
+  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<=" 65)
+  fixes lt :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<" 65)
+  assumes order_refl: "x \<^loc><<= x"
+  assumes order_trans: "x \<^loc><<= y ==> y \<^loc><<= z ==> x \<^loc><<= z"
+  assumes order_antisym: "x \<^loc><<= y ==> y \<^loc><<= x ==> x = y"
+
+declare order_refl [simp, intro]
+
+defs
+  lt_def: "x << y == (x <<= y \<and> x \<noteq> y)"
+
+lemma lt_intro [intro]:
+  assumes "x <<= y" and "x \<noteq> y"
+  shows "x << y"
+unfolding lt_def ..
+
+lemma lt_elim [elim]:
+  assumes "(x::'a::ordered) << y"
+  and Q: "!!x y::'a::ordered. x <<= y \<Longrightarrow> x \<noteq> y \<Longrightarrow> P"
+  shows P
+proof -
+  from prems have R1: "x <<= y" and R2: "x \<noteq> y" by (simp_all add: lt_def)
+  show P by (rule Q [OF R1 R2])
+qed
+
+lemma lt_trans:
+  assumes "x << y" and "y << z"
+  shows "x << z"
+proof
+  from prems lt_def have prems': "x <<= y" "y <<= z" by auto
+  show "x <<= z" by (rule order_trans, auto intro: prems')
+next
+  show "x \<noteq> z"
+  proof
+    from prems lt_def have prems': "x <<= y" "y <<= z" "x \<noteq> y" by auto
+    assume "x = z"
+    with prems' have "x <<= y" and "y <<= x" by auto
+    with order_antisym have "x = y" .
+    with prems' show False by auto
+  qed
+qed
+
+definition (in ordered)
+  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  "min x y = (if x \<^loc><<= y then x else y)"
+  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  "max x y = (if x \<^loc><<= y then y else x)"
+
+definition
+  min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
+  "min x y = (if x <<= y then x else y)"
+  max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
+  "max x y = (if x <<= y then y else x)"
+
+consts
+  abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+
+function
+  "abs_sorted cmp [] = True"
+  "abs_sorted cmp [x] = True"
+  "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
+by pat_completeness simp_all
+termination by (auto_term "measure (length o snd)")
+
+abbreviation (in ordered)
+  "sorted \<equiv> abs_sorted le"
+
+abbreviation
+  "sorted \<equiv> abs_sorted le"
+
+lemma (in ordered) sorted_weakening:
+  assumes "sorted (x # xs)"
+  shows "sorted xs"
+using prems proof (induct xs)
+  case Nil show ?case by simp 
+next
+  case (Cons x' xs)
+  from this(5) have "sorted (x # x' # xs)" .
+  then show "sorted (x' # xs)" by auto
+qed
+
+instance bool :: ordered
+  "p <<= q == (p --> q)"
+  by default (unfold ordered_bool_def, blast+)
+
+instance nat :: ordered
+  "m <<= n == m <= n"
+  by default (simp_all add: ordered_nat_def)
+
+instance int :: ordered
+  "k <<= l == k <= l"
+  by default (simp_all add: ordered_int_def)
+
+instance unit :: ordered
+  "u <<= v == True"
+  by default (simp_all add:  ordered_unit_def)
+
+consts
+  le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
+
+function
+  "le_option' None y = True"
+  "le_option' (Some x) None = False"
+  "le_option' (Some x) (Some y) = x <<= y"
+  by pat_completeness simp_all
+termination by (auto_term "{}")
+
+instance (ordered) option :: ordered
+  "x <<= y == le_option' x y"
+proof (default, unfold ordered_option_def)
+  fix x
+  show "le_option' x x" by (cases x) simp_all
+next
+  fix x y z
+  assume "le_option' x y" "le_option' y z"
+  then show "le_option' x z"
+    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
+    (erule order_trans, assumption)
+next
+  fix x y
+  assume "le_option' x y" "le_option' y x"
+  then show "x = y"
+    by (cases x, simp_all, cases y, simp_all, cases y, simp_all)
+    (erule order_antisym, assumption)
+qed
+
+lemma [simp, code]:
+  "None <<= y = True"
+  "Some x <<= None = False"
+  "Some v <<= Some w = v <<= w"
+  unfolding ordered_option_def le_option'.simps by rule+
+
+consts
+  le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+
+function
+  "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
+  by pat_completeness simp_all
+termination by (auto_term "{}")
+
+instance (ordered, ordered) * :: ordered
+  "x <<= y == le_pair' x y"
+apply (default, unfold "ordered_*_def", unfold split_paired_all)
+apply simp_all
+apply (auto intro: lt_trans order_trans)[1]
+unfolding lt_def apply (auto intro: order_antisym)[1]
+done
+
+lemma [simp, code]:
+  "(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
+  unfolding "ordered_*_def" le_pair'.simps ..
+
+(* consts
+  le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
+
+function
+  "le_list' [] ys = True"
+  "le_list' (x#xs) [] = False"
+  "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
+    by pat_completeness simp_all
+termination by (auto_term "measure (length o fst)")
+
+instance (ordered) list :: ordered
+  "xs <<= ys == le_list' xs ys"
+proof (default, unfold "ordered_list_def")
+  fix xs
+  show "le_list' xs xs" by (induct xs) simp_all
+next
+  fix xs ys zs
+  assume "le_list' xs ys" and "le_list' ys zs"
+  then show "le_list' xs zs"
+  apply (induct xs zs rule: le_list'.induct)
+  apply simp_all
+  apply (cases ys) apply simp_all
+  
+  apply (induct ys) apply simp_all
+  apply (induct ys)
+  apply simp_all
+  apply (induct zs)
+  apply simp_all
+next
+  fix xs ys
+  assume "le_list' xs ys" and "le_list' ys xs"
+  show "xs = ys" sorry
+qed
+
+lemma [simp, code]:
+  "[] <<= ys = True"
+  "(x#xs) <<= [] = False"
+  "(x#xs) <<= (y#ys) = (x << y \<or> x = y \<and> xs <<= ys)"
+  unfolding "ordered_list_def" le_list'.simps by rule+*)
+
+class infimum = ordered +
+  fixes inf
+  assumes inf: "inf \<^loc><<= x"
+
+lemma (in infimum)
+  assumes prem: "a \<^loc><<= inf"
+  shows no_smaller: "a = inf"
+using prem inf by (rule order_antisym)
+
+consts
+  abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
+
+ML {* set quick_and_dirty *}
+function
+  "abs_max_of cmp inff [] = inff"
+  "abs_max_of cmp inff [x] = x"
+  "abs_max_of cmp inff (x#xs) =
+     ordered.max cmp x (abs_max_of cmp inff xs)"
+apply pat_completeness sorry
+
+abbreviation (in infimum)
+  "max_of xs \<equiv> abs_max_of le inf"
+
+abbreviation
+  "max_of xs \<equiv> abs_max_of le inf"
+
+instance bool :: infimum
+  "inf == False"
+  by default (simp add: infimum_bool_def)
+
+instance nat :: infimum
+  "inf == 0"
+  by default (simp add: infimum_nat_def)
+
+instance unit :: infimum
+  "inf == ()"
+  by default (simp add: infimum_unit_def)
+
+instance (ordered) option :: infimum
+  "inf == None"
+  by default (simp add: infimum_option_def)
+
+instance (infimum, infimum) * :: infimum
+  "inf == (inf, inf)"
+  by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf)
+
+class enum = ordered +
+  fixes enum :: "'a list"
+  assumes member_enum: "x \<in> set enum"
+  and ordered_enum: "abs_sorted le enum"
+
+(*
+FIXME:
+- abbreviations must be propagated before locale introduction
+- then also now shadowing may occur
+*)
+(*abbreviation (in enum)
+  "local.sorted \<equiv> abs_sorted le"*)
+
+instance bool :: enum
+  (* FIXME: better name handling of definitions *)
+  "_1": "enum == [False, True]"
+  by default (simp_all add: enum_bool_def)
+
+instance unit :: enum
+  "_2": "enum == [()]"
+  by default (simp_all add: enum_unit_def)
+
+(*consts
+  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
+
+primrec
+  "product [] ys = []"
+  "product (x#xs) ys = map (Pair x) ys @ product xs ys"
+
+lemma product_all:
+  assumes "x \<in> set xs" "y \<in> set ys"
+  shows "(x, y) \<in> set (product xs ys)"
+using prems proof (induct xs)
+  case Nil
+  then have False by auto
+  then show ?case ..
+next
+  case (Cons z xs)
+  then show ?case
+  proof (cases "x = z")
+    case True
+    with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
+    with True show ?thesis by simp
+  next
+    case False
+    with Cons have "x \<in> set xs" by auto
+    with Cons have "(x, y) \<in> set (product xs ys)" by auto
+    then show "(x, y) \<in> set (product (z#xs) ys)" by auto
+  qed
+qed
+
+lemma product_sorted:
+  assumes "sorted xs" "sorted ys"
+  shows "sorted (product xs ys)"
+using prems proof (induct xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  from Cons ordered.sorted_weakening have "sorted xs" by auto
+  with Cons have "sorted (product xs ys)" by auto
+  then show ?case apply simp
+  proof -
+    assume 
+apply simp
+  
+  proof (cases "x = z")
+    case True
+    with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
+    with True show ?thesis by simp
+  next
+    case False
+    with Cons have "x \<in> set xs" by auto
+    with Cons have "(x, y) \<in> set (product xs ys)" by auto
+    then show "(x, y) \<in> set (product (z#xs) ys)" by auto
+  qed
+qed
+
+instance (enum, enum) * :: enum
+  "_3": "enum == product enum enum"
+apply default
+apply (simp_all add: "enum_*_def")
+apply (unfold split_paired_all)
+apply (rule product_all)
+apply (rule member_enum)+
+sorry*)
+
+instance (enum) option :: enum
+  "_4": "enum == None # map Some enum"
+proof (default, unfold enum_option_def)
+  fix x :: "'a::enum option"
+  show "x \<in> set (None # map Some enum)"
+  proof (cases x)
+    case None then show ?thesis by auto
+  next
+    case (Some x) then show ?thesis by (auto intro: member_enum)
+  qed
+next
+  show "sorted (None # map Some (enum :: ('a::enum) list))"
+  sorry
+  (*proof (cases "enum :: 'a list")
+    case Nil then show ?thesis by simp
+  next
+   case (Cons x xs)
+   then have "sorted (None # map Some (x # xs))" sorry
+   then show ?thesis apply simp
+  apply simp_all
+  apply auto*)
+qed
+
+ML {* reset quick_and_dirty *}
+
+consts
+  get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option"
+
+primrec
+  "get_first p [] = None"
+  "get_first p (x#xs) = (if p x then Some x else get_first p xs)"
+
+consts
+  get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option"
+
+primrec
+  "get_index p n [] = None"
+  "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)"
+
+definition
+  between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option"
+  "between x y = get_first (\<lambda>z. x << z & z << y) enum"
+
+definition
+  index :: "'a::enum \<Rightarrow> nat"
+  "index x = the (get_index (\<lambda>y. y = x) 0 enum)"
+
+definition
+  add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a"
+  "add x y =
+    (let
+      enm = enum
+    in enm ! ((index x + index y) mod length enm))"
+
+consts
+  sum :: "'a::{enum, infimum} list \<Rightarrow> 'a"
+
+primrec
+  "sum [] = inf"
+  "sum (x#xs) = add x (sum xs)"
+
+definition
+  "test1 = sum [None, Some True, None, Some False]"
+  "test2 = (inf :: nat \<times> unit)"
+
+code_generate eq
+code_generate "op <<="
+code_generate "op <<"
+code_generate inf
+code_generate between
+code_generate index
+code_generate sum
+code_generate test1
+code_generate test2
+
+code_serialize ml (-)
+
+end
\ No newline at end of file
diff -r d2a30fed7596 -r 0af8655ab0bb src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Aug 30 08:30:09 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Aug 30 08:34:45 2006 +0200
@@ -7,6 +7,7 @@
 no_document time_use_thy "Classpackage";
 no_document time_use_thy "Codegenerator";
 no_document time_use_thy "CodeOperationalEquality";
+no_document time_use_thy "CodeCollections";
 no_document time_use_thy "CodeEval";
 no_document time_use_thy "CodeRandom";