Theory Expr

(*  Title:      JinjaDCI/J/Expr.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/Expr.thy by Tobias Nipkow
*)

section ‹ Expressions ›

theory Expr
imports "../Common/Exceptions"
begin

datatype bop = Eq | Add     ― ‹names of binary operations›

datatype 'a exp
  = new cname      ― ‹class instance creation›
  | Cast cname "('a exp)"      ― ‹type cast›
  | Val val      ― ‹value›
  | BinOp "('a exp)" bop "('a exp)"     ("_ «_» _" [80,0,81] 80)      ― ‹binary operation›
  | Var 'a                                               ― ‹local variable (incl. parameter)›
  | LAss 'a "('a exp)"     ("_:=_" [90,90]90)                    ― ‹local assignment›
  | FAcc "('a exp)" vname cname     ("_∙_{_}" [10,90,99]90)      ― ‹field access›
  | SFAcc cname vname cname     ("_∙s_{_}" [10,90,99]90)      ― ‹static field access›
  | FAss "('a exp)" vname cname "('a exp)"     ("_∙_{_} := _" [10,90,99,90]90)      ― ‹field assignment›
  | SFAss cname vname cname "('a exp)"     ("_∙s_{_} := _" [10,90,99,90]90)      ― ‹static field assignment›
  | Call "('a exp)" mname "('a exp list)"     ("_∙_'(_')" [90,99,0] 90)            ― ‹method call›
  | SCall cname mname "('a exp list)"     ("_∙s_'(_')" [90,99,0] 90)            ― ‹static method call›
  | Block 'a ty "('a exp)"     ("'{_:_; _}")
  | Seq "('a exp)" "('a exp)"     ("_;;/ _"             [61,60]60)
  | Cond "('a exp)" "('a exp)" "('a exp)"     ("if '(_') _/ else _" [80,79,79]70)
  | While "('a exp)" "('a exp)"     ("while '(_') _"     [80,79]70)
  | throw "('a exp)"
  | TryCatch "('a exp)" cname 'a "('a exp)"     ("try _/ catch'(_ _') _"  [0,99,80,79] 70)
  | INIT cname "cname list" bool "('a exp)" ("INIT _ '(_,_') ← _" [60,60,60,60] 60) ― ‹internal initialization command: class, list of superclasses to initialize, preparation flag; command on hold›
  | RI cname "('a exp)" "cname list" "('a exp)" ("RI '(_,_') ; _ ← _" [60,60,60,60] 60) ― ‹running of the initialization procedure for class with expression, classes still to initialize command on hold›

type_synonym
  expr = "vname exp"            ― ‹Jinja expression›
type_synonym
  J_mb = "vname list × expr"    ― ‹Jinja method body: parameter names and expression›
type_synonym
  J_prog = "J_mb prog"          ― ‹Jinja program›

type_synonym
  init_stack = "expr list × bool"  ― ‹Stack of expressions waiting on initialization in small step; indicator boolean True if current expression has been init checked›

text‹The semantics of binary operators: ›

fun binop :: "bop × val × val ⇒ val option" where
  "binop(Eq,v1,v2) = Some(Bool (v1 = v2))"
| "binop(Add,Intg i1,Intg i2) = Some(Intg(i1+i2))"
| "binop(bop,v1,v2) = None"

lemma [simp]:
  "(binop(Add,v1,v2) = Some v) = (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ v = Intg(i1+i2))"
(*<*)by(cases v1; cases v2) auto(*>*)


lemma map_Val_throw_eq:
 "map Val vs @ throw ex # es = map Val vs' @ throw ex' # es' ⟹ ex = ex'"
(*<*)by(induct vs arbitrary: vs'; case_tac vs') auto(*>*)

lemma map_Val_nthrow_neq:
 "map Val vs = map Val vs' @ throw ex' # es' ⟹ False"
(*<*)by(induct vs arbitrary: vs'; case_tac vs') auto(*>*)

lemma map_Val_eq:
 "map Val vs = map Val vs' ⟹ vs = vs'"
(*<*)by(induct vs arbitrary: vs'; case_tac vs') auto(*>*)


lemma init_rhs_neq [simp]: "e ≠ INIT C (Cs,b) ← e"
proof -
  have "size e ≠ size (INIT C (Cs,b) ← e)" by auto
  then show ?thesis by fastforce
qed

