# Theory Example_Misc

theory Example_Misc
imports Main
```section ‹Examples›

subsection ‹Misc›

theory Example_Misc
imports Main
begin

paragraph ‹Lists›

fun min_list :: "'a::ord list ⇒ 'a" where
"min_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ min x (min_list xs))"

lemma fold_min_commute:
"fold min xs (min a b) = min a (fold min xs b)" for a :: "'a :: linorder"
by (induction xs arbitrary: a; auto; metis min.commute min.assoc)

lemma min_list_fold:
"min_list (x # xs) = fold min xs x" for x :: "'a :: linorder"
by (induction xs arbitrary: x; auto simp: fold_min_commute[symmetric]; metis min.commute)

(* FIXME mv List *)
lemma induct_list012:
"⟦P []; ⋀x. P [x]; ⋀x y zs. P (y # zs) ⟹ P (x # y # zs)⟧ ⟹ P xs"
by induction_schema (pat_completeness, lexicographic_order)

lemma min_list_Min: "xs ≠ [] ⟹ min_list xs = Min (set xs)"
by (induction xs rule: induct_list012)(auto)

(*
paragraph ‹Code Setup›

definition map1⇩T' where
"map1⇩T' f xs ≡ ⟨rec_list ⟨[]⟩ (λx xs a. ⟨λy. ⟨λys. ⟨y#ys⟩⟩⟩ . (f x) . a)⟩ . ⟨xs⟩ "

lemma map1⇩T_map1⇩T':
"map1⇩T = ⟨λf. ⟨λxs. map1⇩T' f xs⟩⟩"
unfolding map1⇩T_def map1⇩T'_def ..

lemmas [code] =
mem_defs.checkmem'_def

lemmas [code_unfold] =
map⇩T_def
map1⇩T_map1⇩T'

lemma app_return_right:
"f . ⟨g⟩ = do {f ← f; f g}"
unfolding fun_app_lifted_def left_identity ..

lemma app_return_left:
"⟨f⟩ . g = g ⤜ f"
unfolding fun_app_lifted_def left_identity ..

lemma get_return:
"(do {m ← get; ⟨f m⟩}) = State (λ mem. (f mem, mem))"
unfolding get_def bind_def return_def by simp

lemma get_put:
"do {m ← get; put (f m)} = State (λ mem. ((), f mem))"
unfolding get_def put_def bind_def return_def by simp

lemma bind_return_assoc:
"(do {
x ← a;
⟨f x⟩
}) ⤜
b =
do {
x ← a;
b (f x)
}"
by (auto split: prod.split simp add: bind_def return_def)

lemma app_lifted_return_assoc:
"(do {
x ← a;
⟨f x⟩
}) .
b =
do {
x ← a;
b ⤜ f x
}"
unfolding fun_app_lifted_def bind_return_assoc ..

(* There could be a simpproc for this pattern *)
lemma bind_return_assoc2:
"(do {
x ← a;
y ← b;
⟨f x y⟩
}) ⤜
c =
do {
x ← a;
y ← b;
c (f x y)
}"
by (auto split: prod.split simp add: bind_def return_def)

lemma bind_return_assoc3:
"(do {
x ← a;
y ← b;
z ← c;
⟨f x y z⟩
}) ⤜
d =
do {
x ← a;
y ← b;
z ← c;
d (f x y z)
}"
by (auto split: prod.split simp add: bind_def return_def)

lemma if⇩T_return:
"if⇩T ⟨b⟩ x⇩T y⇩T ≡ if b then x⇩T else y⇩T"
unfolding if⇩T_def return_def bind_def by simp

(* Would it be a good idea to just unfold fun_app_lifted? *)