Theory BigStep

(*  Title:      Jinja/J/BigStep.thy
    ID:         $Id: BigStep.thy,v 1.8 2007-07-19 21:23:11 makarius Exp $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Big Step Semantics} *}

theory BigStep imports Expr State begin

inductive
  eval :: "J_prog => expr => state => expr => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and evals :: "J_prog => expr list => state => expr list => state => bool"
           ("_ \<turnstile> ((1⟨_,/_⟩) [=>]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: J_prog
where

  New:
  "[| new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(C,init_fields FDTs)) |]
  ==> P \<turnstile> ⟨new C,(h,l)⟩ => ⟨addr a,(h',l)⟩"

| NewFail:
  "new_Addr h = None ==>
  P \<turnstile> ⟨new C, (h,l)⟩ => ⟨THROW OutOfMemory,(h,l)⟩"

| Cast:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨addr a,(h,l)⟩; h a = Some(D,fs); P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨Cast C e,s0⟩ => ⟨addr a,(h,l)⟩"

| CastNull:
  "P \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile> ⟨Cast C e,s0⟩ => ⟨null,s1⟩"

| CastFail:
  "[| P \<turnstile> ⟨e,s0⟩=> ⟨addr a,(h,l)⟩; h a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨Cast C e,s0⟩ => ⟨THROW ClassCast,(h,l)⟩"

| CastThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨Cast C e,s0⟩ => ⟨throw e',s1⟩"

| Val:
  "P \<turnstile> ⟨Val v,s⟩ => ⟨Val v,s⟩"

| BinOp:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Val v1,s1⟩; P \<turnstile> ⟨e2,s1⟩ => ⟨Val v2,s2⟩; binop(bop,v1,v2) = Some v |]
  ==> P \<turnstile> ⟨e1 «bop» e2,s0⟩=>⟨Val v,s2⟩"

| BinOpThrow1:
  "P \<turnstile> ⟨e1,s0⟩ => ⟨throw e,s1⟩ ==>
  P \<turnstile> ⟨e1 «bop» e2, s0⟩ => ⟨throw e,s1⟩"

| BinOpThrow2:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Val v1,s1⟩; P \<turnstile> ⟨e2,s1⟩ => ⟨throw e,s2⟩ |]
  ==> P \<turnstile> ⟨e1 «bop» e2,s0⟩ => ⟨throw e,s2⟩"

| Var:
  "l V = Some v ==>
  P \<turnstile> ⟨Var V,(h,l)⟩ => ⟨Val v,(h,l)⟩"

| LAss:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨Val v,(h,l)⟩; l' = l(V\<mapsto>v) |]
  ==> P \<turnstile> ⟨V:=e,s0⟩ => ⟨unit,(h,l')⟩"

| LAssThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨V:=e,s0⟩ => ⟨throw e',s1⟩"

| FAcc:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨addr a,(h,l)⟩; h a = Some(C,fs); fs(F,D) = Some v |]
  ==> P \<turnstile> ⟨e•F{D},s0⟩ => ⟨Val v,(h,l)⟩"

| FAccNull:
  "P \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile> ⟨e•F{D},s0⟩ => ⟨THROW NullPointer,s1⟩"

| FAccThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨e•F{D},s0⟩ => ⟨throw e',s1⟩"