lemma init_rhs_neq' [simp]: "INIT C (Cs,b) ← e ≠ e"
proof -
  have "size e ≠ size (INIT C (Cs,b) ← e)" by auto
  then show ?thesis by fastforce
qed

lemma ri_rhs_neq [simp]: "e ≠ RI(C,e');Cs ← e"
proof -
  have "size e ≠ size (RI(C,e');Cs ← e)" by auto
  then show ?thesis by fastforce
qed

lemma ri_rhs_neq' [simp]: "RI(C,e');Cs ← e ≠ e"
proof -
  have "size e ≠ size (RI(C,e');Cs ← e)" by auto
  then show ?thesis by fastforce
qed

subsection "Syntactic sugar"

abbreviation (input)
  InitBlock:: "'a ⇒ ty ⇒ 'a exp ⇒ 'a exp ⇒ 'a exp"   ("(1'{_:_ := _;/ _})") where
  "InitBlock V T e1 e2 == {V:T; V := e1;; e2}"

abbreviation unit where "unit == Val Unit"
abbreviation null where "null == Val Null"
abbreviation "addr a == Val(Addr a)"
abbreviation "true == Val(Bool True)"
abbreviation "false == Val(Bool False)"

abbreviation
  Throw :: "addr ⇒ 'a exp" where
  "Throw a == throw(Val(Addr a))"

abbreviation
  THROW :: "cname ⇒ 'a exp" where
  "THROW xc == Throw(addr_of_sys_xcpt xc)"


subsection‹Free Variables›

primrec fv :: "expr ⇒ vname set" and fvs :: "expr list ⇒ vname set" where
  "fv(new C) = {}"
| "fv(Cast C e) = fv e"
| "fv(Val v) = {}"
| "fv(e1 «bop» e2) = fv e1 ∪ fv e2"
| "fv(Var V) = {V}"
| "fv(LAss V e) = {V} ∪ fv e"
| "fv(e∙F{D}) = fv e"
| "fv(C∙sF{D}) = {}"
| "fv(e1∙F{D}:=e2) = fv e1 ∪ fv e2"
| "fv(C∙sF{D}:=e2) = fv e2"
| "fv(e∙M(es)) = fv e ∪ fvs es"
| "fv(C∙sM(es)) = fvs es"
| "fv({V:T; e}) = fv e - {V}"
| "fv(e1;;e2) = fv e1 ∪ fv e2"
| "fv(if (b) e1 else e2) = fv b ∪ fv e1 ∪ fv e2"
| "fv(while (b) e) = fv b ∪ fv e"
| "fv(throw e) = fv e"
| "fv(try e1 catch(C V) e2) = fv e1 ∪ (fv e2 - {V})"
| "fv(INIT C (Cs,b) ← e) = fv e"
| "fv(RI (C,e);Cs ← e') = fv e ∪ fv e'"
| "fvs([]) = {}"
| "fvs(e#es) = fv e ∪ fvs es"

lemma [simp]: "fvs(es1 @ es2) = fvs es1 ∪ fvs es2"
(*<*)by (induct es1 type:list) auto(*>*)

lemma [simp]: "fvs(map Val vs) = {}"
(*<*)by (induct vs) auto(*>*)


subsection‹Accessing expression constructor arguments›

fun val_of :: "'a exp ⇒ val option" where
"val_of (Val v) = Some v" |
"val_of _ = None"

lemma val_of_spec: "val_of e = Some v ⟹ e = Val v"
proof(cases e) qed(auto)

fun lass_val_of :: "'a exp ⇒ ('a × val) option" where
"lass_val_of (V:=Val v) = Some (V, v)" |
"lass_val_of _ = None"

lemma lass_val_of_spec:
assumes "lass_val_of e = ⌊a⌋"
shows "e = (fst a:=Val (snd a))"
using assms proof(cases e)
  case (LAss V e') then show ?thesis using assms proof(cases e')qed(auto)
qed(auto)

fun map_vals_of :: "'a exp list ⇒ val list option" where
"map_vals_of (e#es) = (case val_of e of Some v ⇒ (case map_vals_of es of Some vs ⇒ Some (v#vs) 
                                                                        | _ ⇒ None)
                                      | _ ⇒ None)" |
"map_vals_of [] = Some []"

lemma map_vals_of_spec: "map_vals_of es = Some vs ⟹ es = map Val vs"
proof(induct es arbitrary: vs) qed(auto simp: val_of_spec)

