# HG changeset patch
# User haftmann
# Date 1164187220 -3600
# Node ID cda5cd8bfd1644c2c4fd0050764b16e1ab4ca992
# Parent  20c2ddee8bc58fee5ef7fb08962a83470d60d02b
example tuned

diff -r 20c2ddee8bc5 -r cda5cd8bfd16 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Wed Nov 22 10:20:19 2006 +0100
+++ b/src/HOL/ex/Classpackage.thy	Wed Nov 22 10:20:20 2006 +0100
@@ -320,10 +320,7 @@
 definition "y2 = Y (1::int) 2 3"
 
 code_gen "op \<otimes>" \<one> inv
-code_gen X Y (SML) (Haskell)
-code_gen x1 x2 y2 (SML) (Haskell)
-
-code_gen (SML *)
-code_gen (Haskell -)
+code_gen X Y (SML *) (Haskell -)
+code_gen x1 x2 y2 (SML *) (Haskell -)
 
 end
diff -r 20c2ddee8bc5 -r cda5cd8bfd16 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Wed Nov 22 10:20:19 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Wed Nov 22 10:20:20 2006 +0100
@@ -1,127 +1,53 @@
-(*  ID:         $Id$
+ (*  ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Collection classes as examples for code generation *}
 
 theory CodeCollections
-imports Main
+imports Main Product_ord List_lexord
 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
+fun
+  abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "abs_sorted cmp [] \<longleftrightarrow> True"
+  "abs_sorted cmp [x] \<longleftrightarrow> True"
+  "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"
 
-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" where
-  "min x y = (if x \<^loc><<= y then x else y)"
-
-definition (in ordered)
-  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "max x y = (if x \<^loc><<= y then y else x)"
-
-definition
-  min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "min x y = (if x <<= y then x else y)"
-
-definition
-  max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "max x y = (if x <<= y then y else x)"
-
-fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-where
-  "abs_sorted cmp [] = True"
-| "abs_sorted cmp [x] = True"
-| "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
-
-thm abs_sorted.simps
-
-abbreviation (in ordered)
-  "sorted \<equiv> abs_sorted le"
+abbreviation (in ord)
+  "sorted \<equiv> abs_sorted less_eq"
 
 abbreviation
-  "sorted \<equiv> abs_sorted le"
+  "sorted \<equiv> abs_sorted less_eq"
 
-lemma (in ordered) sorted_weakening:
+lemma (in partial_order) 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)" .
+  from this have "sorted (x # x' # xs)" by auto
   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 :: order
+  "u \<le> v \<equiv> True"
+  "u < v \<equiv> False"
+  by default (simp_all add: order_unit_def)
 
-instance unit :: ordered
-  "u <<= v == True"
-  by default (simp_all add:  ordered_unit_def)
-
+fun le_option' :: "'a\<Colon>order option \<Rightarrow> 'a option \<Rightarrow> bool"
+  where "le_option' None y \<longleftrightarrow> True"
+  | "le_option' (Some x) None \<longleftrightarrow> False"
+  | "le_option' (Some x) (Some y) \<longleftrightarrow> x \<le> y"
 
-fun le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
-where
-  "le_option' None y = True"
-| "le_option' (Some x) None = False"
-| "le_option' (Some x) (Some y) = x <<= y"
-
-instance option :: (ordered) ordered
-  "x <<= y == le_option' x y"
-proof (default, unfold ordered_option_def)
+instance option :: (order) order
+  "x \<le> y \<equiv> le_option' x y"
+  "x < y \<equiv> x \<le> y \<and> x \<noteq> y"
+proof (default, unfold order_option_def)
   fix x
   show "le_option' x x" by (cases x) simp_all
 next
@@ -129,146 +55,61 @@
   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+
-
-fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-where
-  "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
-
-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 ..
-
-(*   
-
-fun le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
-where
-  "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)"
-
-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
+  fix x y
+  show "le_option' x y \<and> x \<noteq> y \<longleftrightarrow> le_option' x y \<and> x \<noteq> y" ..
 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+*)
+  "None \<le> y \<longleftrightarrow> True"
+  "Some x \<le> None \<longleftrightarrow> False"
+  "Some v \<le> Some w \<longleftrightarrow> v \<le> w"
+  unfolding order_option_def le_option'.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)
-
+lemma forall_all [simp]:
+  "list_all P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
+  by (induct xs) auto
 
-ML {* set quick_and_dirty *}
-function abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
-where
-  "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
+lemma exists_ex [simp]:
+  "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
+  by (induct xs) auto
 
-abbreviation (in infimum)
-  "max_of xs \<equiv> abs_max_of le inf"
-
-abbreviation
-  "max_of xs \<equiv> abs_max_of le inf"
+class fin =
+  fixes fin :: "'a list"
+  assumes member_fin: "x \<in> set fin"
+begin
 
-instance bool :: infimum
-  "inf == False"
-  by default (simp add: infimum_bool_def)
-
-instance nat :: infimum
-  "inf == 0"
-  by default (simp add: infimum_nat_def)
+lemma set_enum_UNIV:
+  "set fin = UNIV"
+  using member_fin by auto
 
