Theory Expr

(*  Title:      JinjaThreads/J/Expr.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Expressions›

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

datatype (dead 'a, dead 'b, dead 'addr) exp
  = new cname      ― ‹class instance creation›
  | newArray ty "('a,'b,'addr) exp" (‹newA _⌊_⌉› [99,0] 90)    ― ‹array instance creation: type, size in outermost dimension›
  | Cast ty "('a,'b,'addr) exp"      ― ‹type cast›
  | InstanceOf "('a,'b,'addr) exp" ty (‹_ instanceof _› [99, 99] 90) ― ‹instance of›
  | Val "'addr val"      ― ‹value›
  | BinOp "('a,'b,'addr) exp" bop "('a,'b,'addr) exp"     (‹_ «_» _› [80,0,81] 80)      ― ‹binary operation›
  | Var 'a                                               ― ‹local variable (incl. parameter)›
  | LAss 'a "('a,'b,'addr) exp"            (‹_:=_› [90,90]90)                    ― ‹local assignment›
  | AAcc "('a,'b,'addr) exp" "('a,'b,'addr) exp"            (‹_⌊_⌉› [99,0] 90)          ― ‹array cell read›
  | AAss "('a,'b,'addr) exp" "('a,'b,'addr) exp" "('a,'b,'addr) exp" (‹_⌊_⌉ := _› [10,99,90] 90)    ― ‹array cell assignment›
  | ALen "('a,'b,'addr) exp"                 (‹_∙length› [10] 90)          ― ‹array length›
  | FAcc "('a,'b,'addr) exp" vname cname     (‹_∙_{_}› [10,90,99]90)       ― ‹field access›
  | FAss "('a,'b,'addr) exp" vname cname "('a,'b,'addr) exp"     (‹_∙_{_} := _› [10,90,99,90]90)      ― ‹field assignment›
  | CompareAndSwap "('a,'b,'addr) exp" cname vname "('a,'b,'addr) exp" "('a,'b,'addr) exp" (‹_∙compareAndSwap('(_∙_, _, _'))› [10,90,90,90,90] 90) ― ‹compare and swap›
  | Call "('a,'b,'addr) exp" mname "('a,'b,'addr) exp list"     (‹_∙_'(_')› [90,99,0] 90)            ― ‹method call›
  | Block 'a ty "'addr val option" "('a,'b,'addr) exp"    (‹'{_:_=_; _}›)
  | Synchronized 'b "('a,'b,'addr) exp" "('a,'b,'addr) exp" (‹sync⇘_⇙ '(_') _› [99,99,90] 90)
  | InSynchronized 'b 'addr "('a,'b,'addr) exp" (‹insync⇘_⇙ '(_') _› [99,99,90] 90)
  | Seq "('a,'b,'addr) exp" "('a,'b,'addr) exp"     (‹_;;/ _›             [61,60]60)
  | Cond "('a,'b,'addr) exp" "('a,'b,'addr) exp" "('a,'b,'addr) exp"     (‹if '(_') _/ else _› [80,79,79]70)
  | While "('a,'b,'addr) exp" "('a,'b,'addr) exp"     (‹while '(_') _›     [80,79]70)
  | throw "('a,'b,'addr) exp"
  | TryCatch "('a,'b,'addr) exp" cname 'a "('a,'b,'addr) exp"     (‹try _/ catch'(_ _') _›  [0,99,80,79] 70)

type_synonym
  'addr expr = "(vname, unit, 'addr) exp"    ― ‹Jinja expression›
type_synonym
  'addr J_mb = "vname list × 'addr expr"    ― ‹Jinja method body: parameter names and expression›
type_synonym
  'addr J_prog = "'addr J_mb prog"          ― ‹Jinja program›

translations
  (type) "'addr expr" <= (type) "(String.literal, unit, 'addr) exp"
  (type) "'addr J_prog" <= (type) "(String.literal list × 'addr expr) prog"