lemma map_vals_of_Vals[simp]: "map_vals_of (map Val vs) = ⌊vs⌋" by(induct vs, auto)

lemma map_vals_of_throw[simp]:
 "map_vals_of (map Val vs @ throw e # es') = None"
 by(induct vs, auto)


fun bool_of :: "'a exp ⇒ bool option" where
"bool_of true = Some True" |
"bool_of false = Some False" |
"bool_of _ = None"

lemma bool_of_specT:
assumes "bool_of e = Some True" shows "e = true"
proof -
  have "bool_of e = Some True" by fact
  then show ?thesis
  proof(cases e)
    case (Val x3) with assms show ?thesis
    proof(cases x3)
      case (Bool x) with assms Val show ?thesis
      proof(cases x)qed(auto)
    qed(simp_all)
  qed(auto)
qed

lemma bool_of_specF:
assumes "bool_of e = Some False" shows "e = false"
proof -
  have "bool_of e = Some False" by fact
  then show ?thesis
  proof(cases e)
    case (Val x3) with assms show ?thesis
    proof(cases x3)
      case (Bool x) with assms Val show ?thesis
      proof(cases x)qed(auto)
    qed(simp_all)
  qed(auto)
qed


fun throw_of :: "'a exp ⇒ 'a exp option" where
"throw_of (throw e') = Some e'" |
"throw_of _ = None"

lemma throw_of_spec: "throw_of e = Some e' ⟹ e = throw e'"
proof(cases e) qed(auto)

fun init_exp_of :: "'a exp ⇒ 'a exp option" where
"init_exp_of (INIT C (Cs,b) ← e) = Some e" |
"init_exp_of (RI(C,e');Cs ← e) = Some e" |
"init_exp_of _ = None"

lemma init_exp_of_neq [simp]: "init_exp_of e = ⌊e'⌋ ⟹ e' ≠ e" by(cases e, auto)
lemma init_exp_of_neq'[simp]: "init_exp_of e = ⌊e'⌋ ⟹ e ≠ e'" by(cases e, auto)


subsection‹Class initialization›

text ‹ This section defines a few functions that return information
 about an expression's current initialization status. ›

 ― ‹ True if expression contains @{text INIT}, @{text RI}, or a call to a static method @{term clinit} ›
primrec sub_RI :: "'a exp ⇒ bool" and sub_RIs :: "'a exp list ⇒ bool" where
  "sub_RI(new C) = False"
| "sub_RI(Cast C e) = sub_RI e"
| "sub_RI(Val v) = False"
| "sub_RI(e1 «bop» e2) = (sub_RI e1 ∨ sub_RI e2)"
| "sub_RI(Var V) = False"
| "sub_RI(LAss V e) = sub_RI e"
| "sub_RI(e∙F{D}) = sub_RI e"
| "sub_RI(C∙sF{D}) = False"
| "sub_RI(e1∙F{D}:=e2) = (sub_RI e1 ∨ sub_RI e2)"
| "sub_RI(C∙sF{D}:=e2) = sub_RI e2"
| "sub_RI(e∙M(es)) = (sub_RI e ∨ sub_RIs es)"
| "sub_RI(C∙sM(es)) = (M = clinit ∨ sub_RIs es)"
| "sub_RI({V:T; e}) = sub_RI e"
| "sub_RI(e1;;e2) = (sub_RI e1 ∨ sub_RI e2)"
| "sub_RI(if (b) e1 else e2) = (sub_RI b ∨ sub_RI e1 ∨ sub_RI e2)"
| "sub_RI(while (b) e) = (sub_RI b ∨ sub_RI e)"
| "sub_RI(throw e) = sub_RI e"
| "sub_RI(try e1 catch(C V) e2) = (sub_RI e1 ∨ sub_RI e2)"
| "sub_RI(INIT C (Cs,b) ← e) = True"
| "sub_RI(RI (C,e);Cs ← e') = True"
| "sub_RIs([]) = False"
| "sub_RIs(e#es) = (sub_RI e ∨ sub_RIs es)"


lemmas sub_RI_sub_RIs_induct = sub_RI.induct sub_RIs.induct

lemma nsub_RIs_def[simp]:
 "¬sub_RIs es ⟹ ∀e ∈ set es. ¬sub_RI e"
 by(induct es, auto)

