Theory Certification_Monads.Check_Monad

(* Title:     Check_Monad
   Author:    Christian Sternagel
   Author:    René Thiemann
*)

section ‹A Special Error Monad for Certification with Informative Error Messages›

theory Check_Monad
imports Error_Monad
begin

text ‹A check is either successful or fails with some error.›
type_synonym
  'e check = "'e + unit"

abbreviation succeed :: "'e check"
where
  "succeed ≡ return ()"

definition check :: "bool ⇒ 'e ⇒ 'e check"
where
  "check b e = (if b then succeed else error e)"

lemma isOK_check [simp]:
  "isOK (check b e) = b" by (simp add: check_def)

lemma isOK_check_catch [simp]:
  "isOK (try check b e catch f) ⟷ b ∨ isOK (f e)"
  by (auto simp add: catch_def check_def)

definition check_return :: "'a check ⇒ 'b ⇒ 'a + 'b"
where
  "check_return chk res = (chk ⪢ return res)"

lemma check_return [simp]:
  "check_return chk res = return res' ⟷ isOK chk ∧ res' = res"
  unfolding check_return_def by (cases chk) auto

lemma [code_unfold]:
  "check_return chk res = (case chk of Inr _ ⇒ Inr res | Inl e ⇒ Inl e)"
  unfolding check_return_def bind_def ..

abbreviation check_allm :: "('a ⇒ 'e check) ⇒ 'a list ⇒ 'e check"
where
  "check_allm f xs ≡ forallM f xs <+? snd"

abbreviation check_exm :: "('a ⇒ 'e check) ⇒ 'a list ⇒ ('e list ⇒ 'e) ⇒ 'e check"
where
  "check_exm f xs fld ≡ existsM f xs <+? fld"

lemma isOK_check_allm:
  "isOK (check_allm f xs) ⟷ (∀x ∈ set xs. isOK (f x))"
  by simp

abbreviation check_allm_index :: "('a ⇒ nat ⇒ 'e check) ⇒ 'a list ⇒ 'e check"
where
  "check_allm_index f xs ≡ forallM_index f xs <+? snd"

abbreviation check_all :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a check"
where
  "check_all f xs ≡ check_allm (λx. if f x then succeed else error x) xs"

abbreviation check_all_index :: "('a ⇒ nat ⇒ bool) ⇒ 'a list ⇒ ('a × nat) check"
where
  "check_all_index f xs ≡ check_allm_index (λx i. if f x i then succeed else error (x, i)) xs"

lemma isOK_check_all_index [simp]:
  "isOK (check_all_index f xs) ⟷ (∀i < length xs. f (xs ! i) i)"
  by auto

text ‹The following version allows to modify the index during the check.›
definition
  check_allm_gen_index ::
    "('a ⇒ nat ⇒ nat) ⇒ ('a ⇒ nat ⇒ 'e check) ⇒ nat ⇒ 'a list ⇒ 'e check"
where
  "check_allm_gen_index g f n xs = snd (foldl (λ(i, m) x. (g x i, m ⪢ f x i)) (n, succeed) xs)"

lemma foldl_error:
  "snd (foldl (λ(i, m) x . (g x i, m ⪢ f x i)) (n, error e) xs) = error e"
  by (induct xs arbitrary: n) auto

lemma isOK_check_allm_gen_index [simp]:
  assumes "isOK (check_allm_gen_index g f n xs)"
  shows "∀x∈set xs. ∃i. isOK (f x i)"
using assms
proof (induct xs arbitrary: n)
  case (Cons x xs)
  show ?case
  proof (cases "isOK (f x n)")
    case True
    then have "∃i. isOK (f x i)" by auto
    with True Cons show ?thesis
      unfolding check_allm_gen_index_def by (force simp: isOK_iff)
  next
    case False
    then obtain e where "f x n = error e" by (cases "f x n") auto
    with foldl_error [of g f _ e] and Cons show ?thesis
      unfolding check_allm_gen_index_def by auto
  qed
qed simp

lemma check_allm_gen_index [fundef_cong]:
  fixes f :: "'a ⇒ nat ⇒ 'e check"
  assumes "⋀x n. x ∈ set xs ⟹ g x n = g' x n"
    and "⋀x n. x ∈ set xs ⟹ f x n = f' x n"
  shows "check_allm_gen_index g f n xs = check_allm_gen_index g' f' n xs"