subsection "Syntactic sugar"

abbreviation unit :: "('a,'b,'addr) exp"
where "unit ≡ Val Unit"

abbreviation null :: "('a,'b,'addr) exp"
where "null ≡ Val Null"

abbreviation addr :: "'addr ⇒ ('a,'b,'addr) exp"
where "addr a == Val (Addr a)"

abbreviation true :: "('a,'b,'addr) exp"
where "true == Val (Bool True)"

abbreviation false :: "('a,'b,'addr) exp"
where "false == Val (Bool False)"

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

abbreviation (in heap_base) THROW :: "cname ⇒ ('a,'b,'addr) exp"
where "THROW xc == Throw (addr_of_sys_xcpt xc)"

abbreviation sync_unit_syntax :: "('a,unit,'addr) exp ⇒ ('a,unit,'addr) exp ⇒ ('a,unit,'addr) exp" (‹sync'(_') _› [99,90] 90)
where "sync(e1) e2 ≡ sync⇘()⇙ (e1) e2"

abbreviation insync_unit_syntax :: "'addr ⇒ ('a,unit,'addr) exp ⇒ ('a,unit,'addr) exp" (‹insync'(_') _› [99,90] 90)
where "insync(a) e2 ≡ insync⇘()⇙ (a) e2"

text ‹Java syntax for binary operators›

abbreviation BinOp_Eq :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
  (‹_ «==» _› [80,81] 80)
where "e «==» e' ≡ e «Eq» e'"

abbreviation BinOp_NotEq :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «!=» _› [80,81] 80)
where "e «!=» e' ≡ e «NotEq» e'"

abbreviation BinOp_LessThan :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «<» _› [80,81] 80)
where "e «<» e' ≡ e «LessThan» e'"

abbreviation BinOp_LessOrEqual :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «<=» _› [80,81] 80)
where "e «<=» e' ≡ e «LessOrEqual» e'"

abbreviation BinOp_GreaterThan :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «>» _› [80,81] 80)
where "e «>» e' ≡ e «GreaterThan» e'"

abbreviation BinOp_GreaterOrEqual :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «>=» _› [80,81] 80)
where "e «>=» e' ≡ e «GreaterOrEqual» e'"

abbreviation BinOp_Add :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «+» _› [80,81] 80)
where "e «+» e' ≡ e «Add» e'"

abbreviation BinOp_Subtract :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «-» _› [80,81] 80)
where "e «-» e' ≡ e «Subtract» e'"

abbreviation BinOp_Mult :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «*» _› [80,81] 80)
where "e «*» e' ≡ e «Mult» e'"

abbreviation BinOp_Div :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «'/» _› [80,81] 80)
where "e «/» e' ≡ e «Div» e'"

abbreviation BinOp_Mod :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «%» _› [80,81] 80)
where "e «%» e' ≡ e «Mod» e'"

abbreviation BinOp_BinAnd :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «&» _› [80,81] 80)
where "e «&» e' ≡ e «BinAnd» e'"

abbreviation BinOp_BinOr :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «|» _› [80,81] 80)
where "e «|» e' ≡ e «BinOr» e'"

abbreviation BinOp_BinXor :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «^» _› [80,81] 80)
where "e «^» e' ≡ e «BinXor» e'"

abbreviation BinOp_ShiftLeft :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «<<» _› [80,81] 80)
where "e «<<» e' ≡ e «ShiftLeft» e'"

abbreviation BinOp_ShiftRightZeros :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «>>>» _› [80,81] 80)
where "e «>>>» e' ≡ e «ShiftRightZeros» e'"

abbreviation BinOp_ShiftRightSigned :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «>>» _› [80,81] 80)
where "e «>>» e' ≡ e «ShiftRightSigned» e'"

abbreviation BinOp_CondAnd :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «&&» _› [80,81] 80)
where "e «&&» e' ≡ if (e) e' else false"

