theory Termin9 imports Main "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/Code_Target_Numeral"
begin
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
typedef slist = "{xs. sorted xs}" morphisms list_of as_sorted
by (rule exI[where x = "[]"]) simp
setup_lifting type_definition_slist
lift_definition Singleton :: "nat \ slist" is "\x. [x]" by simp
lift_definition set_of :: "slist \ nat set" is set.
lift_definition take :: "nat \ slist \ slist" is List.take by (rule sorted_takeI)
lift_definition smerge :: "slist \ slist \ slist" is merge by (rule sorted_merge_sorted)
lift_definition sorted_list :: "nat list \ slist" is msort by (rule sorted_msort)
lemma set_of_Singleton: "set_of (Singleton x) = {x}"
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 transfer simp
section \Code generator\
definition rev_append :: "'a list \ 'a list \ 'a list"
where "rev_append xs ys = ys @ xs"
export_code rev_append in Haskell
term the
export_code the in Haskell
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
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 (rule notI, induction "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)
export_code collatz in Haskell
lemma "collatz 1000000000123" by eval
export_code insert hd take list_of set_of sorted_list in Haskell
inductive rtc :: "('a \ 'a \ bool) \ 'a \ 'a \ bool"
for r :: "'a \ 'a \ bool"
where refl: "rtc r x x"
| trans: "r x y \ rtc r y z \ rtc r x z"
coinductive cortc :: "('a \ 'a \ bool) \ 'a \ 'a \ bool"
for r :: "'a \ 'a \ bool"
where refl: "cortc r x x"
| trans: "r x y \ cortc r y z \ cortc r x z"
thm rtc.induct cortc.coinduct
datatype a = A | B | C | D
fun r :: "a \ a \ bool"
where "r A B = True"
| "r B D = True"
| "r C C = True"
| "r x y = False"
lemma "cortc r C A"
apply (coinduct rule: cortc.coinduct [where X="\x y. x=C \ y=A"])
apply simp
thm cortc.coinduct
apply simp
apply (rule exI[where x=C])
apply simp
done
lemma "\ cortc r D A"
apply (rule notI)
apply (erule cortc.cases)
apply simp
thm r.simps
apply simp
done
end