Theory Example_Misc

section ‹Examples›

subsection ‹Misc›

theory Example_Misc
  imports
    Main
    "HOL-Library.Extended"
    "../state_monad/State_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 ‹Extended Data Type›

(* TODO: Move to distribution! *)
lemma Pinf_add_right[simp]:
  "∞ + x = ∞"
  by (cases x; simp)

paragraph ‹Syntax›

bundle app_syntax begin

notation App (infixl ‹$› 999)
notation Wrap (‹⟪_⟫›)

end

(*
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'


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 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? *)
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
  map1⇩T_map1⇩T'
  if⇩T_return
*)
end