Theory Big_Step_Unclocked

section "A simpler version with no clock parameter and factored-out matching"

theory Big_Step_Unclocked
imports
  Semantic_Extras
  Big_Step_Determ
begin

inductive

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

"lit" : " ⋀ env l s.

evaluate env s (Lit l) (s, Rval (Litv l))"

|

"raise1" : " ⋀ env e s1 s2 v1.
evaluate s1 env e (s2, Rval v1)
==>
evaluate s1 env (Raise e) (s2, Rerr (Rraise v1))"

|

"raise2" : " ⋀ env e s1 s2 err.
evaluate s1 env e (s2, Rerr err)
==>
evaluate s1 env (Raise e) (s2, Rerr err)"

|

"handle1" : " ⋀ s1 s2 env e v1 pes.
evaluate s1 env e (s2, Rval v1)
==>
evaluate s1 env (Handle e pes) (s2, Rval v1)"

|

"handle2" : " ⋀ s1 s2 env e pes v1 bv.
evaluate env s1 e (s2, Rerr (Rraise v1)) ⟹
match_result env s2 v1 pes v1 = 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" : " ⋀ s1 s2 env e pes v1.
evaluate env s1 e (s2, Rerr (Rraise v1)) ⟹
match_result env s2 v1 pes v1 = Rerr err
==>
evaluate env s1 (Handle e pes) (s2, Rerr err)"

|

"handle3" : " ⋀ s1 s2 env e pes a.
evaluate env s1 e (s2, Rerr (Rabort a))
==>
evaluate env s1 (Handle e pes) (s2, Rerr (Rabort a))"

|