lemma sub_RI_base:
 "e = INIT C (Cs, b) ← e' ∨ e = RI(C,e0);Cs ← e' ⟹ sub_RI e"
 by(cases e, auto)

lemma nsub_RI_Vals[simp]: "¬sub_RIs (map Val vs)"
 by(induct vs, auto)

lemma lass_val_of_nsub_RI: "lass_val_of e = ⌊a⌋ ⟹ ¬sub_RI e"
 by(drule lass_val_of_spec, simp)


 ― ‹ is not currently initializing class @{text C'} (point past checking flag) ›
primrec not_init :: "cname ⇒ 'a exp ⇒ bool" and not_inits :: "cname ⇒ 'a exp list ⇒ bool" where
  "not_init C' (new C) = True"
| "not_init C' (Cast C e) = not_init C' e"
| "not_init C' (Val v) = True"
| "not_init C' (e1 «bop» e2) = (not_init C' e1 ∧ not_init C' e2)"
| "not_init C' (Var V) = True"
| "not_init C' (LAss V e) = not_init C' e"
| "not_init C' (e∙F{D}) = not_init C' e"
| "not_init C' (C∙sF{D}) = True"
| "not_init C' (e1∙F{D}:=e2) = (not_init C' e1 ∧ not_init C' e2)"
| "not_init C' (C∙sF{D}:=e2) = not_init C' e2"
| "not_init C' (e∙M(es)) = (not_init C' e ∧ not_inits C' es)"
| "not_init C' (C∙sM(es)) = not_inits C' es"
| "not_init C' ({V:T; e}) = not_init C' e"
| "not_init C' (e1;;e2) = (not_init C' e1 ∧ not_init C' e2)"
| "not_init C' (if (b) e1 else e2) = (not_init C' b ∧ not_init C' e1 ∧ not_init C' e2)"
| "not_init C' (while (b) e) = (not_init C' b ∧ not_init C' e)"
| "not_init C' (throw e) = not_init C' e"
| "not_init C' (try e1 catch(C V) e2) = (not_init C' e1 ∧ not_init C' e2)"
| "not_init C' (INIT C (Cs,b) ← e) = ((b ⟶ Cs = Nil ∨ C' ≠ hd Cs) ∧ C' ∉ set(tl Cs) ∧ not_init C' e)"
| "not_init C' (RI (C,e);Cs ← e') = (C' ∉ set (C#Cs) ∧ not_init C' e ∧ not_init C' e')"
| "not_inits C' ([]) = True"
| "not_inits C' (e#es) = (not_init C' e ∧ not_inits C' es)"

lemma not_inits_def'[simp]:
 "not_inits C es ⟹ ∀e ∈ set es. not_init C e"
 by(induct es, auto)

lemma nsub_RIs_not_inits_aux: "∀e ∈ set es. ¬sub_RI e ⟶ not_init C e
  ⟹ ¬sub_RIs es ⟹ not_inits C es"
 by(induct es, auto)

lemma nsub_RI_not_init: "¬sub_RI e ⟹ not_init C e"
proof(induct e) qed(auto intro: nsub_RIs_not_inits_aux)

lemma nsub_RIs_not_inits: "¬sub_RIs es ⟹ not_inits C es"
by(rule nsub_RIs_not_inits_aux) (simp_all add: nsub_RI_not_init)

subsection‹Subexpressions›

 ― ‹ all strictly smaller subexpressions; does not include self ›
 primrec subexp :: "'a exp ⇒ 'a exp set" and subexps :: "'a exp list ⇒ 'a exp set" where
  "subexp(new C) = {}"
| "subexp(Cast C e) = {e} ∪ subexp e"
| "subexp(Val v) = {}"
| "subexp(e1 «bop» e2) = {e1, e2} ∪ subexp e1 ∪ subexp e2"
| "subexp(Var V) = {}"
| "subexp(LAss V e) = {e} ∪ subexp e"
| "subexp(e∙F{D}) = {e} ∪ subexp e"
| "subexp(C∙sF{D}) = {}"
| "subexp(e1∙F{D}:=e2) = {e1, e2} ∪ subexp e1 ∪ subexp e2"
| "subexp(C∙sF{D}:=e2) = {e2} ∪subexp e2"
| "subexp(e∙M(es)) = {e} ∪ set es ∪ subexp e ∪ subexps es"
| "subexp(C∙sM(es)) = set es ∪ subexps es"
| "subexp({V:T; e}) = {e} ∪ subexp e"
| "subexp(e1;;e2) = {e1, e2} ∪ subexp e1 ∪ subexp e2"
| "subexp(if (b) e1 else e2) = {b, e1, e2} ∪ subexp b ∪ subexp e1 ∪ subexp e2"
| "subexp(while (b) e) = {b, e} ∪ subexp b ∪ subexp e"
| "subexp(throw e) = {e} ∪ subexp e"
| "subexp(try e1 catch(C V) e2) = {e1, e2} ∪ subexp e1 ∪ subexp e2"
| "subexp(INIT C (Cs,b) ← e) = {e} ∪ subexp e"
| "subexp(RI (C,e);Cs ← e') = {e, e'} ∪ subexp e ∪ subexp e'"
| "subexps([]) = {}"
| "subexps(e#es) = {e} ∪ subexp e ∪ subexps es"


lemmas subexp_subexps_induct = subexp.induct subexps.induct

abbreviation subexp_of :: "'a exp ⇒ 'a exp ⇒ bool" where
 "subexp_of e e' ≡ e ∈ subexp e'"

lemma subexp_size_le:
 "(e' ∈ subexp e ⟶ size e' < size e) ∧ (e' ∈ subexps es ⟶ size e' < size_list size es)"
proof(induct rule: subexp_subexps.induct)
  case Call:11 then show ?case using not_less_eq size_list_estimation by fastforce
next
  case SCall:12 then show ?case using not_less_eq size_list_estimation by fastforce
qed(auto)

lemma subexps_def2: "subexps es = set es ∪ (⋃e ∈ set es. subexp e)" by(induct es, auto)

 ― ‹ strong induction ›
lemma shows subexp_induct[consumes 1]: 
"(⋀e. subexp e = {} ⟹ R e) ⟹ (⋀e. (⋀e'. e' ∈ subexp e ⟹ R e') ⟹ R e)
   ⟹ (⋀es. (⋀e'. e' ∈ subexps es ⟹ R e') ⟹ Rs es) ⟹ (∀e'. e' ∈ subexp e ⟶ R e') ∧ R e"
and subexps_induct[consumes 1]:
 "(⋀es. subexps es = {} ⟹ Rs es) ⟹ (⋀e. (⋀e'. e' ∈ subexp e ⟹ R e') ⟹ R e)
   ⟹ (⋀es. (⋀e'. e' ∈ subexps es ⟹ R e') ⟹ Rs es) ⟹ (∀e'. e' ∈ subexps es ⟶ R e') ∧ Rs es"
proof(induct rule: subexp_subexps_induct)
  case (Cast x1 x2)
  then have "(∀e'. subexp_of e' x2 ⟶ R e') ∧ R x2" by fast
  then have "(∀e'. subexp_of e' (Cast x1 x2) ⟶ R e')" by auto
  then show ?case using Cast.prems(2) by fast
next
  case (BinOp x1 x2 x3)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. subexp_of e' x3 ⟶ R e') ∧ R x3"
   by fast+
  then have "(∀e'. subexp_of e' (x1 «x2» x3) ⟶ R e')" by auto
  then show ?case using BinOp.prems(2) by fast
next
  case (LAss x1 x2)
  then have "(∀e'. subexp_of e' x2 ⟶ R e') ∧ R x2" by fast
  then have "(∀e'. subexp_of e' (LAss x1 x2) ⟶ R e')" by auto
  then show ?case using LAss.prems(2) by fast
next
  case (FAcc x1 x2 x3)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" by fast
  then have "(∀e'. subexp_of e' (x1∙x2{x3}) ⟶ R e')" by auto
  then show ?case using FAcc.prems(2) by fast
next
  case (FAss x1 x2 x3 x4)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. subexp_of e' x4 ⟶ R e') ∧ R x4"
   by fast+
  then have "(∀e'. subexp_of e' (x1∙x2{x3} := x4) ⟶ R e')" by auto
  then show ?case using FAss.prems(2) by fast
next
  case (SFAss x1 x2 x3 x4)
  then have "(∀e'. subexp_of e' x4 ⟶ R e') ∧ R x4" by fast
  then have "(∀e'. subexp_of e' (x1∙sx2{x3} := x4) ⟶ R e')" by auto
  then show ?case using SFAss.prems(2) by fast
next
  case (Call x1 x2 x3)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. e' ∈ subexps x3 ⟶ R e') ∧ Rs x3"
   by fast+
  then have "(∀e'. subexp_of e' (x1∙x2(x3)) ⟶ R e')" using subexps_def2 by auto
  then show ?case using Call.prems(2) by fast
