Theory Wasm_Properties_Aux

section ‹Auxiliary Type System Properties›

theory Wasm_Properties_Aux imports Wasm_Axioms begin

lemma typeof_i32:
  assumes "typeof v = T_i32"
  shows "∃c. v = ConstInt32 c"
  using assms
  unfolding typeof_def
  by (cases v) auto

lemma typeof_i64:
  assumes "typeof v = T_i64"
  shows "∃c. v = ConstInt64 c"
  using assms
  unfolding typeof_def
  by (cases v) auto

lemma typeof_f32:
  assumes "typeof v = T_f32"
  shows "∃c. v = ConstFloat32 c"
  using assms
  unfolding typeof_def
  by (cases v) auto

lemma typeof_f64:
  assumes "typeof v = T_f64"
  shows "∃c. v = ConstFloat64 c"
  using assms
  unfolding typeof_def
  by (cases v) auto

lemma exists_v_typeof: "∃v v. typeof v = t"
proof (cases t)
  case T_i32
  fix v
  have "typeof (ConstInt32 v) = t"
    using T_i32
    unfolding typeof_def
    by simp
  thus ?thesis
    using T_i32
    by fastforce
next
  case T_i64
  fix v
  have "typeof (ConstInt64 v) = t"
    using T_i64
    unfolding typeof_def
    by simp
  thus ?thesis
    using T_i64
    by fastforce
next
  case T_f32
  fix v
  have "typeof (ConstFloat32 v) = t"
    using T_f32
    unfolding typeof_def
    by simp
  thus ?thesis
    using T_f32
    by fastforce
next
  case T_f64
  fix v
  have "typeof (ConstFloat64 v) = t"
    using T_f64
    unfolding typeof_def
    by simp
  thus ?thesis
    using T_f64
    by fastforce
qed

lemma lfilled_collapse1:
  assumes "Lfilled n lholed (vs@es) LI"
          "const_list vs"
          "length vs ≥ l"
  shows "∃lholed'. Lfilled n lholed' ((drop (length vs - l) vs)@es) LI"
  using assms(1)
