Theory BigStep

(*  Title:      Jinja/J/BigStep.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Big Step Semantics›

theory BigStep imports Expr State begin

inductive
  eval :: "J_prog ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
          (‹_ ⊢ ((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))› [51,0,0,0,0] 81)
  and evals :: "J_prog ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
           (‹_ ⊢ ((1⟨_,/_⟩) [⇒]/ (1⟨_,/_⟩))› [51,0,0,0,0] 81)
  for P :: J_prog
where

  New:
  "⟦ new_Addr h = Some a; P ⊢ C has_fields FDTs; h' = h(a↦(C,init_fields FDTs)) ⟧
  ⟹ P ⊢ ⟨new C,(h,l)⟩ ⇒ ⟨addr a,(h',l)⟩"

| NewFail:
  "new_Addr h = None ⟹
  P ⊢ ⟨new C, (h,l)⟩ ⇒ ⟨THROW OutOfMemory,(h,l)⟩"

| Cast:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,(h,l)⟩; h a = Some(D,fs); P ⊢ D ≼* C ⟧
  ⟹ P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨addr a,(h,l)⟩"

| CastNull:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨null,s1⟩"

| CastFail:
  "⟦ P ⊢ ⟨e,s0⟩⇒ ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨THROW ClassCast,(h,l)⟩"

| CastThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨throw e',s1⟩"

| Val:
  "P ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩"

| BinOp:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v2,s2⟩; binop(bop,v1,v2) = Some v ⟧
  ⟹ P ⊢ ⟨e1 «bop» e2,s0⟩⇒⟨Val v,s2⟩"

| BinOpThrow1:
  "P ⊢ ⟨e1,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢ ⟨e1 «bop» e2, s0⟩ ⇒ ⟨throw e,s1⟩"

| BinOpThrow2:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨throw e,s2⟩ ⟧
  ⟹ P ⊢ ⟨e1 «bop» e2,s0⟩ ⇒ ⟨throw e,s2⟩"

| Var:
  "l V = Some v ⟹
  P ⊢ ⟨Var V,(h,l)⟩ ⇒ ⟨Val v,(h,l)⟩"

| LAss:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨Val v,(h,l)⟩; l' = l(V↦v) ⟧
  ⟹ P ⊢ ⟨V:=e,s0⟩ ⇒ ⟨unit,(h,l')⟩"

| LAssThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨V:=e,s0⟩ ⇒ ⟨throw e',s1⟩"

| FAcc:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,(h,l)⟩; h a = Some(C,fs); fs(F,D) = Some v ⟧
  ⟹ P ⊢ ⟨e∙F{D},s0⟩ ⇒ ⟨Val v,(h,l)⟩"

| FAccNull:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢ ⟨e∙F{D},s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"

| FAccThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨e∙F{D},s0⟩ ⇒ ⟨throw e',s1⟩"

| FAss:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2)⟩;
     h2 a = Some(C,fs); fs' = fs((F,D)↦v); h2' = h2(a↦(C,fs')) ⟧
  ⟹ P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨unit,(h2',l2)⟩"

| FAssNull:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨null,s1⟩;  P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v,s2⟩ ⟧ ⟹
  P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"

| FAssThrow1:
  "P ⊢ ⟨e1,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨throw e',s1⟩"

| FAssThrow2:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨throw e',s2⟩ ⟧
  ⟹ P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨throw e',s2⟩"

| CallObjThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨throw e',s1⟩"

| CallParamsThrow:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨es,s1⟩ [⇒] ⟨map Val vs @ throw ex # es',s2⟩ ⟧
   ⟹ P ⊢ ⟨e∙M(es),s0⟩ ⇒ ⟨throw ex,s2⟩"

| CallNull:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩;  P ⊢ ⟨ps,s1⟩ [⇒] ⟨map Val vs,s2⟩ ⟧
  ⟹ P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"

| Call:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩;  P ⊢ ⟨ps,s1⟩ [⇒] ⟨map Val vs,(h2,l2)⟩;
     h2 a = Some(C,fs);  P ⊢ C sees M:Ts→T = (pns,body) in D;
     length vs = length pns;  l2' = [this↦Addr a, pns[↦]vs];
     P ⊢ ⟨body,(h2,l2')⟩ ⇒ ⟨e',(h3,l3)⟩ ⟧
  ⟹ P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨e',(h3,l2)⟩"

| Block:
  "P ⊢ ⟨e0,(h0,l0(V:=None))⟩ ⇒ ⟨e1,(h1,l1)⟩ ⟹
  P ⊢ ⟨{V:T; e0},(h0,l0)⟩ ⇒ ⟨e1,(h1,l1(V:=l0 V))⟩"

| Seq:
  "⟦ P ⊢ ⟨e0,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨e1,s1⟩ ⇒ ⟨e2,s2⟩ ⟧
  ⟹ P ⊢ ⟨e0;;e1,s0⟩ ⇒ ⟨e2,s2⟩"

| SeqThrow:
  "P ⊢ ⟨e0,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢ ⟨e0;;e1,s0⟩⇒⟨throw e,s1⟩"

| CondT:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢ ⟨e1,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢ ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"

| CondF:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨false,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢ ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"

| CondThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨if (e) e1 else e2, s0⟩ ⇒ ⟨throw e',s1⟩"

| WhileF:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨false,s1⟩ ⟹
  P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨unit,s1⟩"

| WhileT:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢ ⟨c,s1⟩ ⇒ ⟨Val v1,s2⟩; P ⊢ ⟨while (e) c,s2⟩ ⇒ ⟨e3,s3⟩ ⟧
  ⟹ P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨e3,s3⟩"

| WhileCondThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨ throw e',s1⟩ ⟹
  P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s1⟩"

| WhileBodyThrow:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢ ⟨c,s1⟩ ⇒ ⟨throw e',s2⟩⟧
  ⟹ P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s2⟩"

| Throw:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩ ⟹
  P ⊢ ⟨throw e,s0⟩ ⇒ ⟨Throw a,s1⟩"

| ThrowNull:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢ ⟨throw e,s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"

| ThrowThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨throw e,s0⟩ ⇒ ⟨throw e',s1⟩"

| Try:
  "P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩ ⟹
  P ⊢ ⟨try e1 catch(C V) e2,s0⟩ ⇒ ⟨Val v1,s1⟩"

| TryCatch:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,l1)⟩;  h1 a = Some(D,fs);  P ⊢ D ≼* C;
     P ⊢ ⟨e2,(h1,l1(V↦Addr a))⟩ ⇒ ⟨e2',(h2,l2)⟩ ⟧
  ⟹ P ⊢ ⟨try e1 catch(C V) e2,s0⟩ ⇒ ⟨e2',(h2,l2(V:=l1 V))⟩"

| TryThrow:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,l1)⟩;  h1 a = Some(D,fs);  ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢ ⟨try e1 catch(C V) e2,s0⟩ ⇒ ⟨Throw a,(h1,l1)⟩"

| Nil:
  "P ⊢ ⟨[],s⟩ [⇒] ⟨[],s⟩"

| Cons:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨es,s1⟩ [⇒] ⟨es',s2⟩ ⟧
  ⟹ P ⊢ ⟨e#es,s0⟩ [⇒] ⟨Val v # es',s2⟩"

| ConsThrow:
  "P ⊢ ⟨e, s0⟩ ⇒ ⟨throw e', s1⟩ ⟹
  P ⊢ ⟨e#es, s0⟩ [⇒] ⟨throw e' # es, s1⟩"

(*<*)
lemmas eval_evals_induct = eval_evals.induct [split_format (complete)]
  and eval_evals_inducts = eval_evals.inducts [split_format (complete)]

inductive_cases eval_cases [cases set]:
 "P ⊢ ⟨Cast C e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨Val v,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e1 «bop» e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨V:=e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e∙F{D},s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e1∙F{D}:=e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e∙M{D}(es),s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨{V:T;e1},s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e1;;e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨if (e) e1 else e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨while (b) c,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨throw e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨try e1 catch(C V) e2,s⟩ ⇒ ⟨e',s'⟩"
 
inductive_cases evals_cases [cases set]:
 "P ⊢ ⟨[],s⟩ [⇒] ⟨e',s'⟩"
 "P ⊢ ⟨e#es,s⟩ [⇒] ⟨e',s'⟩"
(*>*) 


subsection"Final expressions"

definition final :: "'a exp ⇒ bool"
where
  "final e  ≡  (∃v. e = Val v) ∨ (∃a. e = Throw a)"

definition finals:: "'a exp list ⇒ bool"
where
  "finals es  ≡  (∃vs. es = map Val vs) ∨ (∃vs a es'. es = map Val vs @ Throw a # es')"

lemma [simp]: "final(Val v)"
(*<*)by(simp add:final_def)(*>*)

lemma [simp]: "final(throw e) = (∃a. e = addr a)"
(*<*)by(simp add:final_def)(*>*)

lemma finalE: "⟦ final e;  ⋀v. e = Val v ⟹ R;  ⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
(*<*)by(auto simp:final_def)(*>*)

lemma [iff]: "finals []"
(*<*)by(simp add:finals_def)(*>*)

lemma [iff]: "finals (Val v # es) = finals es"
(*<*)
proof(rule iffI)
  assume "finals (Val v # es)"
  moreover {
    fix vs a es'
    assume "∀vs a es'. es ≠ map Val vs @ Throw a # es'"
      and "Val v # es = map Val vs @ Throw a # es'"
    then have "∃vs. es = map Val vs" by(case_tac vs; simp)
  }
  ultimately show "finals es" by(clarsimp simp add: finals_def)
next
  assume "finals es"
  moreover {
    fix vs a es'
    assume "es = map Val vs @ Throw a # es'"
    then have "∃vs' a' es''. Val v # map Val vs @ Throw a # es' = map Val vs' @ Throw a' # es''"
      by(rule_tac x = "v#vs" in exI) simp
  }
  ultimately show "finals (Val v # es)" by(clarsimp simp add: finals_def)
qed
(*>*)

lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
(*<*)by(induct_tac vs, auto)(*>*)

lemma [iff]: "finals (map Val vs)"
(*<*)using finals_app_map[of vs "[]"]by(simp)(*>*)

lemma [iff]: "finals (throw e # es) = (∃a. e = addr a)"
(*<*)
proof(rule iffI)
  assume "finals (throw e # es)"
  moreover {
    fix vs a es'
    assume "throw e # es = map Val vs @ Throw a # es'"
    then have "∃a. e = addr a" by(case_tac vs; simp)
  }
  ultimately show "∃a. e = addr a" by(clarsimp simp add: finals_def)
next
  assume "∃a. e = addr a"
  moreover {
    fix vs a es'
    assume "e = addr a"
    then have "∃vs aa es'. Throw a # es = map Val vs @ Throw aa # es'"
      by(rule_tac x = "[]" in exI) simp
  }
  ultimately show "finals (throw e # es)" by(clarsimp simp add: finals_def)
qed
(*>*)

lemma not_finals_ConsI: "¬ final e ⟹ ¬ finals(e#es)"
(*<*)
proof -
  assume "¬ final e"
  moreover {
    fix vs a es'
    assume "∀v. e ≠ Val v" and "∀a. e ≠ Throw a"
    then have "e # es ≠ map Val vs @ Throw a # es'" by(case_tac vs; simp)
  }
  ultimately show ?thesis by(clarsimp simp add:finals_def final_def)
qed
(*>*)


lemma eval_final: "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ final e'"
 and evals_final: "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es'"
(*<*)by(induct rule:eval_evals.inducts, simp_all)(*>*)


lemma eval_lcl_incr: "P ⊢ ⟨e,(h0,l0)⟩ ⇒ ⟨e',(h1,l1)⟩ ⟹ dom l0 ⊆ dom l1"
 and evals_lcl_incr: "P ⊢ ⟨es,(h0,l0)⟩ [⇒] ⟨es',(h1,l1)⟩ ⟹ dom l0 ⊆ dom l1"
(*<*)
proof (induct rule: eval_evals_inducts)
  case BinOp show ?case by(rule subset_trans)(rule BinOp.hyps)+
next
  case Call thus ?case
    by(simp del: fun_upd_apply) 
next
  case Seq show ?case by(rule subset_trans)(rule Seq.hyps)+
next
  case CondT show ?case by(rule subset_trans)(rule CondT.hyps)+
next
  case CondF show ?case by(rule subset_trans)(rule CondF.hyps)+
next
  case WhileT thus ?case by(blast)
next
  case TryCatch thus ?case by(clarsimp simp:dom_def split:if_split_asm) blast
next
  case Cons show ?case by(rule subset_trans)(rule Cons.hyps)+
next
  case Block thus ?case by(auto simp del:fun_upd_apply)
qed auto
(*>*)

text‹Only used later, in the small to big translation, but is already a
good sanity check:›

lemma eval_finalId:  "final e ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e,s⟩"
(*<*)by (erule finalE) (iprover intro: eval_evals.intros)+(*>*)


lemma eval_finalsId:
assumes finals: "finals es" shows "P ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩"
(*<*)
  using finals
proof (induct es type: list)
  case Nil show ?case by (rule eval_evals.intros)
next
  case (Cons e es)
  have hyp: "finals es ⟹ P ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩"
   and finals: "finals (e # es)" by fact+
  show "P ⊢ ⟨e # es,s⟩ [⇒] ⟨e # es,s⟩"
  proof cases
    assume "final e"
    thus ?thesis
    proof (cases rule: finalE)
      fix v assume e: "e = Val v"
      have "P ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩" by (simp add: eval_finalId)
      moreover from finals e have "P ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩" by(fast intro:hyp)
      ultimately have "P ⊢ ⟨Val v#es,s⟩ [⇒] ⟨Val v#es,s⟩"
        by (rule eval_evals.intros)
      with e show ?thesis by simp
    next
      fix a assume e: "e = Throw a"
      have "P ⊢ ⟨Throw a,s⟩ ⇒ ⟨Throw a,s⟩" by (simp add: eval_finalId)
      hence "P ⊢ ⟨Throw a#es,s⟩ [⇒] ⟨Throw a#es,s⟩" by (rule eval_evals.intros)
      with e show ?thesis by simp
    qed
  next
    assume "¬ final e"
    with not_finals_ConsI finals have False by blast
    thus ?thesis ..
  qed
qed
(*>*)


theorem eval_hext: "P ⊢ ⟨e,(h,l)⟩ ⇒ ⟨e',(h',l')⟩ ⟹ h ⊴ h'"
and evals_hext:  "P ⊢ ⟨es,(h,l)⟩ [⇒] ⟨es',(h',l')⟩ ⟹ h ⊴ h'"
(*<*)
proof (induct rule: eval_evals_inducts)
  case New thus ?case
    by(fastforce intro!: hext_new intro:LeastI simp:new_Addr_def
                split:if_split_asm simp del:fun_upd_apply)
next
  case BinOp thus ?case by (fast elim!:hext_trans)
next
  case BinOpThrow2 thus ?case by(fast elim!: hext_trans)
next
  case FAss thus ?case
    by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
            elim!: hext_trans)
next
  case FAssNull thus ?case by (fast elim!:hext_trans)
next
  case FAssThrow2 thus ?case by (fast elim!:hext_trans)
next
  case CallParamsThrow thus ?case by(fast elim!: hext_trans)
next
  case CallNull thus ?case by(fast elim!: hext_trans)
next
  case Call thus ?case by(fast elim!: hext_trans)
next
  case Seq thus ?case by(fast elim!: hext_trans)
next
  case CondT thus ?case by(fast elim!: hext_trans)
next
  case CondF thus ?case by(fast elim!: hext_trans)
next
  case WhileT thus ?case by(fast elim!: hext_trans)
next
  case WhileBodyThrow thus ?case by (fast elim!: hext_trans)
next
  case TryCatch thus ?case  by(fast elim!: hext_trans)
next
  case Cons thus ?case by (fast intro: hext_trans)
qed auto
(*>*)


end