# Theory Evaluate_Single

section "Simplifiying the definition: no mutual recursion"

theory Evaluate_Single
imports Evaluate_Clock
begin

fun evaluate_list ::
"('ffi state  exp  'ffi state*(v, v) result)
'ffi state  exp list  'ffi state*(v list, v) result" where

Nil:
"evaluate_list eval s [] = (s, Rval [])" |

Cons:
"evaluate_list eval s (e#es) =
(case fix_clock s (eval s e) of
(s', Rval v)
(case evaluate_list eval s' es of
(s'', Rval vs)  (s'', Rval (v#vs))
| res  res)
|  (s', Rerr err)  (s', Rerr err))"

lemma evaluate_list_cong[fundef_cong]:
assumes "e s. e  set es1  clock s  clock s1  eval1 s e = eval2 s e" "s1 = s2" "es1 = es2"
shows "evaluate_list eval1 s1 es1 = evaluate_list eval2 s2 es2"
using assms by (induction es1 arbitrary: es2 s1 s2) (fastforce simp: fix_clock_alt_def split: prod.splits result.splits)+

function (sequential)
evaluate :: " v sem_env 'ffi state  exp  'ffi state*(v,v) result" where

Lit:
"evaluate env s (Lit l) = (s, Rval (Litv l))" |

Raise:
"evaluate env s (Raise e) =
(case evaluate env s e of
(s', Rval v)  (s', Rerr (Rraise (v)))
| res  res)" |

Handle:
"evaluate env s (Handle e pes) =
(case evaluate env s e of
(s', Rerr (Rraise v))
(case match_result env s' v pes v of
(Rval (e', env'))
evaluate (env  sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ) s' e'
| (Rerr err)  (s', Rerr err))
| res  res)" |

Con:
"evaluate env s (Con cn es) =
(if do_con_check (c env) cn (length es) then
(case evaluate_list (evaluate env) s (rev es) of
(s', Rval vs)
(case build_conv (c env) cn (rev vs) of
Some v  (s', Rval v)
| None  (s', Rerr (Rabort Rtype_error)))
| (s', Rerr err)  (s', Rerr err))
else (s, Rerr (Rabort Rtype_error)))" |

Var:
"evaluate env s (Var n) =
(case nsLookup (sem_env.v env) n of
Some v  (s, Rval v)
| None  (s, Rerr (Rabort Rtype_error)))" |

Fun:
"evaluate env s (Fun n e) = (s, Rval (Closure env n e))" |

App:
"evaluate env s (App op0 es) =
(case evaluate_list (evaluate env) s (rev es) of
(s', Rval vs)
(if op0 = Opapp then
(case do_opapp (rev vs) of
Some (env', e)
(if (clock s' = 0) then
(s', Rerr (Rabort Rtimeout_error))
else
evaluate env' (dec_clock s') e)
| None  (s', Rerr (Rabort Rtype_error)))
else
(case do_app (refs s', ffi s') op0 (rev vs) of
Some ((refs',ffi'), res)  (s' refs:=refs',ffi:=ffi', res)
| None  (s', Rerr (Rabort Rtype_error))))
| (s', Rerr err)  (s', Rerr err))" |

Log:
"evaluate env s (Log op0 e1 e2) =
(case evaluate env s e1 of
(s', Rval v)
(case do_log op0 v e2 of
Some (Exp e')  evaluate env s' e'
| Some (Val bv)  (s', Rval bv)
| None  (s', Rerr (Rabort Rtype_error)))
| res  res)" |

If:
"evaluate env s (If e1 e2 e3) =
(case evaluate env s e1 of
(s', Rval v)
(case do_if v e2 e3 of
Some e'  evaluate env s' e'
| None  (s', Rerr (Rabort Rtype_error)))
| res  res)" |

Mat:
"evaluate env s (Mat e pes) =
(case evaluate env s e of
(s', Rval v)
(case match_result env s' v pes Bindv of
Rval (e', env')
evaluate (env  sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ) s' e'
| Rerr err  (s', Rerr err))
| res  res)" |

Let:
"evaluate env s (Let n e1 e2) =
(case evaluate env s e1 of
(s', Rval v)
evaluate ( env  sem_env.v := (nsOptBind n v(sem_env.v env)) ) s' e2
| res  res)" |

Letrec:
"evaluate env s (Letrec funs e) =
(if distinct (List.map (λx. (case  x of (x,y,z) => x )) funs) then
evaluate ( env  sem_env.v := (build_rec_env funs env(sem_env.v env)) ) s e
else
(s, Rerr (Rabort Rtype_error)))" |

Tannot:
"evaluate env s (Tannot e t0) = evaluate env s e" |

Lannot:
"evaluate env s (Lannot e l) = evaluate env s e"
by pat_completeness auto

context
notes do_app.simps[simp del]
begin

lemma match_result_elem:
assumes "match_result env s v0 pes err_v = Rval (e, env')"
shows "pat. (pat, e)  set pes"
using assms proof (induction pes)
case Nil
then show ?case by auto
next
case (Cons pe pes)
then obtain p e where "pe = (p, e)" by force
show ?case
using Cons(2)
unfolding pe = _
apply (cases "allDistinct (pat_bindings p [])")
apply (cases "pmatch (c env) (refs s) p v0 []")
using Cons(1) by auto+
qed

private lemma evaluate_list_clock_monotone: "clock (fst (evaluate_list eval s es))  clock s"
apply (induction es arbitrary: s)
apply (auto split:prod.splits result.splits simp add:fix_clock_alt_def dest!:fstI intro:le_trans)
apply (metis state.record_simps(1))+
done

lemma i_hate_words_helper:
"i  (j - k :: nat)  i  j"
by simp

thm i_hate_words_helper [THEN le_trans, no_vars]

private lemma evaluate_clock_monotone:
‹clock (fst (evaluate env s e))  clock s
if ‹evaluate_dom (env, s, e)
proof -
have *: i  j - k  j  r  i  r for i j k r :: nat
by arith
from that show ?thesis
by induction (fastforce simp add: evaluate.psimps do_con_check_build_conv evaluate_list_clock_monotone
split: prod.splits result.splits option.splits exp_or_val.splits error_result.splits
dest: fstI intro: *)+
qed

private definition fun_evaluate_single_relation where
"fun_evaluate_single_relation = inv_image (less_than <*lex*> less_than) (λx.
case x of (_, s, e)  (clock s, size_exp' e))"

private lemma pat_elem_less_size:
"(pat, e)  set pes  size_exp' e < (size_list (size_prod size size_exp') pes)"
by (induction pes) auto

private lemma elem_less_size: "e  set es  size_exp' e  size_list size_exp' es"
by (induction es) auto

lemma evaluate_total: "All evaluate_dom"
proof (relation "fun_evaluate_single_relation", unfold fun_evaluate_single_relation_def, goal_cases)
case 7
then show ?case
using evaluate_list_clock_monotone "7"(1)[symmetric]
by (auto dest!: fstI simp add:evaluate_list_clock_monotone Suc_le_lessD)
qed (auto simp add: less_Suc_eq_le Suc_le_lessD do_if_def do_log_alt_def evaluate_list_clock_monotone elem_less_size
split:lop.splits v.splits option.splits tid_or_exn.splits if_splits id0.splits list.splits
dest!:evaluate_clock_monotone match_result_elem fstI dest:sym pat_elem_less_size intro:le_neq_implies_less)

termination evaluate by (rule evaluate_total)

lemma evaluate_clock_monotone': "evaluate eval s e = (s', r)   clock s'  clock s"
using fst_conv evaluate_clock_monotone evaluate_total
by metis

fun evaluate_list' :: "v sem_env  'ffi state  exp list  'ffi state*(v list, v) result" where
"evaluate_list' env s [] = (s, Rval [])" |
"evaluate_list' env s (e#es) =
(case evaluate env s e of
(s', Rval v)
(case evaluate_list' env s' es of
(s'', Rval vs)  (s'', Rval (v#vs))
| res  res)
|  (s', Rerr err)  (s', Rerr err))"

lemma fix_clock_evaluate[simp]: "fix_clock s (evaluate eval s e) = evaluate eval s e"
unfolding fix_clock_alt_def
apply (auto simp: datatype_record_update split: state.splits prod.splits)
using evaluate_clock_monotone' by fastforce

lemma evaluate_list_eq[simp]: "evaluate_list (evaluate env) = evaluate_list' env"
apply (rule ext)+
subgoal for s es
by (induction rule:evaluate_list'.induct) (auto split:prod.splits result.splits)
done

declare evaluate_list.simps[simp del]

lemma fun_evaluate_equiv:
"fun_evaluate_match s env v pes err_v = (case match_result env s v pes err_v of
Rerr err  (s, Rerr err)
| Rval (e, env')  evaluate_list (evaluate (env  sem_env.v := (nsAppend (alist_to_ns env') (sem_env.v env)) )) s [e])"
"fun_evaluate s env es = evaluate_list (evaluate env) s es"
by (induction rule: fun_evaluate_induct)
(auto split: prod.splits result.splits match_result.splits option.splits exp_or_val.splits
if_splits match_result.splits error_result.splits
simp: all_distinct_alt_def)

corollary fun_evaluate_equiv':
"evaluate env s e = map_prod id (map_result hd id) (fun_evaluate s env [e])"
by (subst fun_evaluate_equiv) (simp split: prod.splits result.splits add: error_result.map_id)

end

end