Theory AutoCorres_Misc

theory AutoCorres_Misc imports
  "../l4v/lib/OptionMonadWP"
begin

section ‹Auxilliary Lemmas for Autocorres›

subsection ‹Option monad›

definition owhile_inv :: "('a ⇒ 's ⇒ bool) ⇒ ('a ⇒ ('s,'a) lookup) ⇒ 'a ⇒ ('a ⇒ 's ⇒ bool) ⇒ 'a rel ⇒ ('s,'a) lookup"   where
 "owhile_inv c b a I R ≡ owhile c b a"

lemma owhile_unfold: "owhile C B r s = ocondition (C r) (B r |>> owhile C B) (oreturn r) s"
  by (auto simp: ocondition_def obind_def oreturn_def owhile_def option_while_simps split: option.split)

lemma ovalidNF_owhile:
  assumes "⋀s. P r s ⟹ I r s"
    and "⋀r s. ovalidNF (λs'. I r s' ∧ C r s' ∧ s' = s) (B r) (λr' s'. I r' s' ∧ (r', r) ∈ R)"
    and "wf R"
    and "⋀r s. I r s ⟹ ¬ C r s ⟹ Q r s"
  shows "ovalidNF (P r) (OptionMonad.owhile C B r) Q"
  unfolding ovalidNF_def
proof (intro allI impI)
  fix s assume "P r s"
  then have "I r s" by fact
  moreover note ‹wf R›
  moreover have "⋀r r'. I r s ⟹ C r s ⟹ B r s = Some r' ⟹ (r', r) ∈ R"
    using assms(2) unfolding ovalidNF_def by fastforce
  moreover have "⋀r r'. I r s ⟹ C r s ⟹ B r s = Some r' ⟹ I r' s"
    using assms(2) unfolding ovalidNF_def by blast
  moreover have "⋀r. I r s ⟹ C r s ⟹ B r s = None ⟹
      None ≠ None ∧ (∀r'. None = Some r' ⟶ Q r' s)"
    using assms(2) unfolding ovalidNF_def by blast
  moreover have "⋀r. I r s ⟹ ¬ C r s ⟹ Some r ≠ None ∧ (∀r'. Some r = Some r' ⟶ Q r' s)"
    using assms(4) unfolding ovalidNF_def by blast
  ultimately
  show "owhile C B r s ≠ None ∧ (∀r'. owhile C B r s = Some r' ⟶ Q r' s)"
    by (rule owhile_rule[where I=I])
qed

lemma ovalidNF_owhile_inv[wp]:
  assumes "⋀r s. ovalidNF (λs'. I r s' ∧ C r s' ∧ s' = s) (B r) (λr' s'. I r' s' ∧ (r', r) ∈ R)"
    and "wf R"
    and "⋀r s. I r s ⟹ ¬ C r s ⟹ Q r s"
  shows "ovalidNF (I r) (owhile_inv C B r I R) Q"
  unfolding owhile_inv_def using _ assms by (rule ovalidNF_owhile)



end