Theory Big_Step_Fun_Equiv
section "Equivalence to the functional semantics"
theory Big_Step_Fun_Equiv
imports
Big_Step_Determ
Big_Step_Total
Evaluate_Clock
begin
locale eval =
fixes
eval :: "v sem_env ⇒ exp ⇒ 'a state ⇒ 'a state × (v, v) result" and
eval_list :: "v sem_env ⇒ exp list ⇒ 'a state ⇒ 'a state × (v list, v) result" and
eval_match :: "v sem_env ⇒ v ⇒ (pat × exp) list ⇒ v ⇒ 'a state ⇒ 'a state × (v, v) result"
assumes
valid_eval: "evaluate True env s e (eval env e s)" and
valid_eval_list: "evaluate_list True env s es (eval_list env es s)" and
valid_eval_match: "evaluate_match True env s v pes err_v (eval_match env v pes err_v s)"
begin
lemmas eval_all = valid_eval valid_eval_list valid_eval_match
lemma evaluate_iff:
"evaluate True env st e r ⟷ (r = eval env e st)"
"evaluate_list True env st es r' ⟷ (r' = eval_list env es st)"
"evaluate_match True env st v pes v' r ⟷ (r = eval_match env v pes v' st)"
by (metis eval_all evaluate_determ)+
lemma evaluate_iff_sym:
"evaluate True env st e r ⟷ (eval env e st = r)"
"evaluate_list True env st es r' ⟷ (eval_list env es st = r')"
"evaluate_match True env st v pes v' r ⟷ (eval_match env v pes v' st = r)"
by (auto simp: evaluate_iff)
lemma other_eval_eq:
assumes "Big_Step_Fun_Equiv.eval eval' eval_list' eval_match'"
shows "eval' = eval" "eval_list' = eval_list" "eval_match' = eval_match"
proof -
interpret other: Big_Step_Fun_Equiv.eval eval' eval_list' eval_match' by fact
show "eval' = eval"
apply (rule ext)+
using evaluate_iff other.evaluate_iff
by (metis evaluate_determ)
show "eval_list' = eval_list"
apply (rule ext)+
using evaluate_iff other.evaluate_iff
by (metis evaluate_determ)
show "eval_match' = eval_match"
apply (rule ext)+
using evaluate_iff other.evaluate_iff
by (metis evaluate_determ)
qed
lemma eval_list_singleton:
"eval_list env [e] st = map_prod id list_result (eval env e st)"
proof -
define res where "res = eval_list env [e] st"
then have e: "evaluate_list True env st [e] res"
by (metis evaluate_iff)
then obtain st' r where "res = (st', r)"
by (metis surj_pair)
then have "map_prod id list_result (eval env e st) = (st', r)"
proof (cases r)
case (Rval vs)
with e obtain v where "vs = [v]" "evaluate True env st e (st', Rval v)"
unfolding ‹res = (st', r)› by (metis evaluate_list_singleton_valE)
then have "eval env e st = (st', Rval v)"
by (metis evaluate_iff_sym)
then show ?thesis
unfolding ‹r = _› ‹vs = _› by auto
next
case (Rerr err)
with e have "evaluate True env st e (st', Rerr err)"
unfolding ‹res = (st', r)› by (metis evaluate_list_singleton_errD)
then have "eval env e st = (st', Rerr err)"
by (metis evaluate_iff_sym)
then show ?thesis
unfolding ‹r = _› by (cases err) auto
qed
then show ?thesis
using res_def ‹res = (st', r)›
by metis
qed
lemma eval_eqI:
assumes "⋀r. evaluate True env st1 e1 r ⟷ evaluate True env st2 e2 r"
shows "eval env e1 st1 = eval env e2 st2"
using assms by (metis evaluate_iff)
lemma eval_match_eqI:
assumes "⋀r. evaluate_match True env1 st1 v1 pes1 err_v1 r ⟷ evaluate_match True env2 st2 v2 pes2 err_v2 r"
shows "eval_match env1 v1 pes1 err_v1 st1 = eval_match env2 v2 pes2 err_v2 st2"
using assms by (metis evaluate_iff)
lemma eval_tannot[simp]: "eval env (Tannot e t1) st = eval env e st"
by (rule eval_eqI) (auto elim: evaluate.cases intro: evaluate_match_evaluate_list_evaluate.intros)
lemma eval_lannot[simp]: "eval env (Lannot e t1) st = eval env e st"
by (rule eval_eqI) (auto elim: evaluate.cases intro: evaluate_match_evaluate_list_evaluate.intros)
lemma eval_match[simp]:
"eval env (Mat e pes) st =
(case eval env e st of
(st', Rval v) ⇒ eval_match env v pes Bindv st'
| (st', Rerr err) ⇒ (st', Rerr err))"
apply (subst evaluate_iff_sym[symmetric])
apply (simp only: split!: prod.splits result.splits)
subgoal
apply (subst (asm) evaluate_iff_sym[symmetric])
apply (rule mat1, rule)
apply assumption
apply (subst Bindv_def)
apply (metis valid_eval_match)
done
subgoal
apply (subst (asm) evaluate_iff_sym[symmetric])
by (auto intro: evaluate_match_evaluate_list_evaluate.intros)
done
lemma eval_match_empty[simp]: "eval_match env v2 [] err_v st = (st, Rerr (Rraise err_v))"
by (subst evaluate_iff_sym[symmetric]) (auto intro: evaluate_match_evaluate_list_evaluate.intros)
end
lemma run_eval: "∃run_eval. ∀env e s. evaluate True env s e (run_eval env e s)"
proof -
define f where "f env_e_s = (case env_e_s of (env, e, s::'a state) ⇒ evaluate True env s e)" for env_e_s
have "∃g. ∀env_e_s. f env_e_s (g env_e_s)"
proof (rule choice, safe, unfold f_def prod.case)
fix env e
fix s :: "'a state"
obtain s' r where "evaluate True env s e (s', r)"
by (metis evaluate_total)
then show "∃r. evaluate True env s e r"
by auto
qed
then show ?thesis
unfolding f_def
by force
qed
lemma run_eval_list: "∃run_eval_list. ∀env es s. evaluate_list True env s es (run_eval_list env es s)"
proof -
define f where "f env_es_s = (case env_es_s of (env, es, s::'a state) ⇒ evaluate_list True env s es)" for env_es_s
have "∃g. ∀env_es_s. f env_es_s (g env_es_s)"
proof (rule choice, safe, unfold f_def prod.case)
fix env es
fix s :: "'a state"
obtain s' r where "evaluate_list True env s es (s', r)"
by (metis evaluate_list_total)
then show "∃r. evaluate_list True env s es r"
by auto
qed
then show ?thesis
unfolding f_def
by force
qed
lemma run_eval_match: "∃run_eval_match. ∀env v pes err_v s. evaluate_match True env s v pes err_v (run_eval_match env v pes err_v s)"
proof -
define f where "f env_v_pes_err_v_s = (case env_v_pes_err_v_s of (env, v, pes, err_v, s::'a state) ⇒ evaluate_match True env s v pes err_v)" for env_v_pes_err_v_s
have "∃g. ∀env_es_s. f env_es_s (g env_es_s)"
proof (rule choice, safe, unfold f_def prod.case)
fix env v pes err_v
fix s :: "'a state"
obtain s' r where "evaluate_match True env s v pes err_v (s', r)"
by (metis evaluate_match_total)
then show "∃r. evaluate_match True env s v pes err_v r"
by auto
qed
then show ?thesis
unfolding f_def
by force
qed
global_interpretation run: eval
"SOME f. ∀env e s. evaluate True env s e (f env e s)"
"SOME f. ∀env es s. evaluate_list True env s es (f env es s)"
"SOME f. ∀env v pes err_v s. evaluate_match True env s v pes err_v (f env v pes err_v s)"
defines
run_eval = "SOME f. ∀env e s. evaluate True env s e (f env e s)" and
run_eval_list = "SOME f. ∀env es s. evaluate_list True env s es (f env es s)" and
run_eval_match = "SOME f. ∀env v pes err_v s. evaluate_match True env s v pes err_v (f env v pes err_v s)"
proof (standard, goal_cases)
case 1
show ?case
using someI_ex[OF run_eval, rule_format] .
next
case 2
show ?case
using someI_ex[OF run_eval_list, rule_format] .
next
case 3
show ?case
using someI_ex[OF run_eval_match, rule_format] .
qed
hide_fact run_eval
hide_fact run_eval_list
hide_fact run_eval_match
lemma fun_evaluate:
"evaluate_match True env s v pes err_v (map_prod id (map_result hd id) (fun_evaluate_match s env v pes err_v))"
"evaluate_list True env s es (fun_evaluate s env es)"
proof (induction rule: fun_evaluate_induct)
case (5 st env e pes)
from 5(1) show ?case
apply (rule evaluate_list_singleton_cases)
subgoal
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons1)
apply (intro conjI)
apply (rule handle1)
apply assumption
apply (rule evaluate_match_evaluate_list_evaluate.empty)
done
subgoal for s' err
apply (simp split!: error_result.splits)
subgoal for exn
apply (cases "fun_evaluate_match s' env exn pes exn" rule: prod_result_cases; simp only:)
subgoal premises prems
using prems(4)
apply (rule fun_evaluate_matchE)
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons1)
apply (intro conjI)
apply (rule handle2)
apply (intro conjI)
apply (rule prems)
using 5(2)[OF prems(1)[symmetric] refl refl, unfolded prems(4)]
apply simp
by (rule evaluate_match_evaluate_list_evaluate.empty)
subgoal premises prems
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
apply (rule handle2)
apply (intro conjI)
apply (rule prems)
supply error_result.map_ident[simp]
using 5(2)[OF prems(1)[symmetric] refl refl, unfolded prems(4), simplified] .
done
subgoal
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
apply (rule handle3)
by assumption
done
done
next
case (6 st env cn es)
show ?case
proof (cases "do_con_check (c env) cn (length es)")
case True
then show ?thesis
apply simp
apply (frule 6)
apply (cases "fun_evaluate st env (rev es)" rule: prod_result_cases; simp)
subgoal for _ vs
apply (frule do_con_check_build_conv[where vs = "rev vs"], auto split: option.splits)
apply (rule evaluate_match_evaluate_list_evaluate.cons1)
apply (intro conjI)
apply (rule con1)
apply (intro conjI)
apply assumption+
by (rule evaluate_match_evaluate_list_evaluate.empty)
subgoal
by (auto intro: evaluate_match_evaluate_list_evaluate.intros)
done
next
case False
then show ?thesis
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
apply (rule con2)
by assumption
qed
next
case (9 st env op es)
note do_app.simps[simp del]
show ?case
apply (cases "fun_evaluate st env (rev es)" rule: prod_result_cases; simp)
subgoal
apply (safe; simp split!: option.splits)
subgoal using 9 by (auto intro: evaluate_match_evaluate_list_evaluate.intros)
subgoal premises prems
apply (rule conjI)
using 9 prems apply (fastforce intro: evaluate_match_evaluate_list_evaluate.intros)
apply safe
using 9(2)[OF prems(1)[symmetric] refl prems(2) prems(3) refl]
apply (cases rule: evaluate_list_singleton_cases)
subgoal by simp
subgoal
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons1)
using 9 prems
by (auto intro: evaluate_match_evaluate_list_evaluate.intros simp: dec_clock_def)
subgoal
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
using 9 prems
by (auto intro: evaluate_match_evaluate_list_evaluate.intros simp: dec_clock_def)
done
subgoal using 9 by (auto intro: evaluate_match_evaluate_list_evaluate.intros)
subgoal
apply (rule evaluate_list_singletonI)
apply (rule app4)
apply (intro conjI)
using 9 by auto
done
subgoal
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
apply (rule app6)
using 9(1) by simp
done
next
case (12 st env e pes)
from 12(1) show ?case
apply (rule evaluate_list_singleton_cases)
subgoal for s' v
apply simp
apply (cases "fun_evaluate_match s' env v pes Bindv" rule: prod_result_cases; simp only:)
subgoal premises prems
using prems(3)
apply (rule fun_evaluate_matchE)
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons1)
apply (intro conjI)
apply (rule mat1)
apply (fold Bindv_def)
apply (intro conjI)
apply (rule prems)
supply error_result.map_ident[simp]
using 12(2)[OF prems(1)[symmetric] refl, simplified, unfolded prems(3), simplified]
apply simp
by (rule evaluate_match_evaluate_list_evaluate.empty)
subgoal premises prems
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
apply (rule mat1)
apply (fold Bindv_def)
apply (intro conjI)
apply (rule prems)
supply error_result.map_ident[simp]
using 12(2)[OF prems(1)[symmetric] refl, simplified, unfolded prems(3), simplified] .
done
subgoal
apply simp
apply (rule evaluate_match_evaluate_list_evaluate.cons2)
apply (rule mat2)
by assumption
done
next
case (14 st env funs e)
then show ?case
by (cases "allDistinct (map (λ(x, y, z). x) funs)")
(fastforce intro: evaluate_match_evaluate_list_evaluate.intros elim: evaluate_list_singleton_cases)+
next
case (18 st env v2 p e pes err_v)
show ?case
proof (cases "allDistinct (pat_bindings p [])")
case True
show ?thesis
proof (cases "pmatch (c env) (refs st) p v2 []")
case No_match
with True show ?thesis
apply (simp del: id_apply)
apply (rule mat_cons2)
apply (intro conjI)
apply assumption+
apply (rule 18)
apply assumption+
done
next
case Match_type_error
with True show ?thesis
apply simp
apply (rule mat_cons3)
apply assumption+
done
next
case Match
with True show ?thesis
apply (simp del: id_apply)
apply (rule mat_cons1)
apply (intro conjI)
apply assumption+
using 18(2)
apply (rule evaluate_list_singleton_cases)
apply assumption+
apply (auto simp: error_result.map_ident)
done
qed
next
case False
show ?thesis
using False by (auto intro: mat_cons4)
qed
qed (fastforce
intro: evaluate_match_evaluate_list_evaluate.intros
elim: evaluate_list_singleton_cases
split: option.splits prod.splits result.splits if_splits exp_or_val.splits)+
global_interpretation "fun": eval
"λenv e s. map_prod id (map_result hd id) (fun_evaluate s env [e])"
"λenv es s. fun_evaluate s env es"
"λenv v pes err_v s. map_prod id (map_result hd id) (fun_evaluate_match s env v pes err_v)"
proof (standard, goal_cases)
case (1 env s e)
have "evaluate_list True env s [e] (fun_evaluate s env [e])"
by (metis fun_evaluate)
then show ?case
by (rule evaluate_list_singleton_cases) (auto simp: error_result.map_id)
next
case (2 env s es)
show ?case
by (rule fun_evaluate)
next
case (3 env s v pes err_v)
show ?case
by (rule fun_evaluate)
qed
lemmas big_fun_equivalence =
fun.other_eval_eq[OF run.eval_axioms]
end