| FAss:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨addr a,s1⟩; P \<turnstile> ⟨e2,s1⟩ => ⟨Val v,(h2,l2)⟩;
     h2 a = Some(C,fs); fs' = fs((F,D)\<mapsto>v); h2' = h2(a\<mapsto>(C,fs')) |]
  ==> P \<turnstile> ⟨e1•F{D}:=e2,s0⟩ => ⟨unit,(h2',l2)⟩"

| FAssNull:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨null,s1⟩;  P \<turnstile> ⟨e2,s1⟩ => ⟨Val v,s2⟩ |] ==>
  P \<turnstile> ⟨e1•F{D}:=e2,s0⟩ => ⟨THROW NullPointer,s2⟩"

| FAssThrow1:
  "P \<turnstile> ⟨e1,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨e1•F{D}:=e2,s0⟩ => ⟨throw e',s1⟩"

| FAssThrow2:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Val v,s1⟩; P \<turnstile> ⟨e2,s1⟩ => ⟨throw e',s2⟩ |]
  ==> P \<turnstile> ⟨e1•F{D}:=e2,s0⟩ => ⟨throw e',s2⟩"

| CallObjThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨e•M(ps),s0⟩ => ⟨throw e',s1⟩"

| CallParamsThrow:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨Val v,s1⟩; P \<turnstile> ⟨es,s1⟩ [=>] ⟨map Val vs @ throw ex # es',s2⟩ |]
   ==> P \<turnstile> ⟨e•M(es),s0⟩ => ⟨throw ex,s2⟩"

| CallNull:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩;  P \<turnstile> ⟨ps,s1⟩ [=>] ⟨map Val vs,s2⟩ |]
  ==> P \<turnstile> ⟨e•M(ps),s0⟩ => ⟨THROW NullPointer,s2⟩"

| Call:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨addr a,s1⟩;  P \<turnstile> ⟨ps,s1⟩ [=>] ⟨map Val vs,(h2,l2)⟩;
     h2 a = Some(C,fs);  P \<turnstile> C sees M:Ts->T = (pns,body) in D;
     length vs = length pns;  l2' = [this\<mapsto>Addr a, pns[\<mapsto>]vs];
     P \<turnstile> ⟨body,(h2,l2')⟩ => ⟨e',(h3,l3)⟩ |]
  ==> P \<turnstile> ⟨e•M(ps),s0⟩ => ⟨e',(h3,l2)⟩"

| Block:
  "P \<turnstile> ⟨e0,(h0,l0(V:=None))⟩ => ⟨e1,(h1,l1)⟩ ==>
  P \<turnstile> ⟨{V:T; e0},(h0,l0)⟩ => ⟨e1,(h1,l1(V:=l0 V))⟩"

| Seq:
  "[| P \<turnstile> ⟨e0,s0⟩ => ⟨Val v,s1⟩; P \<turnstile> ⟨e1,s1⟩ => ⟨e2,s2⟩ |]
  ==> P \<turnstile> ⟨e0;;e1,s0⟩ => ⟨e2,s2⟩"

| SeqThrow:
  "P \<turnstile> ⟨e0,s0⟩ => ⟨throw e,s1⟩ ==>
  P \<turnstile> ⟨e0;;e1,s0⟩=>⟨throw e,s1⟩"

| CondT:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨true,s1⟩; P \<turnstile> ⟨e1,s1⟩ => ⟨e',s2⟩ |]
  ==> P \<turnstile> ⟨if (e) e1 else e2,s0⟩ => ⟨e',s2⟩"

| CondF:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨false,s1⟩; P \<turnstile> ⟨e2,s1⟩ => ⟨e',s2⟩ |]
  ==> P \<turnstile> ⟨if (e) e1 else e2,s0⟩ => ⟨e',s2⟩"

| CondThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨if (e) e1 else e2, s0⟩ => ⟨throw e',s1⟩"

| WhileF:
  "P \<turnstile> ⟨e,s0⟩ => ⟨false,s1⟩ ==>
  P \<turnstile> ⟨while (e) c,s0⟩ => ⟨unit,s1⟩"

| WhileT:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨true,s1⟩; P \<turnstile> ⟨c,s1⟩ => ⟨Val v1,s2⟩; P \<turnstile> ⟨while (e) c,s2⟩ => ⟨e3,s3⟩ |]
  ==> P \<turnstile> ⟨while (e) c,s0⟩ => ⟨e3,s3⟩"

| WhileCondThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨ throw e',s1⟩ ==>
  P \<turnstile> ⟨while (e) c,s0⟩ => ⟨throw e',s1⟩"

| WhileBodyThrow:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨true,s1⟩; P \<turnstile> ⟨c,s1⟩ => ⟨throw e',s2⟩|]
  ==> P \<turnstile> ⟨while (e) c,s0⟩ => ⟨throw e',s2⟩"

| Throw:
  "P \<turnstile> ⟨e,s0⟩ => ⟨addr a,s1⟩ ==>
  P \<turnstile> ⟨throw e,s0⟩ => ⟨Throw a,s1⟩"

| ThrowNull:
  "P \<turnstile> ⟨e,s0⟩ => ⟨null,s1⟩ ==>
  P \<turnstile> ⟨throw e,s0⟩ => ⟨THROW NullPointer,s1⟩"

| ThrowThrow:
  "P \<turnstile> ⟨e,s0⟩ => ⟨throw e',s1⟩ ==>
  P \<turnstile> ⟨throw e,s0⟩ => ⟨throw e',s1⟩"

| Try:
  "P \<turnstile> ⟨e1,s0⟩ => ⟨Val v1,s1⟩ ==>
  P \<turnstile> ⟨try e1 catch(C V) e2,s0⟩ => ⟨Val v1,s1⟩"

