header {* \isaheader{Expressions} *}
theory Expr imports
"../Common/Exceptions"
"../Common/BinOp"
"../Common/ExternalCall"
begin
datatype ('a,'b) exp
= new cname -- "class instance creation"
| newArray ty "('a,'b) exp" ("newA _⌊_⌉" [99,0] 90) -- "array instance creation: type, size in outermost dimension"
| Cast ty "('a,'b) exp" -- "type cast"
| Val val -- "value"
| BinOp "('a,'b) exp" bop "('a,'b) exp" ("_ «_» _" [80,0,81] 80) -- "binary operation"
| Var 'a -- "local variable (incl. parameter)"
| LAss 'a "('a,'b) exp" ("_:=_" [90,90]90) -- "local assignment"
| AAcc "('a,'b) exp" "('a,'b) exp" ("_⌊_⌉" [99,0] 90) -- "array cell read"
| AAss "('a,'b) exp" "('a,'b) exp" "('a,'b) exp" ("_⌊_⌉ := _" [10,99,90] 90) -- "array cell assignment"
| ALen "('a,'b) exp" ("_•length" [10] 90) -- "array length"
| FAcc "('a,'b) exp" vname cname ("_•_{_}" [10,90,99]90) -- "field access"
| FAss "('a,'b) exp" vname cname "('a,'b) exp" ("_•_{_} := _" [10,90,99,90]90) -- "field assignment"
| Call "('a,'b) exp" mname "('a,'b) exp list" ("_•_'(_')" [90,99,0] 90) -- "method call"
| Block 'a ty "val option" "('a,'b) exp" ("'{_:_=_; _}")
| Synchronized 'b "('a,'b) exp" "('a,'b) exp" ("sync_ '(_') _" [99,99,90] 90)
| InSynchronized 'b addr "('a,'b) exp" ("insync_ '(_') _" [99,99,90] 90)
| Seq "('a,'b) exp" "('a,'b) exp" ("_;;/ _" [61,60]60)
| Cond "('a,'b) exp" "('a,'b) exp" "('a,'b) exp" ("if '(_') _/ else _" [80,79,79]70)
| While "('a,'b) exp" "('a,'b) exp" ("while '(_') _" [80,79]70)
| throw "('a,'b) exp"
| TryCatch "('a,'b) exp" cname 'a "('a,'b) exp" ("try _/ catch'(_ _') _" [0,99,80,79] 70)
types
expr = "(vname, unit) exp" -- "Jinja expression"
J_mb = "vname list × expr" -- "Jinja method body: parameter names and expression"
J_prog = "J_mb prog" -- "Jinja program"
translations
"expr" <= (type) "(message_string, unit) exp"
"J_prog" <= (type) "(message_string list × expr) prog"
subsection "Syntactic sugar"
abbreviation unit :: "('a,'b) exp"
where "unit ≡ Val Unit"
abbreviation null :: "('a,'b) exp"
where "null ≡ Val Null"
abbreviation addr :: "addr => ('a,'b) exp"
where "addr a == Val (Addr a)"
abbreviation true :: "('a,'b) exp"
where "true == Val (Bool True)"
abbreviation false :: "('a,'b) exp"
where "false == Val (Bool False)"
abbreviation Throw :: "addr => ('a,'b) exp"
where "Throw a == throw (Val (Addr a))"
abbreviation THROW :: "cname => ('a,'b) exp"
where "THROW xc == Throw (addr_of_sys_xcpt xc)"
abbreviation sync_unit_syntax :: "('a,unit) exp => ('a,unit) exp => ('a,unit) exp" ("sync'(_') _" [99,90] 90)
where "sync(e1) e2 ≡ sync() (e1) e2"
abbreviation insync_unit_syntax :: "addr => ('a,unit) exp => ('a,unit) exp" ("insync'(_') _" [99,90] 90)
where "insync(a) e2 ≡ insync() (a) e2"
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*}
consts
fv :: "('a,'b) exp => 'a set"
fvs :: "('a,'b) exp list => 'a set"
primrec
"fv(new C) = {}"
"fv(newA T⌊e⌉) = fv e"
"fv(Cast C e) = 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(e•M(es)) = fv e ∪ fvs es"
"fv({V:T=vo; e}) = fv e - {V}"
"fv(syncV (h) e) = fv h ∪ fv e"
"fv(insyncV (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*}
consts
expr_locks :: "('a,'b) exp => addr => nat"
expr_lockss :: "('a,'b) exp list => addr => nat"
primrec
"expr_locks (new C) = (λad. 0)"
"expr_locks (newA T⌊e⌉) = expr_locks e"
"expr_locks (Cast T e) = 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•m(ps)) = (λad. expr_locks e ad + expr_lockss ps ad)"
"expr_locks ({V : T=vo; e}) = expr_locks e"
"expr_locks (syncV (o') e) = (λad. expr_locks o' ad + expr_locks e ad)"
"expr_locks (insyncV (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)"
apply(induct es)
apply(auto intro: ext)
done
lemma expr_lockss_map_Val [simp]: "expr_lockss (map Val vs) = (λad. 0)"
apply(induct vs)
apply(auto)
done
consts
contains_insync :: "('a,'b) exp => bool"
contains_insyncs :: "('a,'b) exp list => bool"
primrec
"contains_insync (new C) = False"
"contains_insync (newA T⌊i⌉) = contains_insync i"
"contains_insync (Cast T e) = 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•m(pns)) = (contains_insync e ∨ contains_insyncs pns)"
"contains_insync ({V : T=vo; e}) = contains_insync e"
"contains_insync (syncV (o') e) = (contains_insync o' ∨ contains_insync e)"
"contains_insync (insyncV (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) exp"
and es :: "('a, 'b) 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)(auto)
lemma contains_insyncs_map_Val [simp]: "¬ contains_insyncs (map Val vs)"
by(induct vs) auto
lemma fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows contains_insync_expr_locks_conv: "contains_insync e <-> (∃l. expr_locks e l > 0)"
and contains_insyncs_expr_lockss_conv: "contains_insyncs es <-> (∃l. expr_lockss es l > 0)"
apply(induct e and es)
apply auto
done
subsection {* Value expressions *}
inductive is_val :: "('a,'b) 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)
fun is_vals :: "('a,'b) 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'"
apply(induct es, auto)
done
lemma is_vals_conv: "is_vals es = (∃vs. es = map Val vs)"
apply(induct es, auto)
apply(rule_tac x="v#vsa" in exI, simp)
done
lemma is_vals_map_Vals [simp]: "is_vals (map Val vs) = True"
unfolding is_vals_conv by auto
inductive is_addr :: "('a,'b) 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
end