abbreviation BinOp_CondOr :: "('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp ⇒ ('a, 'b, 'c) exp"
   (‹_ «||» _› [80,81] 80)
where "e «||» e' ≡ if (e) true else e'"

lemma inj_Val [simp]: "inj Val"
by(rule inj_onI)(simp)

lemma expr_ineqs [simp]: "Val v ;; e ≠ e" "if (e1) e else e2 ≠ e" "if (e1) e2 else e ≠ e"
by(induct e) auto

subsection‹Free Variables›

primrec fv  :: "('a,'b,'addr) exp      ⇒ 'a set"
  and fvs :: "('a,'b,'addr) exp list ⇒ 'a set"
where
  "fv(new C) = {}"
| "fv(newA T⌊e⌉) = fv e"
| "fv(Cast C e) = fv e"
| "fv(e instanceof T) = fv e"
| "fv(Val v) = {}"
| "fv(e1 «bop» e2) = fv e1 ∪ fv e2"
| "fv(Var V) = {V}"
| "fv(a⌊i⌉) = fv a ∪ fv i"
| "fv(AAss a i e) = fv a ∪ fv i ∪ fv e"
| "fv(a∙length) = fv a"
| "fv(LAss V e) = {V} ∪ fv e"
| "fv(e∙F{D}) = fv e"
| "fv(FAss e1 F D e2) = fv e1 ∪ fv e2"
| "fv(e1∙compareAndSwap(D∙F, e2, e3)) = fv e1 ∪ fv e2 ∪ fv e3"
| "fv(e∙M(es)) = fv e ∪ fvs es"
| "fv({V:T=vo; e}) = fv e - {V}"
| "fv(sync⇘V⇙ (h) e) = fv h ∪ fv e"
| "fv(insync⇘V⇙ (a) e) = fv e"
| "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})"

| "fvs([]) = {}"
| "fvs(e#es) = fv e ∪ fvs es"

lemma [simp]: "fvs(es @ es') = fvs es ∪ fvs es'"
by(induct es) auto

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

subsection‹Locks and addresses›

primrec expr_locks :: "('a,'b,'addr) exp ⇒ 'addr ⇒ nat"
  and expr_lockss :: "('a,'b,'addr) exp list ⇒ 'addr ⇒ nat"
where
  "expr_locks (new C) = (λad. 0)"
| "expr_locks (newA T⌊e⌉) = expr_locks e"
| "expr_locks (Cast T e) = expr_locks e"
| "expr_locks (e instanceof T) = expr_locks e"
| "expr_locks (Val v) = (λad. 0)"
| "expr_locks (Var v) = (λad. 0)"
| "expr_locks (e «bop» e') = (λad. expr_locks e ad + expr_locks e' ad)"
| "expr_locks (V := e) = expr_locks e"
| "expr_locks (a⌊i⌉) = (λad. expr_locks a ad + expr_locks i ad)"
| "expr_locks (AAss a i e) = (λad. expr_locks a ad + expr_locks i ad + expr_locks e ad)"
| "expr_locks (a∙length) = expr_locks a"
| "expr_locks (e∙F{D}) = expr_locks e"
| "expr_locks (FAss e F D e') = (λad. expr_locks e ad + expr_locks e' ad)"
| "expr_locks (e∙compareAndSwap(D∙F, e', e'')) = (λad. expr_locks e ad + expr_locks e' ad + expr_locks e'' ad)"
| "expr_locks (e∙m(ps)) = (λad. expr_locks e ad + expr_lockss ps ad)"
| "expr_locks ({V : T=vo; e}) = expr_locks e"
| "expr_locks (sync⇘V⇙ (o') e) = (λad. expr_locks o' ad + expr_locks e ad)"
| "expr_locks (insync⇘V⇙ (a) e) = (λad. if (a = ad) then Suc (expr_locks e ad) else expr_locks e ad)"
| "expr_locks (e;;e') = (λad. expr_locks e ad + expr_locks e' ad)"
| "expr_locks (if (b) e else e') = (λad. expr_locks b ad + expr_locks e ad + expr_locks e' ad)"
| "expr_locks (while (b) e) = (λad. expr_locks b ad + expr_locks e ad)"
| "expr_locks (throw e) = expr_locks e"
| "expr_locks (try e catch(C v) e') = (λad. expr_locks e ad + expr_locks e' ad)"