next
  case (SCall x1 x2 x3)
  then have "(∀e'. e' ∈ subexps x3 ⟶ R e') ∧ Rs x3" by fast
  then have "(∀e'. subexp_of e' (x1∙sx2(x3)) ⟶ R e')" using subexps_def2 by auto
  then show ?case using SCall.prems(2) by fast
next
  case (Block x1 x2 x3)
  then have "(∀e'. subexp_of e' x3 ⟶ R e') ∧ R x3" by fast
  then have "(∀e'. subexp_of e' {x1:x2; x3} ⟶ R e')" by auto
  then show ?case using Block.prems(2) by fast
next
  case (Seq x1 x2)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. subexp_of e' x2 ⟶ R e') ∧ R x2"
   by fast+
  then have "(∀e'. subexp_of e' (x1;; x2) ⟶ R e')" by auto
  then show ?case using Seq.prems(2) by fast
next
  case (Cond x1 x2 x3)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. subexp_of e' x2 ⟶ R e') ∧ R x2"
    and "(∀e'. subexp_of e' x3 ⟶ R e') ∧ R x3" by fast+
  then have "(∀e'. subexp_of e' (if (x1) x2 else x3) ⟶ R e')" by auto
  then show ?case using Cond.prems(2) by fast
next
  case (While x1 x2)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. subexp_of e' x2 ⟶ R e') ∧ R x2"
   by fast+
  then have "(∀e'. subexp_of e' (while (x1) x2) ⟶ R e')" by auto
  then show ?case using While.prems(2) by fast