"con1" : " ⋀ env cn es vs s s' v1.
do_con_check(c   env) cn (List.length es) ⟹
build_conv(c   env) cn (List.rev vs) = Some v1 ⟹
evaluate_list env s (List.rev es) (s', Rval vs)
==>
evaluate env s (Con cn es) (s', Rval v1)"

|

"con2" : " ⋀ env cn es s.
¬ (do_con_check(c   env) cn (List.length es))
==>
evaluate env s (Con cn es) (s, Rerr (Rabort Rtype_error))"

|

"con3" : " ⋀ env cn es err s s'.
do_con_check(c   env) cn (List.length es) ⟹
evaluate_list env s (List.rev es) (s', Rerr err)
==>
evaluate env s (Con cn es) (s', Rerr err)"

|

"var1" : " ⋀ env n v1 s.
nsLookup(sem_env.v   env) n = Some v1
==>
evaluate env s (Var n) (s, Rval v1)"

|

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

|

"fn" : " ⋀ env n e s.

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

|

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

|

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

|

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

|

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

|

"app6" : " ⋀ env op0 es err s1 s2.
evaluate_list env s1 (List.rev es) (s2, Rerr err)
==>
evaluate env s1 (App op0 es) (s2, Rerr err)"

|

"log1" : " ⋀ env op0 e1 e2 v1 e' bv s1 s2.
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" : " ⋀ env op0 e1 e2 v1 bv s1 s2.
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" : " ⋀ env op0 e1 e2 v1 s1 s2.
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" : " ⋀ env op0 e1 e2 err s s'.
evaluate env s e1 (s', Rerr err)
==>
evaluate env s (Log op0 e1 e2) (s', Rerr err)"

|

"if1" : " ⋀ env e1 e2 e3 v1 e' bv s1 s2.
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" : " ⋀ env e1 e2 e3 v1 s1 s2.
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" : " ⋀ env e1 e2 e3 err s s'.
evaluate env s e1 (s', Rerr err)
==>
evaluate env s (If e1 e2 e3) (s', Rerr err)"

|

"mat1" : " ⋀ env e pes v1 bv s1 s2.
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" : " ⋀ env e pes v1 s1 s2.
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" : " ⋀ env e pes err s s'.
evaluate env s e (s', Rerr err)
==>
evaluate env s (Mat e pes) (s', Rerr err)"

|

"let1" : " ⋀ env n e1 e2 v1 bv s1 s2.
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" : " ⋀ env n e1 e2 err s s'.
evaluate env s e1 (s', Rerr err)
==>
evaluate env s (Let n e1 e2) (s', Rerr err)"

|

"letrec1" : " ⋀ env funs e bv s.
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" : " ⋀ env funs e s.
¬ (distinct (List.map ( λx .
  (case  x of (x,y,z) => x )) funs))
==>
evaluate env s (Letrec funs e) (s, Rerr (Rabort Rtype_error))"

|

"tannot" : " ⋀ env e t0 s bv.
evaluate env s e bv
==>
evaluate env s (Tannot e t0) bv "

|

"locannot" : " ⋀ env e l s bv.
evaluate env s e bv
==>
evaluate env s (Lannot e l) bv "

|

"empty" : " ⋀ env s.

evaluate_list env s [] (s, Rval [])"

|

"cons1" : " ⋀ env e es v1 vs s1 s2 s3.
evaluate env s1 e (s2, Rval v1) ⟹
evaluate_list env s2 es (s3, Rval vs)
==>
evaluate_list env s1 (e # es) (s3, Rval (v1 # vs))"

|

"cons2" : " ⋀ env e es err s s'.
evaluate env s e (s', Rerr err)
==>
evaluate_list env s (e # es) (s', Rerr err)"

|

"cons3" : " ⋀ env e es v1 err s1 s2 s3.
evaluate env s1 e (s2, Rval v1) ⟹
evaluate_list env s2 es (s3, Rerr err)
==>
evaluate_list env s1 (e # es) (s3, Rerr err)"

lemma unclocked_sound:
  "evaluate_list v s es bv ⟹ BigStep.evaluate_list False v s es bv"
  "evaluate v s e bv' ⟹ BigStep.evaluate False v s e bv'"
proof (induction rule: evaluate_list_evaluate.inducts)
  case (handle2 e' env' s1 s2 env e pes v1 bv)
  show ?case
    apply (rule BigStep.handle2, intro conjI)
    apply fact
    apply (rule match_result_sound_val)
    apply fact+
    done
next
  case (handle2b err s1 s2 env e pes v1)
  show ?case
    apply (rule BigStep.handle2, intro conjI)
    apply fact
    apply (rule match_result_sound_err)
    apply fact
    done
next
  case (mat1 e' env' env e pes v1 bv s1 s2)
  show ?case
    apply (rule BigStep.mat1, fold Bindv_def, intro conjI)
    apply fact
    apply (rule match_result_sound_val)
    apply fact+
    done
next
  case (mat1b err env e pes v1 s1 s2)
  show ?case
    apply (rule BigStep.mat1, fold Bindv_def, intro conjI)
    apply fact
    apply (rule match_result_sound_err)
    apply fact
    done
qed (fastforce simp: all_distinct_alt_def[symmetric] intro: evaluate_match_evaluate_list_evaluate.intros)+

context begin

private lemma unclocked_complete0:
  "BigStep.evaluate_match ck env s v0 pes err_v (s', bv) ⟹ ¬ ck ⟹ (
    case bv of
        Rval v ⇒
          ∃e env'.
            match_result env s v0 pes err_v = Rval (e, env') ∧
            evaluate (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 (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s e (s', Rerr err)))"
  "BigStep.evaluate_list ck v s es (s', bv0) ⟹ ¬ ck ⟹ evaluate_list v s es (s', bv0)"
  "BigStep.evaluate ck v s e (s', bv) ⟹ ¬ ck ⟹ evaluate v s e (s', bv)"
proof (induction rule: evaluate_induct)
  case (handle2 ck s1 s2 env e pes v1 s3 bv)
  show ?case
    proof (cases bv)
      case (Rval v)
      with handle2 obtain e env' where
        "match_result env s2 v1 pes v1 = Rval (e, env')"
        "evaluate (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s2 e (s3, Rval v)"
        by auto

      show ?thesis
        unfolding ‹bv = _›
        apply (rule evaluate_list_evaluate.handle2)
        using handle2 apply blast
        by fact+
    next
      case (Rerr err)
      with handle2 consider
        (match_err) "match_result env s2 v1 pes v1 = Rerr err" |
        (eval_err) e env' where
          "match_result env s2 v1 pes v1 = Rval (e, env')"
          "evaluate (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈) s2 e (s3, Rerr err)"
        by auto
      then show ?thesis
        proof cases
          case match_err
          then have "evaluate_match ck env s2 v1 pes v1 (s2, Rerr err)"
            by (metis match_result_sound_err)
          moreover have "evaluate_match ck env s2 v1 pes v1 (s3, Rerr err)"
            using handle2 unfolding ‹bv = _› by blast
          ultimately have "s2 = s3"
            by (metis evaluate_determ fst_conv)

          show ?thesis
            unfolding ‹bv = _›
            apply (rule evaluate_list_evaluate.handle2b)
            using handle2 unfolding ‹s2 = _› apply blast
            using match_err unfolding ‹s2 = _› .
        next
          case eval_err
          show ?thesis
            unfolding ‹bv = _›
            apply (rule evaluate_list_evaluate.handle2)
            using handle2 apply blast
            by fact+
        qed
    qed
next
  case (mat1 ck env e pes v1 s3 v' s1 s2)
  then show ?case
    (* this is the same proof as above, but with less Isar and more apply *)
    apply (auto split: result.splits simp: Bindv_def[symmetric])
    subgoal by (rule evaluate_list_evaluate.mat1) auto
    subgoal
      apply (frule match_result_sound_err)
      apply (subgoal_tac "s2 = s3")
      apply (rule evaluate_list_evaluate.mat1b)
      apply force
      apply force
      apply (drule evaluate_determ)
      apply assumption
      by auto
    subgoal by (rule evaluate_list_evaluate.mat1) auto
    done
next
  case (mat_cons1 ck env env' v1 p pes e a b err_v s)
  then show ?case
    by (auto split: result.splits)
next
  case (mat_cons2 ck env v1 p e pes a b s err_v)
  then show ?case
    by (auto split: result.splits)
qed (fastforce simp: all_distinct_alt_def intro: evaluate_list_evaluate.intros)+

lemma unclocked_complete:
  "BigStep.evaluate_list False v s es bv' ⟹ evaluate_list v s es bv'"
  "BigStep.evaluate False v s e bv ⟹ evaluate v s e bv"
apply (cases bv'; metis unclocked_complete0)
apply (cases bv; metis unclocked_complete0)
done

end

lemma unclocked_eq:
  "evaluate_list = BigStep.evaluate_list False"
  "evaluate = BigStep.evaluate False"
by (auto intro: unclocked_sound unclocked_complete intro!: ext)

lemma unclocked_determ:
  "evaluate_list env s es r2a ⟹ evaluate_list env s es r2b ⟹ r2a = r2b"
  "evaluate env s e r3a ⟹ evaluate env s e r3b ⟹ r3a = r3b"
by (metis unclocked_eq evaluate_determ)+

end