-instance unit :: infimum
-  "inf == ()"
-  by default (simp add: infimum_unit_def)
-
-instance option :: (ordered) infimum
-  "inf == None"
-  by default (simp add: infimum_option_def)
+lemma all_forall [code func, code inline]:
+  "(\<forall>x. P x) \<longleftrightarrow> list_all P fin"
+  using set_enum_UNIV by simp_all
 
-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"
+lemma ex_exists [code func, code inline]:
+  "(\<exists>x. P x) \<longleftrightarrow> list_ex P fin"
+  using set_enum_UNIV by simp_all
 
-(*
-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
+end
+  
+instance bool :: fin
   (* FIXME: better name handling of definitions *)
-  "_1": "enum == [False, True]"
-  by default (simp_all add: enum_bool_def)
+  "_1": "fin == [False, True]"
+  by default (simp_all add: fin_bool_def)
 
-instance unit :: enum
-  "_2": "enum == [()]"
-  by default (simp_all add: enum_unit_def)
+instance unit :: fin
+  "_2": "fin == [()]"
+  by default (simp_all add: fin_unit_def)
 
-(*consts
+fun
   product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
-
-primrec
+  where
   "product [] ys = []"
   "product (x#xs) ys = map (Pair x) ys @ product xs ys"
 
@@ -294,67 +135,27 @@
   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"
+instance * :: (fin, fin) fin
+  "_3": "fin == product fin fin"
 apply default
-apply (simp_all add: "enum_*_def")
+apply (simp_all add: "fin_*_def")
 apply (unfold split_paired_all)
 apply (rule product_all)
-apply (rule member_enum)+
-sorry*)
+apply (rule member_fin)+
+done
 
-instance option :: (enum) 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)"
+instance option :: (fin) fin
+  "_4": "fin == None # map Some fin"
+proof (default, unfold fin_option_def)
+  fix x :: "'a::fin option"
+  show "x \<in> set (None # map Some fin)"
   proof (cases x)
     case None then show ?thesis by auto
   next
-    case (Some x) then show ?thesis by (auto intro: member_enum)
+    case (Some x) then show ?thesis by (auto intro: member_fin)
   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"
 
@@ -369,7 +170,7 @@
   "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
+(*definition
   between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where
   "between x y = get_first (\<lambda>z. x << z & z << y) enum"
 
@@ -389,18 +190,13 @@
 
 primrec
   "sum [] = inf"
-  "sum (x#xs) = add x (sum xs)"
-
-definition "test1 = sum [None, Some True, None, Some False]"
-definition "test2 = (inf :: nat \<times> unit)"
+  "sum (x#xs) = add x (sum xs)"*)
 
-code_gen "op <<="
-code_gen "op <<"
-code_gen inf
-code_gen between
-code_gen index
-code_gen test1
-code_gen test2
+(*definition "test1 = sum [None, Some True, None, Some False]"*)
+(*definition "test2 = (inf :: nat \<times> unit)"*)
+definition "test3 \<longleftrightarrow> (\<exists>x \<Colon> bool option. case x of Some P \<Rightarrow> P | None \<Rightarrow> False)"
+
+code_gen test3
 
 code_gen (SML *)
 code_gen (Haskell -)
diff -r 20c2ddee8bc5 -r cda5cd8bfd16 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Wed Nov 22 10:20:19 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Wed Nov 22 10:20:20 2006 +0100
@@ -179,16 +179,16 @@
   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   (SML) (Haskell)
 code_gen
-  "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
-  "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
-  "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
-  "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
-  "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
-  "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
-  "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
-  "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
-  "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
+  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
+  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
+  "op = :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
+  "op = :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+  "op = :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
+  "op = :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
+  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
+  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
+  "op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
 
 code_gen (SML *) (Haskell -)
 
diff -r 20c2ddee8bc5 -r cda5cd8bfd16 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Wed Nov 22 10:20:19 2006 +0100
+++ b/src/HOL/ex/NormalForm.thy	Wed Nov 22 10:20:20 2006 +0100
@@ -66,11 +66,11 @@
 
 lemma "[] @ [] = []" by normalization
 lemma "[] @ xs = xs" by normalization
-lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
-lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
+normal_form "[a, b, c] @ xs = a # b # c # xs"
+normal_form "map f [x,y,z::'x] = [f x, f y, f z]"
 normal_form "map (%f. f True) [id, g, Not] = [True, g True, False]"
 normal_form "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
-lemma "rev [a, b, c] = [c, b, a]" by normalization
+normal_form "rev [a, b, c] = [c, b, a]"
 normal_form "rev (a#b#cs) = rev cs @ [b, a]"
 normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
 normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
@@ -85,8 +85,8 @@
 normal_form "filter (%x. x) ([True,False,x]@xs)"
 normal_form "filter Not ([True,False,x]@xs)"
 
-lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]" by normalization
-lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
+normal_form "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]"
+normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]"
 normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
 
 lemma "last [a, b, c] = c"
@@ -108,7 +108,7 @@
 normal_form "min 0 (x::nat)"
 lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
 
-lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
+normal_form "nat 4 = Suc (Suc (Suc (Suc 0)))"
 
 normal_form "Suc 0 \<in> set ms"