theory Termin9 imports Main "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/Efficient_Nat"
begin

section {* Code generation *}

definition rev_append :: "'a list \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a my_type"
where "dummy (K1 a) = K2 [a]"
| "dummy k2 = k2"

export_code dummy in Haskell file -


(*fun collatz :: "nat \<Rightarrow> 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 \<Rightarrow> bool"
where "collatz 1"
  | "\<lbrakk> n mod 2 = 0; collatz (n div 2) \<rbrakk> \<Longrightarrow> collatz n"
  | "\<lbrakk> n mod 2 = 1; collatz (3 * n + 1) \<rbrakk> \<Longrightarrow> collatz n"

declare One_nat_def [simp del]

lemma collatz_0: "\<not> 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 \<longleftrightarrow>
    n \<noteq> 0 \<and> (n \<noteq> 1 \<longrightarrow> (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 \<Rightarrow> nat list \<Rightarrow> bool"
  where "le n []     = True"
  | "le n (x#xs) = (n \<le> x \<and> le n xs)"

fun sorted :: "nat list \<Rightarrow> bool"
  where "sorted []     = True"
  | "sorted (x#xs) = (le x xs \<and> sorted xs)"

fun merge :: "nat list \<Rightarrow> nat list \<Rightarrow> nat list"
where
  "merge xs []         = xs"
| "merge [] ys         = ys"
| "merge (x#xs) (y#ys) = 
    (if (x \<le> y) then x#(merge xs (y#ys)) else y#(merge (x#xs) ys))"

fun msort :: "nat list \<Rightarrow> 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:
  "\<lbrakk> le x xs;  x' \<le> x \<rbrakk> \<Longrightarrow> le x' xs"
by (induct xs) auto

lemma le_merge:
  "\<lbrakk> le x xs; le x ys \<rbrakk> \<Longrightarrow> le x (merge xs ys)"
by (induct xs ys rule:merge.induct) auto

lemma sorted_merge_sorted:
  "\<lbrakk> sorted xs; sorted ys \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<union> 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 \<Rightarrow> slist" is "\<lambda>x. [x]" by simp
lift_definition hd :: "slist \<Rightarrow> nat" is "List.hd" ..
lift_definition take :: "nat \<Rightarrow> slist \<Rightarrow> slist" is "List.take" ..
lift_definition smerge :: "slist \<Rightarrow> slist \<Rightarrow> slist" is "merge" by (rule sorted_merge_sorted)
lift_definition set_of :: "slist \<Rightarrow> nat set" is "List.set" ..
lift_definition sorted_list :: "nat list \<Rightarrow> 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 \<union> set_of ys"
  by transfer simp

lemma "list_of xs = a#b#ys \<Longrightarrow> a \<le> b"
  by transfer simp

definition insert :: "nat \<Rightarrow> slist \<Rightarrow> slist"
  where "insert x xs = smerge xs (Singleton x)"

lemma set_of_insert [simp]: "x \<in> 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 \<rightharpoonup> 'b"

definition MyMap :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a, 'b) my_map"
  where "MyMap m = Map m"

code_datatype MyMap

fun lookup :: "('a,'b) my_map \<Rightarrow> 'a \<Rightarrow> '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