src/HOL/IMP/OO.thy
author kleing
Mon Jun 06 16:29:38 2011 +0200 (2011-06-06)
changeset 43158 686fa0a0696e
child 47818 151d137f1095
permissions -rw-r--r--
imported rest of new IMP
     1 theory OO imports Main begin
     2 
     3 subsection "Towards an OO Language: A Language of Records"
     4 
     5 (* FIXME: move to HOL/Fun *)
     6 abbreviation fun_upd2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
     7   ("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
     8 where "f(x,y := z) == f(x := (f x)(y := z))"
     9 
    10 type_synonym addr = nat
    11 datatype ref = null | Ref addr
    12 
    13 type_synonym obj = "string \<Rightarrow> ref"
    14 type_synonym venv = "string \<Rightarrow> ref"
    15 type_synonym store = "addr \<Rightarrow> obj"
    16 
    17 datatype exp =
    18   Null |
    19   New |
    20   V string |
    21   Faccess exp string       ("_\<bullet>/_" [63,1000] 63) |
    22   Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
    23   Fassign exp string exp   ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
    24   Mcall exp string exp     ("(_\<bullet>/_<_>)" [63,0,0] 63) |
    25   Semi exp exp             ("_;/ _" [61,60] 60) |
    26   If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
    27 and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
    28 
    29 type_synonym menv = "string \<Rightarrow> exp"
    30 type_synonym config = "venv \<times> store \<times> addr"
    31 
    32 inductive
    33   big_step :: "menv \<Rightarrow> exp \<times> config \<Rightarrow> ref \<times> config \<Rightarrow> bool"
    34     ("(_ \<turnstile>/ (_/ \<Rightarrow> _))" [60,0,60] 55) and
    35   bval ::  "menv \<Rightarrow> bexp \<times> config \<Rightarrow> bool \<times> config \<Rightarrow> bool"
    36     ("_ \<turnstile> _ \<rightarrow> _" [60,0,60] 55)
    37 where
    38 Null:
    39 "me \<turnstile> (Null,c) \<Rightarrow> (null,c)" |
    40 New:
    41 "me \<turnstile> (New,ve,s,n) \<Rightarrow> (Ref n,ve,s(n := (\<lambda>f. null)),n+1)" |
    42 Vaccess:
    43 "me \<turnstile> (V x,ve,sn) \<Rightarrow> (ve x,ve,sn)" |
    44 Faccess:
    45 "me \<turnstile> (e,c) \<Rightarrow> (Ref a,ve',s',n') \<Longrightarrow>
    46  me \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" |
    47 Vassign:
    48 "me \<turnstile> (e,c) \<Rightarrow> (r,ve',sn') \<Longrightarrow>
    49  me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" |
    50 Fassign:
    51 "\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (Ref a,c\<^isub>2);  me \<turnstile> (e,c\<^isub>2) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3,n\<^isub>3) \<rbrakk> \<Longrightarrow>
    52  me \<turnstile> (oe\<bullet>f ::= e,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3(a,f := r),n\<^isub>3)" |
    53 Mcall:
    54 "\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (or,c\<^isub>2);  me \<turnstile> (pe,c\<^isub>2) \<Rightarrow> (pr,ve\<^isub>3,sn\<^isub>3);
    55    ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
    56    me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
    57   \<Longrightarrow>
    58  me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
    59 Semi:
    60 "\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
    61  me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
    62 IfTrue:
    63 "\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (True,c\<^isub>2);  me \<turnstile> (e\<^isub>1,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
    64  me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
    65 IfFalse:
    66 "\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (False,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
    67  me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
    68 
    69 "me \<turnstile> (B bv,c) \<rightarrow> (bv,c)" |
    70 
    71 "me \<turnstile> (b,c\<^isub>1) \<rightarrow> (bv,c\<^isub>2) \<Longrightarrow> me \<turnstile> (Not b,c\<^isub>1) \<rightarrow> (\<not>bv,c\<^isub>2)" |
    72 
    73 "\<lbrakk> me \<turnstile> (b\<^isub>1,c\<^isub>1) \<rightarrow> (bv\<^isub>1,c\<^isub>2);  me \<turnstile> (b\<^isub>2,c\<^isub>2) \<rightarrow> (bv\<^isub>2,c\<^isub>3) \<rbrakk> \<Longrightarrow>
    74  me \<turnstile> (And b\<^isub>1 b\<^isub>2,c\<^isub>1) \<rightarrow> (bv\<^isub>1\<and>bv\<^isub>2,c\<^isub>3)" |
    75 
    76 "\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r\<^isub>1,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> (r\<^isub>2,c\<^isub>3) \<rbrakk> \<Longrightarrow>
    77  me \<turnstile> (Eq e\<^isub>1 e\<^isub>2,c\<^isub>1) \<rightarrow> (r\<^isub>1=r\<^isub>2,c\<^isub>3)"
    78 
    79 
    80 code_pred (modes: i => i => o => bool) big_step .
    81 
    82 text{* Example: natural numbers encoded as objects with a predecessor
    83 field. Null is zero. Method succ adds an object in front, method add
    84 adds as many objects in front as the parameter specifies.
    85 
    86 First, the method bodies: *}
    87 
    88 definition
    89 "m_succ  =  (''s'' ::= New)\<bullet>''pred'' ::= V ''this''; V ''s''"
    90 
    91 definition "m_add =
    92   IF Eq (V ''param'') Null
    93   THEN V ''this''
    94   ELSE V ''this''\<bullet>''succ''<Null>\<bullet>''add''<V ''param''\<bullet>''pred''>"
    95 
    96 text{* The method environment: *}
    97 definition
    98 "menv = (\<lambda>m. Null)(''succ'' := m_succ, ''add'' := m_add)"
    99 
   100 text{* The main code, adding 1 and 2: *}
   101 definition "main =
   102   ''1'' ::= Null\<bullet>''succ''<Null>;
   103   ''2'' ::= V ''1''\<bullet>''succ''<Null>;
   104   V ''2'' \<bullet> ''add'' <V ''1''>"
   105 
   106 text{* Execution of semantics. The final variable environment and store are
   107 converted into lists of references based on given lists of variable and field
   108 names to extract. *}
   109 
   110 values
   111  "{(r, map ve' [''1'',''2''], map (\<lambda>n. map (s' n)[''pred'']) [0..<n])|
   112     r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}"
   113 
   114 end