Quelle  OO.thy

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"
    (‹(_ ⊨/ (_/ ==> _))› [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,c🪙1) ==> (r,ve🪙3,sn🪙4)" for or |
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''"

definition "m_add =
  IF Eq (V ''param'') Null
  THEN V ''this''
  ELSE V ''this''∙''succ''∙''add''∙''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'';
  ''2'' ::= V ''1''∙''succ'';
  V ''2'' ∙ ''add'' "

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

end