| "expr_lockss [] = (λa. 0)"
| "expr_lockss (x#xs) = (λad. expr_locks x ad + expr_lockss xs ad)"

lemma expr_lockss_append [simp]:
  "expr_lockss (es @ es') = (λad. expr_lockss es ad + expr_lockss es' ad)"
by(induct es) auto

lemma expr_lockss_map_Val [simp]: "expr_lockss (map Val vs) = (λad. 0)"
by(induct vs) auto

primrec contains_insync :: "('a,'b,'addr) exp ⇒ bool"
  and contains_insyncs :: "('a,'b,'addr) exp list ⇒ bool"
where
  "contains_insync (new C) = False"
| "contains_insync (newA T⌊i⌉) = contains_insync i"
| "contains_insync (Cast T e) = contains_insync e"
| "contains_insync (e instanceof T) = contains_insync e"
| "contains_insync (Val v) = False"
| "contains_insync (Var v) = False"
| "contains_insync (e «bop» e') = (contains_insync e ∨ contains_insync e')"
| "contains_insync (V := e) = contains_insync e"
| "contains_insync (a⌊i⌉) = (contains_insync a ∨ contains_insync i)"
| "contains_insync (AAss a i e) = (contains_insync a ∨ contains_insync i ∨ contains_insync e)"
| "contains_insync (a∙length) = contains_insync a"
| "contains_insync (e∙F{D}) = contains_insync e"
| "contains_insync (FAss e F D e') = (contains_insync e ∨ contains_insync e')"
| "contains_insync (e∙compareAndSwap(D∙F, e', e'')) = (contains_insync e ∨ contains_insync e' ∨ contains_insync e'')"
| "contains_insync (e∙m(pns)) = (contains_insync e ∨ contains_insyncs pns)"
| "contains_insync ({V : T=vo; e}) = contains_insync e"
| "contains_insync (sync⇘V⇙ (o') e) = (contains_insync o' ∨ contains_insync e)"
| "contains_insync (insync⇘V⇙ (a) e) = True"
| "contains_insync (e;;e') = (contains_insync e ∨ contains_insync e')"
| "contains_insync (if (b) e else e') = (contains_insync b ∨ contains_insync e ∨ contains_insync e')"
| "contains_insync (while (b) e) = (contains_insync b ∨ contains_insync e)"
| "contains_insync (throw e) = contains_insync e"
| "contains_insync (try e catch(C v) e') = (contains_insync e ∨ contains_insync e')"

| "contains_insyncs [] = False"
| "contains_insyncs (x # xs) = (contains_insync x ∨ contains_insyncs xs)"
  
lemma contains_insyncs_append [simp]:
  "contains_insyncs (es @ es') ⟷ contains_insyncs es ∨ contains_insyncs es'"
by(induct es, auto)

lemma fixes e :: "('a, 'b, 'addr) exp"
  and es :: "('a, 'b, 'addr) exp list"
  shows contains_insync_conv: "(contains_insync e ⟷ (∃ad. expr_locks e ad > 0))"
    and contains_insyncs_conv: "(contains_insyncs es ⟷ (∃ad. expr_lockss es ad > 0))"
by(induct e and es rule: expr_locks.induct expr_lockss.induct)(auto)

lemma contains_insyncs_map_Val [simp]: "¬ contains_insyncs (map Val vs)"
by(induct vs) auto

subsection ‹Value expressions›

inductive is_val :: "('a,'b,'addr) exp ⇒ bool" where
  "is_val (Val v)"