next
  case (throw x)
  then have "(∀e'. subexp_of e' x ⟶ R e') ∧ R x" by fast
  then have "(∀e'. subexp_of e' (throw x) ⟶ R e')" by auto
  then show ?case using throw.prems(2) by fast
next
  case (TryCatch x1 x2 x3 x4)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. subexp_of e' x4 ⟶ R e') ∧ R x4"
   by fast+
  then have "(∀e'. subexp_of e' (try x1 catch(x2 x3) x4) ⟶ R e')" by auto
  then show ?case using TryCatch.prems(2) by fast
next
  case (INIT x1 x2 x3 x4)
  then have "(∀e'. subexp_of e' x4 ⟶ R e') ∧ R x4" by fast
  then have "(∀e'. subexp_of e' (INIT x1 (x2,x3) ← x4) ⟶ R e')" by auto
  then show ?case using INIT.prems(2) by fast
next
  case (RI x1 x2 x3 x4)
  then have "(∀e'. subexp_of e' x2 ⟶ R e') ∧ R x2" and "(∀e'. subexp_of e' x4 ⟶ R e') ∧ R x4"
   by fast+
  then have "(∀e'. subexp_of e' (RI (x1,x2) ; x3 ← x4) ⟶ R e')" by auto
  then show ?case using RI.prems(2) by fast
next
  case (Cons_exp x1 x2)
  then have "(∀e'. subexp_of e' x1 ⟶ R e') ∧ R x1" and "(∀e'. e' ∈ subexps x2 ⟶ R e') ∧ Rs x2"
   by fast+
  then have "(∀e'. e' ∈ subexps (x1 # x2) ⟶ R e')" using subexps_def2 by auto
  then show ?case using Cons_exp.prems(3) by fast
qed(auto)


subsection"Final expressions"
(* these definitions and most of the lemmas were in BigStep.thy in the original Jinja *)

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 final_fv[iff]: "final e ⟹ fv e = {}"
 by (auto simp: final_def)

lemma finalsE:
 "⟦ finals es;  ⋀vs. es = map Val vs ⟹ R;  ⋀vs a es'. es = map Val vs @ Throw a # es' ⟹ R ⟧ ⟹ R"
(*<*)by(auto simp:finals_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 not_finals_ConsI2: "e = Val v ⟹ ¬ finals es ⟹ ¬ finals(e#es)"
(*<*)
proof -
  assume [simp]: "e = Val v" and "¬ finals es"
  moreover {
    fix vs a es'
    assume "∀vs. es ≠ map Val vs" and "∀vs a es'. es ≠ map Val vs @ Throw a # es'"
    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
(*>*)


end