Theory Option_Binders

subsection ‹Binders for the option type \label{sect:binders}›

theory Option_Binders
  imports Main
begin

text ‹
  The following functions are used as binders in the theorems that are proven.
  At all times, when a result is None, the theorem becomes vacuously true.
  The expression ``$m \rightharpoonup \alpha$'' means ``First compute $m$, if it is None then return True, otherwise pass the result to $\alpha$''.
  B2 is a short hand for sequentially doing two independent computations. The following syntax is associated to B2:
  ``$m_1 || m_2 \rightharpoonup \alpha$'' represents ``First compute $m_1$ and $m_2$, if one of them is None then return True, otherwise pass the result to $\alpha$''.
›
definition B :: "'a option ⇒ ('a ⇒ bool) ⇒ bool" (infixl ‹⇀› 65)
where "B m α ≡ case m of None ⇒ True | (Some a) ⇒ α a"

definition B2 :: "'a option ⇒ 'a option ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
where "B2 m1 m2 α ≡ m1 ⇀ (λ a . m2 ⇀ (λ b . α a b))"

syntax "B2" :: "['a option, 'a option, ('a ⇒ 'a ⇒ bool)] => bool" (‹(_ ∥ _ ⇀ _)›  [0, 0, 10] 10)


  
text ‹
  Some rewriting rules for the binders
›
lemma rewrite_B2_to_cases[simp]:
  shows "B2 s t f = (case s of None ⇒ True | (Some s1) ⇒ (case t of None ⇒ True | (Some t1) ⇒ f s1 t1))"
unfolding B2_def B_def by(cases s,cases t,simp+)
lemma rewrite_B_None[simp]:
  shows "None ⇀ α = True"
unfolding B_def by(auto)
lemma rewrite_B_m_True[simp]:
  shows "m ⇀ (λ a . True) = True"
unfolding B_def by(cases m,simp+)
lemma rewrite_B2_cases:
  shows "(case a of None ⇒ True | (Some s) ⇒ (case b of None ⇒ True | (Some t) ⇒ f s t))
          = (∀ s t . a = (Some s) ∧ b = (Some t) ⟶ f s t)"
by(cases a,simp,cases b,simp+)

definition strict_equal :: "'a option ⇒ 'a ⇒ bool"
where "strict_equal m a ≡ case m of None ⇒ False | (Some a') ⇒ a' = a"

end