# Theory Auxiliary

(*  Title:       CoreC++
Author:      David von Oheimb, Tobias Nipkow, Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Auxiliary Definitions›

theory Auxiliary
imports Complex_Main "HOL-Library.While_Combinator"
begin

declare
option.splits[split]
Let_def[simp]
subset_insertI2 [simp]
Cons_eq_map_conv [iff]

(* FIXME move and possibly turn into a general simproc *)
"((n::nat) + max i j ≤ m) = (n + i ≤ m ∧ n + j ≤ m)"
by arith

"(Suc(n + max i j) ≤ m) = (Suc(n + i) ≤ m ∧ Suc(n + j) ≤ m)"
by arith

notation Some  ("(⌊_⌋)")

lemma butlast_tail:
"butlast (Xs@[X,Y]) = Xs@[X]"
by (induct Xs) auto

lemma butlast_noteq:"Cs ≠ [] ⟹ butlast Cs ≠ Cs"
by(induct Cs)simp_all

lemma app_hd_tl:"⟦Cs ≠ []; Cs = Cs' @ tl Cs⟧ ⟹ Cs' = [hd Cs]"

apply (subgoal_tac "[hd Cs] @ tl Cs = Cs' @ tl Cs")
apply fast
apply simp
done

lemma only_one_append:"⟦C' ∉ set Cs; C' ∉ set Cs'; Ds@ C'#Ds' = Cs@ C'#Cs'⟧
⟹ Cs = Ds ∧ Cs' = Ds'"

apply -
apply (auto simp:in_set_conv_decomp)
apply (subgoal_tac "hd (us @ C'#Ds') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply simp
apply (subgoal_tac "hd (us @ C'#Ds') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply simp
apply (subgoal_tac "hd (us @ C'#Cs') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply (subgoal_tac "hd(C'#Ds') = C'")
apply simp
apply (simp (no_asm))
apply (subgoal_tac "hd (us @ C'#Cs') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply (subgoal_tac "hd(C'#Ds') = C'")
apply simp
apply (simp (no_asm))
done

definition pick :: "'a set ⇒ 'a" where
"pick A ≡ SOME x. x ∈ A"

lemma pick_is_element:"x ∈ A ⟹ pick A ∈ A"
by (unfold pick_def,rule_tac x="x" in someI)

definition set2list :: "'a set ⇒ 'a list" where
"set2list A ≡ fst (while (λ(Es,S). S ≠ {})
(λ(Es,S). let x = pick S in (x#Es,S-{x}))
([],A) )"

lemma card_pick:"⟦finite A; A ≠ {}⟧ ⟹ Suc(card(A-{pick(A)})) = card A"
by (drule card_Suc_Diff1,auto dest!:pick_is_element simp:ex_in_conv)

lemma set2list_prop:"⟦finite A; A ≠ {}⟧ ⟹
∃xs. while (λ(Es,S). S ≠ {})
(λ(Es,S). let x = pick S in (x#Es,S-{x}))
([],A) = (xs,{}) ∧ (set xs ∪ {} = A)"

apply(rule_tac P="(λxs. (set(fst xs) ∪ snd xs = A))" and
r="measure (card o snd)"  in while_rule)
apply(auto dest:pick_is_element)
apply(auto dest:card_pick simp:ex_in_conv measure_def inv_image_def)
done

lemma set2list_correct:"⟦finite A; A ≠ {}; set2list A = xs⟧ ⟹ set xs = A"
by (auto dest:set2list_prop simp:set2list_def)

subsection ‹‹distinct_fst››

definition distinct_fst :: "('a × 'b) list ⇒ bool" where
"distinct_fst  ≡  distinct ∘ map fst"

lemma distinct_fst_Nil [simp]:
"distinct_fst []"

apply (unfold distinct_fst_def)
apply (simp (no_asm))
done

lemma distinct_fst_Cons [simp]:
"distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"

apply (unfold distinct_fst_def)
apply (auto simp:image_def)
done

lemma map_of_SomeI:
"⟦ distinct_fst kxs; (k,x) ∈ set kxs ⟧ ⟹ map_of kxs k = Some x"
by (induct kxs) (auto simp:fun_upd_apply)

subsection ‹Using @{term list_all2} for relations›

definition fun_of :: "('a × 'b) set ⇒ 'a ⇒ 'b ⇒ bool" where
"fun_of S ≡ λx y. (x,y) ∈ S"

text ‹Convenience lemmas›

declare fun_of_def [simp]

lemma rel_list_all2_Cons [iff]:
"list_all2 (fun_of S) (x#xs) (y#ys) =
((x,y) ∈ S ∧ list_all2 (fun_of S) xs ys)"
by simp

lemma rel_list_all2_Cons1:
"list_all2 (fun_of S) (x#xs) ys =
(∃z zs. ys = z#zs ∧ (x,z) ∈ S ∧ list_all2 (fun_of S) xs zs)"
by (cases ys) auto

lemma rel_list_all2_Cons2:
"list_all2 (fun_of S) xs (y#ys) =
(∃z zs. xs = z#zs ∧ (z,y) ∈ S ∧ list_all2 (fun_of S) zs ys)"
by (cases xs) auto

lemma rel_list_all2_refl:
"(⋀x. (x,x) ∈ S) ⟹ list_all2 (fun_of S) xs xs"

lemma rel_list_all2_antisym:
"⟦ (⋀x y. ⟦(x,y) ∈ S; (y,x) ∈ T⟧ ⟹ x = y);
list_all2 (fun_of S) xs ys; list_all2 (fun_of T) ys xs ⟧ ⟹ xs = ys"
by (rule list_all2_antisym) auto

lemma rel_list_all2_trans:
"⟦ ⋀a b c. ⟦(a,b) ∈ R; (b,c) ∈ S⟧ ⟹ (a,c) ∈ T;
list_all2 (fun_of R) as bs; list_all2 (fun_of S) bs cs⟧
⟹ list_all2 (fun_of T) as cs"
by (rule list_all2_trans) auto

lemma rel_list_all2_update_cong:
"⟦ i<size xs; list_all2 (fun_of S) xs ys; (x,y) ∈ S ⟧
⟹ list_all2 (fun_of S) (xs[i:=x]) (ys[i:=y])"

lemma rel_list_all2_nthD:
"⟦ list_all2 (fun_of S) xs ys; p < size xs ⟧ ⟹ (xs!p,ys!p) ∈ S"
by (drule list_all2_nthD) auto

lemma rel_list_all2I:
"⟦ length a = length b; ⋀n. n < length a ⟹ (a!n,b!n) ∈ S ⟧ ⟹ list_all2 (fun_of S) a b"
by (erule list_all2_all_nthI) simp

declare fun_of_def [simp del]

end


# Theory Type

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/Decl.thy by David von Oheimb and Tobias Nipkow
*)

section ‹CoreC++ types›

theory Type imports Auxiliary begin

type_synonym cname = string ― ‹class names›
type_synonym mname = string ― ‹method name›
type_synonym vname = string ― ‹names for local/field variables›

definition this :: vname where
"this ≡ ''this''"

― ‹types›
datatype ty
= Void          ― ‹type of statements›
| Boolean
| Integer
| NT            ― ‹null type›
| Class cname   ― ‹class type›

datatype base  ― ‹superclass›
= Repeats cname  ― ‹repeated (nonvirtual) inheritance›
| Shares cname   ― ‹shared (virtual) inheritance›

primrec getbase :: "base ⇒ cname" where
"getbase (Repeats C) = C"
| "getbase (Shares C)  = C"

primrec isRepBase :: "base ⇒ bool" where
"isRepBase (Repeats C) = True"
| "isRepBase (Shares C) = False"

primrec isShBase :: "base ⇒ bool" where
"isShBase(Repeats C) = False"
| "isShBase(Shares C) = True"

definition is_refT :: "ty ⇒ bool" where
"is_refT T  ≡  T = NT ∨ (∃C. T = Class C)"

lemma [iff]: "is_refT NT"

lemma [iff]: "is_refT(Class C)"

lemma refTE:
"⟦is_refT T; T = NT ⟹ Q; ⋀C. T = Class C ⟹ Q ⟧ ⟹ Q"

lemma not_refTE:
"⟦ ¬is_refT T; T = Void ∨ T = Boolean ∨ T = Integer ⟹ Q ⟧ ⟹ Q"
by (cases T, auto simp add: is_refT_def)

type_synonym
env  = "vname ⇀ ty"

end



# Theory Value

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/Value.thy by David von Oheimb and Tobias Nipkow
*)

section ‹CoreC++ values›

theory Value imports Type begin

type_synonym path = "cname list"            ― ‹Path-component in subobjects›
type_synonym reference = "addr × path"

datatype val
= Unit           ― ‹dummy result value of void expressions›
| Null           ― ‹null reference›
| Bool bool      ― ‹Boolean value›
| Intg int       ― ‹integer value›
| Ref reference  ― ‹Address on the heap and subobject-path›

primrec the_Intg :: "val ⇒ int" where
"the_Intg (Intg i) = i"

"the_addr (Ref r) = fst r"

primrec the_path :: "val ⇒ path" where
"the_path (Ref r) = snd r"

primrec default_val :: "ty ⇒ val"   ― ‹default value for all types› where
"default_val Void       = Unit"
| "default_val Boolean    = Bool False"
| "default_val Integer    = Intg 0"
| "default_val NT         = Null"
| "default_val (Class C)  = Null"

lemma default_val_no_Ref:"default_val T = Ref(a,Cs) ⟹ False"
by(cases T)simp_all

primrec typeof :: "val ⇒ ty option" where
"typeof Unit     = Some Void"
| "typeof Null     = Some NT"
| "typeof (Bool b) = Some Boolean"
| "typeof (Intg i) = Some Integer"
| "typeof (Ref r)  = None"

lemma [simp]: "(typeof v = Some Boolean) = (∃b. v = Bool b)"
by(induct v) auto

lemma [simp]: "(typeof v = Some Integer) = (∃i. v = Intg i)"
by(cases v) auto

lemma [simp]: "(typeof v = Some NT) = (v = Null)"
by(cases v) auto

lemma [simp]: "(typeof v = Some Void) = (v = Unit)"
by(cases v) auto

end


# Theory Expr

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
Based on the Jinja theory J/Expr.thy by Tobias Nipkow
*)

section ‹Expressions›

theory Expr imports Value begin

subsection ‹The expressions›

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

datatype expr
= new cname            ― ‹class instance creation›
| Cast cname expr      ― ‹dynamic type cast›
| StatCast cname expr  ― ‹static type cast›
("⦇_⦈_" [80,81] 80)
| Val val              ― ‹value›
| BinOp expr bop expr          ("_ «_» _" [80,0,81] 80)
― ‹binary operation›
| Var vname            ― ‹local variable›
| LAss vname expr              ("_:=_" [70,70] 70)
― ‹local assignment›
| FAcc expr vname path         ("_∙_{_}" [10,90,99] 90)
― ‹field access›
| FAss expr vname path expr    ("_∙_{_} := _" [10,70,99,70] 70)
― ‹field assignment›
| Call expr "cname option" mname "expr list"
― ‹method call›
| Block vname ty expr          ("'{_:_; _}")
| Seq expr expr                ("_;;/ _" [61,60] 60)
| Cond expr expr expr          ("if '(_') _/ else _" [80,79,79] 70)
| While expr expr              ("while '(_') _" [80,79] 70)
| throw expr

abbreviation (input)
DynCall :: "expr ⇒ mname ⇒ expr list ⇒ expr" ("_∙_'(_')" [90,99,0] 90) where
"e∙M(es) == Call e None M es"

abbreviation (input)
StaticCall :: "expr ⇒ cname ⇒ mname ⇒ expr list ⇒ expr"
("_∙'(_::')_'(_')" [90,99,99,0] 90) where
"e∙(C::)M(es) == Call e (Some C) M es"

text‹The semantics of binary operators:›

fun binop :: "bop × val × val ⇒ val option" where
"binop(Eq,v⇩1,v⇩2) = Some(Bool (v⇩1 = v⇩2))"
| "binop(Add,Intg i⇩1,Intg i⇩2) = Some(Intg(i⇩1+i⇩2))"
| "binop(bop,v⇩1,v⇩2) = None"

lemma [simp]:
"(binop(Add,v⇩1,v⇩2) = Some v) = (∃i⇩1 i⇩2. v⇩1 = Intg i⇩1 ∧ v⇩2 = Intg i⇩2 ∧ v = Intg(i⇩1+i⇩2))"
apply(cases v⇩1)
apply auto
apply(cases v⇩2)
apply auto
done

lemma binop_not_ref[simp]:
"binop(bop,v⇩1,v⇩2) = Some (Ref r) ⟹ False"
by(cases bop)auto

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(⦇C⦈e) = fv e"
| "fv(Val v) = {}"
| "fv(e⇩1 «bop» e⇩2) = fv e⇩1 ∪ fv e⇩2"
| "fv(Var V) = {V}"
| "fv(V := e) = {V} ∪ fv e"
| "fv(e∙F{Cs}) = fv e"
| "fv(e⇩1∙F{Cs}:=e⇩2) = fv e⇩1 ∪ fv e⇩2"
| "fv(Call e Copt M es) = fv e ∪ fvs es"
| "fv({V:T; e}) = fv e - {V}"
| "fv(e⇩1;;e⇩2) = fv e⇩1 ∪ fv e⇩2"
| "fv(if (b) e⇩1 else e⇩2) = fv b ∪ fv e⇩1 ∪ fv e⇩2"
| "fv(while (b) e) = fv b ∪ fv e"
| "fv(throw e) = fv e"

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

lemma [simp]: "fvs(es⇩1 @ es⇩2) = fvs es⇩1 ∪ fvs es⇩2"
by (induct es⇩1 type:list) auto

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

end


# Theory Decl

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/Decl.thy by David von Oheimb
*)

section ‹Class Declarations and Programs›

theory Decl imports Expr begin

type_synonym
fdecl    = "vname × ty"                        ― ‹field declaration›
type_synonym
"method" = "ty list × ty × (vname list × expr)"    ― ‹arg.\ types, return type, params, body›
type_synonym
mdecl = "mname × method"                         ― ‹method declaration›
type_synonym
"class" = "base list × fdecl list × mdecl list"  ― ‹class = superclasses, fields, methods›
type_synonym
cdecl = "cname × class"                        ― ‹classa declaration›
type_synonym
prog  = "cdecl list"                           ― ‹program›

translations
(type) "fdecl" <= (type) "vname × ty"
(type) "mdecl" <= (type) "mname × ty list × ty × (vname list × expr)"
(type) "class" <= (type) "cname × fdecl list × mdecl list"
(type) "cdecl" <= (type) "cname × class"
(type) "prog " <= (type) "cdecl list"

definition "class" :: "prog ⇒ cname ⇀ class" where
"class ≡ map_of"

definition is_class :: "prog ⇒ cname ⇒ bool" where
"is_class P C ≡ class P C ≠ None"

definition baseClasses :: "base list ⇒ cname set" where
"baseClasses Bs ≡ set ((map getbase) Bs)"

definition RepBases :: "base list ⇒ cname set" where
"RepBases Bs ≡ set ((map getbase) (filter isRepBase Bs))"

definition SharedBases :: "base list ⇒ cname set" where
"SharedBases Bs ≡ set ((map getbase) (filter isShBase Bs))"

lemma not_getbase_repeats:
"D ∉ set (map getbase xs) ⟹ Repeats D ∉ set xs"
by (induct rule: list.induct, auto)

lemma not_getbase_shares:
"D ∉ set (map getbase xs) ⟹ Shares D ∉ set xs"
by (induct rule: list.induct, auto)

lemma RepBaseclass_isBaseclass:
"⟦class P C = Some(Bs,fs,ms); Repeats D ∈ set Bs⟧
⟹ D ∈ baseClasses Bs"
by (simp add:baseClasses_def, induct rule: list.induct,
auto simp:not_getbase_repeats)

lemma ShBaseclass_isBaseclass:
"⟦class P C = Some(Bs,fs,ms); Shares D ∈ set Bs⟧
⟹ D ∈ baseClasses Bs"
by (simp add:baseClasses_def, induct rule: list.induct,
auto simp:not_getbase_shares)

lemma base_repeats_or_shares:
"⟦B ∈ set Bs; D = getbase B⟧
⟹ Repeats D ∈ set Bs ∨ Shares D ∈ set Bs"
by(induct B rule:base.induct) simp+

lemma baseClasses_repeats_or_shares:
"D ∈ baseClasses Bs ⟹ Repeats D ∈ set Bs ∨ Shares D ∈ set Bs"
by (auto elim!:bexE base_repeats_or_shares

lemma finite_is_class: "finite {C. is_class P C}"

apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done

lemma finite_baseClasses:
"class P C = Some(Bs,fs,ms) ⟹ finite (baseClasses Bs)"

apply (unfold is_class_def class_def baseClasses_def)
apply clarsimp
done

definition is_type :: "prog ⇒ ty ⇒ bool" where
"is_type P T  ≡
(case T of Void ⇒ True | Boolean ⇒ True | Integer ⇒ True | NT ⇒ True
| Class C ⇒ is_class P C)"

lemma is_type_simps [simp]:
"is_type P Void ∧ is_type P Boolean ∧ is_type P Integer ∧
is_type P NT ∧ is_type P (Class C) = is_class P C"

abbreviation
"types P == Collect (CONST is_type P)"

lemma typeof_lit_is_type:
"typeof v = Some T ⟹ is_type P T"
by (induct v) (auto)

end


# Theory ClassRel

(*  Title:       CoreC++

Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/TypeRel.thy by Tobias Nipkow
*)

section ‹The subclass relation›

theory ClassRel imports Decl begin

― ‹direct repeated subclass›
inductive_set
subclsR :: "prog ⇒ (cname × cname) set"
and subclsR' :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇩R _" [71,71,71] 70)
for P :: prog
where
"P ⊢ C ≺⇩R D ≡ (C,D) ∈ subclsR P"
| subclsRI: "⟦class P C = Some (Bs,rest); Repeats(D) ∈ set Bs⟧ ⟹ P ⊢ C ≺⇩R D"

― ‹direct shared subclass›
inductive_set
subclsS :: "prog ⇒ (cname × cname) set"
and subclsS' :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇩S _" [71,71,71] 70)
for P :: prog
where
"P ⊢ C ≺⇩S D ≡ (C,D) ∈ subclsS P"
| subclsSI: "⟦class P C = Some (Bs,rest); Shares(D) ∈ set Bs⟧ ⟹ P ⊢ C ≺⇩S D"

― ‹direct subclass›
inductive_set
subcls1 :: "prog ⇒ (cname × cname) set"
and subcls1' :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇧1 _" [71,71,71] 70)
for P :: prog
where
"P ⊢ C ≺⇧1 D ≡ (C,D) ∈ subcls1 P"
| subcls1I: "⟦class P C = Some (Bs,rest); D ∈  baseClasses Bs⟧ ⟹ P ⊢ C ≺⇧1 D"

abbreviation
subcls    :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≼⇧* _"  [71,71,71] 70) where
"P ⊢ C ≼⇧* D ≡ (C,D) ∈ (subcls1 P)⇧*"

lemma subclsRD:
"P ⊢ C ≺⇩R D ⟹ ∃fs ms Bs. (class P C = Some (Bs,fs,ms)) ∧ (Repeats(D) ∈ set Bs)"
by(auto elim: subclsR.cases)

lemma subclsSD:
"P ⊢ C ≺⇩S D ⟹ ∃fs ms Bs. (class P C = Some (Bs,fs,ms)) ∧ (Shares(D) ∈ set Bs)"
by(auto elim: subclsS.cases)

lemma subcls1D:
"P ⊢ C ≺⇧1 D ⟹ ∃fs ms Bs. (class P C = Some (Bs,fs,ms)) ∧ (D ∈ baseClasses Bs)"
by(auto elim: subcls1.cases)

lemma subclsR_subcls1:
"P ⊢ C ≺⇩R D ⟹ P ⊢ C ≺⇧1 D"
by (auto elim!:subclsR.cases intro:subcls1I simp:RepBaseclass_isBaseclass)

lemma subclsS_subcls1:
"P ⊢ C ≺⇩S D ⟹ P ⊢ C ≺⇧1 D"
by (auto elim!:subclsS.cases intro:subcls1I simp:ShBaseclass_isBaseclass)

lemma subcls1_subclsR_or_subclsS:
"P ⊢ C ≺⇧1 D ⟹ P ⊢ C ≺⇩R D ∨ P ⊢ C ≺⇩S D"
by (auto dest!:subcls1D intro:subclsRI
dest:baseClasses_repeats_or_shares subclsSI)

lemma finite_subcls1: "finite (subcls1 P)"

apply(subgoal_tac "subcls1 P = (SIGMA C: {C. is_class P C} .
{D. D ∈ baseClasses (fst(the(class P C)))})")
prefer 2
apply(fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
apply simp
apply(rule finite_SigmaI [OF finite_is_class])
apply(rule_tac B = "baseClasses (fst (the (class P C)))" in finite_subset)
apply (auto intro:finite_baseClasses simp:is_class_def)
done

lemma finite_subclsR: "finite (subclsR P)"
by(rule_tac B = "subcls1 P" in finite_subset,
auto simp:subclsR_subcls1 finite_subcls1)

lemma finite_subclsS: "finite (subclsS P)"
by(rule_tac B = "subcls1 P" in finite_subset,
auto simp:subclsS_subcls1 finite_subcls1)

lemma subcls1_class:
"P ⊢ C ≺⇧1 D ⟹ is_class P C"
by (auto dest:subcls1D simp:is_class_def)

lemma subcls_is_class:
"⟦P ⊢ D ≼⇧* C; is_class P C⟧ ⟹ is_class P D"
by (induct rule:rtrancl_induct,auto dest:subcls1_class)

end


# Theory SubObj

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Definition of Subobjects›

theory SubObj
imports ClassRel
begin

subsection ‹General definitions›

type_synonym
subobj = "cname  × path"

definition mdc :: "subobj ⇒ cname" where
"mdc S = fst S"

definition ldc :: "subobj ⇒ cname" where
"ldc S = last (snd S)"

lemma mdc_tuple [simp]: "mdc (C,Cs) = C"

lemma ldc_tuple [simp]: "ldc (C,Cs) = last Cs"

subsection ‹Subobjects according to Rossie-Friedman›

fun is_subobj :: "prog ⇒ subobj ⇒ bool" ― ‹legal subobject to class hierarchie› where
"is_subobj P (C, []) ⟷ False"
| "is_subobj P (C, [D]) ⟷ (is_class P C ∧ C = D)
∨ (∃ X. P ⊢ C ≼⇧* X ∧ P ⊢ X ≺⇩S D)"
| "is_subobj P (C, D # E # Xs) = (let Ys=butlast (D # E # Xs);
Y=last (D # E # Xs);
X=last Ys
in is_subobj P (C, Ys) ∧ P ⊢ X ≺⇩R Y)"

lemma subobj_aux_rev:
assumes 1:"is_subobj P ((C,C'#rev Cs@[C'']))"
shows "is_subobj P ((C,C'#rev Cs))"
proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
hence rev:"Cs'@[C''] = rev Cs@[C'']" by simp
from this obtain D Ds where DDs:"Cs'@[C''] = D#Ds" by (cases Cs') auto
with 1 rev have subo:"is_subobj P ((C,C'#D#Ds))" by simp
from DDs have "butlast (C'#D#Ds) = C'#Cs'" by (cases Cs') auto
with subo have "is_subobj P ((C,C'#Cs'))" by simp
with Cs' show ?thesis by simp
qed

lemma subobj_aux:
assumes 1:"is_subobj P ((C,C'#Cs@[C'']))"
shows "is_subobj P ((C,C'#Cs))"
proof -
from 1 obtain Cs' where Cs':"Cs' = rev Cs" by simp
with 1 have "is_subobj P ((C,C'#rev Cs'@[C'']))" by simp
hence "is_subobj P ((C,C'#rev Cs'))" by (rule subobj_aux_rev)
with Cs' show ?thesis by simp
qed

lemma isSubobj_isClass:
assumes 1:"is_subobj P (R)"
shows "is_class P (mdc R)"

proof -
obtain C' Cs' where R:"R = (C',Cs')" by(cases R) auto
with 1 have ne:"Cs' ≠ []" by (cases Cs') auto
from this obtain C'' Cs'' where C''Cs'':"Cs' = C''#Cs''" by (cases Cs') auto
from this obtain Ds where "Ds = rev Cs''" by simp
with 1 R C''Cs'' have subo1:"is_subobj P ((C',C''#rev Ds))" by simp
with R show ?thesis
by (induct Ds,auto simp:mdc_def split:if_split_asm dest:subobj_aux,
auto elim:converse_rtranclE dest!:subclsS_subcls1 elim:subcls1_class)
qed

lemma isSubobjs_subclsR_rev:
assumes 1:"is_subobj P ((C,Cs@[D,D']@(rev Cs')))"
shows "P ⊢ D ≺⇩R D'"
using 1
proof (induct Cs')
case Nil
from this obtain Cs' X Y Xs where Cs'1:"Cs' = Cs@[D,D']"
and "X = hd(Cs@[D,D'])" and "Y = hd(tl(Cs@[D,D']))"
and "Xs =  tl(tl(Cs@[D,D']))" by simp
hence Cs'2:"Cs' = X#Y#Xs" by (cases Cs) auto
from Cs'1 have last:"last Cs' = D'" by simp
from Cs'1 have butlast:"last(butlast Cs') = D" by (simp add:butlast_tail)
from Nil Cs'1 Cs'2 have "is_subobj P ((C,X#Y#Xs))" by simp
with last butlast Cs'2 show ?case by simp
next
case (Cons C'' Cs'')
have IH:"is_subobj P ( (C, Cs @ [D, D'] @ rev Cs'')) ⟹ P ⊢ D ≺⇩R D'" by fact
from Cons obtain Cs' X Y Xs where Cs'1:"Cs' = Cs@[D,D']@(rev (C''#Cs''))"
and "X = hd(Cs@[D,D']@(rev (C''#Cs'')))"
and "Y = hd(tl(Cs@[D,D']@(rev (C''#Cs''))))"
and "Xs =  tl(tl(Cs@[D,D']@(rev (C''#Cs''))))" by simp
hence Cs'2:"Cs' = X#Y#Xs" by (cases Cs) auto
from Cons Cs'1 Cs'2 have "is_subobj P ((C,X#Y#Xs))" by simp
hence sub:"is_subobj P ((C,butlast (X#Y#Xs)))" by simp
from Cs'1 obtain E Es where Cs'3:"Cs' = Es@[E]" by (cases Cs') auto
with Cs'1 have butlast:"Es = Cs@[D,D']@(rev Cs'')" by simp
from Cs'3 have "butlast Cs' = Es" by simp
with butlast have "butlast Cs' = Cs@[D,D']@(rev Cs'')" by simp
with Cs'2 sub have "is_subobj P ((C,Cs@[D,D']@(rev Cs'')))"
by simp
with IH show ?case by simp
qed

lemma isSubobjs_subclsR:
assumes 1:"is_subobj P ((C,Cs@[D,D']@Cs'))"
shows "P ⊢ D ≺⇩R D'"

proof -
from 1 obtain Cs'' where "Cs'' = rev Cs'" by simp
with 1 have "is_subobj P ((C,Cs@[D,D']@(rev Cs'')))" by simp
thus ?thesis by (rule isSubobjs_subclsR_rev)
qed

lemma mdc_leq_ldc_aux:
assumes 1:"is_subobj P ((C,C'#rev Cs'))"
shows "P ⊢ C ≼⇧* last (C'#rev Cs')"
using 1
proof (induct Cs')
case Nil
from 1 have "is_class P C"
by (drule_tac R="(C,C'#rev Cs')" in isSubobj_isClass, simp add:mdc_def)
with Nil show ?case
proof (cases "C=C'")
case True
thus ?thesis by simp
next
case False
with Nil show ?thesis
by (auto dest!:subclsS_subcls1)
qed
next
case (Cons C'' Cs'')
have IH:"is_subobj P ( (C, C' # rev Cs'')) ⟹ P ⊢ C ≼⇧* last (C' # rev Cs'')"
and subo:"is_subobj P ( (C, C' # rev (C'' # Cs'')))" by fact+
hence "is_subobj P ( (C, C' # rev Cs''))" by (simp add:subobj_aux_rev)
with IH have rel:"P ⊢ C ≼⇧* last (C' # rev Cs'')" by simp
from subo obtain D Ds where DDs:"C' # rev Cs'' = Ds@[D]"
by (cases Cs'') auto
hence " C' # rev (C'' # Cs'') = Ds@[D,C'']" by simp
with subo have "is_subobj P ((C,Ds@[D,C'']))" by (cases Ds) auto
hence "P ⊢ D ≺⇩R C''" by (rule_tac Cs'="[]" in isSubobjs_subclsR) simp
hence rel1:"P ⊢ D ≺⇧1 C''" by (rule subclsR_subcls1)
from DDs have "D = last (C' # rev Cs'')" by simp
with rel1 have lastrel1:"P ⊢ last (C' # rev Cs'') ≺⇧1 C''" by simp
with rel have "P ⊢ C ≼⇧* C''"
by(rule_tac b="last (C' # rev Cs'')" in rtrancl_into_rtrancl) simp
thus ?case by simp
qed

lemma mdc_leq_ldc:
assumes 1:"is_subobj P (R)"
shows "P ⊢ mdc R ≼⇧* ldc R"

proof -
from 1 obtain C Cs where R:"R = (C,Cs)" by (cases R) auto
with 1 have ne:"Cs ≠ []" by (cases Cs) auto
from this obtain C' Cs' where Cs:"Cs = C'#Cs'" by (cases Cs) auto
from this obtain Cs'' where Cs':"Cs'' = rev Cs'" by simp
with R Cs 1 have "is_subobj P ((C,C'#rev Cs''))" by simp
hence rel:"P ⊢ C ≼⇧* last (C'#rev Cs'')" by (rule mdc_leq_ldc_aux)
from R Cs Cs' have ldc:"last (C'#rev Cs'') = ldc R" by(simp add:ldc_def)
from R have "mdc R = C" by(simp add:mdc_def)
with ldc rel show ?thesis by simp
qed

text‹Next three lemmas show subobject property as presented in literature›

lemma class_isSubobj:
"is_class P C ⟹ is_subobj P ((C,[C]))"
by simp

lemma repSubobj_isSubobj:
assumes 1:"is_subobj P ((C,Xs@[X]))" and 2:"P ⊢ X ≺⇩R Y"
shows "is_subobj P ((C,Xs@[X,Y]))"

using 1
proof -
obtain Cs D E Cs' where Cs1:"Cs = Xs@[X,Y]" and  "D = hd(Xs@[X,Y])"
and "E = hd(tl(Xs@[X,Y]))" and "Cs' = tl(tl(Xs@[X,Y]))"by simp
hence Cs2:"Cs = D#E#Cs'" by (cases Xs) auto
with 1 Cs1 have subobj_butlast:"is_subobj P ((C,butlast(D#E#Cs')))"
with 2 Cs1 Cs2 have "P ⊢ (last(butlast(D#E#Cs'))) ≺⇩R last(D#E#Cs')"
with subobj_butlast have "is_subobj P ((C,(D#E#Cs')))" by simp
with Cs1 Cs2 show ?thesis by simp
qed

lemma shSubobj_isSubobj:
assumes 1:  "is_subobj P ((C,Xs@[X]))" and 2:"P ⊢ X ≺⇩S Y"
shows "is_subobj P ((C,[Y]))"

using 1
proof -
from 1 have classC:"is_class P C"
by (drule_tac R="(C,Xs@[X])" in isSubobj_isClass, simp add:mdc_def)
from 1 have "P ⊢ C ≼⇧* X"
by (drule_tac R="(C,Xs@[X])" in mdc_leq_ldc, simp add:mdc_def ldc_def)
with classC 2 show ?thesis by fastforce
qed

text‹Auxiliary lemmas›

lemma build_rec_isSubobj_rev:
assumes 1:"is_subobj P ((D,D#rev Cs))" and 2:" P ⊢ C ≺⇩R D"
shows "is_subobj P ((C,C#D#rev Cs))"
using 1
proof (induct Cs)
case Nil
from 2 have "is_class P C" by (auto dest:subclsRD simp add:is_class_def)
with 1 2 show ?case by simp
next
case (Cons C' Cs')
have suboD:"is_subobj P ((D,D#rev (C'#Cs')))"
and IH:"is_subobj P ((D,D#rev Cs')) ⟹ is_subobj P ((C,C#D#rev Cs'))" by fact+
obtain E Es where E:"E = hd (rev (C'#Cs'))" and Es:"Es = tl (rev (C'#Cs'))"
by simp
with E have E_Es:"rev (C'#Cs') = E#Es" by simp
with E Es have butlast:"butlast (D#E#Es) = D#rev Cs'" by simp
from E_Es suboD have suboDE:"is_subobj P ((D,D#E#Es))" by simp
hence "is_subobj P ((D,butlast (D#E#Es)))" by simp
with butlast have "is_subobj P ((D,D#rev Cs'))" by simp
with IH have suboCD:"is_subobj P ( (C, C#D#rev Cs'))" by simp
from suboDE obtain Xs X Y Xs' where Xs':"Xs' = D#E#Es"
and bb:"Xs = butlast (butlast (D#E#Es))"
and lb:"X = last(butlast (D#E#Es))" and l:"Y = last (D#E#Es)" by simp
from this obtain Xs'' where Xs'':"Xs'' = Xs@[X]" by simp
with bb lb have "Xs'' = butlast (D#E#Es)" by simp
with l have "D#E#Es = Xs''@[Y]" by simp
with Xs'' have "D#E#Es = Xs@[X]@[Y]" by simp
with suboDE have "is_subobj P ((D,Xs@[X,Y]))" by simp
hence subR:"P ⊢ X ≺⇩R Y"  by(rule_tac Cs="Xs" and Cs'="[]" in isSubobjs_subclsR) simp
from E_Es Es have "last (D#E#Es) = C'" by simp
with subR lb l butlast have "P ⊢ last(D#rev Cs') ≺⇩R C'"
by (auto split:if_split_asm)
with suboCD show ?case by simp
qed

lemma build_rec_isSubobj:
assumes 1:"is_subobj P ((D,D#Cs))" and 2:" P ⊢ C ≺⇩R D"
shows "is_subobj P ((C,C#D#Cs))"

proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with 1 have "is_subobj P ((D,D#rev Cs'))" by simp
with 2 have "is_subobj P ((C,C#D#rev Cs'))"
by - (rule build_rec_isSubobj_rev)
with Cs' show ?thesis by simp
qed

lemma isSubobj_isSubobj_isSubobj_rev:
assumes 1:"is_subobj P ((C,[D]))" and 2:"is_subobj P ((D,D#(rev Cs)))"
shows "is_subobj P ((C,D#(rev Cs)))"
using 2
proof (induct Cs)
case Nil
with 1 show ?case by simp
next
case (Cons C' Cs')
have IH:"is_subobj P ((D,D#rev Cs')) ⟹ is_subobj P ((C,D#rev Cs'))"
and "is_subobj P ((D,D#rev (C'#Cs')))" by fact+
hence suboD:"is_subobj P ((D,D#rev Cs'@[C']))" by simp
hence "is_subobj P ((D,D#rev Cs'))" by (rule subobj_aux_rev)
with IH have suboC:"is_subobj P ((C,D#rev Cs'))" by simp
obtain C'' where C'': "C'' = last (D # rev Cs')" by simp
moreover have "D # rev Cs' = butlast (D # rev Cs') @ [last (D # rev Cs')]"
by (rule append_butlast_last_id [symmetric]) simp
ultimately have butlast: "D # rev Cs' = butlast (D  #rev Cs') @ [C'']"
by simp
hence butlast2:"D#rev Cs'@[C'] = butlast(D#rev Cs')@[C'']@[C']" by simp
with suboD have "is_subobj P ((D,butlast(D#rev Cs')@[C'']@[C']))"
by simp
with C'' have subR:"P ⊢ C'' ≺⇩R C'"
by (rule_tac Cs="butlast(D#rev Cs')" and Cs'="[]" in isSubobjs_subclsR)simp
with C'' suboC butlast have "is_subobj P ((C,butlast(D#rev Cs')@[C'']@[C']))"
by (auto intro:repSubobj_isSubobj simp del:butlast.simps)
with butlast2 have "is_subobj P ((C,D#rev Cs'@[C']))"
by (cases Cs')auto
thus ?case by simp
qed

lemma isSubobj_isSubobj_isSubobj:
assumes 1:"is_subobj P ((C,[D]))" and 2:"is_subobj P ((D,D#Cs))"
shows "is_subobj P ((C,D#Cs))"

proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with 2 have "is_subobj P ((D,D#rev Cs'))" by simp
with 1 have "is_subobj P ((C,D#rev Cs'))"
by - (rule isSubobj_isSubobj_isSubobj_rev)
with Cs' show ?thesis by simp
qed

subsection ‹Subobject handling and lemmas›

text‹Subobjects consisting of repeated inheritance relations only:›

inductive Subobjs⇩R :: "prog ⇒ cname ⇒ path ⇒ bool" for P :: prog
where
SubobjsR_Base: "is_class P C ⟹ Subobjs⇩R P C [C]"
| SubobjsR_Rep: "⟦P ⊢ C ≺⇩R D; Subobjs⇩R P D Cs⟧ ⟹ Subobjs⇩R P C (C # Cs)"

text‹All subobjects:›

inductive Subobjs :: "prog ⇒ cname ⇒ path ⇒ bool" for P :: prog
where
Subobjs_Rep: "Subobjs⇩R P C Cs ⟹ Subobjs P C Cs"
| Subobjs_Sh: "⟦P ⊢ C ≼⇧* C'; P ⊢ C' ≺⇩S D; Subobjs⇩R P D Cs⟧
⟹ Subobjs P C Cs"

lemma Subobjs_Base:"is_class P C ⟹ Subobjs P C [C]"
by (fastforce intro:Subobjs_Rep SubobjsR_Base)

lemma SubobjsR_nonempty: "Subobjs⇩R P C Cs ⟹ Cs ≠ []"
by (induct rule: Subobjs⇩R.induct, simp_all)

lemma Subobjs_nonempty: "Subobjs P C Cs ⟹ Cs ≠ []"
by (erule Subobjs.induct)(erule SubobjsR_nonempty)+

lemma hd_SubobjsR:
"Subobjs⇩R P C Cs ⟹ ∃Cs'. Cs = C#Cs'"
by(erule Subobjs⇩R.induct,simp+)

lemma SubobjsR_subclassRep:
"Subobjs⇩R P C Cs ⟹ (C,last Cs) ∈ (subclsR P)⇧*"

apply(erule Subobjs⇩R.induct)
apply simp
done

lemma SubobjsR_subclass: "Subobjs⇩R P C Cs ⟹ P ⊢ C ≼⇧* last Cs"

apply(erule Subobjs⇩R.induct)
apply simp
apply(blast intro:subclsR_subcls1 rtrancl_trans)
done

lemma Subobjs_subclass: "Subobjs P C Cs ⟹ P ⊢ C ≼⇧* last Cs"

apply(erule Subobjs.induct)
apply(erule SubobjsR_subclass)
apply(erule rtrancl_trans)
apply(blast intro:subclsS_subcls1 SubobjsR_subclass rtrancl_trans)
done

lemma Subobjs_notSubobjsR:
"⟦Subobjs P C Cs; ¬ Subobjs⇩R P C Cs⟧
⟹ ∃C' D. P ⊢ C ≼⇧* C' ∧ P ⊢ C' ≺⇩S D ∧ Subobjs⇩R P D Cs"
apply (induct rule: Subobjs.induct)
apply clarsimp
apply fastforce
done

lemma assumes subo:"Subobjs⇩R P (hd (Cs@ C'#Cs')) (Cs@ C'#Cs')"
shows SubobjsR_Subobjs:"Subobjs P C' (C'#Cs')"
using subo
proof (induct Cs)
case Nil
thus ?case by -(frule hd_SubobjsR,fastforce intro:Subobjs_Rep)
next
case (Cons D Ds)
have subo':"Subobjs⇩R P (hd ((D#Ds) @ C'#Cs')) ((D#Ds) @ C'#Cs')"
and IH:"Subobjs⇩R P (hd (Ds @ C'#Cs')) (Ds @ C'#Cs') ⟹ Subobjs P C' (C'#Cs')" by fact+
from subo' have "Subobjs⇩R P (hd (Ds @ C' # Cs')) (Ds @ C' # Cs')"
apply -
apply (drule Subobjs⇩R.cases)
apply auto
apply (rename_tac D')
apply (subgoal_tac "D' = hd (Ds @ C' # Cs')")
apply (auto dest:hd_SubobjsR)
done
with IH show ?case by simp
qed

lemma Subobjs_Subobjs:"Subobjs P C (Cs@ C'#Cs') ⟹ Subobjs P C' (C'#Cs')"

apply -
apply (drule Subobjs.cases)
apply auto
apply (subgoal_tac "C = hd(Cs @ C' # Cs')")
apply (fastforce intro:SubobjsR_Subobjs)
apply (fastforce dest:hd_SubobjsR)
apply (subgoal_tac "D = hd(Cs @ C' # Cs')")
apply (fastforce intro:SubobjsR_Subobjs)
apply (fastforce dest:hd_SubobjsR)
done

lemma SubobjsR_isClass:
assumes subo:"Subobjs⇩R P C Cs"
shows "is_class P C"

using subo
proof (induct rule:Subobjs⇩R.induct)
case SubobjsR_Base thus ?case by assumption
next
case SubobjsR_Rep thus ?case by (fastforce intro:subclsR_subcls1 subcls1_class)
qed

lemma Subobjs_isClass:
assumes subo:"Subobjs P C Cs"
shows "is_class P C"

using subo
proof (induct rule:Subobjs.induct)
case Subobjs_Rep thus ?case by (rule SubobjsR_isClass)
next
case (Subobjs_Sh C C' D Cs)
have leq:"P ⊢ C ≼⇧* C'" and leqS:"P ⊢ C' ≺⇩S D" by fact+
hence "(C,D) ∈ (subcls1 P)⇧+" by (fastforce intro:rtrancl_into_trancl1 subclsS_subcls1)
thus ?case by (induct rule:trancl_induct, fastforce intro:subcls1_class)
qed

lemma Subobjs_subclsR:
assumes subo:"Subobjs P C (Cs@[D,D']@Cs')"
shows "P ⊢ D ≺⇩R D'"

using subo
proof -
from subo have "Subobjs P D (D#D'#Cs')" by -(rule Subobjs_Subobjs,simp)
then obtain C' where subo':"Subobjs⇩R P C' (D#D'#Cs')"
by (induct rule:Subobjs.induct,blast+)
hence "C' = D" by -(drule hd_SubobjsR,simp)
with subo' have "Subobjs⇩R P D (D#D'#Cs')" by simp
thus ?thesis by (fastforce elim:Subobjs⇩R.cases dest:hd_SubobjsR)
qed

lemma assumes subo:"Subobjs⇩R P (hd Cs) (Cs@[D])" and notempty:"Cs ≠ []"
shows butlast_Subobjs_Rep:"Subobjs⇩R P (hd Cs) Cs"
using subo notempty
proof (induct Cs)
case Nil thus ?case by simp
next
case (Cons C' Cs')
have subo:"Subobjs⇩R P (hd(C'#Cs')) ((C'#Cs')@[D])"
and IH:"⟦Subobjs⇩R P (hd Cs') (Cs'@[D]); Cs' ≠ []⟧ ⟹ Subobjs⇩R P (hd Cs') Cs'" by fact+
from subo have subo':"Subobjs⇩R P C' (C'#Cs'@[D])" by simp
show ?case
proof (cases "Cs' = []")
case True
with subo' have "Subobjs⇩R P C' [C',D]" by simp
hence "is_class P C'" by(rule SubobjsR_isClass)
hence "Subobjs⇩R P C' [C']" by (rule SubobjsR_Base)
with True show ?thesis by simp
next
case False
with subo' obtain D' where subo'':"Subobjs⇩R P D' (Cs'@[D])"
and subR:"P ⊢ C' ≺⇩R D'"
by (auto elim:Subobjs⇩R.cases)
from False subo'' have hd:"D' = hd Cs'"
by (induct Cs',auto dest:hd_SubobjsR)
with subo'' False IH have "Subobjs⇩R P (hd Cs') Cs'" by simp
with subR hd have "Subobjs⇩R P C' (C'#Cs')" by (fastforce intro:SubobjsR_Rep)
thus ?thesis by simp
qed
qed

lemma assumes subo:"Subobjs P C (Cs@[D])" and notempty:"Cs ≠ []"
shows butlast_Subobjs:"Subobjs P C Cs"

using subo
proof (rule Subobjs.cases,auto)
assume suboR:"Subobjs⇩R P C (Cs@[D])" and "Subobjs P C (Cs@[D])"
from suboR notempty have hd:"C = hd Cs"
by (induct Cs,auto dest:hd_SubobjsR)
with suboR notempty have "Subobjs⇩R P (hd Cs) Cs"
by(fastforce intro:butlast_Subobjs_Rep)
with hd show "Subobjs P C Cs" by (fastforce intro:Subobjs_Rep)
next
fix C' D' assume leq:"P ⊢ C ≼⇧* C'" and subS:"P ⊢ C' ≺⇩S D'"
and suboR:"Subobjs⇩R P D' (Cs@[D])" and "Subobjs P C (Cs@[D])"
from suboR notempty have hd:"D' = hd Cs"
by (induct Cs,auto dest:hd_SubobjsR)
with suboR notempty have "Subobjs⇩R P (hd Cs) Cs"
by(fastforce intro:butlast_Subobjs_Rep)
with hd leq subS show "Subobjs P C Cs"
by(fastforce intro:Subobjs_Sh)
qed

lemma assumes subo:"Subobjs P C (Cs@(rev Cs'))" and notempty:"Cs ≠ []"
shows rev_appendSubobj:"Subobjs P C Cs"
using subo
proof(induct Cs')
case Nil thus ?case by simp
next
case (Cons D Ds)
have subo':"Subobjs P C (Cs@rev(D#Ds))"
and IH:"Subobjs P C (Cs@rev Ds) ⟹ Subobjs P C Cs" by fact+
from notempty subo' have "Subobjs P C (Cs@rev Ds)"
by (fastforce intro:butlast_Subobjs)
with IH show ?case by simp
qed

lemma appendSubobj:
assumes subo:"Subobjs P C (Cs@Cs')" and notempty:"Cs ≠ []"
shows "Subobjs P C Cs"

proof -
obtain Cs'' where Cs'':"Cs'' = rev Cs'" by simp
with subo have "Subobjs P C (Cs@(rev Cs''))" by simp
with notempty show ?thesis by - (rule rev_appendSubobj)
qed

lemma SubobjsR_isSubobj:
"Subobjs⇩R P C Cs ⟹ is_subobj P ((C,Cs))"
by(erule Subobjs⇩R.induct,simp,
auto dest:hd_SubobjsR intro:build_rec_isSubobj)

lemma leq_SubobjsR_isSubobj:
"⟦P ⊢ C ≼⇧* C'; P ⊢ C' ≺⇩S D; Subobjs⇩R P D Cs⟧
⟹ is_subobj P ((C,Cs))"

apply (subgoal_tac "is_subobj P ((C,[D]))")
apply (frule hd_SubobjsR)
apply (drule SubobjsR_isSubobj)
apply (erule exE)
apply (simp del: is_subobj.simps)
apply (erule isSubobj_isSubobj_isSubobj)
apply simp
apply auto
done

lemma Subobjs_isSubobj:
"Subobjs P C Cs ⟹ is_subobj P ((C,Cs))"
by (auto elim:Subobjs.induct SubobjsR_isSubobj

subsection ‹Paths›

subsection ‹Appending paths›

text‹Avoided name clash by calling one path Path.›

definition path_via :: "prog ⇒ cname ⇒ cname ⇒ path ⇒ bool" ("_ ⊢ Path _ to _ via _ " [51,51,51,51] 50) where
"P ⊢ Path C to D via Cs ≡ Subobjs P C Cs ∧ last Cs = D"

definition path_unique :: "prog ⇒ cname ⇒ cname ⇒ bool" ("_ ⊢ Path _ to _ unique" [51,51,51] 50) where
"P ⊢ Path C to D unique ≡ ∃!Cs. Subobjs P C Cs ∧ last Cs = D"

definition appendPath :: "path ⇒ path ⇒ path" (infixr "@⇩p" 65) where
"Cs @⇩p Cs' ≡ if (last Cs = hd Cs') then Cs @ (tl Cs') else Cs'"

lemma appendPath_last: "Cs ≠ [] ⟹ last Cs = last (Cs'@⇩pCs)"
by(auto simp:appendPath_def last_append)(cases Cs, simp_all)+

inductive
casts_to :: "prog ⇒ ty ⇒ val ⇒ val ⇒ bool"
("_ ⊢ _ casts _ to _ " [51,51,51,51] 50)
for P :: prog
where

casts_prim: "∀C. T ≠ Class C ⟹ P ⊢ T casts v to v"

| casts_null: "P ⊢ Class C casts Null to Null"

| casts_ref: "⟦ P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P ⊢ Class C casts Ref(a,Cs) to Ref(a,Ds)"

inductive
Casts_to :: "prog ⇒ ty list ⇒ val list ⇒ val list ⇒ bool"
("_ ⊢ _ Casts _ to _ " [51,51,51,51] 50)
for P :: prog
where

Casts_Nil: "P ⊢ [] Casts [] to []"

| Casts_Cons: "⟦ P ⊢ T casts v to v'; P ⊢ Ts Casts vs to vs' ⟧
⟹ P ⊢ (T#Ts) Casts (v#vs) to (v'#vs')"

lemma length_Casts_vs:
"P ⊢ Ts Casts vs to vs' ⟹ length Ts = length vs"
by (induct rule:Casts_to.induct,simp_all)

lemma length_Casts_vs':
"P ⊢ Ts Casts vs to vs' ⟹ length Ts = length vs'"
by (induct rule:Casts_to.induct,simp_all)

subsection ‹The relation on paths›

inductive_set
leq_path1 :: "prog ⇒ cname ⇒ (path × path) set"
and leq_path1' :: "prog ⇒ cname ⇒ [path, path] ⇒ bool" ("_,_ ⊢ _ ⊏⇧1 _" [71,71,71] 70)
for P :: prog and C :: cname
where
"P,C ⊢ Cs ⊏⇧1 Ds ≡ (Cs,Ds) ∈ leq_path1 P C"
| leq_pathRep: "⟦ Subobjs P C Cs; Subobjs P C Ds; Cs = butlast Ds⟧
⟹ P,C ⊢ Cs ⊏⇧1 Ds"
| leq_pathSh:  "⟦ Subobjs P C Cs; P ⊢ last Cs ≺⇩S D ⟧
⟹ P,C ⊢ Cs ⊏⇧1 [D]"

abbreviation
leq_path :: "prog ⇒ cname ⇒ [path, path] ⇒ bool" ("_,_ ⊢ _ ⊑ _"  [71,71,71] 70) where
"P,C ⊢ Cs ⊑ Ds ≡ (Cs,Ds) ∈ (leq_path1 P C)⇧*"

lemma leq_path_rep:
"⟦ Subobjs P C (Cs@[C']); Subobjs P C (Cs@[C',C''])⟧
⟹ P,C ⊢ (Cs@[C']) ⊏⇧1 (Cs@[C',C''])"

lemma leq_path_sh:
"⟦ Subobjs P C (Cs@[C']); P ⊢ C' ≺⇩S C''⟧
⟹ P,C ⊢ (Cs@[C']) ⊏⇧1 [C'']"
by(erule leq_pathSh)simp

subsection‹Member lookups›

definition FieldDecls :: "prog ⇒ cname ⇒ vname ⇒ (path × ty) set" where
"FieldDecls P C F ≡
{(Cs,T). Subobjs P C Cs ∧ (∃Bs fs ms. class P (last Cs) = Some(Bs,fs,ms)
∧ map_of fs F = Some T)}"

definition LeastFieldDecl  :: "prog ⇒ cname ⇒ vname ⇒ ty ⇒ path ⇒ bool"
("_ ⊢ _ has least _:_ via _" [51,0,0,0,51] 50) where
"P ⊢ C has least F:T via Cs ≡
(Cs,T) ∈ FieldDecls P C F ∧
(∀(Cs',T') ∈ FieldDecls P C F. P,C ⊢ Cs ⊑ Cs')"

definition MethodDefs :: "prog ⇒ cname ⇒ mname ⇒ (path × method)set" where
"MethodDefs P C M ≡
{(Cs,mthd). Subobjs P C Cs ∧ (∃Bs fs ms. class P (last Cs) = Some(Bs,fs,ms)
∧ map_of ms M = Some mthd)}"

― ‹needed for well formed criterion›
definition HasMethodDef :: "prog ⇒ cname ⇒ mname ⇒ method ⇒ path ⇒ bool"
("_ ⊢ _ has _ = _ via _" [51,0,0,0,51] 50) where
"P ⊢ C has M = mthd via Cs ≡ (Cs,mthd) ∈ MethodDefs P C M"

definition LeastMethodDef :: "prog ⇒ cname ⇒ mname ⇒ method ⇒ path ⇒ bool"
("_ ⊢ _ has least _ = _ via _" [51,0,0,0,51] 50) where
"P ⊢ C has least M = mthd via Cs ≡
(Cs,mthd) ∈ MethodDefs P C M ∧
(∀(Cs',mthd') ∈ MethodDefs P C M. P,C ⊢ Cs ⊑ Cs')"

definition MinimalMethodDefs :: "prog ⇒ cname ⇒ mname ⇒ (path × method)set" where
"MinimalMethodDefs P C M ≡
{(Cs,mthd). (Cs,mthd) ∈ MethodDefs P C M ∧
(∀(Cs',mthd')∈ MethodDefs P C M. P,C ⊢ Cs' ⊑ Cs ⟶ Cs' = Cs)}"

definition OverriderMethodDefs :: "prog ⇒ subobj ⇒ mname ⇒ (path × method)set" where
"OverriderMethodDefs P R M ≡
{(Cs,mthd). ∃Cs' mthd'. P ⊢ (ldc R) has least M = mthd' via Cs' ∧
(Cs,mthd) ∈ MinimalMethodDefs P (mdc R) M ∧
P,mdc R ⊢ Cs ⊑ (snd R)@⇩pCs'}"

definition FinalOverriderMethodDef :: "prog ⇒ subobj ⇒ mname ⇒ method ⇒ path ⇒ bool"
("_ ⊢ _ has overrider _ = _ via _" [51,0,0,0,51] 50) where
"P ⊢ R has overrider M = mthd via Cs ≡
(Cs,mthd) ∈ OverriderMethodDefs P R M ∧
card(OverriderMethodDefs P R M) = 1"
(*(∀(Cs',mthd') ∈ OverriderMethodDefs P R M. Cs = Cs' ∧ mthd = mthd')"*)

inductive
SelectMethodDef :: "prog ⇒ cname ⇒ path ⇒ mname ⇒ method ⇒ path ⇒ bool"
("_ ⊢ '(_,_') selects _ = _ via _" [51,0,0,0,0,51] 50)
for P :: prog
where

dyn_unique:
"P ⊢ C has least M = mthd via Cs' ⟹ P ⊢ (C,Cs) selects M = mthd via Cs'"

| dyn_ambiguous:
"⟦∀mthd Cs'. ¬ P ⊢ C has least M = mthd via Cs';
P ⊢ (C,Cs) has overrider M = mthd via Cs'⟧
⟹ P ⊢ (C,Cs) selects M = mthd via Cs'"

lemma sees_fields_fun:
"(Cs,T) ∈ FieldDecls P C F ⟹ (Cs,T') ∈ FieldDecls P C F ⟹ T = T'"
by(fastforce simp:FieldDecls_def)

lemma sees_field_fun:
"⟦P ⊢ C has least F:T via Cs; P ⊢ C has least F:T' via Cs⟧
⟹ T = T'"
by (fastforce simp:LeastFieldDecl_def dest:sees_fields_fun)

lemma has_least_method_has_method:
"P ⊢ C has least M = mthd via Cs ⟹ P ⊢ C has M = mthd via Cs"

lemma visible_methods_exist:
"(Cs,mthd) ∈ MethodDefs P C M ⟹
(∃Bs fs ms. class P (last Cs) = Some(Bs,fs,ms) ∧ map_of ms M = Some mthd)"
by(auto simp:MethodDefs_def)

lemma sees_methods_fun:
"(Cs,mthd) ∈ MethodDefs P C M ⟹ (Cs,mthd') ∈ MethodDefs P C M ⟹ mthd = mthd'"
by(fastforce simp:MethodDefs_def)

lemma sees_method_fun:
"⟦P ⊢ C has least M = mthd via Cs; P ⊢ C has least M = mthd' via Cs⟧
⟹ mthd = mthd'"
by (fastforce simp:LeastMethodDef_def dest:sees_methods_fun)

lemma overrider_method_fun:
assumes overrider:"P ⊢ (C,Cs) has overrider M = mthd via Cs'"
and overrider':"P ⊢ (C,Cs) has overrider M = mthd' via Cs''"
shows "mthd = mthd' ∧ Cs' = Cs''"
proof -
from overrider' have omd:"(Cs'',mthd') ∈ OverriderMethodDefs P (C,Cs) M"
from overrider have "(Cs',mthd) ∈ OverriderMethodDefs P (C,Cs) M"
and "card(OverriderMethodDefs P (C,Cs) M) = 1"
hence "∀(Ds,mthd'') ∈ OverriderMethodDefs P (C,Cs) M. (Cs',mthd) = (Ds,mthd'')"
by(fastforce simp:card_Suc_eq)
with omd show ?thesis by fastforce
qed

end


# Theory Objects

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/Objects.thy by Tobias Nipkow
*)

section ‹Objects and the Heap›

theory Objects imports SubObj begin

subsection‹Objects›

type_synonym
subo = "(path × (vname ⇀ val))"     ― ‹subobjects realized on the heap›
type_synonym
obj  = "cname × subo set"            ― ‹mdc and subobject›

definition init_class_fieldmap :: "prog ⇒ cname ⇒ (vname ⇀ val)" where
"init_class_fieldmap P C ≡
map_of (map (λ(F,T).(F,default_val T)) (fst(snd(the(class P C)))) )"

inductive
init_obj :: "prog ⇒ cname ⇒ (path × (vname ⇀ val)) ⇒ bool"
for P :: prog and C :: cname
where
"Subobjs P C Cs ⟹ init_obj P C (Cs,init_class_fieldmap P (last Cs))"

lemma init_obj_nonempty: "init_obj P C (Cs,fs) ⟹ Cs ≠ []"
by (fastforce elim:init_obj.cases dest:Subobjs_nonempty)

lemma init_obj_no_Ref:
"⟦init_obj P C (Cs,fs);  fs F = Some(Ref(a',Cs'))⟧ ⟹ False"
by (fastforce elim:init_obj.cases default_val_no_Ref
simp:init_class_fieldmap_def map_of_map)

lemma SubobjsSet_init_objSet:
"{Cs. Subobjs P C Cs} = {Cs. ∃vmap. init_obj P C (Cs,vmap)}"
by ( fastforce intro:init_obj.intros elim:init_obj.cases)

definition obj_ty :: "obj ⇒ ty" where
"obj_ty obj  ≡  Class (fst obj)"

― ‹a new, blank object with default values in all fields:›
definition blank :: "prog ⇒ cname ⇒ obj" where
"blank P C  ≡ (C, Collect (init_obj P C))"

lemma [simp]: "obj_ty (C,S) = Class C"

subsection‹Heap›

type_synonym heap  = "addr ⇀ obj"

abbreviation
cname_of :: "heap ⇒ addr ⇒ cname" where
"cname_of hp a == fst (the (hp a))"

"new_Addr h  ≡  if ∃a. h a = None then Some(SOME a. h a = None) else None"

"new_Addr h = Some a ⟹ h a = None"

end


# Theory Exceptions

(*  Title:       CoreC++
Author:      Gerwin Klein, Martin Strecker, Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Exceptions›

theory Exceptions imports Objects begin

subsection ‹Exceptions›

definition NullPointer :: cname where
"NullPointer ≡ ''NullPointer''"

definition ClassCast :: cname where
"ClassCast ≡ ''ClassCast''"

definition OutOfMemory :: cname where
"OutOfMemory ≡ ''OutOfMemory''"

definition sys_xcpts :: "cname set" where
"sys_xcpts  ≡  {NullPointer, ClassCast, OutOfMemory}"

"addr_of_sys_xcpt s ≡ if s = NullPointer then 0 else
if s = ClassCast then 1 else
if s = OutOfMemory then 2 else undefined"

definition start_heap :: "prog ⇒ heap" where
"start_heap P ≡ Map.empty (addr_of_sys_xcpt NullPointer ↦ blank P NullPointer)
(addr_of_sys_xcpt ClassCast ↦ blank P ClassCast)
(addr_of_sys_xcpt OutOfMemory ↦ blank P OutOfMemory)"

definition preallocated :: "heap ⇒ bool" where
"preallocated h ≡ ∀C ∈ sys_xcpts. ∃S. h (addr_of_sys_xcpt C) = Some (C,S)"

subsection "System exceptions"

lemma [simp]:
"NullPointer ∈ sys_xcpts ∧ OutOfMemory ∈ sys_xcpts ∧ ClassCast ∈ sys_xcpts"

lemma sys_xcpts_cases [consumes 1, cases set]:
"⟦ C ∈ sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast⟧ ⟹ P C"

subsection "@{term preallocated}"

lemma preallocated_dom [simp]:
"⟦ preallocated h; C ∈ sys_xcpts ⟧ ⟹ addr_of_sys_xcpt C ∈ dom h"
by (fastforce simp:preallocated_def dom_def)

lemma preallocatedD:
"⟦ preallocated h; C ∈ sys_xcpts ⟧ ⟹ ∃S. h (addr_of_sys_xcpt C) = Some (C,S)"

lemma preallocatedE [elim?]:
"⟦ preallocated h;  C ∈ sys_xcpts; ⋀S. h (addr_of_sys_xcpt C) = Some(C,S) ⟹ P h C⟧
⟹ P h C"
by (fast dest: preallocatedD)

lemma cname_of_xcp [simp]:
"⟦ preallocated h; C ∈ sys_xcpts ⟧ ⟹ cname_of h (addr_of_sys_xcpt C) = C"
by (auto elim: preallocatedE)

lemma preallocated_start:
"preallocated (start_heap P)"
by (auto simp add: start_heap_def blank_def sys_xcpts_def fun_upd_apply

subsection "@{term start_heap}"

lemma start_Subobj:
"⟦start_heap P a = Some(C, S); (Cs,fs) ∈ S⟧ ⟹ Subobjs P C Cs"
by (fastforce elim:init_obj.cases simp:start_heap_def blank_def
fun_upd_apply split:if_split_asm)

lemma start_SuboSet:
"⟦start_heap P a = Some(C, S); Subobjs P C Cs⟧ ⟹ ∃fs. (Cs,fs) ∈ S"
by (fastforce intro:init_obj.intros simp:start_heap_def blank_def
split:if_split_asm)

lemma start_init_obj: "start_heap P a = Some(C,S) ⟹ S = Collect (init_obj P C)"
by (auto simp:start_heap_def blank_def split:if_split_asm)

lemma start_subobj:
"⟦start_heap P a = Some(C, S); ∃fs. (Cs, fs) ∈ S⟧ ⟹ Subobjs P C Cs"
by (fastforce elim:init_obj.cases simp:start_heap_def blank_def
split:if_split_asm)

end


# Theory Syntax

(*  Title:       CoreC++

Author:      Tobias Nipkow, Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Extracted from the Jinja theory J/Expr.thy by Tobias Nipkow
*)

section ‹Syntax›

theory Syntax imports Exceptions begin

text‹Syntactic sugar›

abbreviation (input)
InitBlock :: "vname ⇒ ty ⇒ expr ⇒ expr ⇒ expr"   ("(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 "ref r == Val(Ref r)"
abbreviation "true == Val(Bool True)"
abbreviation "false == Val(Bool False)"

abbreviation
Throw :: "reference ⇒ expr" where
"Throw r == throw(ref r)"

abbreviation (input)
THROW :: "cname ⇒ expr" where

end


# Theory State

(*  Title:       CoreC++
Author:      Tobias Nipkow
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Program State›

theory State imports Exceptions begin

type_synonym
locals = "vname ⇀ val"      ― ‹local vars, incl. params and this''›
type_synonym
state  = "heap × locals"

definition hp :: "state ⇒ heap" where
"hp  ≡  fst"

definition lcl :: "state ⇒ locals" where
"lcl  ≡  snd"

declare hp_def[simp] lcl_def[simp]

end


# Theory BigStep

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Big Step Semantics›

theory BigStep
imports Syntax State
begin

subsection ‹The rules›

inductive
eval :: "prog ⇒ env ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
and evals :: "prog ⇒ env ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) [⇒]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
for P :: prog
where

New:
"⟦ new_Addr h = Some a; h' = h(a↦(C,Collect (init_obj P C))) ⟧
⟹ P,E ⊢ ⟨new C,(h,l)⟩ ⇒ ⟨ref (a,[C]),(h',l)⟩"

| NewFail:
P,E ⊢ ⟨new C, (h,l)⟩ ⇒ ⟨THROW OutOfMemory,(h,l)⟩"

| StaticUpCast:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩; P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨ref (a,Ds),s⇩1⟩"

| StaticDownCast:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]@Cs'),s⇩1⟩
⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]),s⇩1⟩"

| StaticCastNull:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩"

| StaticCastFail:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩; ¬ P ⊢ (last Cs) ≼⇧* C; C ∉ set Cs ⟧
⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨THROW ClassCast,s⇩1⟩"

| StaticCastThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| StaticUpDynCast:(* path uniqueness not necessary for type proof but for determinism *)
"⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a,Cs),s⇩1⟩; P ⊢ Path last Cs to C unique;
P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨ref(a,Ds),s⇩1⟩"

| StaticDownDynCast:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]@Cs'),s⇩1⟩
⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]),s⇩1⟩"

| DynCast: (* path uniqueness not necessary for type proof but for determinism *)
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S);
P ⊢ Path D to C via Cs'; P ⊢ Path D to C unique ⟧
⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨ref (a,Cs'),(h,l)⟩"

| DynCastNull:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩"

| DynCastFail: (* fourth premise not necessary for type proof but for determinism *)
"⟦ P,E ⊢ ⟨e,s⇩0⟩⇒ ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S); ¬ P ⊢ Path D to C unique;
¬ P ⊢ Path last Cs to C unique; C ∉ set Cs ⟧
⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨null,(h,l)⟩"

| DynCastThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| Val:
"P,E ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩"

| BinOp:
"⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v⇩2,s⇩2⟩;
binop(bop,v⇩1,v⇩2) = Some v ⟧
⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩⇒⟨Val v,s⇩2⟩"

| BinOpThrow1:
"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩ ⟹
P,E ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩"

| BinOpThrow2:
"⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e,s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨throw e,s⇩2⟩"

| Var:
"l V = Some v ⟹
P,E ⊢ ⟨Var V,(h,l)⟩ ⇒ ⟨Val v,(h,l)⟩"

| LAss:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val v,(h,l)⟩; E V = Some T;
P ⊢ T casts v to v'; l' = l(V↦v') ⟧
⟹ P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨Val v',(h,l')⟩"

| LAssThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAcc:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs'),(h,l)⟩; h a = Some(D,S);
Ds = Cs'@⇩pCs; (Ds,fs) ∈ S; fs F = Some v ⟧
⟹ P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨Val v,(h,l)⟩"

| FAccNull:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩"

| FAccThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAss:
"⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref (a,Cs'),s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2)⟩;
h⇩2 a = Some(D,S); P ⊢ (last Cs') has least F:T via Cs; P ⊢ T casts v to v';
Ds = Cs'@⇩pCs; (Ds,fs) ∈ S; fs' = fs(F↦v');
S' = S - {(Ds,fs)} ∪ {(Ds,fs')}; h⇩2' = h⇩2(a↦(D,S'))⟧
⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨Val v',(h⇩2',l⇩2)⟩"

| FAssNull:
"⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,s⇩2⟩ ⟧ ⟹
P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"

| FAssThrow1:
"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAssThrow2:
"⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| CallObjThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| CallParamsThrow:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨map Val vs @ throw ex # es',s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"

| Call:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩;  P,E ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2)⟩;
h⇩2 a = Some(C,S);  P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds;
P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs'; length vs = length pns;
P ⊢ Ts Casts vs to vs'; l⇩2' = [this↦Ref (a,Cs'), pns[↦]vs'];
new_body = (case T' of Class D ⇒ ⦇D⦈body   | _  ⇒ body);
P,E(this↦Class(last Cs'), pns[↦]Ts) ⊢ ⟨new_body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3)⟩ ⟧
⟹ P,E ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2)⟩"

| StaticCall:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩;  P,E ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2)⟩;
P ⊢ Path (last Cs) to C unique; P ⊢ Path (last Cs) to C via Cs'';
P ⊢ C has least M = (Ts,T,pns,body) via Cs'; Ds = (Cs@⇩pCs'')@⇩pCs';
length vs = length pns; P ⊢ Ts Casts vs to vs';
l⇩2' = [this↦Ref (a,Ds), pns[↦]vs'];
P,E(this↦Class(last Ds), pns[↦]Ts) ⊢ ⟨body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3)⟩ ⟧
⟹ P,E ⊢ ⟨e∙(C::)M(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2)⟩"

| CallNull:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"

| Block:
"⟦P,E(V ↦ T) ⊢ ⟨e⇩0,(h⇩0,l⇩0(V:=None))⟩ ⇒ ⟨e⇩1,(h⇩1,l⇩1)⟩ ⟧ ⟹
P,E ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0)⟩ ⇒ ⟨e⇩1,(h⇩1,l⇩1(V:=l⇩0 V))⟩"

| Seq:
"⟦ P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒ ⟨e⇩2,s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨e⇩0;;e⇩1,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"

| SeqThrow:
"P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩ ⟹
P,E ⊢ ⟨e⇩0;;e⇩1,s⇩0⟩⇒⟨throw e,s⇩1⟩"

| CondT:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒ ⟨e',s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e',s⇩2⟩"

| CondF:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨e',s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e',s⇩2⟩"

| CondThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| WhileF:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩1⟩ ⟹
P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨unit,s⇩1⟩"

| WhileT:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ ⇒ ⟨Val v⇩1,s⇩2⟩;
P,E ⊢ ⟨while (e) c,s⇩2⟩ ⇒ ⟨e⇩3,s⇩3⟩ ⟧
⟹ P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩3,s⇩3⟩"

| WhileCondThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| WhileBodyThrow:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩⟧
⟹ P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| Throw:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref r,s⇩1⟩ ⟹
P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨Throw r,s⇩1⟩"

| ThrowNull:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩"

| ThrowThrow:
"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| Nil:
"P,E ⊢ ⟨[],s⟩ [⇒] ⟨[],s⟩"

| Cons:
"⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨es',s⇩2⟩ ⟧
⟹ P,E ⊢ ⟨e#es,s⇩0⟩ [⇒] ⟨Val v # es',s⇩2⟩"

| ConsThrow:
"P,E ⊢ ⟨e, s⇩0⟩ ⇒ ⟨throw e', s⇩1⟩ ⟹
P,E ⊢ ⟨e#es, s⇩0⟩ [⇒] ⟨throw e' # es, s⇩1⟩"

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,E ⊢ ⟨new C,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨Cast C e,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨⦇C⦈e,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨Val v,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨Var V,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨V:=e,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨e∙F{Cs},s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨e∙M(es),s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨e∙(C::)M(es),s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨{V:T;e⇩1},s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨e⇩1;;e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨while (b) c,s⟩ ⇒ ⟨e',s'⟩"
"P,E ⊢ ⟨throw e,s⟩ ⇒ ⟨e',s'⟩"

inductive_cases evals_cases [cases set]:
"P,E ⊢ ⟨[],s⟩ [⇒] ⟨e',s'⟩"
"P,E ⊢ ⟨e#es,s⟩ [⇒] ⟨e',s'⟩"

subsection ‹Final expressions›

definition final :: "expr ⇒ bool" where
"final e  ≡  (∃v. e = Val v) ∨ (∃r. e = Throw r)"

definition finals:: "expr list ⇒ bool" where
"finals es  ≡  (∃vs. es = map Val vs) ∨ (∃vs r es'. es = map Val vs @ Throw r # es')"

lemma [simp]: "final(Val v)"

lemma [simp]: "final(throw e) = (∃r. e = ref r)"

lemma finalE: "⟦ final e;  ⋀v. e = Val v ⟹ Q;  ⋀r. e = Throw r ⟹ Q ⟧ ⟹ Q"
by(auto simp:final_def)

lemma [iff]: "finals []"

lemma [iff]: "finals (Val v # es) = finals es"

apply(rule iffI)
apply(erule disjE)
apply simp
apply(rule disjI2)
apply clarsimp
apply(case_tac vs)
apply simp
apply fastforce
apply(erule disjE)
apply (rule disjI1)
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) = (∃r. e = ref r)"

apply(rule iffI)
apply clarsimp
apply(case_tac vs)
apply simp
apply fastforce
apply fastforce
done

lemma not_finals_ConsI: "¬ final e ⟹ ¬ finals(e#es)"

apply(case_tac vs)
apply auto
done

lemma eval_final: "P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ final e'"
and evals_final: "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es'"
by(induct rule:eval_evals.inducts, simp_all)

lemma eval_lcl_incr: "P,E ⊢ ⟨e,(h⇩0,l⇩0)⟩ ⇒ ⟨e',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
and evals_lcl_incr: "P,E ⊢ ⟨es,(h⇩0,l⇩0)⟩ [⇒] ⟨es',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
by (induct rule:eval_evals_inducts) (auto simp del:fun_upd_apply)

text‹Only used later, in the small to big translation, but is already a
good sanity check:›

lemma eval_finalId:  "final e ⟹ P,E ⊢ ⟨e,s⟩ ⇒ ⟨e,s⟩"
by (erule finalE) (fastforce intro: eval_evals.intros)+

lemma eval_finalsId:
assumes finals: "finals es" shows "P,E ⊢ ⟨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,E ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩"
and finals: "finals (e # es)" by fact+
show "P,E ⊢ ⟨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,E ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩" by (simp add: eval_finalId)
moreover from finals e have "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩" by(fast intro:hyp)
ultimately have "P,E ⊢ ⟨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,E ⊢ ⟨Throw a,s⟩ ⇒ ⟨Throw a,s⟩" by (simp add: eval_finalId)
hence "P,E ⊢ ⟨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

lemma
eval_preserves_obj:"P,E ⊢ ⟨e,(h,l)⟩ ⇒ ⟨e',(h',l')⟩ ⟹ (⋀S. h a = Some(D,S)
⟹ ∃S'. h' a = Some(D,S'))"
and evals_preserves_obj:"P,E ⊢ ⟨es,(h,l)⟩ [⇒] ⟨es',(h',l')⟩
⟹ (⋀S. h a = Some(D,S) ⟹ ∃S'. h' a = Some(D,S'))"

end


# Theory SmallStep

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Small Step Semantics›

theory SmallStep imports Syntax State begin

subsection ‹Some pre-definitions›

fun blocks :: "vname list × ty list × val list × expr ⇒ expr"
where
blocks_Cons:"blocks(V#Vs, T#Ts, v#vs, e) = {V:T := Val v; blocks(Vs,Ts,vs,e)}" |
blocks_Nil: "blocks([],[],[],e) = e"

lemma blocks_old_induct:
fixes P :: "vname list ⇒ ty list ⇒ val list ⇒ expr ⇒ bool"
shows
"⟦⋀aj ak al. P [] [] (aj # ak) al; ⋀ad ae a b. P [] (ad # ae) a b;
⋀V Vs a b. P (V # Vs) [] a b; ⋀V Vs T Ts aw. P (V # Vs) (T # Ts) [] aw;
⋀V Vs T Ts v vs e. P Vs Ts vs e ⟹ P (V # Vs) (T # Ts) (v # vs) e; ⋀e. P [] [] [] e⟧
⟹ P u v w x"
by (induction_schema) (pat_completeness, lexicographic_order)

lemma [simp]:
"⟦ size vs = size Vs; size Ts = size Vs ⟧ ⟹ fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"

apply(induct rule:blocks_old_induct)
apply simp_all
apply blast
done

definition assigned :: "vname ⇒ expr ⇒ bool" where
"assigned V e  ≡  ∃v e'. e = (V:= Val v;; e')"

subsection ‹The rules›

inductive_set
red  :: "prog ⇒ (env × (expr × state) × (expr × state)) set"
and reds  :: "prog ⇒ (env × (expr list × state) × (expr list × state)) set"
and red' :: "prog ⇒ env ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) →/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
and reds' :: "prog ⇒ env ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) [→]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
for P :: prog
where

"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ≡ (E,(e,s), e',s') ∈ red P"
| "P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ≡ (E,(es,s), es',s') ∈ reds P"

| RedNew:
"⟦ new_Addr h = Some a; h' = h(a↦(C,Collect (init_obj P C))) ⟧
⟹ P,E ⊢ ⟨new C, (h,l)⟩ → ⟨ref (a,[C]), (h',l)⟩"

| RedNewFail:
P,E ⊢ ⟨new C, (h,l)⟩ → ⟨THROW OutOfMemory, (h,l)⟩"

| StaticCastRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨⦇C⦈e, s⟩ → ⟨⦇C⦈e', s'⟩"

| RedStaticCastNull:
"P,E ⊢ ⟨⦇C⦈null, s⟩ → ⟨null,s⟩"

| RedStaticUpCast:
"⟦ P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P,E ⊢ ⟨⦇C⦈(ref (a,Cs)), s⟩ → ⟨ref (a,Ds), s⟩"

| RedStaticDownCast:
"P,E ⊢ ⟨⦇C⦈(ref (a,Cs@[C]@Cs')), s⟩ → ⟨ref (a,Cs@[C]), s⟩"

| RedStaticCastFail:
"⟦C ∉ set Cs; ¬ P ⊢ (last Cs) ≼⇧* C⟧
⟹ P,E ⊢ ⟨⦇C⦈(ref (a,Cs)), s⟩ → ⟨THROW ClassCast, s⟩"

| DynCastRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨Cast C e, s⟩ → ⟨Cast C e', s'⟩"

| RedDynCastNull:
"P,E ⊢ ⟨Cast C null, s⟩ → ⟨null,s⟩"

| RedStaticUpDynCast: (* path uniqueness not necessary for type proof but for determinism *)
"⟦ P ⊢ Path last Cs to C unique; P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P,E ⊢ ⟨Cast C(ref(a,Cs)),s⟩ → ⟨ref(a,Ds),s⟩"

| RedStaticDownDynCast:
"P,E ⊢ ⟨Cast C (ref (a,Cs@[C]@Cs')), s⟩ → ⟨ref (a,Cs@[C]), s⟩"

| RedDynCast:(* path uniqueness not necessary for type proof but for determinism *)
"⟦ hp s a = Some(D,S); P ⊢ Path D to C via Cs';
P ⊢ Path D to C unique ⟧
⟹ P,E ⊢ ⟨Cast C (ref (a,Cs)), s⟩ → ⟨ref (a,Cs'), s⟩"

| RedDynCastFail:(* third premise not necessary for type proof but for determinism *)
"⟦hp s a = Some(D,S); ¬ P ⊢ Path D to C unique;
¬ P ⊢ Path last Cs to C unique; C ∉ set Cs ⟧
⟹ P,E ⊢ ⟨Cast C (ref (a,Cs)), s⟩ → ⟨null, s⟩"

| BinOpRed1:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e «bop» e⇩2, s⟩ → ⟨e' «bop» e⇩2, s'⟩"

| BinOpRed2:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨(Val v⇩1) «bop» e, s⟩ → ⟨(Val v⇩1) «bop» e', s'⟩"

| RedBinOp:
"binop(bop,v⇩1,v⇩2) = Some v ⟹
P,E ⊢ ⟨(Val v⇩1) «bop» (Val v⇩2), s⟩ → ⟨Val v,s⟩"

| RedVar:
"lcl s V = Some v ⟹
P,E ⊢ ⟨Var V,s⟩ → ⟨Val v,s⟩"

| LAssRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨V:=e,s⟩ → ⟨V:=e',s'⟩"

| RedLAss:
"⟦E V = Some T; P ⊢ T casts v to v'⟧ ⟹
P,E ⊢ ⟨V:=(Val v),(h,l)⟩ → ⟨Val v',(h,l(V↦v'))⟩"

| FAccRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e∙F{Cs}, s⟩ → ⟨e'∙F{Cs}, s'⟩"

| RedFAcc:
"⟦ hp s a = Some(D,S); Ds = Cs'@⇩pCs; (Ds,fs) ∈ S; fs F = Some v ⟧
⟹ P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}, s⟩ → ⟨Val v,s⟩"

| RedFAccNull:
"P,E ⊢ ⟨null∙F{Cs}, s⟩ → ⟨THROW NullPointer, s⟩"

| FAssRed1:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e∙F{Cs}:=e⇩2, s⟩ → ⟨e'∙F{Cs}:=e⇩2, s'⟩"

| FAssRed2:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨Val v∙F{Cs}:=e, s⟩ → ⟨Val v∙F{Cs}:=e', s'⟩"

| RedFAss:
"⟦h a = Some(D,S); P ⊢ (last Cs') has least F:T via Cs;
P ⊢ T casts v to v'; Ds = Cs'@⇩pCs; (Ds,fs) ∈ S⟧ ⟹
P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}:=(Val v), (h,l)⟩ → ⟨Val v', (h(a ↦ (D,insert (Ds,fs(F↦v')) (S - {(Ds,fs)}))),l)⟩"

| RedFAssNull:
"P,E ⊢ ⟨null∙F{Cs}:=Val v, s⟩ → ⟨THROW NullPointer, s⟩"

| CallObj:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨Call e Copt M es,s⟩ → ⟨Call e' Copt M es,s'⟩"

| CallParams:
"P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ⟹
P,E ⊢ ⟨Call (Val v) Copt M es,s⟩ → ⟨Call (Val v) Copt M es',s'⟩"

| RedCall:
"⟦ hp s a = Some(C,S); P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds;
P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs';
size vs = size pns; size Ts = size pns;
bs = blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body);
new_body = (case T' of Class D ⇒ ⦇D⦈bs | _ ⇒ bs)⟧
⟹ P,E ⊢ ⟨(ref (a,Cs))∙M(map Val vs), s⟩ → ⟨new_body, s⟩"

| RedStaticCall:
"⟦ P ⊢ Path (last Cs) to C unique; P ⊢ Path (last Cs) to C via Cs'';
P ⊢ C has least M = (Ts,T,pns,body) via Cs'; Ds = (Cs@⇩pCs'')@⇩pCs';
size vs = size pns; size Ts = size pns ⟧
⟹ P,E ⊢ ⟨(ref (a,Cs))∙(C::)M(map Val vs), s⟩ →
⟨blocks(this#pns,Class(last Ds)#Ts,Ref(a,Ds)#vs,body), s⟩"

| RedCallNull:
"P,E ⊢ ⟨Call null Copt M (map Val vs),s⟩ → ⟨THROW NullPointer,s⟩"

| BlockRedNone:
"⟦ P,E(V ↦ T) ⊢ ⟨e, (h,l(V:=None))⟩ → ⟨e', (h',l')⟩; l' V = None; ¬ assigned V e ⟧
⟹ P,E ⊢ ⟨{V:T; e}, (h,l)⟩ → ⟨{V:T; e'}, (h',l'(V := l V))⟩"

| BlockRedSome:
"⟦ P,E(V ↦ T) ⊢ ⟨e, (h,l(V:=None))⟩ → ⟨e', (h',l')⟩; l' V = Some v;
¬ assigned V e ⟧
⟹ P,E ⊢ ⟨{V:T; e}, (h,l)⟩ → ⟨{V:T := Val v; e'}, (h',l'(V := l V))⟩"

| InitBlockRed:
"⟦ P,E(V ↦ T) ⊢ ⟨e, (h,l(V↦v'))⟩ → ⟨e', (h',l')⟩; l' V = Some v'';
P ⊢ T casts v to v' ⟧
⟹ P,E ⊢ ⟨{V:T := Val v; e}, (h,l)⟩ → ⟨{V:T := Val v''; e'}, (h',l'(V := l V))⟩"

| RedBlock:
"P,E ⊢ ⟨{V:T; Val u}, s⟩ → ⟨Val u, s⟩"

| RedInitBlock:
"P ⊢ T casts v to v' ⟹ P,E ⊢ ⟨{V:T := Val v; Val u}, s⟩ → ⟨Val u, s⟩"

| SeqRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e;;e⇩2, s⟩ → ⟨e';;e⇩2, s'⟩"

| RedSeq:
"P,E ⊢ ⟨(Val v);;e⇩2, s⟩ → ⟨e⇩2, s⟩"

| CondRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⟩ → ⟨if (e') e⇩1 else e⇩2, s'⟩"

| RedCondT:
"P,E ⊢ ⟨if (true) e⇩1 else e⇩2, s⟩ → ⟨e⇩1, s⟩"

| RedCondF:
"P,E ⊢ ⟨if (false) e⇩1 else e⇩2, s⟩ → ⟨e⇩2, s⟩"

| RedWhile:
"P,E ⊢ ⟨while(b) c, s⟩ → ⟨if(b) (c;;while(b) c) else unit, s⟩"

| ThrowRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨throw e, s⟩ → ⟨throw e', s'⟩"

| RedThrowNull:
"P,E ⊢ ⟨throw null, s⟩ → ⟨THROW NullPointer, s⟩"

| ListRed1:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e#es,s⟩ [→] ⟨e'#es,s'⟩"

| ListRed2:
"P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ⟹
P,E ⊢ ⟨Val v # es,s⟩ [→] ⟨Val v # es',s'⟩"

― ‹Exception propagation›

| DynCastThrow: "P,E ⊢ ⟨Cast C (Throw r), s⟩ → ⟨Throw r, s⟩"
| StaticCastThrow: "P,E ⊢ ⟨⦇C⦈(Throw r), s⟩ → ⟨Throw r, s⟩"
| BinOpThrow1: "P,E ⊢ ⟨(Throw r) «bop» e⇩2, s⟩ → ⟨Throw r, s⟩"
| BinOpThrow2: "P,E ⊢ ⟨(Val v⇩1) «bop» (Throw r), s⟩ → ⟨Throw r, s⟩"
| LAssThrow: "P,E ⊢ ⟨V:=(Throw r), s⟩ → ⟨Throw r, s⟩"
| FAccThrow: "P,E ⊢ ⟨(Throw r)∙F{Cs}, s⟩ → ⟨Throw r, s⟩"
| FAssThrow1: "P,E ⊢ ⟨(Throw r)∙F{Cs}:=e⇩2, s⟩ → ⟨Throw r,s⟩"
| FAssThrow2: "P,E ⊢ ⟨Val v∙F{Cs}:=(Throw r), s⟩ → ⟨Throw r, s⟩"
| CallThrowObj: "P,E ⊢ ⟨Call (Throw r) Copt M es, s⟩ → ⟨Throw r, s⟩"
| CallThrowParams: "⟦ es = map Val vs @ Throw r # es' ⟧
⟹ P,E ⊢ ⟨Call (Val v) Copt M es, s⟩ → ⟨Throw r, s⟩"
| BlockThrow: "P,E ⊢ ⟨{V:T; Throw r}, s⟩ → ⟨Throw r, s⟩"
| InitBlockThrow: "P ⊢ T casts v to v'
⟹ P,E ⊢ ⟨{V:T := Val v; Throw r}, s⟩ → ⟨Throw r, s⟩"
| SeqThrow: "P,E ⊢ ⟨(Throw r);;e⇩2, s⟩ → ⟨Throw r, s⟩"
| CondThrow: "P,E ⊢ ⟨if (Throw r) e⇩1 else e⇩2, s⟩ → ⟨Throw r, s⟩"
| ThrowThrow: "P,E ⊢ ⟨throw(Throw r), s⟩ → ⟨Throw r, s⟩"

lemmas red_reds_induct = red_reds.induct [split_format (complete)]
and red_reds_inducts = red_reds.inducts [split_format (complete)]

inductive_cases [elim!]:
"P,E ⊢ ⟨V:=e,s⟩ → ⟨e',s'⟩"
"P,E ⊢ ⟨e1;;e2,s⟩ → ⟨e',s'⟩"

declare Cons_eq_map_conv [iff]

lemma "P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹ True"
and reds_length:"P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ⟹ length es = length es'"
by (induct rule: red_reds.inducts) auto

subsection‹The reflexive transitive closure›

definition Red :: "prog ⇒ env ⇒ ((expr × state) × (expr × state)) set"
where "Red P E = {((e,s),e',s'). P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩}"

definition Reds :: "prog ⇒ env ⇒ ((expr list × state) × (expr list × state)) set"
where "Reds P E = {((es,s),es',s'). P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩}"

lemma[simp]: "((e,s),e',s') ∈ Red P E = P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩"

lemma[simp]: "((es,s),es',s') ∈ Reds P E = P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩"

abbreviation
Step :: "prog ⇒ env ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) →*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81) where
"P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ≡ ((e,s), e',s') ∈ (Red P E)⇧*"

abbreviation
Steps :: "prog ⇒ env ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) [→]*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81) where
"P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩ ≡ ((es,s), es',s') ∈ (Reds P E)⇧*"

lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P,E ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩"
and "⋀e h l. R e h l e h l"
and "⋀e⇩0 h⇩0 l⇩0 e⇩1 h⇩1 l⇩1 e' h' l'.
⟦ P,E ⊢ ⟨e⇩0,(h⇩0,l⇩0)⟩ → ⟨e⇩1,(h⇩1,l⇩1)⟩; R e⇩1 h⇩1 l⇩1 e' h' l' ⟧ ⟹ R e⇩0 h⇩0 l⇩0 e' h' l'"
shows "R e h l e' h' l'"

proof -
{ fix s s'
assume reds: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
and base: "⋀e s. R e (hp s) (lcl s) e (hp s) (lcl s)"
and IH: "⋀e⇩0 s⇩0 e⇩1 s⇩1 e' s'.
⟦ P,E ⊢ ⟨e⇩0,s⇩0⟩ → ⟨e⇩1,s⇩1⟩; R e⇩1 (hp s⇩1) (lcl s⇩1) e' (hp s') (lcl s') ⟧
⟹ R e⇩0 (hp s⇩0) (lcl s⇩0) e' (hp s') (lcl s')"
from reds have "R e (hp s) (lcl s) e' (hp s') (lcl s')"
proof (induct rule:converse_rtrancl_induct2)
case refl show ?case by(rule base)
next
case (step e⇩0 s⇩0 e s)
have Red:"((e⇩0,s⇩0),e,s) ∈ Red P E"
and R:"R e (hp s) (lcl s) e' (hp s') (lcl s')" by fact+
from IH[OF Red[simplified] R] show ?case .
qed
}
with assms show ?thesis by fastforce
qed

lemma steps_length:"P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩ ⟹ length es = length es'"
by(induct rule:rtrancl_induct2,auto intro:reds_length)

subsection‹Some easy lemmas›

lemma [iff]: "¬ P,E ⊢ ⟨[],s⟩ [→] ⟨es',s'⟩"
by(blast elim: reds.cases)

lemma [iff]: "¬ P,E ⊢ ⟨Val v,s⟩ → ⟨e',s'⟩"
by(fastforce elim: red.cases)

lemma [iff]: "¬ P,E ⊢ ⟨Throw r,s⟩ → ⟨e',s'⟩"
by(fastforce elim: red.cases)

lemma red_lcl_incr: "P,E ⊢ ⟨e,(h⇩0,l⇩0)⟩ → ⟨e',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
and "P,E ⊢ ⟨es,(h⇩0,l⇩0)⟩ [→] ⟨es',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
by (induct rule: red_reds_inducts) (auto simp del:fun_upd_apply)

lemma red_lcl_add: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀l⇩0. P,E ⊢ ⟨e,(h,l⇩0++l)⟩ → ⟨e',(h',l⇩0++l')⟩)"
and "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀l⇩0. P,E ⊢ ⟨es,(h,l⇩0++l)⟩ [→] ⟨es',(h',l⇩0++l')⟩)"

proof (induct rule:red_reds_inducts)
case RedLAss thus ?case by(auto intro:red_reds.intros simp del:fun_upd_apply)
next
case RedStaticDownCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedStaticUpDynCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedStaticDownDynCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedDynCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedDynCastFail thus ?case by(fastforce intro:red_reds.intros)
next
case RedFAcc thus ?case by(fastforce intro:red_reds.intros)
next
case RedFAss thus ?case by (fastforce intro:red_reds.intros)
next
case RedCall thus ?case by (fastforce intro!:red_reds.RedCall)
next
case RedStaticCall thus ?case by(fastforce intro:red_reds.intros)
next
case (InitBlockRed E V T e h l v' e' h' l' v'' v l⇩0)
have IH: "⋀l⇩0. P,E(V ↦ T) ⊢ ⟨e,(h, l⇩0 ++ l(V ↦ v'))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = Some v''" and casts:"P ⊢ T casts v to v'" by fact+
from IH have IH': "P,E(V ↦ T) ⊢ ⟨e,(h, (l⇩0 ++ l)(V ↦ v'))⟩ → ⟨e',(h',l⇩0 ++ l')⟩"
by simp
have "(l⇩0 ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.InitBlockRed[OF IH' _ casts] l'V show ?case
by(simp del:fun_upd_apply)
next
case (BlockRedNone E V T e h l e' h' l' l⇩0)
have IH: "⋀l⇩0. P,E(V ↦ T) ⊢ ⟨e,(h, l⇩0 ++ l(V := None))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = None" and unass: "¬ assigned V e" by fact+
have "l⇩0(V := None) ++ l(V := None) = (l⇩0 ++ l)(V := None)"
hence IH': "P,E(V ↦ T) ⊢ ⟨e,(h, (l⇩0++l)(V := None))⟩ → ⟨e',(h', l⇩0(V := None) ++ l')⟩"
using IH[of "l⇩0(V := None)"] by simp
have "(l⇩0(V := None) ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
next
case (BlockRedSome E V T e h l e' h' l' v l⇩0)
have IH: "⋀l⇩0. P,E(V ↦ T) ⊢ ⟨e,(h, l⇩0 ++ l(V := None))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = Some v" and unass: "¬ assigned V e" by fact+
have "l⇩0(V := None) ++ l(V := None) = (l⇩0 ++ l)(V := None)"
hence IH': "P,E(V ↦ T) ⊢ ⟨e,(h, (l⇩0++l)(V := None))⟩ → ⟨e',(h', l⇩0(V := None) ++ l')⟩"
using IH[of "l⇩0(V := None)"] by simp
have "(l⇩0(V := None) ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
next

assumes "P,E ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩" shows "P,E ⊢ ⟨e,(h,l⇩0++l)⟩ →* ⟨e',(h',l⇩0++l')⟩"
using assms
proof(induct rule:converse_rtrancl_induct_red)
case 1 thus ?case by simp
next
case 2 thus ?case
by(auto dest: red_lcl_add intro: converse_rtrancl_into_rtrancl simp:Red_def)
qed

lemma
red_preserves_obj:"⟦P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩; h a = Some(D,S)⟧
⟹ ∃S'. h' a = Some(D,S')"
and reds_preserves_obj:"⟦P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩; h a = Some(D,S)⟧
⟹ ∃S'. h' a = Some(D,S')"

end


# Theory SystemClasses

(*  Title:       CoreC++
Author:      Gerwin Klein
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹System Classes›

theory SystemClasses imports Exceptions begin

text ‹
This theory provides definitions for the system exceptions.
›

definition NullPointerC :: "cdecl" where
"NullPointerC ≡ (NullPointer, ([],[],[]))"

definition ClassCastC :: "cdecl" where
"ClassCastC ≡ (ClassCast, ([],[],[]))"

definition OutOfMemoryC :: "cdecl" where
"OutOfMemoryC ≡ (OutOfMemory, ([],[],[]))"

definition SystemClasses :: "cdecl list" where
"SystemClasses ≡ [NullPointerC, ClassCastC, OutOfMemoryC]"

end


# Theory TypeRel

(*  Title:       CoreC++

Author:      Tobias Nipkow, Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Extracted from the Jinja theory Common/TypeRel.thy by Tobias Nipkow
*)

section ‹The subtype relation›

theory TypeRel imports SubObj begin

inductive
widen   :: "prog ⇒ ty ⇒ ty ⇒ bool" ("_ ⊢ _ ≤ _"   [71,71,71] 70)
for P :: prog
where
widen_refl[iff]: "P ⊢ T ≤ T"
| widen_subcls:    "P ⊢ Path C to D unique ⟹ P ⊢ Class C ≤ Class D"
| widen_null[iff]: "P ⊢ NT ≤ Class C"

abbreviation
widens :: "prog ⇒ ty list ⇒ ty list ⇒ bool"
("_ ⊢ _ [≤] _" [71,71,71] 70) where
"widens P Ts Ts' ≡ list_all2 (widen P) Ts Ts'"

inductive_simps [iff]:
"P ⊢ T ≤ Void"
"P ⊢ T ≤ Boolean"
"P ⊢ T ≤ Integer"
"P ⊢ Void ≤ T"
"P ⊢ Boolean ≤ T"
"P ⊢ Integer ≤ T"
"P ⊢ T ≤ NT"

lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl] for P
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P

end


# Theory WellType

(*  Title:       CoreC++

Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Well-typedness of CoreC++ expressions›

theory WellType imports Syntax TypeRel begin

subsection ‹The rules›

inductive
WT :: "[prog,env,expr     ,ty     ] ⇒ bool"
("_,_ ⊢ _ :: _"   [51,51,51]50)
and WTs :: "[prog,env,expr list,ty list] ⇒ bool"
("_,_ ⊢ _ [::] _" [51,51,51]50)
for P :: prog
where

WTNew:
"is_class P C ⟹
P,E ⊢ new C :: Class C"

| WTDynCast: (* not more than one path between classes *)
"⟦P,E ⊢ e :: Class D; is_class P C;
P ⊢ Path D to C unique ∨ (∀Cs. ¬ P ⊢ Path D to C via Cs)⟧
⟹ P,E ⊢ Cast C e :: Class C"

| WTStaticCast:
"⟦P,E ⊢ e :: Class D; is_class P C;
P ⊢ Path D to C unique ∨
(P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs)) ⟧
⟹ P,E ⊢ ⦇C⦈e :: Class C"

| WTVal:
"typeof v = Some T ⟹
P,E ⊢ Val v :: T"

| WTVar:
"E V = Some T ⟹
P,E ⊢ Var V :: T"

| WTBinOp:
"⟦ P,E ⊢ e⇩1 :: T⇩1;  P,E ⊢ e⇩2 :: T⇩2;
case bop of Eq ⇒ T⇩1 = T⇩2 ∧ T = Boolean
| Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer ⟧
⟹ P,E ⊢ e⇩1 «bop» e⇩2 :: T"

| WTLAss:
"⟦ E V = Some T;  P,E ⊢ e :: T'; P ⊢ T' ≤ T⟧
⟹ P,E ⊢ V:=e :: T"

| WTFAcc:
"⟦ P,E ⊢ e :: Class C;  P ⊢ C has least F:T via Cs⟧
⟹ P,E ⊢ e∙F{Cs} :: T"

| WTFAss:
"⟦ P,E ⊢ e⇩1 :: Class C;  P ⊢ C has least F:T via Cs;
P,E ⊢ e⇩2 :: T'; P ⊢ T' ≤ T⟧
⟹ P,E ⊢ e⇩1∙F{Cs}:=e⇩2 :: T"

| WTStaticCall:
"⟦ P,E ⊢ e :: Class C'; P ⊢ Path C' to C unique;
P ⊢ C has least M = (Ts,T,m) via Cs; P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E ⊢ e∙(C::)M(es) :: T"

| WTCall:
"⟦ P,E ⊢ e :: Class C;  P ⊢ C has least M = (Ts,T,m) via Cs;
P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E ⊢ e∙M(es) :: T"

| WTBlock:
"⟦ is_type P T;  P,E(V ↦ T) ⊢ e :: T' ⟧
⟹  P,E ⊢ {V:T; e} :: T'"

| WTSeq:
"⟦ P,E ⊢ e⇩1::T⇩1;  P,E ⊢ e⇩2::T⇩2 ⟧
⟹  P,E ⊢ e⇩1;;e⇩2 :: T⇩2"

| WTCond:
"⟦ P,E ⊢ e :: Boolean;  P,E ⊢ e⇩1::T;  P,E ⊢ e⇩2::T ⟧
⟹ P,E ⊢ if (e) e⇩1 else e⇩2 :: T"

| WTWhile:
"⟦ P,E ⊢ e :: Boolean;  P,E ⊢ c::T ⟧
⟹ P,E ⊢ while (e) c :: Void"

| WTThrow:
"P,E ⊢ e :: Class C  ⟹
P,E ⊢ throw e :: Void"

― ‹well-typed expression lists›

| WTNil:
"P,E ⊢ [] [::] []"

| WTCons:
"⟦ P,E ⊢ e :: T;  P,E ⊢ es [::] Ts ⟧
⟹  P,E ⊢ e#es [::] T#Ts"

declare WT_WTs.intros[intro!] WTNil[iff]

lemmas WT_WTs_induct = WT_WTs.induct [split_format (complete)]
and WT_WTs_inducts = WT_WTs.inducts [split_format (complete)]

subsection‹Easy consequences›

lemma [iff]: "(P,E ⊢ [] [::] Ts) = (Ts = [])"

apply(rule iffI)
apply (auto elim: WTs.cases)
done

lemma [iff]: "(P,E ⊢ e#es [::] T#Ts) = (P,E ⊢ e :: T ∧ P,E ⊢ es [::] Ts)"

apply(rule iffI)
apply (auto elim: WTs.cases)
done

lemma [iff]: "(P,E ⊢ (e#es) [::] Ts) =
(∃U Us. Ts = U#Us ∧ P,E ⊢ e :: U ∧ P,E ⊢ es [::] Us)"

apply(rule iffI)
apply (auto elim: WTs.cases)
done

lemma [iff]: "⋀Ts. (P,E ⊢ es⇩1 @ es⇩2 [::] Ts) =
(∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ P,E ⊢ es⇩1 [::] Ts⇩1 ∧ P,E ⊢ es⇩2[::]Ts⇩2)"

apply(induct es⇩1 type:list)
apply simp
apply clarsimp
apply(erule thin_rl)
apply (rule iffI)
apply clarsimp
apply(rule exI)+
apply(rule conjI)
prefer 2 apply blast
apply simp
apply fastforce
done

lemma [iff]: "P,E ⊢ Val v :: T = (typeof v = Some T)"

apply(rule iffI)
apply (auto elim: WT.cases)
done

lemma [iff]: "P,E ⊢ Var V :: T = (E V = Some T)"

apply(rule iffI)
apply (auto elim: WT.cases)
done

lemma [iff]: "P,E ⊢ e⇩1;;e⇩2 :: T⇩2 = (∃T⇩1. P,E ⊢ e⇩1::T⇩1 ∧ P,E ⊢ e⇩2::T⇩2)"

apply(rule iffI)
apply (auto elim: WT.cases)
done

lemma [iff]: "(P,E ⊢ {V:T; e} :: T') = (is_type P T ∧ P,E(V↦T) ⊢ e :: T')"

apply(rule iffI)
apply (auto elim: WT.cases)
done

inductive_cases WT_elim_cases[elim!]:
"P,E ⊢ new C :: T"
"P,E ⊢ Cast C e :: T"
"P,E ⊢ ⦇C⦈e :: T"
"P,E ⊢ e⇩1 «bop» e⇩2 :: T"
"P,E ⊢ V:= e :: T"
"P,E ⊢ e∙F{Cs} :: T"
"P,E ⊢ e∙F{Cs} := v :: T"
"P,E ⊢ e∙M(ps) :: T"
"P,E ⊢ e∙(C::)M(ps) :: T"
"P,E ⊢ if (e) e⇩1 else e⇩2 :: T"
"P,E ⊢ while (e) c :: T"
"P,E ⊢ throw e :: T"

lemma wt_env_mono:
"P,E ⊢ e :: T ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E' ⊢ e :: T)" and
"P,E ⊢ es [::] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E' ⊢ es [::] Ts)"

apply(induct rule: WT_WTs_inducts)
apply(fastforce simp: WTDynCast)
apply(fastforce simp: WTStaticCast)
apply(fastforce simp: WTVal)
apply(fastforce simp: WTBinOp)
apply(force simp:map_le_def)
apply(fastforce simp: WTFAcc)
apply(fastforce simp: WTFAss)
apply(fastforce simp: WTCall)
apply(fastforce simp: WTStaticCall)
apply(fastforce simp: map_le_def WTBlock)
apply(fastforce simp: WTSeq)
apply(fastforce simp: WTCond)
apply(fastforce simp: WTWhile)
apply(fastforce simp: WTThrow)
done

lemma WT_fv: "P,E ⊢ e :: T ⟹ fv e ⊆ dom E"
and "P,E ⊢ es [::] Ts ⟹ fvs es ⊆ dom E"

apply(induct rule:WT_WTs.inducts)
apply(simp_all del: fun_upd_apply)
apply fast+
done

end


# Theory WellForm

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/WellForm.thy by Tobias Nipkow
*)

section ‹Generic Well-formedness of programs›

theory WellForm
imports SystemClasses TypeRel WellType
begin

text ‹\noindent This theory defines global well-formedness conditions
for programs but does not look inside method bodies. Well-typing of
expressions is defined elsewhere (in theory ‹WellType›).

CoreC++ allows covariant return types›

type_synonym wf_mdecl_test = "prog ⇒ cname ⇒ mdecl ⇒ bool"

definition wf_fdecl :: "prog ⇒ fdecl ⇒ bool" where
"wf_fdecl P ≡ λ(F,T). is_type P T"

definition wf_mdecl :: "wf_mdecl_test ⇒ wf_mdecl_test" where
"wf_mdecl wf_md P C ≡ λ(M,Ts,T,mb).
(∀T∈set Ts. is_type P T) ∧ is_type P T ∧ T ≠ NT ∧ wf_md P C (M,Ts,T,mb)"

definition wf_cdecl :: "wf_mdecl_test ⇒ prog ⇒ cdecl ⇒ bool" where
"wf_cdecl wf_md P  ≡  λ(C,(Bs,fs,ms)).
(∀M mthd Cs. P ⊢ C has M = mthd via Cs ⟶
(∃mthd' Cs'. P ⊢ (C,Cs) has overrider M = mthd' via Cs')) ∧
(∀f∈set fs. wf_fdecl P f) ∧  distinct_fst fs ∧
(∀m∈set ms. wf_mdecl wf_md P C m) ∧  distinct_fst ms ∧
(∀D ∈ baseClasses Bs.
is_class P D ∧ ¬ P ⊢ D ≼⇧* C ∧
(∀(M,Ts,T,m)∈set ms.
∀Ts' T' m' Cs. P ⊢ D has M = (Ts',T',m') via Cs ⟶
Ts' = Ts ∧ P ⊢ T ≤ T'))"

definition wf_syscls :: "prog ⇒ bool" where
"wf_syscls P  ≡  sys_xcpts ⊆ set(map fst P)"

definition wf_prog :: "wf_mdecl_test ⇒ prog ⇒ bool" where
"wf_prog wf_md P ≡ wf_syscls P ∧ distinct_fst P ∧
(∀c ∈ set P. wf_cdecl wf_md P c)"

subsection‹Well-formedness lemmas›

lemma class_wf:
"⟦class P C = Some c; wf_prog wf_md P⟧ ⟹ wf_cdecl wf_md P (C,c)"

apply (unfold wf_prog_def class_def)
apply (fast dest: map_of_SomeD)
done

lemma is_class_xcpt:
"⟦ C ∈ sys_xcpts; wf_prog wf_md P ⟧ ⟹ is_class P C"

apply (simp add: wf_prog_def wf_syscls_def is_class_def class_def)
apply (fastforce intro!: map_of_SomeI)
done

lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms) ∈ set P" and "(M,Ts,T,m) ∈ set ms"
shows "set Ts ⊆ types P"
proof
from assms have "wf_mdecl wf_md P C (M,Ts,T,m)"
by (unfold wf_prog_def wf_cdecl_def) auto
hence "∀t ∈ set Ts. is_type P t" by (unfold wf_mdecl_def) auto
moreover fix t assume "t ∈ set Ts"
ultimately have "is_type P t" by blast
thus "t ∈ types P" ..
qed

subsection‹Well-formedness subclass lemmas›

lemma subcls1_wfD:
"⟦ P ⊢ C ≺⇧1 D; wf_prog wf_md P ⟧ ⟹ D ≠ C ∧ (D,C) ∉ (subcls1 P)⇧+"

apply( frule r_into_trancl)
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def baseClasses_def)
apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
done

lemma wf_cdecl_supD:
"⟦wf_cdecl wf_md P (C,Bs,r); D ∈ baseClasses Bs⟧ ⟹ is_class P D"
by (auto simp: wf_cdecl_def baseClasses_def)

lemma subcls_asym:
"⟦ wf_prog wf_md P; (C,D) ∈ (subcls1 P)⇧+ ⟧ ⟹ (D,C) ∉ (subcls1 P)⇧+"

apply(erule trancl.cases)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: trancl_trans)
done

lemma subcls_irrefl:
"⟦ wf_prog wf_md P; (C,D) ∈ (subcls1 P)⇧+ ⟧ ⟹ C ≠ D"

apply (erule trancl_trans_induct)
apply  (auto dest: subcls1_wfD subcls_asym)
done

lemma subcls_asym2:
"⟦ (C,D) ∈ (subcls1 P)⇧*; wf_prog wf_md P; (D,C) ∈ (subcls1 P)⇧* ⟧ ⟹ C = D"

apply (induct rule:rtrancl.induct)
apply simp
apply (drule rtrancl_into_trancl1)
apply simp
apply (drule subcls_asym)
apply simp
apply(drule rtranclD)
apply simp
done

lemma acyclic_subcls1:
"wf_prog wf_md P ⟹ acyclic (subcls1 P)"

apply (unfold acyclic_def)
apply (fast dest: subcls_irrefl)
done

lemma wf_subcls1:
"wf_prog wf_md P ⟹ wf ((subcls1 P)¯)"

apply (rule finite_acyclic_wf_converse)
apply (rule finite_subcls1)
apply (erule acyclic_subcls1)
done

lemma subcls_induct:
"⟦ wf_prog wf_md P; ⋀C. ∀D. (C,D) ∈ (subcls1 P)⇧+ ⟶ Q D ⟹ Q C ⟧ ⟹ Q C"

(is "?A ⟹ PROP ?P ⟹ _")

proof -
assume p: "PROP ?P"
assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
apply(drule wf_trancl)
apply(simp only: trancl_converse)
apply(erule_tac a = C in wf_induct)
apply(rule p)
apply(auto)
done
qed

subsection‹Well-formedness leq\_path lemmas›

lemma last_leq_path:
assumes leq:"P,C ⊢ Cs ⊏⇧1 Ds" and wf:"wf_prog wf_md P"
shows "P ⊢ last Cs ≺⇧1 last Ds"

using leq
proof (induct rule:leq_path1.induct)
fix Cs Ds assume suboCs:"Subobjs P C Cs" and suboDs:"Subobjs P C Ds"
and butlast:"Cs = butlast Ds"
from suboDs have notempty:"Ds ≠ []" by -(drule Subobjs_nonempty)
with butlast have DsCs:"Ds = Cs @ [last Ds]" by simp
from suboCs have notempty:"Cs ≠ []" by -(drule Subobjs_nonempty)
with DsCs have "Ds = ((butlast Cs) @ [last Cs]) @ [last Ds]" by simp
with suboDs have "Subobjs P C ((butlast Cs) @ [last Cs,last Ds])"
by simp
thus "P ⊢ last Cs ≺⇧1 last Ds" by (fastforce intro:subclsR_subcls1 Subobjs_subclsR)
next
fix Cs D assume "P ⊢ last Cs ≺⇩S D"
thus "P ⊢ last Cs ≺⇧1 last [D]" by (fastforce intro:subclsS_subcls1)
qed

lemma last_leq_paths:
assumes leq:"(Cs,Ds) ∈ (leq_path1 P C)⇧+" and wf:"wf_prog wf_md P"
shows "(last Cs,last Ds) ∈ (subcls1 P)⇧+"

using leq
proof (induct rule:trancl.induct)
fix Cs Ds assume "P,C ⊢ Cs ⊏⇧1 Ds"
thus "(last Cs, last Ds) ∈ (subcls1 P)⇧+" using wf
by (fastforce intro:r_into_trancl elim:last_leq_path)
next
fix Cs Cs' Ds assume "(last Cs, last Cs') ∈ (subcls1 P)⇧+"
and "P,C ⊢ Cs' ⊏⇧1 Ds"
thus "(last Cs, last Ds) ∈ (subcls1 P)⇧+" using wf
by (fastforce dest:last_leq_path)
qed

lemma leq_path1_wfD:
"⟦ P,C ⊢ Cs ⊏⇧1 Cs'; wf_prog wf_md P ⟧ ⟹ Cs ≠ Cs' ∧ (Cs',Cs) ∉ (leq_path1 P C)⇧+"

apply (rule conjI)
apply (erule leq_path1.cases)
apply simp
apply (drule_tac Cs="Ds" in Subobjs_nonempty)
apply (rule butlast_noteq) apply assumption
apply clarsimp
apply (drule subclsS_subcls1)
apply (drule subcls1_wfD) apply simp_all
apply clarsimp
apply (frule last_leq_path)
apply simp
apply (drule last_leq_paths)
apply simp
apply (drule_tac r="subcls1 P" in r_into_trancl)
apply (drule subcls_asym)
apply auto
done

lemma leq_path_asym:
"⟦(Cs,Cs') ∈ (leq_path1 P C)⇧+; wf_prog wf_md P⟧ ⟹ (Cs',Cs) ∉ (leq_path1 P C)⇧+"

apply(erule tranclE)
apply(fast dest!:leq_path1_wfD )
apply(fast dest!:leq_path1_wfD intro: trancl_trans)
done

lemma leq_path_asym2:"⟦P,C ⊢ Cs ⊑ Cs'; P,C ⊢ Cs' ⊑ Cs; wf_prog wf_md P⟧ ⟹ Cs = Cs'"

apply (induct rule:rtrancl.induct)
apply simp
apply (drule rtrancl_into_trancl1)
apply simp
apply (drule leq_path_asym)
apply simp
apply (drule_tac a="c" and b="a" in rtranclD)
apply simp
done

lemma leq_path_Subobjs:
"⟦P,C ⊢ [C] ⊑ Cs; is_class P C; wf_prog wf_md P⟧ ⟹ Subobjs P C Cs"
by (induct rule:rtrancl_induct,auto intro:Subobjs_Base elim!:leq_path1.cases,
auto dest!:Subobjs_subclass intro!:Subobjs_Sh SubobjsR_Base dest!:subclsSD
intro:wf_cdecl_supD class_wf ShBaseclass_isBaseclass subclsSI)

subsection‹Lemmas concerning Subobjs›

lemma Subobj_last_isClass:"⟦wf_prog wf_md P; Subobjs P C Cs⟧ ⟹ is_class P (last Cs)"

apply (frule Subobjs_isClass)
apply (drule Subobjs_subclass)
apply (drule rtranclD)
apply (erule disjE)
apply simp
apply clarsimp
apply (erule trancl_induct)
apply (fastforce dest:subcls1D class_wf elim:wf_cdecl_supD)
apply (fastforce dest:subcls1D class_wf elim:wf_cdecl_supD)
done

lemma converse_SubobjsR_Rep:
"⟦Subobjs⇩R P C Cs; P ⊢ last Cs ≺⇩R C'; wf_prog wf_md P⟧
⟹ Subobjs⇩R P C (Cs@[C'])"

apply (induct rule:Subobjs⇩R.induct)
apply (frule subclsR_subcls1)
apply (fastforce dest!:subcls1D class_wf wf_cdecl_supD SubobjsR_Base SubobjsR_Rep)
apply (fastforce elim:SubobjsR_Rep simp: SubobjsR_nonempty split:if_split_asm)
done

lemma converse_Subobjs_Rep:
"⟦Subobjs P C Cs; P ⊢ last Cs ≺⇩R C';  wf_prog wf_md P⟧
⟹ Subobjs P C (Cs@[C'])"
by (induct rule:Subobjs.induct, fastforce dest:converse_SubobjsR_Rep Subobjs_Rep,
fastforce dest:converse_SubobjsR_Rep Subobjs_Sh)

lemma isSubobj_Subobjs_rev:
assumes subo:"is_subobj P ((C,C'#rev Cs'))" and wf:"wf_prog wf_md P"
shows "Subobjs P C (C'#rev Cs')"
using subo
proof (induct Cs')
case Nil
show ?case
proof (cases "C=C'")
case True
have "is_subobj P ((C,C'#rev []))" by fact
with True have "is_subobj P ((C,[C]))" by simp
hence "is_class P C"
by (fastforce elim:converse_rtranclE dest:subclsS_subcls1 elim:subcls1_class)
with True show ?thesis by (fastforce intro:Subobjs_Base)
next
case False
have "is_subobj P ((C,C'#rev []))" by fact
with False obtain D where sup:"P ⊢ C ≼⇧* D" and subS:"P ⊢ D ≺⇩S C'"
by fastforce
with wf have "is_class P C'"
by (fastforce dest:subclsS_subcls1 subcls1D class_wf elim:wf_cdecl_supD)
hence "Subobjs⇩R P C' [C']" by (fastforce elim:SubobjsR_Base)
with sup subS have "Subobjs P C [C']" by -(erule Subobjs_Sh, simp)
thus ?thesis by simp
qed
next
case (Cons C'' Cs'')
have IH:"is_subobj P ((C,C'#rev Cs'')) ⟹ Subobjs P C (C'#rev Cs'')"
and subo:"is_subobj P ((C,C'#rev(C''# Cs'')))" by fact+
obtain Ds' where Ds':"Ds' = rev Cs''" by simp
obtain D Ds where DDs:"D#Ds = Ds'@[C'']" by (cases Ds') auto
with Ds' subo have "is_subobj P ((C,C'#D#Ds))" by simp
hence subobl:"is_subobj P ((C,butlast(C'#D#Ds)))"
and subRbl:"P ⊢ last(butlast(C'#D#Ds)) ≺⇩R last(C'#D#Ds)" by simp+
with DDs Ds' have "is_subobj P ((C,C'#rev Cs''))" by (simp del: is_subobj.simps)
with IH have suborev:"Subobjs P C (C'#rev Cs'')" by simp
from subRbl DDs Ds' have subR:"P ⊢ last(C'#rev Cs'') ≺⇩R C''" by simp
with suborev wf show ?case by (fastforce dest:converse_Subobjs_Rep)
qed

lemma isSubobj_Subobjs:
assumes subo:"is_subobj P ((C,Cs))" and wf:"wf_prog wf_md P"
shows "Subobjs P C Cs"

using subo
proof (induct Cs)
case Nil
thus ?case by simp
next
case (Cons C' Cs')
have subo:"is_subobj P ((C,C'#Cs'))" by fact
obtain Cs'' where Cs'':"Cs'' = rev Cs'" by simp
with subo have "is_subobj P ((C,C'#rev Cs''))" by simp
with wf have "Subobjs P C (C'#rev Cs'')" by - (rule isSubobj_Subobjs_rev)
with Cs'' show ?case by simp
qed

lemma isSubobj_eq_Subobjs:
"wf_prog wf_md P ⟹ is_subobj P ((C,Cs)) = (Subobjs P C Cs)"
by(auto elim:isSubobj_Subobjs Subobjs_isSubobj)

lemma subo_trans_subcls:
assumes subo:"Subobjs P C (Cs@ C'#rev Cs')"
shows "∀C'' ∈ set Cs'. (C',C'') ∈ (subcls1 P)⇧+"

using subo
proof (induct Cs')
case Nil
thus ?case by simp
next
case (Cons D Ds)
have IH:"Subobjs P C (Cs @ C' # rev Ds) ⟹
∀C''∈set Ds. (C', C'') ∈ (subcls1 P)⇧+"
and "Subobjs P C (Cs @ C' # rev (D # Ds))" by fact+
hence subo':"Subobjs P C (Cs@ C'#rev Ds @ [D])" by simp
hence "Subobjs P C (Cs@ C'#rev Ds)"
by -(rule appendSubobj,simp_all)
with IH have set:"∀C''∈set Ds. (C', C'') ∈ (subcls1 P)⇧+" by simp
hence revset:"∀C''∈set (rev Ds). (C', C'') ∈ (subcls1 P)⇧+" by simp
have "(C',D) ∈ (subcls1 P)⇧+"
proof (cases "Ds = []")
case True
with subo' have "Subobjs P C (Cs@[C',D])" by simp
thus ?thesis
by (fastforce intro: subclsR_subcls1 Subobjs_subclsR)
next
case False
with revset have hd:"(C',hd Ds) ∈ (subcls1 P)⇧+"
apply -
apply (erule ballE)
apply simp
apply</