Theory AutoCorres2.SimplBucket

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*
 * Random lemmas relating to the SIMPL language.
 *)

theory SimplBucket
  imports AutoCorres_Base
begin

lemma Normal_resultE:
  "⟦ Γ ⊢ ⟨c, s⟩ ⇒ Normal t'; ⋀t. ⟦ Γ ⊢ ⟨c, Normal t⟩ ⇒ Normal t'; s = Normal t⟧ ⟹ P ⟧ ⟹ P"
  by (metis noAbrupt_startD noFault_startD noStuck_startD xstate.exhaust)

(* The final state of a While loop will not have the condition. *)
lemma exec_While_final_cond':
  "⟦ Γ ⊢ ⟨b, s⟩ ⇒ s'; b = While C B; s = Normal v; s' = Normal x ⟧ ⟹ x ∉ C"
  apply (induct arbitrary: v x rule: exec.induct)
  apply simp_all
  apply (atomize, clarsimp)
  apply (erule exec_elim_cases, auto)
  done

lemma exec_While_final_cond:
  "⟦ Γ ⊢ ⟨While C B, s⟩ ⇒ Normal s'⟧ ⟹ s' ∉ C"
  apply (erule Normal_resultE)
  apply (erule exec_While_final_cond', auto)
  done

(*
 * If an invariant is held over a while loop, it will still hold when
 * the loop is complete.
 *)
lemma exec_While_final_inv':
  "⟦ Γ ⊢ ⟨b, s⟩ ⇒ s'; b = While C B; s = Normal v; s' = Normal x; I v; ⋀s s'. ⟦ I s; Γ ⊢ ⟨B, Normal s⟩ ⇒ Normal s' ⟧ ⟹ I s' ⟧ ⟹ I x"
  apply atomize
  apply (induct arbitrary: v x rule: exec.induct)
  (* We avoid using the simplifier here, because of looping. *)
  apply (clarify | (atomize, erule Normal_resultE, metis))+
  done

lemma exec_While_final_inv:
  "⟦ Γ ⊢ ⟨While C B, Normal s⟩ ⇒ Normal s'; I s; ⋀s s'. ⟦ I s; Γ ⊢ ⟨B, Normal s⟩ ⇒ Normal s' ⟧ ⟹ I s' ⟧ ⟹ I s'"
  apply (erule exec_While_final_inv', auto)
  done

(* Determine if the given SIMPL fragment may throw an exception. *)
primrec
  exceptions_thrown :: "('a, 'p, 'e) com ⇒ bool"
where
    "exceptions_thrown Skip = False"
  | "exceptions_thrown (Seq a b) = (exceptions_thrown a ∨ exceptions_thrown b)"
  | "exceptions_thrown (Basic a) = False"
  | "exceptions_thrown (Language.Spec a) = False"
  | "exceptions_thrown (Cond a b c) = (exceptions_thrown b ∨ exceptions_thrown c)"
  | "exceptions_thrown (Catch a b) = (exceptions_thrown a ∧ exceptions_thrown b)"
  | "exceptions_thrown (While a b) = exceptions_thrown b"
  | "exceptions_thrown Throw = True"
  | "exceptions_thrown (Call p) = True"
  | "exceptions_thrown (Guard f g a) = exceptions_thrown a"
  | "exceptions_thrown (DynCom a) = (∃s. exceptions_thrown (a s))"

(* May the given stack of exception handlers throw an exception? *)
primrec
  exceptions_unresolved :: "('a, 'p, 'e) com list ⇒ bool"
where
    "exceptions_unresolved [] = True"
  | "exceptions_unresolved (x#xs) = (exceptions_thrown x ∧ exceptions_unresolved xs)"

(* If code can't throw an exception, it won't result in abrupt termination. *)
lemma exceptions_thrown_not_abrupt:
  "⟦ Γ ⊢ ⟨p, s⟩ ⇒ s'; ¬ exceptions_thrown p; ¬ isAbr s ⟧ ⟹ ¬ isAbr s'"
  apply (induct rule: exec.induct, auto)
  done

end