Theory ExecutableHelper

theory ExecutableHelper
imports Main BeispielTac "HOL-Library.Code_Target_Numeral"
begin

(*is this helpful?*)
term ‹sorted_list_of_set›


section‹Executable Helper›
text‹This is a helper library (and should be excluded from the theory document).›

(*TODO: is there a library function for this?*)
fun the_default :: ‹'a option ⇒ 'a ⇒ 'a› where
  ‹the_default None def = def›
| ‹the_default (Some a) _ = a›



lemma set_of_constructor:
  ‹bij Constr ⟹ (⋀x. deconstruct x = (inv Constr) x) ⟹ {p. Constr p ∈ ps} = deconstruct ` ps›
  apply(simp)
  apply(simp add: vimage_def[symmetric])
  apply(simp add: bij_vimage_eq_inv_image)
  done


(*TODO: why isnt this a library function?*)
definition map_map :: ‹('a ⇒ 'b) ⇒ ('k ⇀ 'a) ⇒ ('k ⇀ 'b)› where
  ‹map_map f m k ≡ case m k of None ⇒ None | Some a ⇒ Some (f a)›

term ‹map_fun id ∘ map_option›

lemma map_map: ‹map_map f m = map_comp (λa. Some (f a)) m›
  by(simp add: fun_eq_iff map_map_def map_comp_def)

(*does this help printing?*)
lemma map_map_map_if_propagate:
  ‹map_map f (λk. if P k then Some y else X k) = (λk. if P k then Some (f y) else map_map f X k)›
  apply(simp add: fun_eq_iff, intro allI conjI)
   apply(simp add: map_map_def)+
  done


text‹Isabelle does not allow printing functions, but it allows printing lists›
definition show_map :: ‹('a::enum ⇀ 'b) ⇒ ('a × 'b) list› where
  ‹show_map m ≡ List.map_filter (λp. map_option (λi. (p, i)) (m p)) (enum_class.enum)›

beispiel ‹show_map [True ↦ (8::int), False ↦ 12] = [(False, 12), (True, 8)]› by eval

lemma List_map_filter_map_some_cons: ‹m x = Some y ⟹
  (List.map_filter (λp. map_option (Pair p) (m p)) (x # xs)) =
       (x,y) # (List.map_filter (λp. map_option (Pair p) (m p)) (xs))›
  apply(simp add: List.map_filter_def)
  done


lemma List_map_filter_map_of_eq_helper: ‹x ∉ set xs
  ⟹  map_of (List.map_filter (λp. map_option (Pair p) ((m(x := None)) p)) xs)
        = (map_of (List.map_filter (λp. map_option (Pair p) (m p)) xs))›
  apply(simp add: map_filter_def)
  apply(rule arg_cong)
  apply(simp)
  apply(subgoal_tac ‹(filter (λxa. xa ≠ x ∧ (xa ≠ x ⟶ (∃y. m xa = Some y))) xs) =
        (filter (λx. ∃y. m x = Some y) xs)›)
   prefer 2
   apply (rule filter_cong)
    apply(simp; fail)
   apply blast
  apply(simp)
  done

lemma show_map_induction_helper:
  ‹distinct xs ⟹ dom m ⊆ set xs ⟹
    map_of (List.map_filter (λp. map_option (Pair p) (m p)) xs) = m›
proof(induction ‹xs› arbitrary: ‹m›)
  case Nil
  then show ‹?case› by(simp add: map_filter_def)
next
  case (Cons x xs)
  then show ‹?case›
  proof(cases ‹∃y. m x = Some y›)
    case True
    from True obtain y where ‹m x = Some y› by blast
    let ‹?m'›=‹m(x:=None)›
    have m: ‹m = ?m'(x ↦ y)› using ‹m x = Some y› by auto
    have ‹x ∉ set xs› using Cons.prems(1) by auto
    have ‹dom ?m' ⊆ set xs› using Cons.prems by auto
    with Cons.IH[of ‹?m'›] have IH':
      ‹map_of (List.map_filter (λp. map_option (Pair p) (?m' p)) xs) = ?m'›
      using Cons.prems(1) by fastforce
    with List_map_filter_map_of_eq_helper[OF ‹x ∉ set xs›, of ‹m›] have IH'':
      ‹map_of (List.map_filter (λp. map_option (Pair p) (m p)) xs) = ?m'›
      by simp
    from ‹m x = Some y› have 1:
      ‹List.map_filter (λp. map_option (Pair p) (m p)) (x # xs) =
        (x, y) # List.map_filter (λp. map_option (Pair p) (m p)) xs›
      using List_map_filter_map_some_cons[of ‹m› ‹x› ‹y› ‹xs›] by simp
    show ‹?thesis›
      apply(subst 1)
      apply(simp)
      apply(subst IH'')
      using m by auto
  next
    case False
    with Cons show ‹?thesis›
      apply(simp add: map_filter_def)
      apply (meson domIff subset_insert)
      done
  qed
qed


lemma map_of_show_map:
  fixes m::‹'a::enum ⇒ 'b option›
  shows ‹map_of (show_map m) = m›
  apply(simp add: show_map_def)
  apply(rule show_map_induction_helper)
  using enum_distinct apply simp
  by(simp add: UNIV_enum[symmetric])


definition show_fun :: ‹('a::enum ⇒ 'b) ⇒ ('a × 'b) list› where
  ‹show_fun f ≡ map (λp. (p, f p)) (enum_class.enum)›


definition show_num_fun :: ‹('a::enum ⇒ 'b::zero) ⇒ ('a × 'b) list› where
  ‹show_num_fun f ≡ List.map_filter
    (λp. if (f p) = 0 then None else Some (p, f p)) (enum_class.enum)›


end