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