theory Termin9 imports Main "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/Efficient_Nat" begin section {* Code generation *} definition rev_append :: "'a list \ 'a list \ 'a list" where "rev_append xs ys = ys @ xs" export_code rev_append in Haskell file - thm the.simps export_code the in Haskell file - datatype 'a my_type = K1 'a | K2 "'a list" fun dummy :: "'a my_type \ 'a my_type" where "dummy (K1 a) = K2 [a]" | "dummy k2 = k2" export_code dummy in Haskell file - (*fun collatz :: "nat \ bool" where "collatz 0 = False" | "collatz (Suc 0) = True" | "collatz n = (if (n mod 2 = 0) then collatz (n div 2) else collatz (3 * n + 1))" *) inductive collatz :: "nat \ bool" where "collatz 1" | "\ n mod 2 = 0; collatz (n div 2) \ \ collatz n" | "\ n mod 2 = 1; collatz (3 * n + 1) \ \ collatz n" declare One_nat_def [simp del] lemma collatz_0: "\ collatz 0" by (induct "0::nat" rule: collatz.induct) auto lemma collatz_greater_zero [elim]: assumes "collatz n" obtains "n > 0" using assms by (metis collatz_0 neq0_conv) lemma collatz_code [code]: "collatz n \ n \ 0 \ (n \ 1 \ (if (n mod 2 = 0) then collatz (n div 2) else collatz (3 * n + 1)))" by (auto elim: collatz.cases intro: collatz.intros) value [code] "collatz 1000000000000000123" export_code collatz in Haskell file - section {* Merge-Sort (Blatt 4) *} hide_const sorted sort fun le :: "nat \ nat list \ bool" where "le n [] = True" | "le n (x#xs) = (n \ x \ le n xs)" fun sorted :: "nat list \ bool" where "sorted [] = True" | "sorted (x#xs) = (le x xs \ sorted xs)" fun merge :: "nat list \ nat list \ nat list" where "merge xs [] = xs" | "merge [] ys = ys" | "merge (x#xs) (y#ys) = (if (x \ y) then x#(merge xs (y#ys)) else y#(merge (x#xs) ys))" fun msort :: "nat list \ nat list" where "msort [] = []" | "msort [x] = [x]" | "msort xs = (let n = (length xs) div 2 in (merge (msort (take n xs)) (msort (drop n xs)) ))" lemma le_le: "\ le x xs; x' \ x \ \ le x' xs" by (induct xs) auto lemma le_merge: "\ le x xs; le x ys \ \ le x (merge xs ys)" by (induct xs ys rule:merge.induct) auto lemma sorted_merge_sorted: "\ sorted xs; sorted ys \ \ sorted(merge xs ys)" by(induct xs ys rule: merge.induct)(auto intro: le_merge simp add: le_le) theorem sorted_msort: "sorted (msort xs)" by (induct xs rule:msort.induct)(auto intro: sorted_merge_sorted) text {* Diese Lemmas sind neu. *} lemma le_takeI [intro]: "le x xs \ le x (take n xs)" proof (induction n arbitrary: xs) case (Suc n xs) thus ?case by (cases xs) auto qed simp lemma sorted_takeI [intro]: "sorted xs \ sorted (take n xs)" proof (induction n arbitrary: xs) case (Suc n xs) thus ?case by (cases xs) auto qed simp lemma set_merge [simp]: "set (merge xs ys) = set xs \ set ys" by (induction xs ys rule: merge.induct) auto section {* Lifting und Transfer *} typedef slist = "{xs. sorted xs}" morphisms list_of as_sorted by (rule_tac x="[]" in exI) simp setup_lifting type_definition_slist lift_definition Singleton :: "nat \ slist" is "\x. [x]" by simp lift_definition hd :: "slist \ nat" is "List.hd" .. lift_definition take :: "nat \ slist \ slist" is "List.take" .. lift_definition smerge :: "slist \ slist \ slist" is "merge" by (rule sorted_merge_sorted) lift_definition set_of :: "slist \ nat set" is "List.set" .. lift_definition sorted_list :: "nat list \ slist" is msort by (rule sorted_msort) lemma set_of_Singleton [simp]: "set_of (Singleton x) = {x}" by transfer simp lemma set_of_smerge [simp]: "set_of (smerge xs ys) = set_of xs \ set_of ys" by transfer simp lemma "list_of xs = a#b#ys \ a \ b" by transfer simp definition insert :: "nat \ slist \ slist" where "insert x xs = smerge xs (Singleton x)" lemma set_of_insert [simp]: "x \ set_of (insert x xs)" unfolding insert_def by simp export_code insert hd take list_of set_of in Haskell file "-" section {* Data refinement *} datatype ('a,'b) my_map = Map "'a \ 'b" definition MyMap :: "('a \ 'b) \ ('a, 'b) my_map" where "MyMap m = Map m" code_datatype MyMap fun lookup :: "('a,'b) my_map \ 'a \ 'b option" where "lookup (Map m) k = m k" lemma lookup_code [code]: "lookup (MyMap m) k = m k" unfolding MyMap_def by simp export_code lookup in Haskell file - end