declare is_val.intros [simp]
declare is_val.cases [elim!]

lemma is_val_iff: "is_val e ⟷ (∃v. e = Val v)"
by(auto)

code_pred is_val .

fun is_vals :: "('a,'b,'addr) exp list ⇒ bool" where
  "is_vals [] = True"
| "is_vals (e#es) = (is_val e ∧ is_vals es)"

lemma is_vals_append [simp]: "is_vals (es @ es') ⟷ is_vals es ∧ is_vals es'"
by(induct es) auto

lemma is_vals_conv: "is_vals es = (∃vs. es = map Val vs)"
by(induct es)(auto simp add: Cons_eq_map_conv)

lemma is_vals_map_Vals [simp]: "is_vals (map Val vs) = True"
unfolding is_vals_conv by auto

inductive is_addr :: "('a,'b,'addr) exp ⇒ bool"
where "is_addr (addr a)"

declare is_addr.intros[intro!]
declare is_addr.cases[elim!]

lemma [simp]: "(is_addr e) ⟷ (∃a. e = addr a)"
by auto

primrec the_Val :: "('a, 'b, 'addr) exp ⇒ 'addr val"
where
  "the_Val (Val v) = v"

inductive is_Throws :: "('a, 'b, 'addr) exp list ⇒ bool"
where
  "is_Throws (Throw a # es)"
| "is_Throws es ⟹ is_Throws (Val v # es)"

inductive_simps is_Throws_simps:
  "is_Throws []"
  "is_Throws (e # es)"

code_pred is_Throws .

lemma is_Throws_conv: "is_Throws es ⟷ (∃vs a es'. es = map Val vs @ Throw a # es')"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs thus ?rhs
    by(induct)(fastforce simp add: Cons_eq_append_conv Cons_eq_map_conv)+
next
  assume ?rhs thus ?lhs
    by(induct es)(auto simp add: is_Throws_simps Cons_eq_map_conv Cons_eq_append_conv)
qed

subsection ‹‹blocks››

fun blocks :: "'a list ⇒ ty list ⇒ 'addr val list ⇒ ('a,'b,'addr) exp ⇒ ('a,'b,'addr) exp"
where
  "blocks (V # Vs) (T # Ts) (v # vs) e = {V:T=⌊v⌋; blocks Vs Ts vs e}"
| "blocks []       []       []       e = e"

lemma [simp]:
  "⟦ size vs = size Vs; size Ts = size Vs ⟧ ⟹ fv (blocks Vs Ts vs e) = fv e - set Vs"
by(induct rule:blocks.induct)(simp_all, blast)

lemma expr_locks_blocks:
  "⟦ length vs = length pns; length Ts = length pns ⟧
  ⟹ expr_locks (blocks pns Ts vs e) = expr_locks e"
by(induct pns Ts vs e rule: blocks.induct)(auto)

subsection ‹Final expressions›

inductive final :: "('a,'b,'addr) exp ⇒ bool" where
  "final (Val v)"
| "final (Throw a)"

declare final.cases [elim]
declare final.intros[simp]

lemmas finalE[consumes 1, case_names Val Throw] = final.cases

lemma final_iff: "final e ⟷ (∃v. e = Val v) ∨ (∃a. e = Throw a)"
by(auto)

lemma final_locks: "final e ⟹ expr_locks e l = 0"
by(auto elim: finalE)

inductive finals :: "('a,'b,'addr) exp list ⇒ bool"
where
  "finals []"
| "finals (Throw a # es)"
| "finals es ⟹ finals (Val v # es)"

inductive_simps finals_simps:
  "finals (e # es)"

lemma [iff]: "finals []"
by(rule finals.intros)

lemma [iff]: "finals (Val v # es) = finals es"
by(simp add: finals_simps)

lemma finals_app_map [iff]: "finals (map Val vs @ es) = finals es"
by(induct vs) simp_all

