Theory OO

theory OO
imports Main
```theory OO imports Main begin

subsection "Towards an OO Language: A Language of Records"

(* FIXME: move to HOL/Fun *)
abbreviation fun_upd2 :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a ⇒ 'b ⇒ 'c ⇒ 'a ⇒ 'b ⇒ 'c"
("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
where "f(x,y := z) == f(x := (f x)(y := z))"

datatype ref = null | Ref addr

type_synonym obj = "string ⇒ ref"
type_synonym venv = "string ⇒ ref"
type_synonym store = "addr ⇒ obj"

datatype exp =
Null |
New |
V string |
Faccess exp string       ("_∙/_" [63,1000] 63) |
Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
Fassign exp string exp   ("(_∙_ ::=/ _)" [63,0,62] 62) |
Mcall exp string exp     ("(_∙/_<_>)" [63,0,0] 63) |
Seq exp exp              ("_;/ _" [61,60] 60) |
If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp

type_synonym menv = "string ⇒ exp"
type_synonym config = "venv × store × addr"

inductive
big_step :: "menv ⇒ exp × config ⇒ ref × config ⇒ bool"
("(_ ⊢/ (_/ ⇒ _))" [60,0,60] 55) and
bval ::  "menv ⇒ bexp × config ⇒ bool × config ⇒ bool"
("_ ⊢ _ → _" [60,0,60] 55)
where
Null:
"me ⊢ (Null,c) ⇒ (null,c)" |
New:
"me ⊢ (New,ve,s,n) ⇒ (Ref n,ve,s(n := (λf. null)),n+1)" |
Vaccess:
"me ⊢ (V x,ve,sn) ⇒ (ve x,ve,sn)" |
Faccess:
"me ⊢ (e,c) ⇒ (Ref a,ve',s',n') ⟹
me ⊢ (e∙f,c) ⇒ (s' a f,ve',s',n')" |
Vassign:
"me ⊢ (e,c) ⇒ (r,ve',sn') ⟹
me ⊢ (x ::= e,c) ⇒ (r,ve'(x:=r),sn')" |
Fassign:
"⟦ me ⊢ (oe,c⇩1) ⇒ (Ref a,c⇩2);  me ⊢ (e,c⇩2) ⇒ (r,ve⇩3,s⇩3,n⇩3) ⟧ ⟹
me ⊢ (oe∙f ::= e,c⇩1) ⇒ (r,ve⇩3,s⇩3(a,f := r),n⇩3)" |
Mcall:
"⟦ me ⊢ (oe,c⇩1) ⇒ (or,c⇩2);  me ⊢ (pe,c⇩2) ⇒ (pr,ve⇩3,sn⇩3);
ve = (λx. null)(''this'' := or, ''param'' := pr);
me ⊢ (me m,ve,sn⇩3) ⇒ (r,ve',sn⇩4) ⟧
⟹
me ⊢ (oe∙m<pe>,c⇩1) ⇒ (r,ve⇩3,sn⇩4)" |
Seq:
"⟦ me ⊢ (e⇩1,c⇩1) ⇒ (r,c⇩2);  me ⊢ (e⇩2,c⇩2) ⇒ c⇩3 ⟧ ⟹
me ⊢ (e⇩1; e⇩2,c⇩1) ⇒ c⇩3" |
IfTrue:
"⟦ me ⊢ (b,c⇩1) → (True,c⇩2);  me ⊢ (e⇩1,c⇩2) ⇒ c⇩3 ⟧ ⟹
me ⊢ (IF b THEN e⇩1 ELSE e⇩2,c⇩1) ⇒ c⇩3" |
IfFalse:
"⟦ me ⊢ (b,c⇩1) → (False,c⇩2);  me ⊢ (e⇩2,c⇩2) ⇒ c⇩3 ⟧ ⟹
me ⊢ (IF b THEN e⇩1 ELSE e⇩2,c⇩1) ⇒ c⇩3" |

"me ⊢ (B bv,c) → (bv,c)" |

"me ⊢ (b,c⇩1) → (bv,c⇩2) ⟹ me ⊢ (Not b,c⇩1) → (¬bv,c⇩2)" |

"⟦ me ⊢ (b⇩1,c⇩1) → (bv⇩1,c⇩2);  me ⊢ (b⇩2,c⇩2) → (bv⇩2,c⇩3) ⟧ ⟹
me ⊢ (And b⇩1 b⇩2,c⇩1) → (bv⇩1∧bv⇩2,c⇩3)" |

"⟦ me ⊢ (e⇩1,c⇩1) ⇒ (r⇩1,c⇩2);  me ⊢ (e⇩2,c⇩2) ⇒ (r⇩2,c⇩3) ⟧ ⟹
me ⊢ (Eq e⇩1 e⇩2,c⇩1) → (r⇩1=r⇩2,c⇩3)"

code_pred (modes: i => i => o => bool) big_step .

text{* Example: natural numbers encoded as objects with a predecessor
field. Null is zero. Method succ adds an object in front, method add
adds as many objects in front as the parameter specifies.

First, the method bodies: *}

definition
"m_succ  =  (''s'' ::= New)∙''pred'' ::= V ''this''; V ''s''"

IF Eq (V ''param'') Null
THEN V ''this''

text{* The method environment: *}
definition

text{* The main code, adding 1 and 2: *}
definition "main =
''1'' ::= Null∙''succ''<Null>;
''2'' ::= V ''1''∙''succ''<Null>;
V ''2'' ∙ ''add'' <V ''1''>"

text{* Execution of semantics. The final variable environment and store are
converted into lists of references based on given lists of variable and field
names to extract. *}

values
"{(r, map ve' [''1'',''2''], map (λn. map (s' n)[''pred'']) [0..<n])|
r ve' s' n. menv ⊢ (main, λx. null, nth[], 0) ⇒ (r,ve',s',n)}"

end
```