# Theory BigStep

(*  Title:      Jinja/J/BigStep.thy

Author:     Tobias Nipkow
*)

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 ::
("_  ((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))

| NewFail:
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,s0Val 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(Vv)
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  eF{D},s0  Val v,(h,l)"

| FAccNull:
"P  e,s0  null,s1
P  eF{D},s0  THROW NullPointer,s1"

| FAccThrow:
"P  e,s0  throw e',s1
P  eF{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  e1F{D}:=e2,s0  unit,(h2',l2)"

| FAssNull:
" P  e1,s0  null,s1;  P  e2,s1  Val v,s2
P  e1F{D}:=e2,s0  THROW NullPointer,s2"

| FAssThrow1:
"P  e1,s0  throw e',s1
P  e1F{D}:=e2,s0  throw e',s1"

| FAssThrow2:
" P  e1,s0  Val v,s1; P  e2,s1  throw e',s2
P  e1F{D}:=e2,s0  throw e',s2"

| CallObjThrow:
"P  e,s0  throw e',s1
P  eM(ps),s0  throw e',s1"

| CallParamsThrow:
" P  e,s0  Val v,s1; P  es,s1 [⇒] map Val vs @ throw ex # es',s2
P  eM(es),s0  throw ex,s2"

| CallNull:
" P  e,s0  null,s1;  P  ps,s1 [⇒] map Val vs,s2
P  eM(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:TsT = (pns,body) in D;
length vs = length pns;  l2' = [thisAddr a, pns[↦]vs];
P  body,(h2,l2')  e',(h3,l3)
P  eM(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,s0throw 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  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  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  eF{D},s  e',s'"
"P  e1F{D}:=e2,s  e',s'"
"P  eM{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)"

lemma [simp]: "final(throw e) = (a. e = addr a)"

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

lemma [iff]: "finals []"

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)
}
next
assume "a. e = addr a"
moreover {
fix vs a es'
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
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