Theory Big_Step_Unclocked_Single

theory Big_Step_Unclocked_Single
imports Big_Step_Unclocked Big_Step_Clocked Evaluate_Single Big_Step_Fun_Equiv
```section "An even simpler version without mutual induction"

theory Big_Step_Unclocked_Single
imports Big_Step_Unclocked Big_Step_Clocked Evaluate_Single Big_Step_Fun_Equiv
begin

inductive evaluate_list ::
"('ffi state ⇒ exp ⇒ 'ffi state*(v,v) result ⇒ bool) ⇒
'ffi state ⇒ exp list ⇒ 'ffi state*(v list, v)result ⇒ bool" for P where
empty:
"evaluate_list P s [] (s,Rval [])" |

cons1:
"P s1 e (s2, Rval v) ⟹
evaluate_list P s2 es (s3, Rval vs) ⟹
evaluate_list P s1 (e#es) (s3, Rval (v#vs))" |

cons2:
"P s1 e (s2, Rerr err) ⟹
evaluate_list P s1 (e#es) (s2, Rerr err)" |

cons3:
"P s1 e (s2, Rval v) ⟹
evaluate_list P s2 es (s3, Rerr err) ⟹
evaluate_list P s1 (e#es) (s3, Rerr err)"

lemma evaluate_list_mono_strong[intro?]:
assumes "evaluate_list R s es r"
assumes "⋀s e r. e ∈ set es ⟹ R s e r ⟹ Q s e r"
shows "evaluate_list Q s es r"
using assms by (induction; fastforce intro: evaluate_list.intros)

lemma evaluate_list_mono[mono]:
assumes "R ≤ Q"
shows "evaluate_list R ≤ evaluate_list Q"
using assms unfolding le_fun_def le_bool_def
by (metis evaluate_list_mono_strong)

inductive evaluate :: "v sem_env ⇒ 'ffi state ⇒ exp ⇒ 'ffi state*(v,v) result ⇒ bool" where

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

raise1:
"evaluate env s1 e (s2, Rval v) ⟹
evaluate env s1 (Raise e) (s2, Rerr (Rraise v))" |

raise2:
"evaluate env s1 e (s2, Rerr err) ⟹
evaluate env s1 (Raise e) (s2, Rerr err)" |

handle1:
"evaluate env s1 e (s2, Rval v) ⟹
evaluate env s1 (Handle e pes) (s2, Rval v)" |

handle2:
"evaluate env s1 e (s2, Rerr (Rraise v)) ⟹
match_result env s2 v pes v = Rval (e', env') ⟹
evaluate (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s2 e' bv ⟹
evaluate env s1 (Handle e pes) bv" |

handle2b:
"evaluate env s1 e (s2, Rerr (Rraise v)) ⟹
match_result env s2 v pes v = Rerr err ⟹
evaluate env s1 (Handle e pes) (s2, Rerr err)" |

handle3:
"evaluate env s1 e (s2, Rerr (Rabort a)) ⟹
evaluate env s1 (Handle e pes) (s2, Rerr (Rabort a))" |

con1:
"do_con_check (c env) cn (length es) ⟹
build_conv (c env) cn (rev vs) = Some v ⟹
evaluate_list (evaluate env) s1 (rev es) (s2, Rval vs) ⟹
evaluate env s1 (Con cn es) (s2, Rval v)" |

con2:
"¬(do_con_check (c env) cn (length es)) ⟹
evaluate env s (Con cn es) (s, Rerr (Rabort Rtype_error))" |

con3:
"do_con_check (c env) cn (length es) ⟹
evaluate_list (evaluate env) s1 (rev es) (s2, Rerr err) ⟹
evaluate env s1 (Con cn es) (s2, Rerr err)" |

var1:
"nsLookup (sem_env.v env) n = Some v ⟹
evaluate env s (Var n) (s, Rval v)" |

var2:
"nsLookup (sem_env.v env) n = None ⟹
evaluate env s (Var n) (s, Rerr (Rabort Rtype_error))" |

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

app1:
"evaluate_list (evaluate env) s1 (rev es) (s2, Rval vs) ⟹
do_opapp (rev vs) = Some (env', e) ⟹
evaluate env' s2 e bv ⟹
evaluate env s1 (App Opapp es) bv" |

app3:
"evaluate_list (evaluate env) s1 (rev es) (s2, Rval vs) ⟹
(do_opapp (rev vs) = None) ⟹
evaluate env s1 (App Opapp es) (s2, Rerr (Rabort Rtype_error))" |

app4:
"evaluate_list (evaluate env) s1 (rev es) (s2, Rval vs) ⟹
do_app (refs s2, ffi s2) op0 (rev vs) = Some ((refs',ffi'), res) ⟹
op0 ≠ Opapp ⟹
evaluate env s1 (App op0 es) (s2 ⦇refs:=refs',ffi:=ffi'⦈, res)" |

app5:
"evaluate_list (evaluate env) s1 (rev es) (s2, Rval vs) ⟹
do_app (refs s2, ffi s2) op0 (rev vs) = None ⟹
op0 ≠ Opapp ⟹
evaluate env s1 (App op0 es) (s2, Rerr (Rabort Rtype_error))" |

app6:
"evaluate_list (evaluate env) s1 (rev es) (s2, Rerr err) ⟹
evaluate env s1 (App op0 es) (s2, Rerr err)" |

log1:
"evaluate env s1 e1 (s2, Rval v1) ⟹
do_log op0 v1 e2 = Some (Exp e') ⟹
evaluate env s2 e' bv ⟹
evaluate env s1 (Log op0 e1 e2) bv " |

log2:
"evaluate env s1 e1 (s2, Rval v1) ⟹
(do_log op0 v1 e2 = Some (Val bv)) ⟹
evaluate env s1 (Log op0 e1 e2) (s2, Rval bv)" |

log3:
"evaluate env s1 e1 (s2, Rval v1) ⟹
(do_log op0 v1 e2 = None) ⟹
evaluate env s1 (Log op0 e1 e2) (s2, Rerr (Rabort Rtype_error))" |

log4:
"evaluate env s e1 (s', Rerr err) ⟹
evaluate env s (Log op0 e1 e2) (s', Rerr err)" |

if1:
"evaluate env s1 e1 (s2, Rval v1) ⟹
do_if v1 e2 e3 = Some e' ⟹
evaluate env s2 e' bv ⟹
evaluate env s1 (If e1 e2 e3) bv " |

if2:
"evaluate env s1 e1 (s2, Rval v1) ⟹
(do_if v1 e2 e3 = None) ⟹
evaluate env s1 (If e1 e2 e3) (s2, Rerr (Rabort Rtype_error))" |

if3:
"evaluate env s e1 (s', Rerr err) ⟹
evaluate env s (If e1 e2 e3) (s', Rerr err)" |

mat1:
"evaluate env s1 e (s2, Rval v1) ⟹
match_result env s2 v1 pes Bindv = Rval (e', env') ⟹
evaluate (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s2 e' bv ⟹
evaluate env s1 (Mat e pes) bv " |

mat1b:
"evaluate env s1 e (s2, Rval v1) ⟹
match_result env s2 v1 pes Bindv = Rerr err ⟹
evaluate env s1 (Mat e pes) (s2, Rerr err)" |

mat2:
"evaluate env s e (s', Rerr err) ⟹
evaluate env s (Mat e pes) (s', Rerr err)" |

let1:
"evaluate env s1 e1 (s2, Rval v1) ⟹
evaluate ( env ⦇ sem_env.v := (nsOptBind n v1(sem_env.v env)) ⦈) s2 e2 bv ⟹
evaluate env s1 (Let n e1 e2) bv " |

let2:
"evaluate env s e1 (s', Rerr err) ⟹
evaluate env s (Let n e1 e2) (s', Rerr err)" |

letrec1:
"distinct (List.map ( λx .
(case  x of (x,y,z) => x )) funs) ⟹
evaluate ( env ⦇ sem_env.v := (build_rec_env funs env(sem_env.v env)) ⦈) s e bv ⟹
evaluate env s (Letrec funs e) bv " |

letrec2:
"¬ (distinct (List.map ( λx .
(case  x of (x,y,z) => x )) funs)) ⟹
evaluate env s (Letrec funs e) (s, Rerr (Rabort Rtype_error))" |

tannot:
"evaluate env s e bv ⟹
evaluate env s (Tannot e t0) bv " |

locannot:
"evaluate env s e bv ⟹
evaluate env s (Lannot e l) bv "

lemma unclocked_single_list_sound:
"evaluate_list (Big_Step_Unclocked.evaluate v) s es bv ⟹ Big_Step_Unclocked.evaluate_list v s es bv"
by (induction rule: evaluate_list.induct) (auto intro: evaluate_list_evaluate.intros)

lemma unclocked_single_sound:
"evaluate v s e bv ⟹ Big_Step_Unclocked.evaluate v s e bv"
by (induction rule:evaluate.induct)
(auto simp del: do_app.simps intro: Big_Step_Unclocked.evaluate_list_evaluate.intros unclocked_single_list_sound
evaluate_list_mono_strong)

lemma unclocked_single_complete:
"Big_Step_Unclocked.evaluate_list v s es bv1 ⟹ evaluate_list (evaluate v) s es bv1"
"Big_Step_Unclocked.evaluate v s e bv2 ⟹ evaluate v s e bv2"
by (induction rule: evaluate_list_evaluate.inducts)
(auto intro: evaluate.intros evaluate_list.intros)

corollary unclocked_single_eq:
"evaluate = Big_Step_Unclocked.evaluate"
by (rule ext)+ (metis unclocked_single_sound unclocked_single_complete)

corollary unclocked_single_eq':
"evaluate = BigStep.evaluate False"

corollary unclocked_single_determ:
"evaluate env s e r3a ⟹ evaluate env s e r3b ⟹ r3a = r3b"
by (metis unclocked_single_eq unclocked_determ)

lemma unclocked_single_fun_eq:
"((∃k. Evaluate_Single.evaluate env (s ⦇ clock:= k ⦈) e = (s', r)) ∧ r ≠  Rerr (Rabort Rtimeout_error) ∧ (clock s) = (clock s')) =
evaluate env s e (s',r)"
apply (subst fun_evaluate_equiv')
apply (subst unclocked_single_eq)
apply (subst unclocked_eq)
apply (subst fun.evaluate_iff_sym(1)[symmetric])
apply (subst big_clocked_unclocked_equiv)
using clocked_evaluate by metis

end```