proof -
  { fix n m
    have "foldl (λ(i, m) x. (g x i, m ⪢ f x i)) (n, m) xs =
      foldl (λ(i, m) x. (g' x i, m ⪢ f' x i)) (n, m) xs"
      using assms by (induct xs arbitrary: n m) auto }
  then show ?thesis unfolding check_allm_gen_index_def by simp
qed

definition check_subseteq :: "'a list ⇒ 'a list ⇒ 'a check"
where
  "check_subseteq xs ys = check_all (λx. x ∈ set ys) xs"

lemma isOK_check_subseteq [simp]:
  "isOK (check_subseteq xs ys) ⟷ set xs ⊆ set ys"
  by (auto simp: check_subseteq_def)

definition check_same_set :: "'a list ⇒ 'a list ⇒ 'a check"
where
  "check_same_set xs ys = (check_subseteq xs ys ⪢ check_subseteq ys xs)"

lemma isOK_check_same_set [simp]:
  "isOK (check_same_set xs ys) ⟷ set xs = set ys"
  unfolding check_same_set_def by auto

definition check_disjoint :: "'a list ⇒ 'a list ⇒ 'a check"
where
  "check_disjoint xs ys = check_all (λx. x ∉ set ys) xs"

lemma isOK_check_disjoint [simp]:
  "isOK (check_disjoint xs ys) ⟷ set xs ∩ set ys = {}"
  unfolding check_disjoint_def by (auto)

definition check_all_combinations :: "('a ⇒ 'a ⇒ 'b check) ⇒ 'a list ⇒ 'b check"
where
  "check_all_combinations c xs = check_allm (λx. check_allm (c x) xs) xs"

lemma isOK_check_all_combinations [simp]:
  "isOK (check_all_combinations c xs) ⟷ (∀x ∈ set xs. ∀y ∈ set xs. isOK (c x y))"
  unfolding check_all_combinations_def by simp

fun check_pairwise :: "('a ⇒ 'a ⇒ 'b check) ⇒ 'a list ⇒ 'b check"
where
  "check_pairwise c [] = succeed" |
  "check_pairwise c (x # xs) = (check_allm (c x) xs ⪢ check_pairwise c xs)"

lemma pairwise_aux:
  "(∀j<length (x # xs). ∀i<j. P ((x # xs) ! i) ((x # xs) ! j))
     = ((∀j<length xs. P x (xs ! j)) ∧ (∀j<length xs. ∀i<j. P (xs ! i) (xs ! j)))"
  (is "?C = (?A ∧ ?B)")
proof (intro iffI conjI)
  assume *: "?A ∧ ?B"
  show "?C"
  proof (intro allI impI)
    fix i j
    assume "j < length (x # xs)" and "i < j"
    then show "P ((x # xs) ! i) ((x # xs) ! j)"
    proof (induct j)
      case (Suc j)
      then show ?case
        using * by (induct i) simp_all
    qed simp
  qed
qed force+

lemma isOK_check_pairwise [simp]:
  "isOK (check_pairwise c xs) ⟷ (∀j<length xs. ∀i<j. isOK (c (xs ! i) (xs ! j)))"
proof (induct xs)
  case (Cons x xs)
  have "isOK (check_allm (c x) xs) = (∀j<length xs. isOK (c x (xs ! j)))"
    using all_set_conv_all_nth [of xs "λy. isOK (c x y)"] by simp
  then have "isOK (check_pairwise c (x # xs)) =
    ((∀j<length xs. isOK (c x (xs ! j))) ∧ (∀j<length xs. ∀i<j. isOK (c (xs ! i) (xs ! j))))"
    by (simp add: Cons)
  then show ?case using pairwise_aux [of x xs "λx y. isOK (c x y)"] by simp
qed auto

abbreviation check_exists :: "('a ⇒ bool) ⇒ 'a list ⇒ ('a list) check"
where
  "check_exists f xs ≡ check_exm (λx. if f x then succeed else error [x]) xs concat"

lemma isOK_choice [simp]:
  "isOK (choice []) ⟷ False"
  "isOK (choice (x # xs)) ⟷ isOK x ∨ isOK (choice xs)"
  by (auto simp: choice.simps isOK_def split: sum.splits)

fun or_ok :: "'a check ⇒ 'a check ⇒ 'a check" where
  "or_ok (Inl a) b = b" |
  "or_ok (Inr a) b = Inr a" 

lemma or_is_or[simp]: "isOK (or_ok a b) ⟷ isOK a ∨ isOK b" by (cases a, auto)

end