# Theory Semantic_Extras

```chapter "Adaptations for Isabelle"

theory Semantic_Extras
imports
"generated/CakeML/BigStep"
"generated/CakeML/SemanticPrimitivesAuxiliary"
"generated/CakeML/AstAuxiliary"
"generated/CakeML/Evaluate"
"HOL-Library.Simps_Case_Conv"
begin

type_synonym exp = exp0

hide_const (open) sem_env.v

code_pred
(modes: evaluate: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool as compute
and evaluate_list: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool
and evaluate_match: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) evaluate .

code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) evaluate_dec .
code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) evaluate_decs .
code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) evaluate_top .
code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool as compute_prog) evaluate_prog .

termination pmatch_list by lexicographic_order
termination do_eq_list by lexicographic_order

lemma all_distinct_alt_def: "allDistinct = distinct"
proof
fix xs :: "'a list"
show "allDistinct xs = distinct xs"
by (induct xs) auto
qed

lemma find_recfun_someD:
assumes "find_recfun n funs = Some (x, e)"
shows "(n, x, e) ∈ set funs"
using assms
by (induct funs) (auto split: if_splits)

lemma find_recfun_alt_def[simp]: "find_recfun n funs = map_of funs n"
by (induction funs) auto

lemma size_list_rev[simp]: "size_list f (rev xs) = size_list f xs"
by (auto simp: size_list_conv_sum_list rev_map[symmetric])

lemma do_if_cases:
obtains
(none) "do_if v e1 e2 = None"
| (true) "do_if v e1 e2 = Some e1"
| (false) "do_if v e1 e2 = Some e2"
unfolding do_if_def
by meson

case_of_simps do_log_alt_def: do_log.simps
case_of_simps do_con_check_alt_def: do_con_check.simps
case_of_simps list_result_alt_def: list_result.simps

context begin

private fun_cases do_logE: "do_log op v e = res"

lemma do_log_exp: "do_log op v e = Some (Exp e') ⟹ e = e'"
by (erule do_logE)
(auto split: v.splits option.splits if_splits tid_or_exn.splits id0.splits list.splits)

end

lemma c_of_merge[simp]: "c (extend_dec_env env2 env1) = nsAppend (c env2) (c env1)"
by (cases env1; cases env2; simp add: extend_dec_env_def)

lemma v_of_merge[simp]: "sem_env.v (extend_dec_env env2 env1) = nsAppend (sem_env.v env2) (sem_env.v env1)"
by (cases env1; cases env2; simp add: extend_dec_env_def)

lemma nsEmpty_nsAppend[simp]: "nsAppend e nsEmpty = e" "nsAppend nsEmpty e = e"
by (cases e; auto simp: nsEmpty_def)+

lemma do_log_cases:
obtains
(none) "do_log op v e = None"
| (val) v' where "do_log op v e = Some (Val v')"
| (exp) "do_log op v e = Some (Exp e)"
proof (cases "do_log op v e")
case None
then show ?thesis using none by metis
next
case (Some res)
with val exp show ?thesis
by (cases res) (metis do_log_exp)+
qed

context begin

private fun_cases do_opappE: "do_opapp vs = Some res"

lemma do_opapp_cases:
assumes "do_opapp vs = Some (env', exp')"
obtains (closure) env n v0
where "vs = [Closure env n exp', v0]"
"env' = (env ⦇ sem_env.v := nsBind n v0 (sem_env.v env) ⦈ )"
| (recclosure) env funs name n v0
where "vs = [Recclosure env funs name, v0]"
and "allDistinct (map (λ(f, _, _). f) funs)"
and "find_recfun name funs = Some (n, exp')"
and "env' = (env ⦇ sem_env.v := nsBind n v0 (build_rec_env funs env (sem_env.v env)) ⦈ )"
proof -
show thesis
using assms
apply (rule do_opappE)
apply (rule closure; auto)
apply (auto split: if_splits option.splits)
apply (rule recclosure)
apply auto
done
qed

end

lemmas evaluate_induct =
evaluate_match_evaluate_list_evaluate.inducts[split_format(complete)]

lemma evaluate_clock_mono:
"evaluate_match ck env s v pes v' (s', r1) ⟹ clock s' ≤ clock s"
"evaluate_list ck env s es (s', r2) ⟹ clock s' ≤ clock s"
"evaluate ck env s e (s', r3) ⟹ clock s' ≤ clock s"
by (induction rule: evaluate_induct)
(auto simp del: do_app.simps simp: datatype_record_update split: state.splits if_splits)

lemma evaluate_list_singleton_valE:
assumes "evaluate_list ck env s [e] (s', Rval vs)"
obtains v where "vs = [v]" "evaluate ck env s e (s', Rval v)"
using assms
by (auto elim: evaluate_list.cases)

lemma evaluate_list_singleton_errD:
assumes "evaluate_list ck env s [e] (s', Rerr err)"
shows "evaluate ck env s e (s', Rerr err)"
using assms
by (auto elim: evaluate_list.cases)

lemma evaluate_list_singleton_cases:
assumes "evaluate_list ck env s [e] res"
obtains (val) s' v where "res = (s', Rval [v])" "evaluate ck env s e (s', Rval v)"
| (err) s' err where "res = (s', Rerr err)" "evaluate ck env s e (s', Rerr err)"
using assms
apply -
apply (ind_cases "evaluate_list ck env s [e] res")
apply auto
apply (ind_cases "evaluate_list ck env s2 [] (s3, Rval vs)" for s2 s3 vs)
apply auto
apply (ind_cases " evaluate_list ck env s2 [] (s3, Rerr err) " for s2 s3 err)
done

lemma evaluate_list_singletonI:
assumes "evaluate ck env s e (s', r)"
shows "evaluate_list ck env s [e] (s', list_result r)"
using assms
by (cases r) (auto intro: evaluate_match_evaluate_list_evaluate.intros)

lemma prod_result_cases:
obtains (val) s v where "r = (s, Rval v)"
| (err) s err where "r = (s, Rerr err)"
apply (cases r)
subgoal for _ b
apply (cases b)
by auto
done

lemma do_con_check_build_conv: "do_con_check (c env) cn (length es) ⟹ build_conv (c env) cn vs ≠ None"
by (cases cn) (auto split: option.splits)

fun match_result :: "(v)sem_env ⇒ 'ffi state ⇒ v ⇒(pat*exp)list ⇒ v ⇒ (exp × (char list × v) list, v)result" where
"match_result _ _ _ [] err_v = Rerr (Rraise err_v)" |
"match_result env s v0 ((p, e) # pes) err_v =
(if Lem_list.allDistinct (pat_bindings p []) then
(case pmatch (sem_env.c env) (refs s) p v0 [] of
Match env' ⇒ Rval (e, env') |
No_match ⇒ match_result env s v0 pes err_v |
Match_type_error ⇒ Rerr (Rabort Rtype_error))
else
Rerr (Rabort Rtype_error))"

case_of_simps match_result_alt_def: match_result.simps

lemma match_result_sound:
"case match_result env s v0 pes err_v of
Rerr err ⇒ evaluate_match ck env s v0 pes err_v (s, Rerr err)
| Rval (e, env') ⇒
∀bv.
evaluate ck (env ⦇ sem_env.v := nsAppend (alist_to_ns env')(sem_env.v env) ⦈) s e bv ⟶
evaluate_match ck env s v0 pes err_v bv"
by (induction rule: match_result.induct)
(auto intro: evaluate_match_evaluate_list_evaluate.intros split: match_result.splits result.splits)

lemma match_result_sound_val:
assumes "match_result env s v0 pes err_v = Rval (e, env')"
assumes "evaluate ck (env ⦇ sem_env.v := nsAppend (alist_to_ns env')(sem_env.v env) ⦈) s e bv"
shows "evaluate_match ck env s v0 pes err_v bv"
proof -
note match_result_sound[where env = env and s = s and ?v0.0 = v0 and pes = pes and err_v = err_v, unfolded assms result.case prod.case]
with assms show ?thesis by blast
qed

lemma match_result_sound_err:
assumes "match_result env s v0 pes err_v = Rerr err"
shows "evaluate_match ck env s v0 pes err_v (s, Rerr err)"
proof -
note match_result_sound[where env = env and s = s and ?v0.0 = v0 and pes = pes and err_v = err_v, unfolded assms result.case prod.case]
then show ?thesis by blast
qed

lemma match_result_correct:
assumes "evaluate_match ck env s v0 pes err_v (s', bv)"
shows "case bv of
Rval v ⇒
∃e env'. match_result env s v0 pes err_v = Rval (e, env') ∧ evaluate ck (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s e (s', Rval v)
| Rerr err ⇒
(match_result env s v0 pes err_v = Rerr err) ∨
(∃e env'. match_result env s v0 pes err_v = Rval (e, env') ∧ evaluate ck (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s e (s', Rerr err))"
using assms
proof (induction pes)
case (Cons pe pes)
from Cons.prems show ?case
proof cases
case (mat_cons1 env' p e)
then show ?thesis
by (cases bv) auto
next
case (mat_cons2 p e)
then show ?thesis
using Cons.IH
by (cases bv) auto
qed auto
qed (auto elim: evaluate_match.cases)

end```