(*  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,s₀⟩ → ⟨addr a,(h,l)⟩; h a = Some(D,fs); P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨Cast C e,s₀⟩ → ⟨addr a,(h,l)⟩"

| CastNull:
  "P ⊨ ⟨e,s₀⟩ → ⟨null,s₁⟩ ==>
  P ⊨ ⟨Cast C e,s₀⟩ → ⟨null,s₁⟩"

| CastFail:
  "[ P ⊨ ⟨e,s₀⟩→ ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨Cast C e,s₀⟩ → ⟨THROW ClassCast,(h,l)⟩"

| CastThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨Cast C e,s₀⟩ → ⟨throw e',s₁⟩"

| Val:
  "P ⊨ ⟨Val v,s⟩ → ⟨Val v,s⟩"

| BinOp:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨Val v₁,s₁⟩; P ⊨ ⟨e₂,s₁⟩ → ⟨Val v₂,s₂⟩; binop(bop,v₁,v₂) = Some v ]
  ==> P ⊨ ⟨e₁ «bop¬ e₂,s₀⟩→⟨Val v,s₂⟩"

| BinOpThrow1:
  "P ⊨ ⟨e₁,s₀⟩ → ⟨throw e,s₁⟩ ==>
  P ⊨ ⟨e₁ «bop¬ e₂, s₀⟩ → ⟨throw e,s₁⟩"

| BinOpThrow2:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨Val v₁,s₁⟩; P ⊨ ⟨e₂,s₁⟩ → ⟨throw e,s₂⟩ ]
  ==> P ⊨ ⟨e₁ «bop¬ e₂,s₀⟩ → ⟨throw e,s₂⟩"

| Var:
  "l V = Some v ==>
  P ⊨ ⟨Var V,(h,l)⟩ → ⟨Val v,(h,l)⟩"

| LAss:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨Val v,(h,l)⟩; l' = l(V↦v) ]
  ==> P ⊨ ⟨V:=e,s₀⟩ → ⟨unit,(h,l')⟩"

| LAssThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨V:=e,s₀⟩ → ⟨throw e',s₁⟩"

| FAcc:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨addr a,(h,l)⟩; h a = Some(C,fs); fs(F,D) = Some v ]
  ==> P ⊨ ⟨e∙F{D},s₀⟩ → ⟨Val v,(h,l)⟩"

| FAccNull:
  "P ⊨ ⟨e,s₀⟩ → ⟨null,s₁⟩ ==>
  P ⊨ ⟨e∙F{D},s₀⟩ → ⟨THROW NullPointer,s₁⟩"

| FAccThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨e∙F{D},s₀⟩ → ⟨throw e',s₁⟩"

| FAss:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨addr a,s₁⟩; P ⊨ ⟨e₂,s₁⟩ → ⟨Val v,(h₂,l₂)⟩;
     h₂ a = Some(C,fs); fs' = fs((F,D)↦v); h₂' = h₂(a↦(C,fs')) ]
  ==> P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ → ⟨unit,(h₂',l₂)⟩"

| FAssNull:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨null,s₁⟩; P ⊨ ⟨e₂,s₁⟩ → ⟨Val v,s₂⟩ ] ==>
  P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ → ⟨THROW NullPointer,s₂⟩"

| FAssThrow1:
  "P ⊨ ⟨e₁,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ → ⟨throw e',s₁⟩"

| FAssThrow2:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨Val v,s₁⟩; P ⊨ ⟨e₂,s₁⟩ → ⟨throw e',s₂⟩ ]
  ==> P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ → ⟨throw e',s₂⟩"

| CallObjThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨e∙M(ps),s₀⟩ → ⟨throw e',s₁⟩"

| CallParamsThrow:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨Val v,s₁⟩; P ⊨ ⟨es,s₁⟩ [→] ⟨map Val vs @ throw ex # es',s₂⟩ ]
   ==> P ⊨ ⟨e∙M(es),s₀⟩ → ⟨throw ex,s₂⟩"

| CallNull:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨null,s₁⟩; P ⊨ ⟨ps,s₁⟩ [→] ⟨map Val vs,s₂⟩ ]
  ==> P ⊨ ⟨e∙M(ps),s₀⟩ → ⟨THROW NullPointer,s₂⟩"

| Call:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨addr a,s₁⟩; P ⊨ ⟨ps,s₁⟩ [→] ⟨map Val vs,(h₂,l₂)⟩;
     h₂ a = Some(C,fs); P ⊨ C sees M:Ts→T = (pns,body) in D;
     length vs = length pns; l₂' = [this↦Addr a, pns[↦]vs];
     P ⊨ ⟨body,(h₂,l₂')⟩ → ⟨e',(h₃,l₃)⟩ ]
  ==> P ⊨ ⟨e∙M(ps),s₀⟩ → ⟨e',(h₃,l₂)⟩"

| Block:
  "P ⊨ ⟨e₀,(h₀,l₀(V:=None))⟩ → ⟨e₁,(h₁,l₁)⟩ ==>
  P ⊨ ⟨{V:T; e₀},(h₀,l₀)⟩ → ⟨e₁,(h₁,l₁(V:=l₀ V))⟩"

| Seq:
  "[ P ⊨ ⟨e₀,s₀⟩ → ⟨Val v,s₁⟩; P ⊨ ⟨e₁,s₁⟩ → ⟨e₂,s₂⟩ ]
  ==> P ⊨ ⟨e₀;;e₁,s₀⟩ → ⟨e₂,s₂⟩"

| SeqThrow:
  "P ⊨ ⟨e₀,s₀⟩ → ⟨throw e,s₁⟩ ==>
  P ⊨ ⟨e₀;;e₁,s₀⟩→⟨throw e,s₁⟩"

| CondT:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨true,s₁⟩; P ⊨ ⟨e₁,s₁⟩ → ⟨e',s₂⟩ ]
  ==> P ⊨ ⟨if (e) e₁ else e₂,s₀⟩ → ⟨e',s₂⟩"

| CondF:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨false,s₁⟩; P ⊨ ⟨e₂,s₁⟩ → ⟨e',s₂⟩ ]
  ==> P ⊨ ⟨if (e) e₁ else e₂,s₀⟩ → ⟨e',s₂⟩"

| CondThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨if (e) e₁ else e₂, s₀⟩ → ⟨throw e',s₁⟩"

| WhileF:
  "P ⊨ ⟨e,s₀⟩ → ⟨false,s₁⟩ ==>
  P ⊨ ⟨while (e) c,s₀⟩ → ⟨unit,s₁⟩"

| WhileT:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨true,s₁⟩; P ⊨ ⟨c,s₁⟩ → ⟨Val v₁,s₂⟩; P ⊨ ⟨while (e) c,s₂⟩ → ⟨e₃,s₃⟩ ]
  ==> P ⊨ ⟨while (e) c,s₀⟩ → ⟨e₃,s₃⟩"

| WhileCondThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨ throw e',s₁⟩ ==>
  P ⊨ ⟨while (e) c,s₀⟩ → ⟨throw e',s₁⟩"

| WhileBodyThrow:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨true,s₁⟩; P ⊨ ⟨c,s₁⟩ → ⟨throw e',s₂⟩]
  ==> P ⊨ ⟨while (e) c,s₀⟩ → ⟨throw e',s₂⟩"

| Throw:
  "P ⊨ ⟨e,s₀⟩ → ⟨addr a,s₁⟩ ==>
  P ⊨ ⟨throw e,s₀⟩ → ⟨Throw a,s₁⟩"

| ThrowNull:
  "P ⊨ ⟨e,s₀⟩ → ⟨null,s₁⟩ ==>
  P ⊨ ⟨throw e,s₀⟩ → ⟨THROW NullPointer,s₁⟩"

| ThrowThrow:
  "P ⊨ ⟨e,s₀⟩ → ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨throw e,s₀⟩ → ⟨throw e',s₁⟩"

| Try:
  "P ⊨ ⟨e₁,s₀⟩ → ⟨Val v₁,s₁⟩ ==>
  P ⊨ ⟨try e₁ catch(C V) e₂,s₀⟩ → ⟨Val v₁,s₁⟩"

| TryCatch:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨Throw a,(h₁,l₁)⟩; h₁ a = Some(D,fs); P ⊨ D ⪯^* C;
     P ⊨ ⟨e₂,(h₁,l₁(V↦Addr a))⟩ → ⟨e₂',(h₂,l₂)⟩ ]
  ==> P ⊨ ⟨try e₁ catch(C V) e₂,s₀⟩ → ⟨e₂',(h₂,l₂(V:=l₁ V))⟩"

| TryThrow:
  "[ P ⊨ ⟨e₁,s₀⟩ → ⟨Throw a,(h₁,l₁)⟩; h₁ a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨try e₁ catch(C V) e₂,s₀⟩ → ⟨Throw a,(h₁,l₁)⟩"

| Nil:
  "P ⊨ ⟨[],s⟩ [→] ⟨[],s⟩"

| Cons:
  "[ P ⊨ ⟨e,s₀⟩ → ⟨Val v,s₁⟩; P ⊨ ⟨es,s₁⟩ [→] ⟨es',s₂⟩ ]
  ==> P ⊨ ⟨e#es,s₀⟩ [→] ⟨Val v # es',s₂⟩"

| ConsThrow:
  "P ⊨ ⟨e, s₀⟩ → ⟨throw e', s₁⟩ ==>
  P ⊨ ⟨e#es, s₀⟩ [→] ⟨throw e' # es, s₁⟩"

(*<*)
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 ⊨ ⟨e₁ «bop¬ e₂,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨V:=e,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨e∙F{D},s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨e₁∙F{D}:=e₂,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨e∙M{D}(es),s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨{V:T;e₁},s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨e₁;;e₂,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨if (e) e₁ else e₂,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨while (b) c,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨throw e,s⟩ → ⟨e',s'⟩"
 "P ⊨ ⟨try e₁ catch(C V) e₂,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,(h₀,l₀)⟩ → ⟨e',(h₁,l₁)⟩ ==> dom l₀ ⊆ dom l₁"
 and evals_lcl_incr: "P ⊨ ⟨es,(h₀,l₀)⟩ [→] ⟨es',(h₁,l₁)⟩ ==> dom l₀ ⊆ dom l₁"
(*<*)
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
  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