proof (induction "vs@es" LI rule: Lfilled.induct)
  case (L0 vs' lholed es')
  obtain vs1 vs2 where "vs = vs1@vs2" "length vs2 = l"
    using assms(3)
    by (metis append_take_drop_id diff_diff_cancel length_drop)
  moreover
  hence "const_list (vs'@vs1)"
    using L0(1) assms(2)
    unfolding const_list_def
    by simp
  ultimately
  show ?case
    using Lfilled.intros(1)[of "vs'@vs1" _ es' "vs2@es"]
      by fastforce
next
  case (LN vs lholed n es' l es'' k lfilledk)
  thus ?case
    using Lfilled.intros(2)
    by fastforce
qed

lemma lfilled_collapse2:
  assumes "Lfilled n lholed (es@es') LI"
  shows "∃lholed' vs'. Lfilled n lholed' es LI"
  using assms
proof (induction "es@es'" LI rule: Lfilled.induct)
  case (L0 vs lholed es')
  thus ?case
    using Lfilled.intros(1)
    by fastforce
next
  case (LN vs lholed n es' l es'' k lfilledk)
  thus ?case
    using Lfilled.intros(2)
    by fastforce
qed

lemma lfilled_collapse3:
  assumes "Lfilled k lholed [Label n les es] LI"
  shows "∃lholed'. Lfilled (Suc k) lholed' es LI"
  using assms
proof (induction "[Label n les es]" LI rule: Lfilled.induct)
  case (L0 vs lholed es')
  have "Lfilled 0 (LBase [] []) es es"
    using Lfilled.intros(1)
    unfolding const_list_def
    by (metis append.left_neutral append_Nil2 list_all_simps(2))
  thus ?case
    using Lfilled.intros(2) L0
    by fastforce
next
  case (LN vs lholed n es' l es'' k lfilledk)
  thus ?case
    using Lfilled.intros(2)
    by fastforce
qed


lemma unlift_b_e: assumes "𝒮∙𝒞 ⊢ $*b_es : tf" shows "𝒞 ⊢ b_es : tf"
using assms proof (induction "𝒮" "𝒞" "($*b_es)" "tf" arbitrary: b_es)
  case (1 𝒞 b_es tf 𝒮)
  then show ?case
    using inj_basic map_injective
    by auto
next
  case (2 𝒮 𝒞 es t1s t2s e t3s)
  obtain es' e' where "es' @ [e'] = b_es"
    using 2(5)
    by (simp add: snoc_eq_iff_butlast)
  then show ?case using 2
    using b_e_typing.composition
    by fastforce
next                            
  case (3 𝒮 𝒞 t1s t2s ts)
  then show ?case
    using b_e_typing.weakening
    by blast
qed auto

lemma store_typing_imp_inst_length_eq:
  assumes "store_typing s 𝒮"
  shows "length (inst s) = length (s_inst 𝒮)"
  using assms list_all2_lengthD
  unfolding store_typing.simps
  by fastforce

lemma store_typing_imp_func_length_eq:
  assumes "store_typing s 𝒮"
  shows "length (funcs s) = length (s_funcs 𝒮)"
  using assms list_all2_lengthD
  unfolding store_typing.simps
  by fastforce

lemma store_typing_imp_mem_length_eq:
  assumes "store_typing s 𝒮"
  shows "length (s.mem s) = length (s_mem 𝒮)"
  using assms list_all2_lengthD
  unfolding store_typing.simps
  by fastforce

lemma store_typing_imp_glob_length_eq:
  assumes "store_typing s 𝒮"
  shows "length (globs s) = length (s_globs 𝒮)"
  using assms list_all2_lengthD
  unfolding store_typing.simps
  by fastforce

lemma store_typing_imp_inst_typing:
  assumes "store_typing s 𝒮"
          "i < length (inst s)"
  shows "inst_typing 𝒮 ((inst s)!i) ((s_inst 𝒮)!i)"
  using assms
  unfolding list_all2_conv_all_nth store_typing.simps
  by fastforce

lemma stab_typed_some_imp_member:
  assumes "stab s i c = Some cl"
          "store_typing s 𝒮"
          "i < length (inst s)"
  shows "Some cl ∈ set (concat (s.tab s))"
proof -
  obtain k' where k_def:"inst.tab ((inst s)!i) = Some k'"
                       "length ((s.tab s)!k') > c"
                       "((s.tab s)!k')!c = Some cl"
    using stab_unfold assms(1,3)
    by fastforce
  hence "Some cl ∈ set ((s.tab s)!k')"
    using nth_mem
    by fastforce
  moreover
  have "inst_typing 𝒮 ((inst s)!i) ((s_inst 𝒮)!i)"
    using assms(2,3) store_typing_imp_inst_typing
    by blast
  hence "k' < length (s_tab 𝒮)"
    using k_def(1)
    unfolding inst_typing.simps stypes_def
    by auto
  hence "k' < length (s.tab s)"
    using assms(2) list_all2_lengthD
    unfolding store_typing.simps
    by fastforce
  ultimately
  show ?thesis
    using k_def
    by auto
qed

lemma stab_typed_some_imp_cl_typed:
  assumes "stab s i c = Some cl"
          "store_typing s 𝒮"
          "i < length (inst s)"
  shows "∃tf. cl_typing 𝒮 cl tf"
proof -
  have "Some cl ∈ set (concat (s.tab s))"
    using assms stab_typed_some_imp_member
    by auto
  moreover
  have "list_all (tab_agree 𝒮) (concat (s.tab s))"
    using assms(2)
    unfolding store_typing.simps
    by auto
  ultimately
  show ?thesis
    unfolding in_set_conv_nth list_all_length tab_agree_def
    by fastforce
qed

lemma b_e_type_empty1[dest]: assumes "𝒞 ⊢ [] : (ts _> ts')" shows "ts = ts'"
  using assms
  by (induction "[]::(b_e list)" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, simp_all)

lemma b_e_type_empty: "(𝒞 ⊢ [] : (ts _> ts')) = (ts = ts')"
proof (safe)
  assume "𝒞 ⊢ [] : (ts _> ts')"
  thus "ts = ts'"
    by blast
next
  assume "ts = ts'"
  thus "𝒞 ⊢ [] : (ts' _> ts')"
    using b_e_typing.empty b_e_typing.weakening
    by fastforce
qed

lemma b_e_type_value:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = C v"
  shows "ts' = ts @ [typeof v]"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_load:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Load t tp_sx a off"
  shows "∃ts'' sec n. ts = ts''@[T_i32] ∧ ts' = ts''@[t] ∧ (memory 𝒞) = Some n"
        "load_store_t_bounds a (option_projl tp_sx) t"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_store:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Store t tp a off"
    shows "ts = ts'@[T_i32, t]"
          "∃sec n. (memory 𝒞) = Some n"
          "load_store_t_bounds a tp t"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_current_memory:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Current_memory"
  shows "∃sec n. ts' = ts @ [T_i32] ∧ (memory 𝒞) = Some n"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_grow_memory:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Grow_memory"
  shows "∃ts''. ts = ts''@[T_i32] ∧ ts = ts' ∧ (∃n. (memory 𝒞) = Some n)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct) auto

lemma b_e_type_nop:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Nop"
  shows "ts = ts'"
  using assms
  by (induction "[e]"  "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

definition arity_2_result :: "b_e ⇒ t" where
  "arity_2_result op2 = (case op2 of
                           Binop_i t _ ⇒ t
                         | Binop_f t _ ⇒ t
                         | Relop_i t _ ⇒ T_i32
                         | Relop_f t _ ⇒ T_i32)"

lemma b_e_type_binop_relop:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Binop_i t iop ∨ e = Binop_f t fop ∨ e = Relop_i t irop ∨ e = Relop_f t frop"
  shows "∃ts''. ts = ts''@[t,t] ∧ ts' = ts''@[arity_2_result(e)]"
        "e = Binop_f t fop ⟹ is_float_t t"
        "e = Relop_f t frop ⟹ is_float_t t"
  using assms
  unfolding arity_2_result_def
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_testop_drop_cvt0:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Testop t testop ∨ e = Drop ∨ e = Cvtop t1 cvtop t2 sx"
  shows "ts ≠ []"
  using assms
  by (induction "[e]" "ts _> ts'" arbitrary: ts' rule: b_e_typing.induct, auto)

definition arity_1_result :: "b_e ⇒ t" where
  "arity_1_result op1 = (case op1 of
                           Unop_i t _ ⇒ t
                         | Unop_f t _ ⇒ t
                         | Testop t _ ⇒ T_i32
                         | Cvtop t1 Convert _ _ ⇒ t1
                         | Cvtop t1 Reinterpret _ _ ⇒ t1)"

lemma b_e_type_unop_testop:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Unop_i t iop ∨ e = Unop_f t fop ∨ e = Testop t testop"
  shows "∃ts''. ts = ts''@[t] ∧ ts' = ts''@[arity_1_result e]"
        "e = Unop_f t fop ⟹ is_float_t t"
  using assms int_float_disjoint
  unfolding arity_1_result_def
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct) fastforce+

lemma b_e_type_cvtop:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Cvtop t1 cvtop t sx"
  shows "∃ts''. ts = ts''@[t] ∧ ts' = ts''@[arity_1_result e]"
        "cvtop = Convert ⟹ (t1 ≠ t) ∧ (sx = None) = ((is_float_t t1 ∧ is_float_t t) ∨ (is_int_t t1 ∧ is_int_t t ∧ (t_length t1 < t_length t)))"
        "cvtop = Reinterpret ⟹ (t1 ≠ t) ∧ t_length t1 = t_length t"
  using assms
  unfolding arity_1_result_def
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_drop:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Drop"
  shows "∃t. ts = ts'@[t]"
  using assms b_e_type_testop_drop_cvt0
by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_select:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Select"
  shows "∃ts'' t. ts = ts''@[t,t,T_i32] ∧ ts' = ts''@[t]"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_call:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Call i"
  shows  "i < length (func_t 𝒞)"
         "∃ts'' tf1 tf2. ts = ts''@tf1 ∧ ts' = ts''@tf2 ∧ (func_t 𝒞)!i = (tf1 _> tf2)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_call_indirect:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Call_indirect i"
  shows "i < length (types_t 𝒞)"
        "∃ts'' tf1 tf2. ts = ts''@tf1@[T_i32] ∧ ts' = ts''@tf2 ∧ (types_t 𝒞)!i = (tf1 _> tf2)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_get_local:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Get_local i"
  shows "∃t. ts' = ts@[t] ∧ (local 𝒞)!i = t" "i < length(local 𝒞)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_set_local:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Set_local i"
  shows "∃t. ts = ts'@[t] ∧ (local 𝒞)!i = t" "i < length(local 𝒞)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_tee_local:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Tee_local i"
  shows "∃ts'' t. ts = ts''@[t] ∧ ts' = ts''@[t] ∧ (local 𝒞)!i = t" "i < length(local 𝒞)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_get_global:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Get_global i"
  shows "∃t. ts' = ts@[t] ∧ tg_t((global 𝒞)!i) = t" "i < length(global 𝒞)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_set_global:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Set_global i"
  shows "∃t. ts = ts'@[t] ∧ (global 𝒞)!i = ⦇tg_mut = T_mut, tg_t = t⦈ ∧ i < length(global 𝒞)"
  using assms is_mut_def
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct) auto

lemma b_e_type_block:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Block tf es"
  shows "∃ts'' tfn tfm. tf = (tfn _> tfm) ∧ (ts = ts''@tfn) ∧ (ts' = ts''@tfm) ∧
                        (𝒞⦇label :=  [tfm] @ label 𝒞⦈ ⊢ es : tf)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_loop:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Loop tf es"
  shows "∃ts'' tfn tfm. tf = (tfn _> tfm) ∧ (ts = ts''@tfn) ∧ (ts' = ts''@tfm) ∧
                        (𝒞⦇label :=  [tfn] @ label 𝒞⦈ ⊢ es : tf)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_if:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = If tf es1 es2"
  shows "∃ts'' tfn tfm. tf = (tfn _> tfm) ∧ (ts = ts''@tfn @ [T_i32]) ∧ (ts' = ts''@tfm) ∧
                        (𝒞⦇label := [tfm] @ label 𝒞⦈ ⊢ es1 : tf) ∧
                        (𝒞⦇label := [tfm] @ label 𝒞⦈ ⊢ es2 : tf)"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_br:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Br i"
        shows "i < length(label 𝒞)"
              "∃ts_c ts''. ts = ts_c @ ts'' ∧ (label 𝒞)!i = ts''"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_br_if:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Br_if i"
        shows "i < length(label 𝒞)"
              "∃ts_c ts''. ts = ts_c @ ts'' @ [T_i32] ∧ ts' = ts_c @ ts'' ∧ (label 𝒞)!i = ts''"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_br_table:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Br_table is i"
  shows "∃ts_c ts''. list_all (λi. i < length(label 𝒞) ∧ (label 𝒞)!i = ts'') (is@[i]) ∧ ts = ts_c @ ts''@[T_i32]"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, fastforce+)

lemma b_e_type_return:
  assumes "𝒞 ⊢ [e] : (ts _> ts')"
          "e = Return"
        shows "∃ts_c ts''. ts = ts_c @ ts'' ∧ (return 𝒞) = Some ts''"
  using assms
  by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)

lemma b_e_type_comp:
  assumes "𝒞 ⊢ es@[e] : (t1s _> t4s)"
  shows "∃ts'. (𝒞 ⊢ es : (t1s _> ts')) ∧ (𝒞 ⊢ [e] : (ts' _> t4s))"
proof (cases es rule: List.rev_cases)
  case Nil
  then show ?thesis
    using assms b_e_typing.empty b_e_typing.weakening
    by fastforce
next
  case (snoc es' e')
  show ?thesis using assms snoc b_e_typing.weakening
    by (induction "es@[e]" "(t1s _> t4s)" arbitrary: t1s t4s, fastforce+)
qed

(* Two special cases - useful for inductions over reduce. *)
lemma b_e_type_comp2_unlift:
  assumes "𝒮∙𝒞 ⊢ [$e1, $e2] : (t1s _> t2s)"
  shows "∃ts'. (𝒞 ⊢ [e1] : (t1s _> ts')) ∧ (𝒞 ⊢ [e2] : (ts' _> t2s))"
  using assms
        unlift_b_e[of 𝒮 𝒞 "([e1, e2])" "(t1s _> t2s)"]
        b_e_type_comp[of 𝒞 "[e1]" e2 t1s t2s]
  by simp

lemma b_e_type_comp2_relift:
  assumes "𝒞 ⊢ [e1] : (t1s _> ts')" "𝒞 ⊢ [e2] : (ts' _> t2s)"
  shows "𝒮∙𝒞 ⊢ [$e1, $e2] : (ts@t1s _> ts@t2s)"
  using assms
        b_e_typing.composition[OF assms]
        e_typing_s_typing.intros(1)[of 𝒞 "[e1, e2]" "(t1s _> t2s)"]
        e_typing_s_typing.intros(3)[of 𝒮 𝒞 "([$e1,$e2])" t1s t2s ts]
  by simp

lemma b_e_type_value2:
  assumes "𝒞 ⊢ [C v1, C v2] : (t1s _> t2s)"
  shows "t2s = t1s @ [typeof v1, typeof v2]"
proof -
  obtain ts' where ts'_def:"𝒞 ⊢ [C v1] : (t1s _> ts')"
                           "𝒞 ⊢ [C v2] : (ts' _> t2s)"
    using b_e_type_comp assms
    by (metis append_butlast_last_id butlast.simps(2) last_ConsL last_ConsR list.distinct(1))
  have "ts' = t1s @ [typeof v1]"
    using b_e_type_value ts'_def(1)
    by fastforce
  thus ?thesis
    using b_e_type_value ts'_def(2)
    by fastforce
qed

(* Lifting the previous results to all expressions. *)
lemma e_type_comp:
  assumes "𝒮∙𝒞 ⊢ es@[e] : (t1s _> t3s)"
  shows "∃ts'. (𝒮∙𝒞 ⊢ es : (t1s _> ts')) ∧ (𝒮∙𝒞 ⊢ [e] : (ts' _> t3s))"
proof (cases es rule: List.rev_cases)
  case Nil
  thus ?thesis
    using assms e_typing_s_typing.intros(1)
    by (metis append_Nil b_e_type_empty list.simps(8))
next
  case (snoc es' e')
  show ?thesis using assms snoc
  proof (induction "es@[e]" "(t1s _> t3s)" arbitrary: t1s t3s)
    case (1 𝒞 b_es 𝒮)
    obtain es'' e'' where b_e_defs:"($* (es'' @ [e''])) = ($* b_es)"
      using 1(1,2)
      by (metis Nil_is_map_conv append_is_Nil_conv not_Cons_self2 rev_exhaust)
    hence "($*es'') = es" "($e'') = e"
      using 1(2) inj_basic map_injective
      by auto
    moreover
    have "𝒞 ⊢ (es'' @ [e'']) : (t1s _> t3s)" using 1(1)
      using inj_basic map_injective b_e_defs
      by blast
    then obtain t2s where "𝒞 ⊢ es'' : (t1s _> t2s)" "𝒞 ⊢ [e''] : (t2s _> t3s)"
      using b_e_type_comp
      by blast
    ultimately
    show ?case
      using e_typing_s_typing.intros(1)
      by fastforce
  next
    case (3 𝒮 𝒞 t1s t2s ts)
    thus ?case
      using e_typing_s_typing.intros(3)
      by fastforce
  qed auto
qed

lemma e_type_comp_conc:
  assumes "𝒮∙𝒞 ⊢ es : (t1s _> t2s)"
          "𝒮∙𝒞 ⊢ es' : (t2s _> t3s)"
  shows "𝒮∙𝒞 ⊢ es@es' : (t1s _> t3s)"
  using assms(2)
proof (induction es' arbitrary: t3s rule: List.rev_induct)
  case Nil
  hence "t2s = t3s"
    using unlift_b_e[of _ _ "[]"] b_e_type_empty[of _ t2s t3s]
    by fastforce
  then show ?case
    using Nil assms(1) e_typing_s_typing.intros(2)
    by fastforce
next
  case (snoc x xs)
  then obtain ts' where "𝒮∙𝒞 ⊢ xs : (t2s _> ts')" "𝒮∙𝒞 ⊢ [x] : (ts' _> t3s)"
    using e_type_comp[of _ _ xs x]
    by fastforce
  then show ?case
    using snoc(1)[of ts'] e_typing_s_typing.intros(2)[of _ _ "es @ xs" t1s ts' x t3s]
    by simp
qed

(* This isn't needed here, but we unlift for convenience. *)
lemma b_e_type_comp_conc:
  assumes "𝒞 ⊢ es : (t1s _> t2s)"
          "𝒞 ⊢ es' : (t2s _> t3s)"
  shows "𝒞 ⊢ es@es' : (t1s _> t3s)"
proof -
  fix 𝒮
  have 1:"𝒮∙𝒞 ⊢ $*es : (t1s _> t2s)"
    using e_typing_s_typing.intros(1)[OF assms(1)]
    by fastforce
  have 2:"𝒮∙𝒞 ⊢ $*es' : (t2s _> t3s)"
    using e_typing_s_typing.intros(1)[OF assms(2)]
    by fastforce
  show ?thesis
    using e_type_comp_conc[OF 1 2]
    by (simp add:  unlift_b_e)
qed

lemma e_type_comp_conc1:
  assumes "𝒮∙𝒞 ⊢ es@es' : (ts _> ts')"
  shows "∃ts''. (𝒮∙𝒞 ⊢ es : (ts _> ts'')) ∧ (𝒮∙𝒞 ⊢ es' : (ts'' _> ts'))"
  using assms
proof (induction es' arbitrary: ts ts' rule: List.rev_induct)
  case Nil
  thus ?case
    using b_e_type_empty[of _ ts' ts'] e_typing_s_typing.intros(1)
    by fastforce
next
  case (snoc x xs)
  then show ?case
    using e_type_comp[of 𝒮 𝒞 "es @ xs" x ts ts'] e_typing_s_typing.intros(2)[of 𝒮 𝒞 xs _ _ x ts']
    by fastforce
qed

lemma e_type_comp_conc2:
  assumes "𝒮∙𝒞 ⊢ es@es'@es'' : (t1s _> t2s)"
  shows "∃ts' ts''. (𝒮∙𝒞 ⊢ es : (t1s _> ts'))
                     ∧ (𝒮∙𝒞 ⊢ es' : (ts' _> ts''))
                     ∧ (𝒮∙𝒞 ⊢ es'' : (ts'' _> t2s))"
proof -
  obtain ts' where "𝒮∙𝒞 ⊢ es : (t1s _> ts')" "𝒮∙𝒞 ⊢ es'@es'' : (ts' _> t2s)"
    using assms(1) e_type_comp_conc1
    by fastforce
  moreover
  then obtain ts'' where "𝒮∙𝒞 ⊢ es' : (ts' _> ts'')" "𝒮∙𝒞 ⊢ es'' : (ts'' _> t2s)"
    using e_type_comp_conc1
    by fastforce
  ultimately
  show ?thesis
    by fastforce
qed

lemma b_e_type_value_list:
  assumes "(𝒞 ⊢ es@[C v] : (ts _> ts'@[t]))"
  shows "(𝒞 ⊢ es : (ts _> ts'))"
        "(typeof v = t)"
proof -
  obtain ts'' where "(𝒞 ⊢ es : (ts _> ts''))" "(𝒞 ⊢ [C v] : (ts'' _> ts' @ [t]))"
    using b_e_type_comp assms
    by blast
  thus "(𝒞 ⊢ es : (ts _> ts'))" "(typeof v = t)"
    using b_e_type_value[of 𝒞 "C v" "ts''" "ts' @ [t]"]
    by auto
qed

lemma e_type_label:
  assumes "𝒮∙𝒞 ⊢ [Label n es0 es] : (ts _> ts')"
  shows "∃tls t2s. (ts' = (ts@t2s))
                ∧ length tls = n
                ∧ (𝒮∙𝒞 ⊢ es0 : (tls _> t2s))
                ∧ (𝒮∙𝒞⦇label := [tls] @ (label 𝒞)⦈ ⊢ es : ([] _> t2s))"
  using assms
proof (induction "𝒮" "𝒞" "[Label n es0 es]" "(ts _> ts')" arbitrary: ts ts')
  case (1 𝒞 b_es 𝒮)
  then show ?case
    by (simp add: map_eq_Cons_conv)
next
  case (2 𝒮 𝒞 es t1s t2s e t3s)
  then show ?case
    by (metis append_self_conv2 b_e_type_empty last_snoc list.simps(8) unlift_b_e)
next
  case (3 𝒮 𝒞 t1s t2s ts)
  then show ?case
    by simp
next
  case (7 𝒮 𝒞 t2s)
  then show ?case
    by fastforce
qed

lemma e_type_callcl_native:
  assumes "𝒮∙𝒞 ⊢ [Callcl cl] : (t1s' _> t2s')"
          "cl = Func_native i tf ts es"
  shows "∃t1s t2s ts_c. (t1s' = ts_c @ t1s)
                         ∧ (t2s' = ts_c @ t2s)
                         ∧ tf = (t1s _> t2s)
                         ∧ i < length (s_inst 𝒮)
                         ∧ (((s_inst 𝒮)!i)⦇local := (local ((s_inst 𝒮)!i)) @ t1s @ ts, label := ([t2s] @ (label ((s_inst 𝒮)!i))), return := Some t2s⦈  ⊢ es : ([] _> t2s))"
  using assms
proof (induction "𝒮" "𝒞" "[Callcl cl]" "(t1s' _> t2s')" arbitrary: t1s' t2s')
  case (1 𝒞 b_es 𝒮)
  thus ?case
    by auto
next
  case (2 𝒮 𝒞 es t1s t2s e t3s)
  have "𝒞 ⊢ [] : (t1s _> t2s)"
    using 2(1,5) unlift_b_e
    by (metis Nil_is_map_conv append_Nil butlast_snoc)
  thus ?case
    using 2(4,5,6)
    by fastforce
next
  case (3 𝒮 𝒞 t1s t2s ts)
    thus ?case
    by fastforce
next
  case (6 𝒮 𝒞)
  thus ?case
    unfolding cl_typing.simps
    by fastforce
qed

lemma e_type_callcl_host:
  assumes "𝒮∙𝒞 ⊢ [Callcl cl] : (t1s' _> t2s')"
          "cl = Func_host tf f"
  shows "∃t1s t2s ts_c. (t1s' = ts_c @ t1s)
                        ∧ (t2s' = ts_c @ t2s)
                        ∧ tf = (t1s _> t2s)"
  using assms
proof (induction "𝒮" "𝒞" "[Callcl cl]" "(t1s' _> t2s')" arbitrary: t1s' t2s')
  case (1 𝒞 b_es 𝒮)
  thus ?case
    by auto
next
  case (2 𝒮 𝒞 es t1s t2s e t3s)
  have "𝒞 ⊢ [] : (t1s _> t2s)"
    using 2(1,5) unlift_b_e
    by (metis Nil_is_map_conv append_Nil butlast_snoc)
  thus ?case
    using 2(4,5,6)
    by fastforce
next
  case (3 𝒮 𝒞 t1s t2s ts)
    thus ?case
    by fastforce
next
  case (6 𝒮 𝒞)
  thus ?case
    unfolding cl_typing.simps
    by fastforce
qed

lemma e_type_callcl:
  assumes "𝒮∙𝒞 ⊢ [Callcl cl] : (t1s' _> t2s')"
  shows "∃t1s t2s ts_c. (t1s' = ts_c @ t1s)
                        ∧ (t2s' = ts_c @ t2s)
                        ∧ cl_type cl = (t1s _> t2s)"
proof (cases cl)
  case (Func_native x11 x12 x13 x14)
  thus ?thesis
    using e_type_callcl_native[OF assms]
    unfolding cl_type_def
    by (cases x12) fastforce
next
  case (Func_host x21 x22)
  thus ?thesis
    using e_type_callcl_host[OF assms]
    unfolding cl_type_def
    by fastforce
qed

lemma s_type_unfold:
  assumes "𝒮∙rs ⊩_i vs;es : ts"
  shows "i < length (s_inst 𝒮)"
        "(rs = Some ts) ∨ rs = None"
        "(𝒮∙((s_inst 𝒮)!i)⦇local := (local ((s_inst 𝒮)!i)) @ (map typeof vs), return := rs⦈ ⊢ es : ([] _> ts))"
  using assms
  by (induction vs es ts, auto)

lemma e_type_local:
  assumes "𝒮∙𝒞 ⊢ [Local n i vs es] : (ts _> ts')"
  shows "∃tls. i < length (s_inst 𝒮)
               ∧ length tls = n
               ∧ (𝒮∙((s_inst 𝒮)!i)⦇local := (local ((s_inst 𝒮)!i)) @ (map typeof vs), return := Some tls⦈ ⊢ es : ([] _> tls))
               ∧ ts' = ts @ tls"
  using assms
proof (induction "𝒮" "𝒞" "[Local n i vs es]" "(ts _> ts')" arbitrary: ts ts')
  case (2 𝒮 𝒞 es' t1s t2s e t3s)
  have "t1s = t2s"
    using 2 unlift_b_e
    by force
  thus ?case
    using 2
    by simp
qed (auto simp add: unlift_b_e s_typing.simps)

lemma e_type_local_shallow:
  assumes "𝒮∙𝒞 ⊢ [Local n i vs es] : (ts _> ts')"
  shows "∃tls. length tls = n ∧ ts' = ts@tls ∧ (𝒮∙(Some tls) ⊩_i vs;es : tls)"
  using assms
proof (induction "𝒮" "𝒞" "[Local n i vs es]" "(ts _> ts')" arbitrary: ts ts')
  case (1 𝒞 b_es 𝒮)
  thus ?case
  by (metis e.distinct(7) map_eq_Cons_D)
next
  case (2 𝒮 𝒞 es t1s t2s e t3s)
  thus ?case
  by simp (metis append_Nil append_eq_append_conv e_type_comp_conc e_type_local)
qed simp_all

(* Some proofs treat (lists of) consts as an opaque (typed) arrangement. *)
lemma e_type_const_unwrap:
  assumes "is_const e"
  shows "∃v. e = $C v"
  using assms
proof (cases e)
  case (Basic x1)
  then show ?thesis
    using assms
  proof (cases x1)
    case (EConst x23)
      thus ?thesis
        using Basic e_typing_s_typing.intros(1,3)
        by fastforce
  qed  (simp_all add: is_const_def)
qed (simp_all add: is_const_def)

lemma is_const_list1:
  assumes "ves = map (Basic ∘ EConst) vs"
  shows "const_list ves"
  using assms
proof (induction vs arbitrary: ves)
  case Nil
  then show ?case
    unfolding const_list_def
    by simp
next
  case (Cons a vs)
  then obtain ves' where "ves' = map (Basic ∘ EConst) vs"
    by blast
  moreover
  have "is_const ((Basic ∘ EConst) a)"
    unfolding is_const_def
    by simp
  ultimately
  show ?case
    using Cons
    unfolding const_list_def
      (* WHYYYYYY *)
    by auto
qed

lemma is_const_list:
  assumes "ves = $$* vs"
  shows "const_list ves"
  using assms is_const_list1
  unfolding comp_def
  by auto

lemma const_list_cons_last:
  assumes "const_list (es@[e])"
  shows "const_list es"
        "is_const e"
  using assms list_all_append[of is_const es "[e]"]
  unfolding const_list_def
  by auto

lemma e_type_const1:
  assumes "is_const e"
  shows "∃t. (𝒮∙𝒞 ⊢ [e] : (ts _> ts@[t]))"
  using assms
proof (cases e)
  case (Basic x1)
  then show ?thesis
    using assms
  proof (cases x1)
    case (EConst x23)
      hence "𝒞 ⊢ [x1] : ([] _> [typeof x23])"
        by (simp add: b_e_typing.intros(1))
      thus ?thesis
        using Basic e_typing_s_typing.intros(1,3)
        by (metis append_Nil2 to_e_list_1)
  qed  (simp_all add: is_const_def)
qed (simp_all add: is_const_def)

lemma e_type_const:
  assumes "is_const e"
          "𝒮∙𝒞 ⊢ [e] : (ts _> ts')"
  shows  "∃t. (ts' = ts@[t]) ∧ (𝒮∙𝒞' ⊢ [e] : ([] _> [t]))"
  using assms
proof (cases e)
  case (Basic x1)
  then show ?thesis
    using assms
  proof (cases x1)
    case (EConst x23)
      then have "ts' = ts @ [typeof x23]"
        by (metis (no_types) Basic assms(2) b_e_type_value list.simps(8,9) unlift_b_e)
      moreover
      have "𝒮∙𝒞' ⊢ [e] : ([] _> [typeof x23])"
        using Basic EConst b_e_typing.intros(1) e_typing_s_typing.intros(1)
        by fastforce
      ultimately
      show ?thesis
        by simp
  qed  (simp_all add: is_const_def)
qed (simp_all add: is_const_def)

lemma const_typeof:
  assumes "𝒮∙𝒞 ⊢ [$C v] : ([] _> [t])"
  shows "typeof v = t"
  using assms
proof -
  have "𝒞 ⊢ [C v] : ([] _> [t])"
    using unlift_b_e assms
    by fastforce
  thus ?thesis
    by (induction "[C v]" "([] _> [t])" rule: b_e_typing.induct, auto)
qed

lemma e_type_const_list:
  assumes "const_list vs"
          "𝒮∙𝒞 ⊢ vs : (ts _> ts')"
  shows   "∃tvs. ts' = ts @ tvs ∧ length vs = length tvs ∧ (𝒮∙𝒞' ⊢ vs : ([] _> tvs))"
  using assms
proof (induction vs arbitrary: ts ts' rule: List.rev_induct)
  case Nil
  have "𝒮∙𝒞' ⊢ [] : ([] _> [])"
    using b_e_type_empty[of 𝒞' "[]" "[]"] e_typing_s_typing.intros(1)
    by fastforce
  thus ?case
    using Nil
    by (metis append_Nil2 b_e_type_empty list.map(1) list.size(3) unlift_b_e)
next
  case (snoc x xs)
  hence v_lists:"list_all is_const xs" "is_const x"
  unfolding const_list_def
  by simp_all
  obtain ts'' where ts''_def:"𝒮∙𝒞 ⊢ xs : (ts _> ts'')" "𝒮∙𝒞 ⊢ [x] : (ts'' _> ts')"
    using snoc(3) e_type_comp
    by fastforce
  then obtain ts_b where ts_b_def:"ts'' = ts @ ts_b" "length xs = length ts_b" "𝒮∙𝒞' ⊢ xs : ([] _> ts_b)"
    using snoc(1) v_lists(1)
    unfolding const_list_def
    by fastforce
  then obtain t where t_def:"ts' = ts @ ts_b @ [t]" "𝒮∙𝒞' ⊢ [x] : ([] _> [t])"
    using e_type_const v_lists(2) ts''_def
    by fastforce
  moreover
  then have "length (ts_b@[t]) = length (xs@[x])"
    using ts_b_def(2)
    by simp
  moreover
  have "𝒮∙𝒞' ⊢ (xs@[x]) : ([] _> ts_b@[t])"
    using ts_b_def(3) t_def e_typing_s_typing.intros(2,3)
    by fastforce
  ultimately
  show ?case
    by simp
qed

lemma e_type_const_list_snoc:
  assumes "const_list vs"
          "𝒮∙𝒞 ⊢ vs : ([] _> ts@[t])"
  shows "∃vs1 v2. (𝒮∙𝒞 ⊢ vs1 : ([] _> ts))
                   ∧ (𝒮∙𝒞 ⊢ [v2] : (ts _> ts@[t]))
                   ∧ (vs = vs1@[v2])
                   ∧ const_list vs1
                   ∧ is_const v2"
  using assms
proof -
  obtain vs' v where vs_def:"vs = vs'@[v]"
    using e_type_const_list[OF assms(1,2)]
    by (metis append_Nil append_eq_append_conv list.size(3) snoc_eq_iff_butlast)
  hence consts_def:"const_list vs'" "is_const v"
    using assms(1)
    unfolding const_list_def
    by auto
  obtain ts' where ts'_def:"𝒮∙𝒞 ⊢ vs' : ([] _> ts')" "𝒮∙𝒞 ⊢ [v] : (ts' _> ts@[t])"
    using vs_def assms(2) e_type_comp[of 𝒮 𝒞 vs' v "[]" "ts@[t]"]
    by fastforce
  obtain c where "v = $C c"
    using e_type_const_unwrap consts_def(2)
    by fastforce
  hence "ts' = ts"
    using ts'_def(2) unlift_b_e[of 𝒮 𝒞 "[C c]"] b_e_type_value
    by fastforce
  thus ?thesis using ts'_def vs_def consts_def
    by simp
qed
    
lemma e_type_const_list_cons:
  assumes "const_list vs"
          "𝒮∙𝒞 ⊢ vs : ([] _> (ts1@ts2))"
  shows "∃vs1 vs2. (𝒮∙𝒞 ⊢ vs1 : ([] _> ts1))
                   ∧ (𝒮∙𝒞 ⊢ vs2 : (ts1 _> (ts1@ts2)))
                   ∧ vs = vs1@vs2
                   ∧ const_list vs1
                   ∧ const_list vs2"
  using assms
proof (induction "ts1@ts2" arbitrary: vs ts1 ts2 rule: List.rev_induct)
  case Nil
  thus ?case
    using e_type_const_list
    by fastforce
next
  case (snoc t ts)
  note snoc_outer = snoc
  show ?case
  proof (cases ts2 rule: List.rev_cases)
    case Nil
    have "𝒮∙𝒞 ⊢ [] : (ts1 _> ts1 @ [])"
      using b_e_typing.empty b_e_typing.weakening e_typing_s_typing.intros(1)
      by fastforce
    then show ?thesis
      using snoc(3,4) Nil
      unfolding const_list_def
      by auto
  next
    case (snoc ts2' a)
    obtain vs1 v2 where vs1_def:"(𝒮∙𝒞 ⊢ vs1 : ([] _> ts1 @ ts2'))"
                                "(𝒮∙𝒞 ⊢ [v2] : (ts1 @ ts2' _> ts1 @ ts2' @[t]))"
                                "(vs = vs1@[v2])"
                                "const_list vs1"
                                "is_const v2"
                                "ts = ts1 @ ts2'"
      using e_type_const_list_snoc[OF snoc_outer(3), of 𝒮 𝒞 "ts1@ts2'" t]
            snoc_outer(2,4) snoc
      by fastforce
    show ?thesis
      using snoc_outer(1)[OF vs1_def(6,4,1)] snoc_outer(2) vs1_def(3,5)
            e_typing_s_typing.intros(2)[OF _ vs1_def(2), of _ ts1]
            snoc
      unfolding const_list_def
      by fastforce
  qed
qed

lemma e_type_const_conv_vs:
  assumes "const_list ves"
  shows "∃vs. ves = $$* vs"
  using assms
proof (induction ves)
  case Nil
  thus ?case
    by simp
next
  case (Cons a ves)
  thus ?case
  using e_type_const_unwrap
  unfolding const_list_def
  by (metis (no_types, lifting) list.pred_inject(2) list.simps(9)) 
qed

lemma types_exist_lfilled:
  assumes "Lfilled k lholed es lfilled"
          "𝒮∙𝒞 ⊢ lfilled : (ts _> ts')"
  shows "∃t1s t2s 𝒞' arb_label. (𝒮∙𝒞⦇label := arb_label@(label 𝒞)⦈ ⊢ es : (t1s _> t2s))"
  using assms
proof (induction arbitrary: 𝒞 ts ts' rule: Lfilled.induct)
  case (L0 vs lholed es' es)
  hence "𝒮∙(𝒞⦇label := label 𝒞⦈) ⊢ vs @ es @ es' : (ts _> ts')"
    by simp
  thus ?case
    using e_type_comp_conc2
    by (metis append_Nil)
next
  case (LN vs lholed n es' l es'' k es lfilledk)
  obtain ts'' ts''' where "𝒮∙𝒞 ⊢ [Label n es' lfilledk]  : (ts'' _> ts''')"
    using e_type_comp_conc2[OF LN(5)]
    by fastforce
  then obtain t1s t2s ts where test:"𝒮∙𝒞⦇label := [ts] @ (label 𝒞)⦈ ⊢ lfilledk  : (t1s _> t2s)"
    using e_type_label
    by metis
  show ?case
    using LN(4)[OF test(1)]
    by simp (metis append.assoc append_Cons append_Nil)
qed

lemma types_exist_lfilled_weak:
  assumes "Lfilled k lholed es lfilled"
          "𝒮∙𝒞 ⊢ lfilled : (ts _> ts')"
  shows "∃t1s t2s 𝒞' arb_label arb_return. (𝒮∙𝒞⦇label := arb_label, return := arb_return⦈ ⊢ es : (t1s _> t2s))"
proof -
  have "∃t1s t2s 𝒞' arb_label. (𝒮∙𝒞⦇label := arb_label, return := (return 𝒞)⦈ ⊢ es : (t1s _> t2s))"
    using types_exist_lfilled[OF assms]
    by fastforce
  thus ?thesis
    by fastforce
qed

lemma store_typing_imp_func_agree:
  assumes "store_typing s 𝒮"
          "i < length (s_inst 𝒮)"
          "j < length (func_t ((s_inst 𝒮)!i))"
  shows "(sfunc_ind s i j) < length (s_funcs 𝒮)"
        "cl_typing 𝒮 (sfunc s i j) ((s_funcs 𝒮)!(sfunc_ind s i j))"
        "((s_funcs 𝒮)!(sfunc_ind s i j)) = (func_t ((s_inst 𝒮)!i))!j"
proof -
  have funcs_agree:"list_all2 (cl_typing 𝒮) (funcs s) (s_funcs 𝒮)"
    using assms(1)
    unfolding store_typing.simps
    by auto
  have "list_all2 (funci_agree (s_funcs 𝒮)) (inst.funcs ((inst s)!i)) (func_t ((s_inst 𝒮)!i))"
    using assms(1,2) store_typing_imp_inst_length_eq store_typing_imp_inst_typing
    by (fastforce simp add: inst_typing.simps)
  hence "funci_agree (s_funcs 𝒮) ((inst.funcs ((inst s)!i))!j) ((func_t ((s_inst 𝒮)!i))!j)"
    using assms(3) list_all2_nthD2
    by blast
  thus "(sfunc_ind s i j) < length (s_funcs 𝒮)"
       "((s_funcs 𝒮)!(sfunc_ind s i j)) = (func_t ((s_inst 𝒮)!i))!j"
    unfolding funci_agree_def sfunc_ind_def
    by auto
  thus "cl_typing 𝒮 (sfunc s i j) ((s_funcs 𝒮)!(sfunc_ind s i j))"
    using funcs_agree list_all2_nthD2
    unfolding sfunc_def
    by fastforce
qed

lemma store_typing_imp_glob_agree:
  assumes "store_typing s 𝒮"
          "i < length (s_inst 𝒮)"
          "j < length (global ((s_inst 𝒮)!i))"
  shows "(sglob_ind s i j) < length (s_globs 𝒮)"
        "glob_agree (sglob s i j) ((s_globs 𝒮)!(sglob_ind s i j))"
        "((s_globs 𝒮)!(sglob_ind s i j)) = (global ((s_inst 𝒮)!i))!j"
proof -
  have globs_agree:"list_all2 glob_agree (globs s) (s_globs 𝒮)"
    using assms(1)
    unfolding store_typing.simps
    by auto
  have "list_all2 (globi_agree (s_globs 𝒮)) (inst.globs ((inst s)!i)) (global ((s_inst 𝒮)!i))"
    using assms(1,2) store_typing_imp_inst_length_eq store_typing_imp_inst_typing
    by (fastforce simp add: inst_typing.simps)
  hence "globi_agree (s_globs 𝒮) ((inst.globs ((inst s)!i))!j) ((global ((s_inst 𝒮)!i))!j)"
    using assms(3) list_all2_nthD2
    by blast
  thus "(sglob_ind s i j) < length (s_globs 𝒮)"
       "((s_globs 𝒮)!(sglob_ind s i j)) = (global ((s_inst 𝒮)!i))!j"
    unfolding globi_agree_def sglob_ind_def
    by auto
  thus "glob_agree (sglob s i j) ((s_globs 𝒮)!(sglob_ind s i j))"
    using globs_agree list_all2_nthD2
    unfolding sglob_def
    by fastforce
qed

lemma store_typing_imp_mem_agree_Some:
  assumes "store_typing s 𝒮"
          "i < length (s_inst 𝒮)"
          "smem_ind s i = Some j"
  shows "j < length (s_mem 𝒮)"
        "mem_agree ((mem s)!j) ((s_mem 𝒮)!j)"
        "∃x. ((s_mem 𝒮)!j) = x ∧ (memory ((s_inst 𝒮)!i)) = Some x"
proof -
  have mems_agree:"list_all2 mem_agree (mem s) (s_mem 𝒮)"
  using assms(1)
  unfolding store_typing.simps
  by auto
  hence "memi_agree (s_mem 𝒮) ((inst.mem ((inst s)!i))) ((memory ((s_inst 𝒮)!i)))"
    using assms(1,2) store_typing_imp_inst_length_eq store_typing_imp_inst_typing
    by (fastforce simp add: inst_typing.simps)
  thus "j < length (s_mem 𝒮)"
       "∃x. ((s_mem 𝒮)!j) = x ∧ (memory ((s_inst 𝒮)!i)) = Some x"
    using assms(3)
    unfolding memi_agree_def smem_ind_def
    by auto
  thus "mem_agree ((mem s)!j) ((s_mem 𝒮)!j)"
    using mems_agree list_all2_nthD2
    unfolding sglob_def
    by fastforce
qed

lemma store_typing_imp_mem_agree_None:
  assumes "store_typing s 𝒮"
          "i < length (s_inst 𝒮)"
          "smem_ind s i = None"
  shows "(memory ((s_inst 𝒮)!i)) = None"
proof -
  have mems_agree:"list_all2 mem_agree (mem s) (s_mem 𝒮)"
  using assms(1)
  unfolding store_typing.simps
  by auto
  hence "memi_agree (s_mem 𝒮) ((inst.mem ((inst s)!i))) ((memory ((s_inst 𝒮)!i)))"
    using assms(1,2) store_typing_imp_inst_length_eq store_typing_imp_inst_typing
    by (fastforce simp add: inst_typing.simps)
  thus ?thesis
    using assms(3)
    unfolding memi_agree_def smem_ind_def
    by auto
qed

lemma store_mem_exists:
  assumes "i < length (s_inst 𝒮)"
          "store_typing s 𝒮"
  shows "Option.is_none (memory ((s_inst 𝒮)!i)) = Option.is_none (inst.mem ((inst s)!i))"
proof -
  obtain j where j_def:"j = (inst.mem ((inst s)!i))"
    by blast
  obtain m where m_def:"m = (memory ((s_inst 𝒮)!i))"
    by blast
  have inst_typ:"inst_typing 𝒮 ((inst s)!i) ((s_inst 𝒮)!i)"
    using assms
    unfolding store_typing.simps list_all2_conv_all_nth
    by auto
  thus ?thesis
    unfolding inst_typing.simps memi_agree_def
    by auto
qed

lemma store_preserved_mem:
  assumes "store_typing s 𝒮"
          "s' = s⦇s.mem := (s.mem s)[i := mem']⦈"
          "mem_size mem' ≥ mem_size orig_mem"
          "((s.mem s)!i) = orig_mem"
  shows "store_typing s' 𝒮"
proof -
  obtain insts fs clss bss gs where "s = ⦇inst = insts, funcs = fs, tab = clss, mem = bss, globs = gs⦈"
    using s.cases
    by blast
  moreover
  obtain insts' fs' clss' bss' gs' where "s' = ⦇inst = insts', funcs = fs', tab = clss', mem = bss', globs = gs'⦈"
    using s.cases
    by blast
  moreover
  obtain 𝒞s tfs ns ms tgs where "𝒮 = ⦇s_inst = 𝒞s, s_funcs = tfs, s_tab = ns, s_mem = ms, s_globs = tgs⦈"
    using s_context.cases
    by blast
  moreover
  note s_S_defs = calculation
  hence
  "insts = insts'"
  "fs = fs'"
  "clss = clss'"
  "gs = gs'"
    using assms(2)
    by simp_all
  hence
  "list_all2 (inst_typing 𝒮) insts' 𝒞s"
  "list_all2 (cl_typing 𝒮) fs' tfs"
  "list_all (tab_agree 𝒮) (concat clss')"
  "list_all2 (λcls n. n ≤ length cls) clss' ns"
  "list_all2 glob_agree gs' tgs"
    using s_S_defs assms(1)
    unfolding store_typing.simps
    by auto
  moreover
  have "list_all2 (λ bs m. m ≤ mem_size bs) bss' ms"
  proof -
    have "length bss = length bss'"
      using assms(2)  s_S_defs
      by (simp)
    moreover
    (* Memory correct before execution. *)
    have initial_mem:"list_all2 (λ bs m. m ≤ mem_size bs) bss ms"
      using assms(1) s_S_defs
      unfolding store_typing.simps mem_agree_def
      by blast
    have "⋀n. n < length bss ⟹ (λ bs m. m ≤ mem_size bs) (bss'!n) (ms!n)"
    proof -
      fix n
      assume local_assms:"n < length bss"
      obtain 𝒞_m where cmdef:"𝒞_m = 𝒞s ! n"
        by blast
      hence "(λ bs m. m ≤ mem_size bs) (bss!n) (ms!n)"
        using initial_mem local_assms
        unfolding list_all2_conv_all_nth
        by simp
      thus "(λ bs m. m ≤ mem_size bs) (bss'!n) (ms!n)"
        using assms(2,3,4) s_S_defs local_assms
        by (cases "n=i", auto)
    qed
    ultimately
    show ?thesis
      by (metis initial_mem list_all2_all_nthI list_all2_lengthD)
  qed
  ultimately
  show ?thesis
    unfolding store_typing.simps mem_agree_def
    by simp
qed

lemma types_agree_imp_e_typing:
  assumes "types_agree t v"
  shows "𝒮∙𝒞 ⊢ [$C v] : ([] _> [t])"
  using assms e_typing_s_typing.intros(1)[OF b_e_typing.intros(1)]
  unfolding types_agree_def
  by fastforce

lemma list_types_agree_imp_e_typing:
  assumes "list_all2 types_agree ts vs"
  shows "𝒮∙𝒞 ⊢ $$* vs : ([] _> ts)"
  using assms
proof (induction rule: list_all2_induct)
  case Nil
  thus ?case
    using b_e_typing.empty e_typing_s_typing.intros(1)
    by fastforce
next
  case (Cons t ts v vs)
  hence "𝒮∙𝒞 ⊢ [$C v] : ([] _> [t])"
    using types_agree_imp_e_typing
    by fastforce
  thus ?case
    using e_typing_s_typing.intros(3)[OF Cons(3), of "[t]"] e_type_comp_conc
    by fastforce
qed

lemma b_e_typing_imp_list_types_agree:
  assumes "𝒞 ⊢ (map (λv. C v) vs) : (ts' _> ts'@ts)"
  shows "list_all2 types_agree ts vs"
  using assms
proof (induction "(map (λv. C v) vs)" "(ts' _> ts'@ts)" arbitrary: ts ts' vs rule: b_e_typing.induct)
  case (composition 𝒞 es t1s t2s e)
  obtain vs1 vs2 where es_e_def:"es = map EConst vs1" "[e] = map EConst vs2" "vs1@vs2=vs"  
    using composition(5)
    by (metis (no_types) last_map list.simps(8,9) map_butlast snoc_eq_iff_butlast)
  have "const_list ($*es)"
    using es_e_def(1) is_const_list1
    by auto
  then obtain tvs1 where "t2s = t1s@tvs1"
    using e_type_const_list e_typing_s_typing.intros(1)[OF composition(1)]
    by fastforce
  moreover
  have "const_list ($*[e])"
    using es_e_def(2) is_const_list1
    by auto
  then obtain tvs2 where "t1s @ ts = t2s @ tvs2"
    using e_type_const_list e_typing_s_typing.intros(1)[OF composition(3)]
    by fastforce
  ultimately
  show ?case
    using composition(2,4,5) es_e_def
    by (auto simp add: list_all2_appendI)
qed (auto simp add: types_agree_def)

lemma e_typing_imp_list_types_agree:
  assumes "𝒮∙𝒞 ⊢ ($$* vs) : (ts' _> ts'@ts)"
  shows "list_all2 types_agree ts vs"
proof -
  have "($$* vs) = $* (map (λv. C v) vs)"
    by simp
  thus ?thesis
    using assms unlift_b_e b_e_typing_imp_list_types_agree
    by (fastforce simp del: map_map)
qed

lemma store_extension_imp_store_typing:
  assumes "store_extension s s'"
          "store_typing s 𝒮"
  shows "store_typing s' 𝒮"
proof -
  obtain insts fs clss bss gs where "s = ⦇inst = insts, funcs = fs, tab = clss, mem = bss, globs = gs⦈"
    using s.cases
    by blast
  moreover
  obtain insts' fs' clss' bss' gs' where "s' = ⦇inst = insts', funcs = fs', tab = clss', mem = bss', globs = gs'⦈"
    using s.cases
    by blast
  moreover
  obtain 𝒞s tfs ns ms tgs where "𝒮 = ⦇s_inst = 𝒞s, s_funcs = tfs, s_tab = ns, s_mem = ms, s_globs = tgs⦈"
    using s_context.cases
    by blast
  moreover
  note s_S_defs = calculation
  hence
  "insts = insts'"
  "fs = fs'"
  "clss = clss'"
  "gs = gs'"
    using assms(1)
    unfolding store_extension.simps
    by simp_all
  hence
  "list_all2 (inst_typing 𝒮) insts' 𝒞s"
  "list_all2 (cl_typing 𝒮) fs' tfs"
  "list_all (tab_agree 𝒮) (concat clss')"
  "list_all2 (λcls n. n ≤ length cls) clss' ns"
  "list_all2 glob_agree gs' tgs"
    using s_S_defs assms(2)
    unfolding store_typing.simps
    by auto
  moreover
  have "list_all2 (λ bs m. m ≤ mem_size bs) bss ms"
    using s_S_defs(1,3) assms(2)
    unfolding store_typing.simps mem_agree_def
    by simp
  hence "list_all2 mem_agree bss' ms"
    using assms(1) s_S_defs(1,2)
    unfolding store_extension.simps list_all2_conv_all_nth mem_agree_def
    by fastforce
  ultimately
  show ?thesis
    using store_typing.intros
    by fastforce
qed

lemma lfilled_deterministic:
  assumes "Lfilled k lfilled es les"
          "Lfilled k lfilled es les'"
  shows "les = les'"
  using assms
proof (induction arbitrary: les' rule: Lfilled.induct)
  case (L0 vs lholed es' es)
  thus ?case
    by (fastforce simp add: Lfilled.simps[of 0])
next
  case (LN vs lholed n es' l es'' k es lfilledk)
  thus ?case
    unfolding Lfilled.simps[of "(k + 1)"]
    by fastforce
qed
end