Quelle  L1Defs.thy

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)


chapter ‹L1 phase›

theory L1Defs
imports CCorresE
begin

(* Definitions of constants used in the SimplConv output. *)
type_synonym 's L1_monad = "(unit, unit, 's) exn_monad"
definition "L1_seq (A :: 's L1_monad) (B :: 's L1_monad) ≡ (A >>= (λ_. B)) :: 's L1_monad"
definition "L1_skip ≡ return () :: 's L1_monad"
definition "L1_modify m ≡ (modify m) :: 's L1_monad"
definition "L1_condition c (A :: 's L1_monad) (B :: 's L1_monad) ≡ condition c A B"
definition "L1_catch (A :: 's L1_monad) (B :: 's L1_monad) ≡ (A <catch> (λ_. B))"
definition "L1_while c (A :: 's L1_monad) ≡ (whileLoop (λ_. c) (λ_. A) ())"
definition "L1_throw ≡ throw () :: 's L1_monad"
definition "L1_spec r ≡ state_select r :: 's L1_monad"
definition "L1_assume f ≡ assume_result_and_state f :: 's L1_monad"
definition "L1_guard c ≡ guard c :: 's L1_monad"
definition "L1_init v ≡ (do { x ← select UNIV; modify (v (λ_. x)) }) :: 's L1_monad"
definition "L1_call scope_setup (dest_fn :: 's L1_monad) scope_teardown result_exn return_xf ≡
    do {
        s ← get_state;
        ((do { modify scope_setup;
              dest_fn })
         <catch> (λ_. L1_seq (modify (λt. result_exn (scope_teardown s t) t)) L1_throw));
        t ← get_state;
        modify (scope_teardown s);
        modify (return_xf t)
    }"


definition "L1_fail ≡ fail :: 's L1_monad"
definition "L1_set_to_pred S ≡ λs. s ∈ S"
definition "L1_rel_to_fun R = (λs. Pair () ` Image R {s})"

lemma L1_rel_to_fun_alt: "L1_rel_to_fun R = (λs. Pair () ` {s'. (s, s') ∈ R})"
  by (auto simp: L1_rel_to_fun_def)

lemmas L1_defs = L1_seq_def L1_skip_def L1_modify_def L1_condition_def
    L1_catch_def L1_while_def L1_throw_def L1_spec_def L1_assume_def L1_guard_def
    L1_fail_def L1_init_def L1_set_to_pred_def L1_rel_to_fun_def

lemmas L1_defs' = 
   L1_seq_def L1_skip_def L1_modify_def L1_condition_def L1_catch_def
   L1_while_def L1_throw_def L1_spec_def  L1_assume_def 
   L1_guard_def 
   L1_fail_def L1_init_def L1_set_to_pred_def L1_rel_to_fun_def

declare L1_set_to_pred_def [simp]
declare L1_rel_to_fun_def [simp]

definition L1_guarded:: "('s ==> bool) ==> 's L1_monad ==> 's L1_monad"
  where
"L1_guarded g f = L1_seq (L1_guard g) f"



locale L1_functions =
  fixes P:: "unit ptr ==> 's L1_monad"
begin
  definition "L1_dyn_call g scope_setup (dest :: 's ==> unit ptr) scope_teardown result_exn return_xf ≡
   L1_guarded g (gets dest >>= (λp. L1_call scope_setup (P p) scope_teardown result_exn return_xf))"
end


lemma L1_dyn_call_const:
  "(gets (λ_. dest) >>= (λp. L1_call scope_setup (P p) scope_teardown result_exn return_xf)) =
  L1_call scope_setup (P dest) scope_teardown result_exn return_xf"
  unfolding L1_call_def
  by (rule spec_monad_eqI) (auto simp add: runs_to_iff )

