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 map1T' where
  "map1T' f xs ≡ ⟨rec_list ⟨[]⟩ (λx xs a. ⟨λy. ⟨λys. ⟨y#ys⟩⟩⟩ . (f x) . a)⟩ . ⟨xs⟩ "

lemma map1T_map1T':
  "map1T = ⟨λf. ⟨λxs. map1T' f xs⟩⟩"
  unfolding map1T_def map1T'_def ..

lemmas [code] =
  mem_defs.checkmem'_def

lemmas [code_unfold] =
  mapT_def
  map1T_map1T'


paragraph ‹Simplifying monad expressions›

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 ifT_return:
  "ifT ⟨b⟩ xT yT ≡ if b then xT else yT"
  unfolding ifT_def return_def bind_def by simp

(* Would it be a good idea to just unfold fun_app_lifted? *)
lemmas monad_unfolds =
  app_return_right app_return_left Monad.left_identity Monad.right_identity
  app_lifted_return_assoc bind_return_assoc bind_return_assoc2 bind_return_assoc3
  get_return get_put
  map1T_map1T'
  ifT_return
*)
end