lemma [iff]: "finals (throw e # es) = (∃a. e = addr a)"
by(simp add: finals_simps)

lemma not_finals_ConsI: "¬ final e ⟹ ¬ finals (e # es)"
by(simp add: finals_simps final_iff)

lemma finals_iff: "finals es ⟷ (∃vs. es = map Val vs) ∨ (∃vs a es'. es = map Val vs @ Throw a # es')"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs thus ?rhs
    by induct(auto simp add: Cons_eq_append_conv Cons_eq_map_conv, metis)
next
  assume ?rhs thus ?lhs by(induct es) auto
qed

code_pred final .

subsection ‹converting results from external calls›

primrec extRet2J :: "('a, 'b, 'addr) exp ⇒ 'addr extCallRet ⇒ ('a, 'b, 'addr) exp"
where
  "extRet2J e (RetVal v) = Val v"
| "extRet2J e (RetExc a) = Throw a"
| "extRet2J e RetStaySame = e"

lemma fv_extRet2J [simp]: "fv (extRet2J e va) ⊆ fv e"
by(cases va) simp_all

subsection ‹expressions at a call›

primrec call :: "('a,'b,'addr) exp ⇒ ('addr × mname × 'addr val list) option"
  and calls :: "('a,'b,'addr) exp list ⇒ ('addr × mname × 'addr val list) option"
where
  "call (new C) = None"
| "call (newA T⌊e⌉) = call e"
| "call (Cast C e) = call e"
| "call (e instanceof T) = call e"
| "call (Val v) = None"
| "call (Var V) = None"
| "call (V:=e) = call e"
| "call (e «bop» e') = (if is_val e then call e' else call e)"
| "call (a⌊i⌉) = (if is_val a then call i else call a)"
| "call (AAss a i e) = (if is_val a then (if is_val i then call e else call i) else call a)"
| "call (a∙length) = call a"
| "call (e∙F{D}) = call e"
| "call (FAss e F D e') = (if is_val e then call e' else call e)"
| "call (e∙compareAndSwap(D∙F, e', e'')) = (if is_val e then if is_val e' then call e'' else call e' else call e)"
| "call (e∙M(es)) = (if is_val e then
                     (if is_vals es ∧ is_addr e then ⌊(THE a. e = addr a, M, THE vs. es = map Val vs)⌋ else calls es) 
                     else call e)"
| "call ({V:T=vo; e}) = call e"
| "call (sync⇘V⇙ (o') e) = call o'"
| "call (insync⇘V⇙ (a) e) = call e"
| "call (e;;e') = call e"
| "call (if (e) e1 else e2) = call e"
| "call (while(b) e) = None"
| "call (throw e) = call e"
| "call (try e1 catch(C V) e2) = call e1"

| "calls [] = None"
| "calls (e#es) = (if is_val e then calls es else call e)"

lemma calls_append [simp]:
  "calls (es @ es') = (if calls es = None ∧ is_vals es then calls es' else calls es)"
by(induct es) auto

lemma call_callE [consumes 1, case_names CallObj CallParams Call]:
  "⟦ call (obj∙M(pns)) = ⌊(a, M', vs)⌋;
     call obj = ⌊(a, M', vs)⌋ ⟹ thesis; 
     ⋀v. ⟦ obj = Val v; calls pns = ⌊(a, M', vs)⌋ ⟧ ⟹ thesis;
     ⟦ obj = addr a; pns = map Val vs; M = M' ⟧ ⟹ thesis ⟧ ⟹ thesis"
by(auto split: if_split_asm simp add: is_vals_conv)

lemma calls_map_Val [simp]:
  "calls (map Val vs) = None"
by(induct vs) auto

lemma call_not_is_val [dest]: "call e = ⌊aMvs⌋ ⟹ ¬ is_val e"
by(cases e) auto

lemma is_calls_not_is_vals [dest]: "calls es = ⌊aMvs⌋ ⟹ ¬ is_vals es"
by(induct es) auto

end