definition "assume_Spec R = guarded_spec_body AssumeError R"
definition exec_spec_monad:: 
  "('s ==> exit_status c_exntype) ==> ((exit_status c_exntype ==> exit_status c_exntype) ==> 's ==> 's) ==>
    ('s ==> 't) ==> ('s ==> 'b) ==> ('b ==> (exit_status, 'a, 't) exn_monad) ==> (('a ==> 'a) ==> 's ==> 's) ==> ('s,'p,strictc_errortype) com" where 
  "exec_spec_monad get_x upd_x st args f res ≡
     Guard Fail {s. succeeds (f (args s)) (st s)}
     (Seq
       (assume_Spec {(s0, s1).
         ∃x t s. reaches (f (args s0)) (st s0) x t ∧ t = st s ∧
           (case x of
             Exn e ==> s1 = upd_x (λ_. Nonlocal e) s
           | Result r ==> s1 = upd_x (λ_. Return) (res (λ_. r) s))})
       (Cond {s. is_local (get_x s)} SKIP THROW))"

lemma terminates_Guard': 
  assumes c: "s∈g ==> Γ⊨c↓(Normal s)"
  shows "Γ⊨Guard f g c↓(Normal s)"
proof (cases "s ∈ g")
  case True
  from True c [OF True] show ?thesis by (rule terminates.Guard) 
next
  case False
  then show ?thesis by (rule terminates.GuardFault)
qed

definition L1_exec_spec_monad:: 
  "((exit_status c_exntype ==> exit_status c_exntype) ==> 's ==> 's) ==>
    ('s ==> 't) ==> ('s ==> 'b) ==> ('b ==> (exit_status, 'a, 't) exn_monad) ==> (('a ==> 'a) ==> 's ==> 's) ==> 's L1_monad" where 
  "L1_exec_spec_monad upd_x st args f res ≡
     do {
      a <- gets (args);
      bind_handle (exec_abstract st (f a))
       (λr. L1_seq (L1_modify (res (λ_. r))) (L1_modify (upd_x (λ_. Return))))
       (λe. L1_seq (L1_modify (upd_x (λ_. Nonlocal (the e)))) L1_throw)} "

(* Our corres rule converting from the deeply-embedded SIMPL to a shallow embedding. *)
definition
  L1corres :: "bool ==> ('p ==> ('s, 'p, strictc_errortype) com option)
                     ==> 's L1_monad ==> ('s, 'p, strictc_errortype) com ==> bool"
where
  "L1corres check_term Γ ≡
   λA C. ∀s. succeeds A s ⟶
       ((∀t. Γ ⊨ ⟨C, Normal s⟩ ==> t ⟶
        (case t of
              Normal s' ==> reaches A s (Result ()) s'
            | Abrupt s' ==> reaches A s (Exn ()) s'
            | Fault e ==> e ∈ {AssumeError, StackOverflow}
            | _ ==> False))
        ∧ (check_term ⟶ Γ ⊨ C ↓ Normal s))"

definition
  L1corres' :: "bool ==> ('p ==> ('s, 'p, strictc_errortype) com option) ==> ('s ==> bool)
                     ==> 's L1_monad ==> ('s, 'p, strictc_errortype) com ==> bool"
where
  "L1corres' check_term Γ P ≡
   λA C. ∀s. (P s) ∧ succeeds A s ⟶
       ((∀t. Γ ⊨ ⟨C, Normal s⟩ ==> t ⟶
        (case t of
              Normal s' ==> reaches A s (Result ()) s'
            | Abrupt s' ==> reaches A s (Exn ()) s'
            | Fault e ==> e ∈ {AssumeError, StackOverflow}
            | _ ==> False))
        ∧ (check_term ⟶ Γ ⊨ C ↓ Normal s))"


lemma L1corres_alt_def: "L1corres ct Γ = ccorresE (λx. x) ct {AssumeError, StackOverflow} Γ ⊤ UNIV"
  apply (rule ext)+
  apply (clarsimp simp: L1corres_def ccorresE_def)
  done

lemma L1corres'_alt_def: "L1corres' ct Γ P = ccorresE (λx. x) ct {AssumeError, StackOverflow} Γ P UNIV"
  apply (rule ext)+
  apply (clarsimp simp: L1corres'_def ccorresE_def)
  done



lemma admissible_nondet_ord_L1corres [corres_admissible]:
  "ccpo.admissible Inf (≥) (λA. L1corres ct Γ A C)"
  unfolding L1corres_def imp_conjR  disj_imp[symmetric] 
  apply (intro admissible_all)
  apply (intro admissible_conj)
   apply (rule ccpo.admissibleI)
   apply (clarsimp split: xstate.splits)
   apply (intro conjI admissible_mem)
  subgoal   
    apply (simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits)
    apply transfer
    apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
    by (metis outcomes.simps(2) post_state.simps(3))
  subgoal
    apply (simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits)
    apply transfer
    apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
   by (metis outcomes.simps(2) post_state.simps(3))
  subgoal
    apply (simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits)
    apply transfer
    apply (clarsimp simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
   by (metis outcomes.simps(2) post_state.simps(3))
  subgoal
    apply (simp add: ccpo.admissible_def chain_def 
        succeeds_def reaches_def split: prod.splits)
    apply transfer
    apply (auto simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
        split: if_split_asm)
    done
  apply (rule ccpo.admissibleI)
  apply (simp split: xstate.splits)
  apply (clarsimp simp add: ccpo.admissible_def chain_def 
      succeeds_def reaches_def split: prod.splits)
  apply transfer
  apply (auto simp add: Inf_post_state_def top_post_state_def image_def vimage_def 
      split: if_split_asm)
  done

lemma L1corres_top [corres_top]: "L1corres ct P ⊤ C"
  by (auto simp add: L1corres_def)

lemma L1corres_le_trans[corres_le_trans]: "L1corres ct Γ A C ==> A ≤ A' ==> L1corres ct Γ A' C"
  apply (auto simp add: L1corres_def)
  subgoal
    using le_succeedsD le_reachesD
    by (fastforce split: xstate.splits )
  subgoal
    using le_succeedsD le_reachesD
    by (fastforce split: xstate.splits simp add: )
  done



lemma L1corres_guard_DynCom:
  "[∧s. s ∈ g ==> L1corres ct Γ (B s) (B' s)] ==>
      L1corres ct Γ (L1_seq (L1_guard (λs. s ∈ g)) (gets B 🍋 (λb. b))) (Guard f g (DynCom B'))"
  apply (clarsimp simp: L1corres_def L1_defs)
  apply (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind)
  done

lemma L1corres'_guard_DynCom_conseq:
  assumes conseq: "∧s. P s ==> g s ==> s ∈ g'"
  assumes corres: "∧s. P s ==> g s ==> L1corres' ct Γ (λs. P s ∧ g s) (B s) (B' s)"
  shows "L1corres' ct Γ P (L1_seq (L1_guard g) (gets B 🍋 (λb. b))) (Guard f g' (DynCom B'))"
  using conseq corres
  apply (clarsimp simp: L1corres'_def L1_defs)
  apply (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind)

  done



lemma L1corres'_guard_DynCom:
  "[∧s. P s ==> s ∈ g ==> L1corres' ct Γ (λs. P s ∧ s ∈ g) (B s) (B' s)] ==>
      L1corres' ct Γ P (L1_seq (L1_guard (λs. s ∈ g)) (gets B 🍋 (λb. b))) (Guard f g (DynCom B'))"
  apply (rule L1corres'_guard_DynCom_conseq [where B=B])
   apply simp
  apply simp
  done

lemma L1corres_DynCom: 
  assumes corres_f: "∧s. L1corres ct Γ (g s) (f s)" 
  shows "L1corres ct Γ (gets g 🍋 (λb. b)) (DynCom f)"
  using corres_f
  apply (clarsimp simp: L1corres_def L1_defs)
  apply (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind)
  done

lemma L1corres'_DynCom: 
  assumes corres_f: "∧s. P s ==> L1corres' ct Γ P (g s) (f s)" 
  shows "L1corres' ct Γ P (gets g 🍋 (λb. b)) (DynCom f)"
  using corres_f
  apply (clarsimp simp: L1corres'_def L1_defs)
  apply (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind)
  done

lemma L1corres'_DynCom_fix_state: 
  assumes corres_f: "∧s. P s ==> L1corres' ct Γ (λs'. P s' ∧ s' = s) (g s) (f s)" 
  shows "L1corres' ct Γ P (gets g 🍋 (λb. b)) (DynCom f)"
  using corres_f
  apply (clarsimp simp: L1corres'_def L1_defs)
  apply (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind)
  done

lemma L1corres'_guard':
  "[ L1corres' ct Γ (λs. P s ∧ s ∈ g) B B' ] ==>
      L1corres' ct Γ P (L1_seq (L1_guard (λs. s ∈ g)) B) (Guard f g B')"
  apply (clarsimp simp: L1corres'_def L1_defs)
  apply (erule_tac x=s in allE)
  apply (rule conjI)
   apply clarsimp
   apply (erule exec_Normal_elim_cases)
  subgoal
    by (auto simp: succeeds_bind reaches_bind split: xstate.splits)
  subgoal
    by (auto simp: succeeds_bind reaches_bind split: xstate.splits)
  subgoal
    by (auto simp: succeeds_bind intro: terminates.intros)
  done

lemma L1corres'_guarded:
  "[ L1corres' ct Γ (λs. P s ∧ s ∈ g) B B' ] ==>
      L1corres' ct Γ P (L1_guarded (λs. s ∈ g) B) (Guard f g B')"
  unfolding L1_guarded_def by (rule L1corres'_guard')


lemma L1corres'_Guard_maybe_guard: 
"L1corres' ct Γ P B (Guard f g B') ==> L1corres' ct Γ P B (maybe_guard f g B')"
  apply (simp add: L1corres'_def maybe_guard_def)
  by (meson exec.Guard iso_tuple_UNIV_I terminates_Normal_elim_cases(2))

lemma L1corres_Guard_maybe_guard: 
"L1corres ct Γ B (Guard f g B') ==> L1corres ct Γ B (maybe_guard f g B')"
  apply (simp add: L1corres_def maybe_guard_def)
  by (meson exec.Guard iso_tuple_UNIV_I terminates_Normal_elim_cases(2))

lemma L1corres'_guarded_DynCom_conseq:
  assumes conseq: "∧s. P s ==> g s ==> s ∈ g'"
  assumes corres_B: "∧s. P s ==> g s ==> L1corres' ct Γ (λs. P s ∧ g s) (B s) (B' s)"
  shows "L1corres' ct Γ P (L1_guarded g (gets B 🍋 (λb. b))) (maybe_guard f g' (DynCom B'))"
  apply (rule L1corres'_Guard_maybe_guard)
  unfolding L1_guarded_def L1_set_to_pred_def
  using corres_B
  by (simp add: L1corres'_guard_DynCom_conseq [OF conseq])

lemma L1corres'_guarded_DynCom:
  assumes corres_B: "∧s. P s ==> s ∈ g ==> L1corres' ct Γ (λs. P s ∧ s ∈ g) (B s) (B' s)"
  shows "L1corres' ct Γ P (L1_guarded (L1_set_to_pred g) (gets B 🍋 (λb. b))) (maybe_guard f g (DynCom B'))"
  apply (rule L1corres'_guarded_DynCom_conseq [where B=B])
   apply simp
  using corres_B
  apply simp
  done

lemma L1corres'_conseq: 
  assumes corres_Q: "L1corres' ct Γ Q B B'"
  assumes conseq: "∧s. P s ==> Q s"
  shows "L1corres' ct Γ P B B'"
  using conseq corres_Q
  by (auto simp add: L1corres'_def)

lemma L1corres_to_L1corres': "L1corres ct Γ = L1corres' ct Γ ⊤"
  by (simp add: L1corres_def L1corres'_def)


lemma L1corres_guarded_DynCom_conseq:
  assumes conseq: "∧s. g s ==> s ∈ g'"
  assumes corres_B: "∧s. g s ==> L1corres ct Γ (B s) (B' s)"
  shows "L1corres ct Γ (L1_guarded g (gets B 🍋 (λb. b))) (maybe_guard f g' (DynCom B'))"
  using corres_B unfolding L1corres_to_L1corres'
  thm L1corres'_guarded_DynCom
  apply - 
  apply (rule L1corres'_guarded_DynCom_conseq [where B=B ])
  using conseq apply simp
  apply (rule L1corres'_conseq [where Q =  "⊤"])
   apply (simp)
  apply simp
  done

lemma L1corres_guarded_DynCom:
  assumes corres_B: "∧s. s ∈ g ==> L1corres ct Γ (B s) (B' s)"
  shows "L1corres ct Γ (L1_guarded (L1_set_to_pred g) (gets B 🍋 (λb. b))) (maybe_guard f g (DynCom B'))"
  using corres_B unfolding L1corres_to_L1corres'
  apply - 
  apply (rule L1corres'_guarded_DynCom [where B=B ])
  apply (rule L1corres'_conseq [where Q =  "⊤"])
   apply simp
  apply simp
  done

lemma L1corres_guarded: 
  assumes B: "L1corres ct Γ B B'"
  shows "L1corres ct Γ (L1_guarded g B) B'"
  using B
  by (auto simp add: L1corres_def L1_guarded_def L1_seq_def L1_guard_def 
      succeeds_bind reaches_bind split: xstate.splits)

lemma L1corres_guarded_DynCom_conseq1:
  assumes corres_B: "∧s. g s ==> L1corres ct Γ (B s) (Guard f {s'. s ∈ g'} (B' s))"
  shows "L1corres ct Γ (L1_guarded g (gets B 🍋 (λb. b))) (Guard f g' (DynCom B'))"
  using corres_B
  apply (simp add: L1corres_def L1_guarded_def L1_seq_def L1_guard_def)
  apply (auto simp add: succeeds_bind reaches_bind split: xstate.splits )
  subgoal
    by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
  subgoal
    by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
  subgoal
    by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
  subgoal
    by (fastforce elim!: exec_Normal_elim_cases intro: exec.intros simp add: exec_Guard)
  subgoal for s
    apply (cases "s ∈ g'")
    apply (fastforce elim!:  terminates_Normal_elim_cases  
        elim: terminates.GuardFault intro: terminates.intros)+
    done
  done

lemma L1corres_guarded_DynCom_conseq2:
  assumes corres_B: "∧s. g s ==> L1corres ct Γ (B s) (Guard f {s'. s ∈ g'} (B' s))"
  shows "L1corres ct Γ (L1_guarded g (gets B 🍋 (λb. b))) (maybe_guard f g' (DynCom B'))"
  apply (rule L1corres_Guard_maybe_guard)
  using corres_B
  by (rule L1corres_guarded_DynCom_conseq1)



(* Wrapper for calling un-translated functions. *)
definition
  "L1_call_simpl check_term Gamma proc
    = do {s ← get_state;
         assert (check_term ⟶ Gamma ⊨ Call proc ↓ Normal s);
         xs ← select {t. Gamma ⊨ ⟨Call proc, Normal s⟩ ==> t};
         case xs :: (_, strictc_errortype) xstate of
             Normal s ==> set_state s
           | Abrupt s ==> do {set_state s; throw () }
           | Fault ft ==> if ft ∈ {AssumeError, StackOverflow} then bot else fail
           | Stuck ==> fail
      }"


lemma L1corres_call_simpl:
  "L1corres ct Γ (L1_call_simpl ct Γ proc) (Call proc)"
  apply (clarsimp simp: L1corres_def L1_call_simpl_def)
  apply safe
  subgoal for s t
    apply (cases t)
       apply (fastforce elim!:  exec_Normal_elim_cases 
        intro: terminates.intros exec.intros
 
        simp add: succeeds_bind reaches_bind Exn_def )+
    subgoal
      apply (auto split: xstate.splits simp add: reaches_bind succeeds_bind)
      apply (smt (verit, ccfv_threshold) image_eqI mem_Collect_eq succeeds_fail_iff)+
      done
    subgoal
      apply (auto split: xstate.splits simp add: reaches_bind succeeds_bind)
      done
    done
  subgoal for s
    apply (auto intro!: terminates.intros simp add: succeeds_bind reaches_bind)
    done
  done

lemma L1_call_simpl_le_trans:
  assumes "L1corres ct Γ P (Call proc)"
  shows "(L1_call_simpl ct Γ proc) ≤ P"
  using assms
  apply (simp add: le_spec_monad_le_refines_iff L1corres_def L1_call_simpl_def)
  apply (auto simp add: refines_def_old)
  subgoal
    by (fastforce simp add: succeeds_bind split: xstate.splits)
  subgoal
    by (auto simp add: succeeds_bind reaches_bind split: xstate.splits)
  done

lemma L1corres_skip:
  "L1corres ct Γ L1_skip SKIP"
  unfolding L1corres_def L1_defs
  by (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind)

lemma L1corres_throw:
  "L1corres ct Γ L1_throw Throw"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)

lemma L1corres_seq:
  "[ L1corres ct Γ L L'; L1corres ct Γ R R' ] ==>
    L1corres ct Γ (L1_seq L R) (L' ;; R')"
  apply (clarsimp simp: L1corres_alt_def)
  apply (clarsimp simp: L1_seq_def)
  apply (rule ccorresE_Seq)
  apply auto
  done

lemma L1corres_modify:
  "L1corres ct Γ (L1_modify m) (Basic m)"
  apply (clarsimp simp: L1corres_def L1_defs)
  apply (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
  done

lemma L1corres_condition:
  "[ L1corres ct Γ L L'; L1corres ct Γ R R' ] ==>
    L1corres ct Γ (L1_condition (L1_set_to_pred c) L R) (Cond c L' R')"
  apply (clarsimp simp: L1corres_alt_def)
  apply (clarsimp simp: L1_defs)
  apply (rule ccorresE_Cond_match)
    apply (erule ccorresE_guard_imp, simp+)[1]
   apply (erule ccorresE_guard_imp, simp+)[1]
  apply simp
  done

lemma L1corres_catch:
  "[ L1corres ct Γ L L'; L1corres ct Γ R R' ] ==>
    L1corres ct Γ (L1_catch L R) (Catch L' R')"
  apply (clarsimp simp: L1corres_alt_def)
  apply (clarsimp simp: L1_catch_def)
  apply (erule ccorresE_Catch)
  apply force
  done

lemma L1corres_while:
  "[ L1corres ct Γ B B' ] ==>
      L1corres ct Γ (L1_while (L1_set_to_pred c) B) (While c B')"
  apply (clarsimp simp: L1corres_alt_def)
  apply (clarsimp simp: L1_defs)
  apply (rule ccorresE_While)
   apply clarsimp
  apply simp
  done

lemma L1corres_guard:
  "[ L1corres ct Γ B B' ] ==>
      L1corres ct Γ (L1_seq (L1_guard (L1_set_to_pred c)) B) (Guard f c B')"
  apply (clarsimp simp: L1corres_alt_def)
  apply (clarsimp simp: ccorresE_def L1_defs)
  apply (erule_tac x=s in allE)
  apply (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
  done


lemma L1corres_spec:
  "L1corres ct Γ (L1_spec x) (com.Spec x)"
  apply (clarsimp simp: L1corres_def L1_defs)
  apply (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
  done

lemma L1_init_alt_def:
  "L1_init upd ≡ L1_spec {(s, t). ∃v. t = upd (λ_. v) s}"
  apply (rule eq_reflection)
  apply (clarsimp simp: L1_defs)
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L1corres_init:
  "L1corres ct Γ (L1_init upd) (lvar_nondet_init upd)"
  by (auto simp: L1_init_alt_def lvar_nondet_init_def intro: L1corres_spec)

lemma L1corres_guarded_spec:
  "L1corres ct Γ (L1_spec R) (guarded_spec_body F R)"
  apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_spec_def guarded_spec_body_def)
  apply (force simp: liftE_def bind_def
               elim: exec_Normal_elim_cases intro: terminates.Guard terminates.Spec)
  done

lemma L1corres_assume:
  "L1corres ct Γ (L1_assume (L1_rel_to_fun R)) (guarded_spec_body AssumeError R)"
  apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_assume_def L1_rel_to_fun_alt guarded_spec_body_def)
  apply (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
  done

lemma L1corres_guarded_spec_pre_post:
  "L1corres ct Γ (L1_spec R) (guarded_spec_pre_post F_pre F_post R)"
  apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_spec_def guarded_spec_pre_post_def)
  apply (force simp: liftE_def bind_def
               elim: exec_Normal_elim_cases intro: terminates.Guard terminates.Spec)
  done

lemma L1corres_assume_guarded_spec_pre_post:
  "L1corres ct Γ
    (L1_seq (L1_guard (λs. s ∈ fst ` R)) ((L1_assume (L1_rel_to_fun R))))
    (guarded_spec_pre_post F_pre AssumeError R)"
  apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_assume_def 
      L1_seq_def L1_guard_def L1_rel_to_fun_alt guarded_spec_pre_post_def)
  apply (force elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
  done

lemma L1corres_assume_spec_pre_post:
  "L1corres ct Γ
    (L1_seq (L1_guard (λs. s ∈ P)) ((L1_assume (L1_rel_to_fun R))))
    (spec_pre_post F_pre AssumeError P R)"
  apply (clarsimp simp: L1corres_alt_def ccorresE_def L1_assume_def 
      L1_seq_def L1_guard_def L1_rel_to_fun_alt spec_pre_post_def)
  apply (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def terminates.Spec terminates_Guard')
  done


lemma pred_conj_apply[simp]: "(P and Q) s ⟷ P s ∧ Q s"
  by (auto simp add: pred_conj_def)

lemma L1corres_call:
  "[ L1corres ct Γ dest_fn (Call dest) ] ==>
    L1corres ct Γ
        (L1_call scope_setup dest_fn scope_teardown_norm scope_teardown_exn f)
        (call_exn scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (f t)))"
  apply (clarsimp simp: L1corres_alt_def)
  apply (unfold call_exn_def block_exn_def L1_call_def)
  apply (rule ccorresE_DynCom)
  apply clarsimp
  apply (rule ccorresE_get)
  apply (rule ccorresE_assume_pre, clarsimp)
  apply (rule ccorresE_guard_imp_stronger)
    apply (rule ccorresE_Seq)
     apply (rule ccorresE_Catch)
      apply (rule ccorresE_Seq)
       apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
      apply assumption
     apply (rule L1corres_seq[unfolded L1corres_alt_def])
      apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
     apply (rule L1corres_throw [unfolded L1corres_alt_def])
    apply (rule ccorresE_DynCom)
    apply (rule ccorresE_get)
    apply (rule ccorresE_assume_pre, clarsimp)
    apply (rule ccorresE_guard_imp)
      apply (rule ccorresE_Seq)
       apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
      apply (rule L1corres_modify[unfolded L1_modify_def L1corres_alt_def])
     apply simp
    apply simp
   apply simp
  apply simp
  done  

lemma (in L1_functions) L1corres_dyn_call_conseq:
  assumes conseq: "∧s. g s ==> s ∈ g'"
  assumes corres_dest: "∧s. g s ==> L1corres ct Γ (P (dest s)) (Call (dest s))"
  shows
    "L1corres ct Γ
        (L1_dyn_call g scope_setup dest scope_teardown_norm scope_teardown_exn result)
        (dynCall_exn f g' scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
proof -
  have eq: "(gets (λs. L1_call scope_setup (P (dest s)) scope_teardown_norm scope_teardown_exn result) 🍋 (λb. b)) =
    (gets dest 🍋 (λp. L1_call scope_setup (P p) scope_teardown_norm scope_teardown_exn result))"
    apply (rule spec_monad_ext)
    apply (simp add: run_bind)
    done
  show ?thesis
    apply (simp add: L1_dyn_call_def dynCall_exn_def)
    apply (rule L1corres_guarded_DynCom_conseq [where B = "λs. L1_call scope_setup (P (dest s)) scope_teardown_norm scope_teardown_exn result", simplified eq])
     apply (simp add: conseq)
    apply (rule L1corres_call)
    apply (rule corres_dest)
    by simp
qed


lemma (in L1_functions) L1corres_dyn_call_same_guard:
  assumes eq: "L1_set_to_pred g ≡ g'"
  assumes corres_dest: "∧s. g' s ==> L1corres ct Γ (P (dest s)) (Call (dest s))"
  shows
    "L1corres ct Γ
        (L1_dyn_call g' scope_setup dest scope_teardown_norm scope_teardown_exn result)
        (dynCall_exn f g scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
  apply (rule L1corres_dyn_call_conseq)
   apply (simp add: eq [symmetric])
  by (rule corres_dest)

lemma (in L1_functions) L1corres_dyn_call_add_and_select_guard:
  assumes eq: "L1_set_to_pred g ≡ g'"
  assumes corres_dest: "∧s. G s ==> L1corres ct Γ (P (dest s)) (Call (dest s))"
  shows
    "L1corres ct Γ
        (L1_dyn_call (G and g') scope_setup dest scope_teardown_norm scope_teardown_exn result)
        (dynCall_exn f g scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
  apply (rule L1corres_dyn_call_conseq)
   apply (simp add: eq [symmetric])
  apply (rule corres_dest)
  apply (simp)
  done

definition "L1_dyn_call_simpl ct Γ g scope_setup (dest :: 's ==> unit ptr) scope_teardown result_exn return_xf ≡
   L1_guarded g (gets dest >>= (λp. L1_call scope_setup (L1_call_simpl ct Γ p) scope_teardown result_exn return_xf))"

lemma L1corres_dyn_call_simpl_conseq:
  assumes conseq: "∧s. g s ==> s ∈ g'"
  shows
    "L1corres ct Γ
        (L1_dyn_call_simpl ct Γ g scope_setup dest scope_teardown_norm scope_teardown_exn result)
        (dynCall_exn f g' scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
proof -
  have eq: "(gets (λs. L1_call scope_setup (L1_call_simpl ct Γ (dest s)) scope_teardown_norm scope_teardown_exn result) 🍋 (λb. b)) =
    (gets dest 🍋 (λp. L1_call scope_setup (L1_call_simpl ct Γ p) scope_teardown_norm scope_teardown_exn result))"
    apply (rule spec_monad_ext)
    apply (simp add: run_bind)
    done
  show ?thesis
    apply (simp add: L1_dyn_call_simpl_def dynCall_exn_def)
    apply (rule L1corres_guarded_DynCom_conseq [where B = "λs. L1_call scope_setup (L1_call_simpl ct Γ (dest s)) scope_teardown_norm scope_teardown_exn result", simplified eq])
     apply (simp add: conseq)
    apply (rule L1corres_call)
    apply (rule L1corres_call_simpl)
    done
qed

definition "L1_dyn_call_map_of_default g scope_setup (dest :: 's ==> unit ptr) ps scope_teardown result_exn return_xf ≡
   L1_guarded g (gets dest >>= (λp. L1_call scope_setup (map_of_default (λ_. ⊤) ps p) scope_teardown result_exn return_xf))"


lemma map_of_default_witness: "p ∈ set (map fst ps) ==> ∃f. (p,f) ∈ set ps ∧ map_of_default d ps p = f"
  by (induct ps) auto

lemma list_all_prod_witness: "list_all (λ(x, v). P x v) xs ==> (x, v) ∈ set xs ==> P x v"
  by (induct xs) auto

lemma L1corres_Guard_UNIV: "L1corres ct Γ X C ==> L1corres ct Γ X (Guard f UNIV C)"
  by (simp add: L1corres_alt_def ccorresE_Guard)

lemma L1corres_dyn_call_map_of_default_conseq:
  assumes conseq: "∧s. g' s ==> dest s ∈ set (map fst ps) ==> s ∈ g"
  assumes ps: "list_all (λ(p, f). L1corres ct Γ f (Call p)) ps"
  shows
    "L1corres ct Γ
        (L1_dyn_call_map_of_default g' scope_setup dest ps scope_teardown_norm scope_teardown_exn result)
        (dynCall_exn f g scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
proof -
  have eq: "(gets (λs. L1_call scope_setup (map_of_default (λ_. ⊤) ps (dest s)) scope_teardown_norm scope_teardown_exn result) 🍋 (λb. b)) =
    (gets dest 🍋 (λp. L1_call scope_setup (map_of_default (λ_. ⊤) ps p) scope_teardown_norm scope_teardown_exn result))"
    apply (rule spec_monad_ext)
    apply (simp add: run_bind)
    done
  show ?thesis
    apply (simp add: L1_dyn_call_map_of_default_def dynCall_exn_def)
    apply (rule L1corres_guarded_DynCom_conseq2 [where B = "λs. L1_call scope_setup (map_of_default (λ_. ⊤) ps (dest s)) scope_teardown_norm scope_teardown_exn result", simplified eq])
    subgoal premises prems for s
    proof (cases "dest s ∈ set (map fst ps)")
      case True
      from map_of_default_witness [OF True] obtain f where 
        elem: "(dest s,f) ∈ set ps" and eq: "map_of_default (λ_. ⊤) ps (dest s) = f"
        by blast
      from list_all_prod_witness [OF ps elem]
      have "L1corres ct Γ f (Call (dest s))" .
      moreover from True prems conseq have "s ∈ g" by blast
      ultimately show ?thesis 
        apply (simp add: eq)
        apply (rule L1corres_Guard_UNIV)
        apply (rule L1corres_call)
        apply assumption
        done
    next
      case False
      then have "(map_of_default (λ_. ⊤) ps (dest s)) = ⊤"
        by (simp add: map_of_default_fallthrough)
      hence "(L1_call scope_setup (map_of_default (λ_. ⊤) ps (dest s)) scope_teardown_norm
               scope_teardown_exn result) = ⊤"
        apply simp
        apply (simp add: L1_call_def)
        apply (rule spec_monad_eqI)
        apply (auto simp add: runs_to_iff)
        done  
      then show ?thesis by (simp add: L1corres_top) 
    qed
    done
qed


lemma L1corres_dyn_call_simpl:
  assumes eq: "L1_set_to_pred g ≡ g'"
  shows
    "L1corres ct Γ
        (L1_dyn_call_simpl ct Γ g' scope_setup dest scope_teardown_norm scope_teardown_exn result)
        (dynCall_exn f g scope_setup dest scope_teardown_norm scope_teardown_exn (λ_ t. Basic (result t)))"
  apply (rule L1corres_dyn_call_simpl_conseq)
  apply (simp add: eq [symmetric])
  done

lemma L1_seq_guard_merge: "L1_seq (L1_guard P) (L1_seq (L1_guard Q) c) = L1_seq (L1_guard (P and Q)) c"
  unfolding L1_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma and_unfold: "(and) = (λP Q s. P s ∧ Q s)"
  by (auto simp add: fun_eq_iff)

lemma L1_seq_guard_eq: "(∧s. P s = Q s) ==> L1_seq (L1_guard P) c = L1_seq (L1_guard Q) c"
  unfolding L1_defs
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma foldr_and_commute: "∧s. foldr (and) gs (P and g) s = (g s ∧ foldr (and) gs P s)"
  by (induct gs arbitrary: P g) (auto simp add:)


lemma L1corres_fail:
  "L1corres ct Γ L1_fail X"
  apply (clarsimp simp: L1corres_alt_def)
  apply (clarsimp simp: L1_fail_def)
  apply (rule ccorresE_fail)
  done

lemma L1corres_prepend_unknown_var':
  "[ L1corres ct Γ A C; ∧s::'s::type. X (λ_::'a::type. (X' s)) s = s ] ==> L1corres ct Γ (L1_seq (L1_init X) A) C"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
      metis+


lemma L1_catch_seq_join: "no_throw (λ_. True) A ==> L1_seq A (L1_catch B C) = (L1_catch (L1_seq A B) C)"
  unfolding no_throw_def L1_defs
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (clarsimp simp add: runs_to_def_old runs_to_partial_def_old Exn_def default_option_def)
  apply (intro conjI impI iffI)
     apply (metis Exn_def Exn_neq_Result)+
  done


lemma no_throw_L1_init [simp]: "no_throw P (L1_init f)"
  unfolding L1_init_def no_throw_def
  apply (clarsimp)
  apply (runs_to_vcg)
  done


lemma L1corres_prepend_unknown_var:
  "[ L1corres ct Γ (L1_catch A B) C; ∧s. X (λ_::'d::type. (X' s)) s = s ]
         ==> L1corres ct Γ (L1_catch (L1_seq (L1_init X) A) B) C"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def succeeds_catch reaches_catch)
    metis+

lemma L1corres_Call:
  "[ Γ X' = Some Z'; L1corres ct Γ Z Z' ] ==>
    L1corres ct Γ Z (Call X')"
  apply (clarsimp simp: L1corres_alt_def)
  apply (erule (1) ccorresE_Call)
  done

lemma L1_call_corres [fundef_cong]:
  "[ scope_setup = scope_setup';
     dest_fn = dest_fn';
     scope_teardown = scope_teardown';
     return_xf = return_xf' ] ==>
    L1_call scope_setup dest_fn scope_teardown return_xf =
    L1_call scope_setup' dest_fn' scope_teardown' return_xf'"
  apply (clarsimp simp: L1_call_def)
  done


lemma L1_corres_cleanup: 
  "L1corres ct Γ (do {y <- state_select {(s,t). t = cleanup s};
                        return ()
                    })
     (Basic cleanup)"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)

lemma L1_corres_spec_cleanup: 
  "L1corres ct Γ (do { y <- state_select cleanup;
                        return ()
                    })
     (com.Spec cleanup)"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def)
 
lemma L1_corres_cleanup_throw: 
  "L1corres ct Γ (do { _ <- state_select {(s,t). t = cleanup s};
                        throw ()
                  })
     (Basic cleanup;; THROW)"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def default_option_def)


lemma L1_corres_spec_cleanup_throw: 
  "L1corres ct Γ (do{ _ <- state_select cleanup;
                        throw ()
                  })
     (com.Spec cleanup;; THROW)"
  unfolding L1corres_def L1_defs
  by (auto elim!:  exec_Normal_elim_cases 
      intro: terminates.intros 
      split: xstate.splits 
      simp add: succeeds_bind reaches_bind Exn_def default_option_def)

lemma on_exit_unit_def: "(on_exit f cleanup::(unit, unit, 's) exn_monad) =
  bind_handle f
    (λv. bind (state_select cleanup) (λ_. return ()))
    (λe. bind (state_select cleanup)(λ_. throw ()))"
  unfolding on_exit_def on_exit'_def bind_handle_eq
  by (intro arg_cong2[where f=bind_exception_or_result])
     (auto simp: fun_eq_iff default_option_def Exn_def
           split: exception_or_result_split)

lemma on_exit_catch_conv: "on_exit f cleanup =
 do {
    r ← (f <catch> (λe. state_select cleanup >>= (λ_. throw e)));
    state_select cleanup;
    return r
  }"
  unfolding on_exit_def on_exit'_def
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff fun_eq_iff Exn_def default_option_def
      intro!: arg_cong[where f="runs_to _ _"])
  by (metis default_option_def exception_or_result_cases not_None_eq)

lemma L2corres_on_exit': 
  assumes m_c: "L1corres ct Γ m c"
  shows "L1corres ct Γ (on_exit m {(s,t). t = cleanup s}) (On_Exit c (Basic cleanup))"
  unfolding on_exit_catch_conv
  apply (simp add: On_Exit_def)
  apply (rule L1corres_seq [simplified L1_seq_def])
   apply (simp add: L1_catch_def [symmetric])
   apply (rule L1corres_catch [OF m_c])
   apply (rule L1_corres_cleanup_throw [simplified])
  apply (rule L1_corres_cleanup [simplified])
  done

lemma L2corres_on_exit: 
  assumes m_c: "L1corres ct Γ m c"
  shows "L1corres ct Γ (on_exit m cleanup) (On_Exit c (com.Spec cleanup))"
  apply (simp add: on_exit_catch_conv On_Exit_def)
  apply (rule L1corres_seq [simplified L1_seq_def])
   apply (simp add: L1_catch_def [symmetric])
   apply (rule L1corres_catch [OF m_c])
   apply (rule L1_corres_spec_cleanup_throw[simplified])
  apply (rule L1_corres_spec_cleanup[simplified])
  done

definition
refines_simpl :: "bool ==> ('p ==> ('s, 'p, strictc_errortype) com option) ==>
  ('s, 'p, strictc_errortype) com ==>
  (('e::default, 'a, 't) spec_monad) ==>
   's ==> 't ==> (('s, strictc_errortype) xstate ==> (('e, 'a) exception_or_result * 't) ==> bool) ==> bool" where
"refines_simpl ct Γ c m s t R ≡
  succeeds m t ⟶
   ((∀s'. Γ ⊨ ⟨c, Normal s⟩ ==> s' ⟶
      (s' ∈ {Fault AssumeError, Fault StackOverflow} ∨
      (∃r t'. reaches m t r t' ∧ R s' (r, t')))) ∧
    (ct ⟶ Γ ⊨ c ↓ Normal s))"


lemma refines_simplI:
  assumes termi: "succeeds m t ==> ct ==> Γ ⊨ c ↓ Normal s"
  assumes sim: "∧s'. succeeds m t ==> Γ ⊨ ⟨c, Normal s⟩ ==> s' ==> s' ∉ {Fault AssumeError, Fault StackOverflow}
    ==> ∃r t'. reaches m t r t' ∧ R s' (r, t')"
  shows "refines_simpl ct Γ c m s t R"
  using termi sim unfolding refines_simpl_def
  by blast

definition
rel_L1 :: "('s, strictc_errortype) xstate ==> ('e, 'a) xval × 's ==> bool" where
"rel_L1 ≡ λs (r, t). (case s of
              Normal s' ==> (∃x. r = Result x) ∧ t = s'
            | Abrupt s' ==> (∃x. r = Exn x) ∧ t = s'
            | Fault e ==> False
            | Stuck ==> False)"

lemma rel_L1_unit: 
"rel_L1 = (λs (r, t). (case s of
              Normal s' ==> r = Result () ∧ t = s'
            | Abrupt s' ==> r = Exn () ∧ t = s'
            | Fault e ==> False
            | Stuck ==> False))"
  by (auto simp add: rel_L1_def split: xstate.splits)

lemma rel_L1_conv [simp]:
 "rel_L1 (Normal s) (r, t) = ((∃x. r = Result x) ∧ t = s)"
 "rel_L1 (Abrupt s) (r, t) = ((∃x. r = Exn x) ∧ t = s)"
 "rel_L1 (Fault e) x = False"
 "rel_L1 Stuck x = False"
  by (auto simp add: rel_L1_def)

lemma refines_simpl_rel_L1I:
  assumes termi: "succeeds m t ==> ct ==> Γ ⊨ c ↓ Normal s"
  assumes sim_Normal: "∧s'. succeeds m t ==> Γ ⊨ ⟨c, Normal s⟩ ==> Normal s'
    ==> ∃r. reaches m t (Result r) s'"
  assumes sim_Abrupt: "∧s'. succeeds m t ==> Γ ⊨ ⟨c, Normal s⟩ ==> Abrupt s'
    ==> ∃r. reaches m t (Exn r) s'"
  assumes sim_Fault: "∧e. succeeds m t ==> Γ ⊨ ⟨c, Normal s⟩ ==> Fault e
    ==> e ∈ {AssumeError, StackOverflow}"
  assumes sim_Stuck: "succeeds m t ==> Γ ⊨ ⟨c, Normal s⟩ ==> Stuck
    ==> False"
  shows "refines_simpl ct Γ c m s t rel_L1"
  apply (rule refines_simplI [OF termi], assumption, assumption)
  apply (simp add: rel_L1_def)
  subgoal for s'
    using sim_Normal sim_Abrupt sim_Fault sim_Stuck
    apply (cases s')
       apply (fastforce split: prod.splits sum.splits)+
    done
  done

lemma L1corres_refines_simpl: 
  "L1corres ct Γ m c ==> refines_simpl ct Γ c m s s rel_L1"
  apply (clarsimp simp add: L1corres_def refines_simpl_def rel_L1_def split: xstate.splits prod.splits sum.splits)
  by (smt (verit) Inl_Inr_False xstate.distinct(1) xstate.inject(1) xstate.inject(2))

lemma refines_simpl_L1corres:
  assumes "∧s. refines_simpl ct Γ c m s s rel_L1"
  shows "L1corres ct Γ m c"
  using assms
  apply (force simp add: L1corres_def refines_simpl_def rel_L1_def split: xstate.splits prod.splits sum.splits)
  done

theorem L1corres_refines_simpl_conv: 
  "L1corres ct Γ m c ⟷ (∀s. refines_simpl ct Γ c m s s rel_L1)"
  using L1corres_refines_simpl refines_simpl_L1corres
  by metis

lemma refines_simpl_DynCom:
  "refines_simpl ct Γ (c s) m s t R ==> refines_simpl ct Γ (DynCom c) m s t R"
  by (auto simp add: refines_simpl_def terminates.DynCom elim: exec_Normal_elim_cases(12))

lemma refines_simpl_StackOverflow:
  assumes c: "s ∈ g ==> refines_simpl ct Γ c m s t R"
  shows "refines_simpl ct Γ (Guard StackOverflow g c) m s t R"
  using c 
  by (auto simp add: refines_simpl_def elim: exec_Normal_elim_cases intro: terminates.intros)



lemma refines_simpl_rel_L1_bind:
  fixes m1:: "('e, 'a, 's) exn_monad"
  fixes m2:: "'a ==> ('e, 'b, 's) exn_monad"
  assumes c1: "refines_simpl ct Γ c1 m1 s s rel_L1"
  assumes c2: "∧r s'. succeeds m1 s ==> Γ ⊨ ⟨c1, Normal s⟩ ==> Normal s' ==> reaches m1 s (Result r) s' ==>
    refines_simpl ct Γ c2 (m2 r) s' s' rel_L1"
  shows "refines_simpl ct Γ (c1;;c2) (m1 >>= m2) s s rel_L1"
proof (rule refines_simpl_rel_L1I)
  assume nofail: "succeeds (m1 >>= m2) s"
  assume ct: "ct"
  from nofail have nofail_m1: "succeeds m1 s"
    by (simp add: succeeds_bind)
  with ct c1 have term_c1: "Γ⊨c1 ↓ Normal s"
    by (simp add: refines_simpl_def)
  then
  show "Γ⊨c1;;c2 ↓ Normal s"
  proof (rule terminates.intros, intro allI impI)
    fix s'
    assume exec_c1: "Γ⊨ ⟨c1,Normal s⟩ ==> s'" 
    show "Γ⊨c2 ↓ s'"
    proof (cases s')
      case (Normal s1)
      with exec_c1 c1 nofail_m1 term_c1 ct obtain r where sim1: "reaches m1 s (Result r) s1"
        by (force simp add: rel_L1_def refines_simpl_def)
      from c2 [OF nofail_m1 exec_c1 [simplified Normal] this]
      have "refines_simpl ct Γ c2 (m2 r) s1 s1 rel_L1" .
      with ct Normal nofail sim1
      show ?thesis
        by (simp add: refines_simpl_def reaches_bind succeeds_bind)
    qed simp_all
  qed   
next
  fix s'
  assume nofail:  "succeeds (m1 >>= m2) s" 
  from nofail have nofail_m1: "succeeds m1 s"
    by (simp add: succeeds_bind)
  assume exec: "Γ⊨ ⟨c1;;c2,Normal s⟩ ==> Normal s'"
  then show "∃r. reaches (m1 >>= m2) s (Result r) s'"
  proof (cases)
    case (1 s1)
    hence exec_c1: "Γ⊨ ⟨c1,Normal s⟩ ==> s1" and
          exec_c2: "Γ⊨ ⟨c2, s1⟩ ==> Normal s'" .
    from exec_c2 obtain s1' where s1': "s1 = Normal s1'"
      by (meson Normal_resultE)
    from exec_c1 c1 nofail_m1  obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
      by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1) s1' refines_simpl_def xstate.simps(7))


    from c2 [OF nofail_m1 exec_c1[simplified s1'] sim1]
    have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" . 
    with nofail exec_c2 obtain r2 where "reaches (m2 r1) s1' (Result r2) s'"
      by (smt (verit) empty_iff insertE rel_L1_conv(1) s1' sim1 refines_simpl_def succeeds_bind 
          reaches_bind xstate.simps(7))
    with sim1 nofail show ?thesis
      by (fastforce simp add: reaches_bind succeeds_bind)
  qed
next
  fix s'
  assume nofail: "succeeds (m1 >>= m2) s" 
  from nofail have nofail_m1: "succeeds m1 s"
    by (simp add: succeeds_bind)
  assume exec: "Γ⊨ ⟨c1;;c2,Normal s⟩ ==> Abrupt s'"
  then show "∃r. reaches (m1 >>= m2) s (Exn r) s'"
  proof (cases)
    case (1 s1)
    hence exec_c1: "Γ⊨ ⟨c1,Normal s⟩ ==> s1" and
          exec_c2: "Γ⊨ ⟨c2,s1⟩ ==> Abrupt s'" .

    show ?thesis
    proof (cases s1)
      case (Normal s1')
      with exec_c1 c1 nofail_m1  obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
        by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1)  refines_simpl_def xstate.simps(7))
      from c2 [OF nofail_m1 exec_c1[simplified Normal] sim1]
      have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" . 
      with nofail exec_c2 sim1 obtain r2 where "reaches (m2 r1) s1' (Exn r2) s'"
        by (smt (verit) Normal empty_iff insertE rel_L1_conv(2) refines_simpl_def succeeds_bind xstate.simps(11))
      with sim1 nofail show ?thesis
        by (fastforce simp add: reaches_bind succeeds_bind)
    next 
      case (Abrupt s1')
      with exec_c1 c1 nofail_m1  obtain r1 where sim1: "reaches m1 s (Exn r1) s1'"
        by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(2) refines_simpl_def xstate.distinct(7))
      from Abrupt exec_c2 have "s' = s1'"
        by (meson Abrupt_end xstate.inject(2))
      with nofail
      show ?thesis 
        apply (clarsimp simp add: reaches_bind succeeds_bind Exn_def)
        using sim1 by fastforce
    next
      case (Fault x)
      with exec_c2 show ?thesis 
        by (meson Fault_end xstate.distinct(7))
    next
      case Stuck
      with exec_c2 show ?thesis
        using noStuck_startD' by blast
    qed
  qed
next
  fix e   
  assume nofail:  "succeeds (m1 >>= m2) s" 
  from nofail have nofail_m1: "succeeds m1 s"
    by (simp add: succeeds_bind) 
  assume exec: "Γ⊨ ⟨c1;;c2,Normal s⟩ ==> Fault e"
  then show "e ∈ {AssumeError, StackOverflow}"
  proof (cases)
    case (1 s1)
    hence exec_c1: "Γ⊨ ⟨c1,Normal s⟩ ==> s1" and
          exec_c2: "Γ⊨ ⟨c2,s1⟩ ==> Fault e" .
   show ?thesis
    proof (cases s1)
      case (Normal s1')
      with exec_c1 c1 nofail_m1  obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
        by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1)  refines_simpl_def xstate.simps(7))
      from c2 [OF nofail_m1 exec_c1[simplified Normal] sim1]
      have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" . 

      with nofail exec_c2 sim1 show "e ∈ {AssumeError, StackOverflow}"
        by (metis (no_types, lifting) Normal insert_iff rel_L1_conv(3) refines_simpl_def singleton_iff 
            succeeds_bind xstate.inject(3))
    next
      case (Abrupt s1')
      with exec_c2 show ?thesis
        by (metis Abrupt_end xstate.distinct(7))
    next
      case (Fault x)
      with exec_c2 c1 exec_c1 show ?thesis
        by (metis exec_Normal_elim_cases(1) insert_iff nofail_m1 rel_L1_conv(3) refines_simpl_def singleton_iff xstate.inject(3))
    next
      case Stuck
      with exec_c2 show ?thesis
        using noStuck_startD' by blast
    qed
  qed
next
  assume nofail:  "succeeds (m1 >>= m2) s" 
  from nofail have nofail_m1: "succeeds m1 s"
    by (simp add: succeeds_bind) 
  assume exec: "Γ⊨ ⟨c1;;c2,Normal s⟩ ==> Stuck"
  then show False
  proof (cases)
    case (1 s1)
    hence exec_c1: "Γ⊨ ⟨c1,Normal s⟩ ==> s1" and
          exec_c2: "Γ⊨ ⟨c2,s1⟩ ==> Stuck" .
    show ?thesis 
    proof (cases s1)
      case (Normal s1')
      with exec_c1 c1 nofail_m1  obtain r1 where sim1: "reaches m1 s (Result r1) s1'"
        by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(1)  refines_simpl_def xstate.simps(7))
      from c2 [OF nofail_m1 exec_c1[simplified Normal] sim1]
      have "refines_simpl ct Γ c2 (m2 r1) s1' s1' rel_L1" . 
      with nofail exec_c2 sim1 show False
        by (metis Normal insertE rel_L1_conv(4) refines_simpl_def singletonD succeeds_bind xstate.simps(15))
    next
      case (Abrupt s1')
      with exec_c2 show ?thesis
        by (metis Abrupt_end xstate.distinct(10))
    next
      case (Fault x)
      with exec_c2 show ?thesis 
        by (metis Fault_end isFault_simps(4) not_isFault_iff)
    next
      case Stuck
      with exec_c2 c1 exec_c1  show ?thesis
        by (metis insert_iff nofail_m1 rel_L1_conv(4) refines_simpl_def singletonD xstate.simps(15))
    qed
  qed
qed


lemma refines_simpl_rel_L1_catch:
  assumes L: "refines_simpl ct Γ L' L s s rel_L1" 
  assumes R: "∧s. refines_simpl ct Γ R' R s s rel_L1" 
  shows "refines_simpl ct Γ (Catch L' R') (L1_catch L R) s s rel_L1"
proof (rule refines_simpl_rel_L1I)
  assume nofault: "succeeds (L1_catch L R) s" 
  assume ct: "ct" 
  show "Γ⊨TRY L' CATCH R' END ↓ Normal s"
  proof (rule terminates.intros, safe)
    show "Γ⊨L' ↓ Normal s"
      using nofault ct L 
      by (simp add: refines_simpl_def L1_catch_def rel_L1_def succeeds_catch)
  next
    fix s'
    assume " Γ⊨ ⟨L',Normal s⟩ ==> Abrupt s'" 
    then show "Γ⊨R' ↓ Normal s'"
      using nofault ct L R       
      by (fastforce simp add: refines_simpl_def L1_catch_def rel_L1_def succeeds_catch)
  qed
next
  fix s'
  assume nofault:  "succeeds (L1_catch L R) s" 
  assume exec: "Γ⊨ ⟨TRY L' CATCH R' END,Normal s⟩ ==> Normal s'"
  then show "∃r. reaches (L1_catch L R) s (Result r) s'"
  proof (cases)
    case (1 s1)
    hence exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Abrupt s1" and
          exec_R': "Γ⊨ ⟨R',Normal s1⟩ ==> Normal s'".
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" and
      nofault_R: "succeeds R s1"
      by (smt (verit, best) L1_defs(5) case_xval_simps(1) insertE refines_simpl_def 
          rel_L1_conv(2) singletonD succeeds_catch xstate.simps(11))
    from nofault_L exec_L' L obtain r1 where r1: "reaches L s (Exn r1) s1"
      by (metis (no_types, lifting) insertE rel_L1_conv(2) refines_simpl_def 
          singletonD xstate.distinct(7))
    from r1 exec_R' R obtain r2 where  "reaches R s1 (Result r2) s'"
      by (metis (no_types, lifting) insertE nofault_R rel_L1_conv(1) 
          refines_simpl_def singletonD xstate.simps(7))
    with r1 nofault show ?thesis 
      by (fastforce simp add: reaches_catch succeeds_catch L1_defs )
  next
    case 2
    have exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Normal s'" by fact
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" 
      by (simp add: L1_defs(5) succeeds_catch)
    with L exec_L' obtain r1 where "reaches L s (Result r1) s'"
      by (metis (no_types, lifting) insertE rel_L1_conv(1) refines_simpl_def singletonD xstate.distinct(3))
    then show ?thesis using nofault
      by (fastforce simp add: L1_catch_def succeeds_catch reaches_catch)
  qed
next
  fix s'
  assume nofault: "succeeds (L1_catch L R) s"
  assume exec: "Γ⊨ ⟨TRY L' CATCH R' END,Normal s⟩ ==> Abrupt s'"
  then show "∃r. reaches (L1_catch L R) s (Exn r) s'"
  proof (cases)
    case (1 s1)
    hence exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Abrupt s1" and
          exec_R': "Γ⊨ ⟨R',Normal s1⟩ ==> Abrupt s'" .
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" and
      nofault_R: "succeeds R s1"
      by (fastforce simp add: L1_catch_def refines_simpl_def reaches_catch succeeds_catch)

    from nofault_L exec_L' L obtain r1 where r1: "reaches L s (Exn r1) s1"
      by (metis (no_types, lifting) insertE rel_L1_conv(2) refines_simpl_def 
          singletonD xstate.distinct(7))
    from nofault_R r1 exec_R' R obtain r2 where  "reaches R s1 (Exn r2) s'"
      by (metis (no_types, lifting) empty_iff insertE rel_L1_conv(2) refines_simpl_def xstate.distinct(7))
    with r1 nofault show ?thesis 
      by (fastforce simp add: L1_catch_def succeeds_catch reaches_catch)
  next
    case 2
    then show ?thesis by simp
  qed
next
  fix e
  assume nofault: "succeeds (L1_catch L R) s"
  assume exec: "Γ⊨ ⟨TRY L' CATCH R' END,Normal s⟩ ==> Fault e"
  then show "e ∈ {AssumeError, StackOverflow}"
  proof (cases)
    case (1 s1)
    hence exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Abrupt s1" and
          exec_R': "Γ⊨ ⟨R',Normal s1⟩ ==> Fault e" .
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" and
      nofault_R: "succeeds R s1"
      by (fastforce simp add: L1_catch_def refines_simpl_def reaches_catch succeeds_catch)
    from nofault_L exec_L' L obtain r1 where r1: "reaches L s (Exn r1) s1"
      by (metis (no_types, lifting) insertE rel_L1_conv(2) refines_simpl_def 
          singletonD xstate.distinct(7))
    from nofault_R r1 exec_R' R show ?thesis
      by (metis insert_iff rel_L1_conv(3) refines_simpl_def singletonD xstate.inject(3))
  next
    case 2
    have exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Fault e" by fact
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" 
      by (simp add: L1_defs(5) succeeds_catch)
    with L exec_L' show ?thesis 
      by (metis insertCI insertE rel_L1_conv(3) refines_simpl_def singleton_iff xstate.inject(3))
  qed
next
  assume nofault: "succeeds (L1_catch L R) s"  
  assume exec: "Γ⊨ ⟨TRY L' CATCH R' END,Normal s⟩ ==> Stuck"
  then show False
  proof (cases)
    case (1 s1)
    hence exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Abrupt s1" and
          exec_R': "Γ⊨ ⟨R',Normal s1⟩ ==> Stuck" .
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" and
      nofault_R: "succeeds R s1"
      by (fastforce simp add: L1_catch_def refines_simpl_def reaches_catch succeeds_catch)

    from nofault_R exec_R' R show ?thesis
      by (metis empty_iff insertE rel_L1_conv(4) refines_simpl_def xstate.distinct(11))
  next
    case 2
    have exec_L': "Γ⊨ ⟨L',Normal s⟩ ==> Stuck" by fact
    from nofault L R exec_L' obtain
      nofault_L: "succeeds L s" 
      by (simp add: L1_defs(5) succeeds_catch)
    with L exec_L' show ?thesis 
      by (metis insertE rel_L1_conv(4) refines_simpl_def singletonD xstate.distinct(11))
  qed
qed




lemmas refines_simpl_cleanup = L1corres_refines_simpl [OF L1_corres_cleanup]
lemmas refines_simpl_cleanup_throw = L1corres_refines_simpl [OF L1_corres_cleanup_throw]
lemmas refines_simpl_spec_cleanup = L1corres_refines_simpl [OF L1_corres_spec_cleanup]
lemmas refines_simpl_spec_cleanup_throw = L1corres_refines_simpl [OF L1_corres_spec_cleanup_throw]

lemma refines_simpl_rel_L1_on_exit': 
  fixes m:: "'s L1_monad"
  assumes m_c: "refines_simpl ct Γ c m s s rel_L1"
  shows "refines_simpl ct Γ (On_Exit c (Basic cleanup)) (on_exit m {(s,t). t = cleanup s}) s s rel_L1"
  unfolding on_exit_catch_conv
  apply (simp add: On_Exit_def)
  apply (rule refines_simpl_rel_L1_bind)
   apply (simp add: L1_catch_def [symmetric])
   apply (rule refines_simpl_rel_L1_catch [OF m_c])
   apply (rule refines_simpl_cleanup_throw [simplified])
  apply (rule refines_simpl_cleanup [simplified])
  done

lemma refines_simpl_rel_L1_on_exit: 
  fixes m:: "'s L1_monad"
  assumes m_c: "refines_simpl ct Γ c m s s rel_L1"
  shows "refines_simpl ct Γ (On_Exit c (com.Spec cleanup)) (on_exit m cleanup) s s rel_L1"
  apply (simp add: on_exit_catch_conv On_Exit_def)
  apply (rule refines_simpl_rel_L1_bind)
   apply (simp add: L1_catch_def [symmetric])
   apply (rule refines_simpl_rel_L1_catch [OF m_c])
   apply (rule refines_simpl_spec_cleanup_throw [simplified])
  apply (rule refines_simpl_spec_cleanup [simplified])
  done


named_theorems L1corres_with_fresh_stack_ptr

context stack_heap_state 
begin
lemma refines_simpl_rel_L1_with_fresh_stack_ptr: 
  fixes m:: "'a::mem_type ptr ==> 's L1_monad"
  assumes c_m: "∧p s. refines_simpl ct Γ (c p) (m p) s s rel_L1"
  shows "refines_simpl ct Γ (With_Fresh_Stack_Ptr n I c) (with_fresh_stack_ptr n I m) s s rel_L1"
  apply (simp add: with_fresh_stack_ptr_def With_Fresh_Stack_Ptr_def)
  apply (rule refines_simpl_StackOverflow)
  apply (rule refines_simpl_DynCom)
  apply (rule refines_simpl_rel_L1_bind)
  subgoal
    apply (rule refines_simpl_rel_L1I)
    subgoal
      by (simp add: terminates.Spec)
    subgoal for s'
      apply (erule exec_Normal_elim_cases)
      subgoal for t   
        by (auto simp add: succeeds_assume_result_and_state)
      by auto
    subgoal for s'
      by (meson exec_Normal_elim_cases(7) xstate.distinct(9) xstate.simps(5))
    subgoal for e
      by (meson exec_Normal_elim_cases(7) xstate.distinct(11) xstate.simps(7))
    subgoal
      apply (erule exec_Normal_elim_cases)
      using Ex_list_of_length by auto blast
    done
  apply (rule refines_simpl_DynCom)
  apply (clarsimp)
  apply (simp add: stack_allocs_allocated_ptrs)
  apply (rule refines_simpl_rel_L1_on_exit[OF c_m])
  done

lemma L1corres_with_fresh_stack_ptr[L1corres_with_fresh_stack_ptr]: 
  fixes m:: "'a::mem_type ptr ==> 's L1_monad"
  assumes c_m: "∧p. L1corres ct Γ (m p) (c p)"
  shows "L1corres ct Γ (with_fresh_stack_ptr n I m) (With_Fresh_Stack_Ptr n I c)"
  apply (rule refines_simpl_L1corres)
  apply (rule refines_simpl_rel_L1_with_fresh_stack_ptr)
  apply (rule L1corres_refines_simpl)
  apply (rule c_m)
  done
end

lemma L1corres_exec_spec_monad:
  assumes l: "lense get_x upd_x"
  shows "L1corres ct Γ (L1_exec_spec_monad upd_x st args f res) (exec_spec_monad get_x upd_x st args f res)"
proof -
  from l interpret l: lense get_x upd_x .
  show ?thesis
  proof (clarsimp simp add: L1corres_def; safe)
    fix s t 
    assume succeeds: "succeeds (L1_exec_spec_monad upd_x st args f res) s"
    assume exec: "Γ⊨ ⟨exec_spec_monad get_x upd_x st args f res,Normal s⟩ ==> t" 
    show  "case t of
           Normal x ==>
             reaches (L1_exec_spec_monad upd_x st args f res) s (Result ()) x
           | Abrupt x ==> reaches (L1_exec_spec_monad upd_x st args f res) s (Exn ()) x
           | Fault e ==> e ∈ {AssumeError, StackOverflow} | Stuck ==> False"
    proof -
      from succeeds exec show ?thesis
        apply (simp add: L1_exec_spec_monad_def exec_spec_monad_def)
        apply (erule exec_Normal_elim_cases)
        subgoal 
          apply (auto simp add: succeeds_bind succeeds_bind_handle)
          apply (erule exec_Normal_elim_cases)
          apply (simp add: assume_Spec_def guarded_spec_body_def)
          apply (erule exec_Normal_elim_cases)
          subgoal for s'
            apply auto
            apply (erule exec_Normal_elim_cases)
            subgoal for b x1 s1 t1
              apply clarsimp
              subgoal for x2 s2
                apply (erule allE [where x="x2"])
                apply (erule allE [where x="s2"])
                apply (clarsimp simp add: reaches_exec_abstract)
                apply (fastforce split: xval_splits 
                    simp add: default_option_def L1_exec_spec_monad_def reaches_bind 
                    L1_modify_def L1_seq_def L1_throw_def
                    case_exception_or_result_iff succeeds_bind
                    reaches_exec_abstract reaches_bind_handle succeeds_bind succeeds_bind_handle
                    elim!: exec_Normal_elim_cases)
                done
              done
            subgoal
              by clarsimp
            done
          subgoal
            apply clarsimp
            apply (erule exec_Normal_elim_cases)
            apply (auto simp add: L1_exec_spec_monad_def reaches_bind )
            done
          done
        subgoal
          by (auto simp add: succeeds_bind succeeds_bind_handle)
        done
    qed
  next
    fix s 
    assume succeeds: "succeeds (L1_exec_spec_monad upd_x st args f res) s" 
    assume "ct"  
    show "Γ⊨exec_spec_monad get_x upd_x st args f res ↓ Normal s"
    proof -
      from succeeds show ?thesis
        apply (auto simp add: L1_exec_spec_monad_def exec_spec_monad_def succeeds_bind_handle succeeds_bind reaches_exec_abstract)
        apply (rule terminates.intros)
        subgoal by blast
        apply (rule terminates.intros)
        subgoal 
          apply (simp add: assume_Spec_def guarded_spec_body_def) 
          apply (rule terminates_Guard')
          apply (rule terminates.intros)
          done
        subgoal
          apply (clarsimp simp add: assume_Spec_def guarded_spec_body_def)

          apply (erule exec_Normal_elim_cases)
          subgoal 
            apply (auto split: xval_splits)
            by (metis (lifting) Abrupt Fault Stuck terminates.CondFalse terminates.CondTrue
                terminates.Throw terminates_Skip' terminates_elim_cases(1))
          subgoal
            by (auto)
          done
        done
    qed
  qed 
qed


(*
 * Implementation of functions that have no bodies.
 *
 * For example, if the user has a call to an "extern" function,
 * but no body is available to the C parser, we do not have any
 * SIMPL to translate. We instead use the following definition.
 *)

definition "UNDEFINED_FUNCTION ≡ False"

definition
  undefined_function_body :: "('a, int, strictc_errortype) com"
where
  "undefined_function_body ≡ Guard (UndefinedFunction {}) {x. UNDEFINED_FUNCTION} SKIP"



definition
  init_return_undefined_function_body::"(('a ==> 'a) ==> (('g, 'l, 'e, 'z) state_scheme ==> ('g, 'l, 'e, 'z) state_scheme))
      ==> (('g, 'l, 'e, 'z) state_scheme, int, strictc_errortype) com" 
where
  "init_return_undefined_function_body ret ≡ Seq (lvar_nondet_init ret) (Guard (UndefinedFunction {}) {x. UNDEFINED_FUNCTION} SKIP)"


lemma L1corres_undefined_call:
    "L1corres ct Γ ((L1_seq (L1_guard (L1_set_to_pred {x. UNDEFINED_FUNCTION})) L1_skip)) (Call X')"
  by (clarsimp simp: L1corres_def L1_defs UNDEFINED_FUNCTION_def)

lemma L1_UNDEFINED_FUNCTION_fail: "(L1_guard (L1_set_to_pred {x. UNDEFINED_FUNCTION})) = L1_fail"
  apply (clarsimp simp add: L1_defs UNDEFINED_FUNCTION_def)
  by (simp add: run_guard spec_monad_ext)

lemma L1_seq_fail: "L1_seq L1_fail X = L1_fail"
  apply (clarsimp simp add: L1_defs)
  done

lemma L1_seq_init_fail: "(L1_seq (L1_init ret) L1_fail) = L1_fail"
  apply (clarsimp simp add: L1_defs)
  apply (rule spec_monad_eqI)
  apply (auto simp add: runs_to_iff)
  done

lemma L1_corres_L1_fail: "L1corres ct Γ L1_fail X"
  by (simp add: L1corres_def L1_defs)

lemma L1corres_init_return_undefined_call:
    "L1corres ct Γ (L1_seq (L1_init ret) ((L1_seq (L1_guard (L1_set_to_pred {x. UNDEFINED_FUNCTION})) L1_skip))) (Call X')"
  by (simp only: L1_UNDEFINED_FUNCTION_fail L1_seq_fail L1_seq_init_fail L1_corres_L1_fail)


(* Unfolding rules to run prior to L1 translation. *)
named_theorems L1unfold
(* L1 postprocessing rules, used by ExceptionRewrite and SimplConv. *)
named_theorems L1except

lemma signed_bounds_one_to_nat: "n <s 1 ==> 0 ≤s n ==> unat n = 0"
  by (metis signed.leD unat_1_0 unat_gt_0 unsigned_eq_0_iff word_msb_0 word_sle_msb_le)

lemma signed_bounds_to_nat_boundsF: "n <s numeral B ==> 0 ≤s n ==> unat n < numeral B"
  by (metis linorder_not_less of_nat_numeral signed.leD unat_less_helper word_msb_0 word_sle_msb_le)

lemma word_bounds_to_nat_boundsF: "(n::'a::len word) < numeral B ==> unat n < numeral B"
  by (simp add: unat_less_helper)

lemma word_bounds_one_to_nat: "(n::'a::len word) < 1 ==> unat n = 0"
  by (simp add: unat_less_helper)

lemma monotone_L1_seq_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  assumes mono_Y: "monotone R (≤) Y"
  shows "monotone R (≤)
    (λf. (L1_seq (X f) (Y f)))"
  unfolding L1_defs
  apply (intro partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma monotone_L1_seq_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  assumes mono_Y: "monotone R (≥) Y"
  shows "monotone R (≥)
    (λf. (L1_seq (X f) (Y f)))"
  unfolding L1_defs
  apply (intro partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma L1_seq_mono [monad_mono_intros]:
  assumes [monad_mono_intros]:"g1 ≤ g2" "f1 ≤ f2"  shows "L1_seq f1 g1 ≤ L1_seq f2 g2"
  unfolding L1_defs
  by (intro monad_mono_intros le_funI)

lemma monotone_L1_catch_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  assumes mono_Y: "monotone R (≤) Y"
  shows "monotone R (≤)
    (λf. (L1_catch (X f) (Y f)))"
  unfolding L1_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma monotone_L1_catch_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  assumes mono_Y: "monotone R (≥) Y"
  shows "monotone R (≥)
    (λf. (L1_catch (X f) (Y f)))"
  unfolding L1_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma L1_catch_mono [monad_mono_intros]:
  assumes [monad_mono_intros]:"f1 ≤ f2" "g1 ≤ g2" shows "L1_catch f1 g1 ≤ L1_catch f2 g2"
  unfolding L1_defs
  by (intro monad_mono_intros le_funI)

lemma monotone_L1_condition_le [partial_function_mono]:
  assumes mono_X: "monotone R (≤) X"
  assumes mono_Y: "monotone R (≤) Y"
  shows "monotone R (≤)
    (λf. (L1_condition C (X f) (Y f)))"
  unfolding L1_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma monotone_L1_condition_ge [partial_function_mono]:
  assumes mono_X: "monotone R (≥) X"
  assumes mono_Y: "monotone R (≥) Y"
  shows "monotone R (≥)
    (λf. (L1_condition C (X f) (Y f)))"
  unfolding L1_defs
  apply (rule partial_function_mono)
   apply (rule mono_X)
  apply (rule mono_Y)
  done

lemma L1_condition_mono [monad_mono_intros]:
  assumes [monad_mono_intros]:"f1 ≤ f2" "g1 ≤ g2" shows "L1_condition c f1 g1 ≤ L1_condition c f2 g2"
  unfolding L1_defs
  by (intro monad_mono_intros le_funI)

lemma monotone_guard: "monotone R (≥) C ==> monotone R (≤) (λf. guard (C f))"
  apply (auto simp add: monotone_def guard_def assert_def)
  apply (rule mono_bind)
  apply (auto simp add: le_fun_def )
  done

lemma monotone_L1_guard: "monotone R (≥) C ==> monotone R (≤) (λf. L1_guard (C f))"
  unfolding L1_guard_def
  by (rule monotone_guard)

lemma monotone_L1_guarded_le [partial_function_mono]:
  assumes mono_X [partial_function_mono]: "monotone R (≥) C" "monotone R (≤) X"
  shows "monotone R (≤)
    (λf. (L1_guarded (C f) (X f)))"
  unfolding L1_guarded_def
  apply (rule partial_function_mono monotone_L1_guard)+
  done

(*
monotone (%x. guard (%s. P x s)) und dann !!x. monotone (%x. P x s) aber bei P bin ich mir nicht sicher ob es monotone oder antitone sein muss
3:06

*)
thm monotone_def
lemma monotone_guard': "(∧s. monotone R (≤) (λf. C f s)) ==> monotone R (≥) (λf. guard (C f))"
  apply (auto simp add: monotone_def guard_def assert_def)
  apply (rule mono_bind)
   apply (auto simp add: le_fun_def )
  done

lemma monotone_guard'': "(monotone R (fun_ord (≤)) (λf s. C f s)) ==> monotone R (≥) (λf. guard (C f))"
  apply (auto simp add: monotone_def guard_def assert_def)
  apply (rule mono_bind)
   apply (auto simp add: le_fun_def fun_ord_def)
  done


lemma monotone_L1_guard': "(∧s. monotone R (≤) (λf. C f s)) ==> monotone R (≥) (λf. L1_guard (C f))"
  unfolding L1_guard_def
  by (rule monotone_guard')

lemma monotone_L1_guard'': "(monotone R (fun_ord (≤)) (λf s. C f s)) ==> monotone R (≥) (λf. L1_guard (C f))"
  unfolding L1_guard_def
  by (rule monotone_guard'')

lemma monotone_L1_guarded_ge' [partial_function_mono ]: (* FIXME *)
  assumes mono_X [partial_function_mono]: "(∧s. monotone R (≤) (λf. C f s))" "monotone R (≥) X"
  shows "monotone R (≥)
    (λf. (L1_guarded (C f) (X f)))"
  unfolding L1_guarded_def
  apply (rule partial_function_mono monotone_L1_guard')+
  done
(*
lemma monotone_L1_guarded_ge'' [partial_function_mono]:
  assumes mono_X [partial_function_mono]: "(monotone R (fun_ord (\<le>)) (\<lambda>f s. C f s))" "monotone R (\<ge>) X"
  shows "monotone R (\<ge>) 
    (\<lambda>f. (L1_guarded (C f) (X f)))"
  unfolding L1_guarded_def
  apply (rule partial_function_mono monotone_L1_guard'')+
  done
*)
(*
lemma monotone_L1_guarded_ge [partial_function_mono]:
  assumes mono_X [partial_function_mono]: "monotone R (\<le>) C" "monotone R (\<ge>) X"
  shows "monotone R (\<ge>) 
    (\<lambda>f. (L1_guarded (C f) (X f)))"
  unfolding L1_guarded_def
  apply (rule partial_function_mono monotone_L1_guard')+
  done
*)
lemma L1_guarded_mono [monad_mono_intros]:
  assumes [monad_mono_intros]:"f ≤ g" shows "L1_guarded c f ≤ L1_guarded c g"
  unfolding L1_defs L1_guarded_def
  by (intro monad_mono_intros le_funI order.refl)


lemma monotone_L1_while_le [partial_function_mono]:
  assumes mono_B: "monotone R (≤) (λf. B f)"
  shows "monotone R (≤) (λf. L1_while C (B f))"
  unfolding L1_defs
  apply (rule partial_function_mono)
  apply (rule mono_B)
  done

lemma monotone_L1_while_ge [partial_function_mono]:
  assumes mono_B: "monotone R (≥) (λf. B f)"
  shows "monotone R (≥) (λf. L1_while C (B f))"
  unfolding L1_defs
  apply (rule partial_function_mono)
  apply (rule mono_B)
  done

lemma L1_while_mono [monad_mono_intros]:
  assumes [monad_mono_intros]:"f ≤ g" shows "L1_while c f ≤ L1_while c g"
  unfolding L1_defs
  by (intro monad_mono_intros le_funI)

lemma monotone_L1_call_le [partial_function_mono]: 
  assumes X[partial_function_mono]:  "monotone R (≤) X" 
  shows "monotone R (≤)
    (λf. L1_call scope_setup (X f) scope_teardown result_exn return_xf)"
  unfolding L1_call_def
  apply (rule partial_function_mono)+
  done

lemma monotone_L1_call_ge [partial_function_mono]: 
  assumes X[partial_function_mono]:  "monotone R (≥) X" 
  shows "monotone R (≥)
    (λf. L1_call scope_setup (X f) scope_teardown result_exn return_xf)"
  unfolding L1_call_def
  apply (rule partial_function_mono)+
  done

lemma L1_call_mono [monad_mono_intros]:
  assumes [monad_mono_intros]:"f ≤ g" 
  shows "L1_call scope_setup f scope_teardown result_exn result_xf ≤ L1_call scope_setup g scope_teardown result_exn result_xf"
  unfolding L1_defs L1_call_def
  by (intro monad_mono_intros le_funI order.refl)

lemma monotone_L1_dyn_call_map_of_default_le [partial_function_mono]:
  assumes [partial_function_mono]: "∧x. monotone R (≤) (λf. map_of_default (λ_. ⊤) (ps f) x)"
  shows "monotone R (≤)
    (λf. L1_dyn_call_map_of_default g scope_setup dest (ps f) scope_teardown result_exn return_xf)"
  unfolding L1_dyn_call_map_of_default_def 
  by (intro partial_function_mono)

lemma monotone_L1_dyn_call_map_of_default_ge [partial_function_mono]:
  assumes [partial_function_mono]: "∧x. monotone R (≥) (λf. map_of_default (λ_. ⊤) (ps f) x)"
  shows "monotone R (≥)
    (λf. L1_dyn_call_map_of_default g scope_setup dest (ps f) scope_teardown result_exn return_xf)"
  unfolding L1_dyn_call_map_of_default_def 
  by (intro partial_function_mono)

lemma L1_dyn_call_map_of_default [monad_mono_intros]:
  assumes [monad_mono_intros]: "∧x. map_of_default (λ_. ⊤) ps x ≤ map_of_default (λ_. ⊤) qs x" 
  shows "L1_dyn_call_map_of_default g scope_setup dest ps scope_teardown result_exn result_xf ≤ L1_dyn_call_map_of_default g scope_setup dest qs scope_teardown result_exn result_xf"
  unfolding L1_dyn_call_map_of_default_def 
  by (intro monad_mono_intros le_funI order.refl)

end