| TryCatch:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Throw a,(h1,l1)⟩;  h1 a = Some(D,fs);  P \<turnstile> D \<preceq>* C;
     P \<turnstile> ⟨e2,(h1,l1(V\<mapsto>Addr a))⟩ => ⟨e2',(h2,l2)⟩ |]
  ==> P \<turnstile> ⟨try e1 catch(C V) e2,s0⟩ => ⟨e2',(h2,l2(V:=l1 V))⟩"

| TryThrow:
  "[| P \<turnstile> ⟨e1,s0⟩ => ⟨Throw a,(h1,l1)⟩;  h1 a = Some(D,fs);  ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨try e1 catch(C V) e2,s0⟩ => ⟨Throw a,(h1,l1)⟩"

| Nil:
  "P \<turnstile> ⟨[],s⟩ [=>] ⟨[],s⟩"

| Cons:
  "[| P \<turnstile> ⟨e,s0⟩ => ⟨Val v,s1⟩; P \<turnstile> ⟨es,s1⟩ [=>] ⟨es',s2⟩ |]
  ==> P \<turnstile> ⟨e#es,s0⟩ [=>] ⟨Val v # es',s2⟩"

| ConsThrow:
  "P \<turnstile> ⟨e, s0⟩ => ⟨throw e', s1⟩ ==>
  P \<turnstile> ⟨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 \<turnstile> ⟨Cast C e,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨Val v,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨e1 «bop» e2,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨V:=e,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨e•F{D},s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨e1•F{D}:=e2,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨e•M{D}(es),s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨{V:T;e1},s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨e1;;e2,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨if (e) e1 else e2,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨while (b) c,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨throw e,s⟩ => ⟨e',s'⟩"
 "P \<turnstile> ⟨try e1 catch(C V) e2,s⟩ => ⟨e',s'⟩"
 
inductive_cases evals_cases [cases set]:
 "P \<turnstile> ⟨[],s⟩ [=>] ⟨e',s'⟩"
 "P \<turnstile> ⟨e#es,s⟩ [=>] ⟨e',s'⟩"
(*>*) 


subsection"Final expressions"

constdefs
  final :: "'a exp => bool"
  "final e  ≡  (∃v. e = Val v) ∨ (∃a. e = Throw a)"
  finals:: "'a exp list => bool"
  "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"
(*<*)
apply(clarsimp simp add: finals_def)
apply(rule iffI)
 apply(erule disjE)
  apply simp
 apply(rule disjI2)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply(erule disjE)
 apply clarsimp
apply(rule disjI2)
apply clarsimp
apply(rule_tac x = "v#vs" in exI)
apply simp
done
(*>*)

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)"
(*<*)
apply(simp add:finals_def)
apply(rule iffI)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply clarsimp
apply(rule_tac x = "[]" in exI)
apply simp
done
(*>*)

lemma not_finals_ConsI: "¬ final e ==> ¬ finals(e#es)"
 (*<*)
apply(clarsimp simp add:finals_def final_def)
apply(case_tac vs)
apply auto
done
(*>*)


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


lemma eval_lcl_incr: "P \<turnstile> ⟨e,(h0,l0)⟩ => ⟨e',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
 and evals_lcl_incr: "P \<turnstile> ⟨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:split_if_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 \<turnstile> ⟨e,s⟩ => ⟨e,s⟩"
(*<*)by (erule finalE) (iprover intro: eval_evals.intros)+(*>*)


lemma eval_finalsId:
assumes finals: "finals es" shows "P \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩"
   and finals: "finals (e # es)" by fact+
  show "P \<turnstile> ⟨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 \<turnstile> ⟨Val v,s⟩ => ⟨Val v,s⟩" by (simp add: eval_finalId)
      moreover from finals e have "P \<turnstile> ⟨es,s⟩ [=>] ⟨es,s⟩" by(fast intro:hyp)
      ultimately have "P \<turnstile> ⟨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 \<turnstile> ⟨Throw a,s⟩ => ⟨Throw a,s⟩" by (simp add: eval_finalId)
      hence "P \<turnstile> ⟨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 \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> h \<unlhd> h'"
and evals_hext:  "P \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ ==> h \<unlhd> h'"
(*<*)
proof (induct rule: eval_evals_inducts)
  case New thus ?case
    by(fastsimp intro!: hext_new intro:someI simp:new_Addr_def
                split:split_if_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