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))"

type_synonym addr = nat
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"
("(_ \<turnstile>/ (_/ => _))" [60,0,60] 55) and
bval :: "menv => bexp × config => bool × config => bool"
("_ \<turnstile> _ -> _" [60,0,60] 55)
where
Null:
"me \<turnstile> (Null,c) => (null,c)" |
New:
"me \<turnstile> (New,ve,s,n) => (Ref n,ve,s(n := (λf. null)),n+1)" |
Vaccess:
"me \<turnstile> (V x,ve,sn) => (ve x,ve,sn)" |
Faccess:
"me \<turnstile> (e,c) => (Ref a,ve',s',n') ==>
me \<turnstile> (e•f,c) => (s' a f,ve',s',n')"
|
Vassign:
"me \<turnstile> (e,c) => (r,ve',sn') ==>
me \<turnstile> (x ::= e,c) => (r,ve'(x:=r),sn')"
|
Fassign:
"[| me \<turnstile> (oe,c1) => (Ref a,c2); me \<turnstile> (e,c2) => (r,ve3,s3,n3) |] ==>
me \<turnstile> (oe•f ::= e,c1) => (r,ve3,s3(a,f := r),n3)"
|
Mcall:
"[| me \<turnstile> (oe,c1) => (or,c2); me \<turnstile> (pe,c2) => (pr,ve3,sn3);
ve = (λx. null)(''this'' := or, ''param'' := pr);
me \<turnstile> (me m,ve,sn3) => (r,ve',sn4) |]
==>
me \<turnstile> (oe•m<pe>,c1) => (r,ve3,sn4)"
|
Seq:
"[| me \<turnstile> (e1,c1) => (r,c2); me \<turnstile> (e2,c2) => c3 |] ==>
me \<turnstile> (e1; e2,c1) => c3"
|
IfTrue:
"[| me \<turnstile> (b,c1) -> (True,c2); me \<turnstile> (e1,c2) => c3 |] ==>
me \<turnstile> (IF b THEN e1 ELSE e2,c1) => c3"
|
IfFalse:
"[| me \<turnstile> (b,c1) -> (False,c2); me \<turnstile> (e2,c2) => c3 |] ==>
me \<turnstile> (IF b THEN e1 ELSE e2,c1) => c3"
|

"me \<turnstile> (B bv,c) -> (bv,c)" |

"me \<turnstile> (b,c1) -> (bv,c2) ==> me \<turnstile> (Not b,c1) -> (¬bv,c2)" |

"[| me \<turnstile> (b1,c1) -> (bv1,c2); me \<turnstile> (b2,c2) -> (bv2,c3) |] ==>
me \<turnstile> (And b1 b2,c1) -> (bv1∧bv2,c3)"
|

"[| me \<turnstile> (e1,c1) => (r1,c2); me \<turnstile> (e2,c2) => (r2,c3) |] ==>
me \<turnstile> (Eq e1 e2,c1) -> (r1=r2,c3)"



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''"

definition "m_add =
IF Eq (V ''param'') Null
THEN V ''this''
ELSE V ''this''•''succ''<Null>•''add''<V ''param''•''pred''>"


text{* The method environment: *}
definition
"menv = (λm. Null)(''succ'' := m_succ, ''add'' := m_add)"

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 \<turnstile> (main, λx. null, nth[], 0) => (r,ve',s',n)}"


end