src/HOL/IMP/OO.thy
changeset 43158 686fa0a0696e
child 47818 151d137f1095
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/OO.thy	Mon Jun 06 16:29:38 2011 +0200
     1.3 @@ -0,0 +1,114 @@
     1.4 +theory OO imports Main begin
     1.5 +
     1.6 +subsection "Towards an OO Language: A Language of Records"
     1.7 +
     1.8 +(* FIXME: move to HOL/Fun *)
     1.9 +abbreviation fun_upd2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
    1.10 +  ("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
    1.11 +where "f(x,y := z) == f(x := (f x)(y := z))"
    1.12 +
    1.13 +type_synonym addr = nat
    1.14 +datatype ref = null | Ref addr
    1.15 +
    1.16 +type_synonym obj = "string \<Rightarrow> ref"
    1.17 +type_synonym venv = "string \<Rightarrow> ref"
    1.18 +type_synonym store = "addr \<Rightarrow> obj"
    1.19 +
    1.20 +datatype exp =
    1.21 +  Null |
    1.22 +  New |
    1.23 +  V string |
    1.24 +  Faccess exp string       ("_\<bullet>/_" [63,1000] 63) |
    1.25 +  Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
    1.26 +  Fassign exp string exp   ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
    1.27 +  Mcall exp string exp     ("(_\<bullet>/_<_>)" [63,0,0] 63) |
    1.28 +  Semi exp exp             ("_;/ _" [61,60] 60) |
    1.29 +  If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
    1.30 +and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
    1.31 +
    1.32 +type_synonym menv = "string \<Rightarrow> exp"
    1.33 +type_synonym config = "venv \<times> store \<times> addr"
    1.34 +
    1.35 +inductive
    1.36 +  big_step :: "menv \<Rightarrow> exp \<times> config \<Rightarrow> ref \<times> config \<Rightarrow> bool"
    1.37 +    ("(_ \<turnstile>/ (_/ \<Rightarrow> _))" [60,0,60] 55) and
    1.38 +  bval ::  "menv \<Rightarrow> bexp \<times> config \<Rightarrow> bool \<times> config \<Rightarrow> bool"
    1.39 +    ("_ \<turnstile> _ \<rightarrow> _" [60,0,60] 55)
    1.40 +where
    1.41 +Null:
    1.42 +"me \<turnstile> (Null,c) \<Rightarrow> (null,c)" |
    1.43 +New:
    1.44 +"me \<turnstile> (New,ve,s,n) \<Rightarrow> (Ref n,ve,s(n := (\<lambda>f. null)),n+1)" |
    1.45 +Vaccess:
    1.46 +"me \<turnstile> (V x,ve,sn) \<Rightarrow> (ve x,ve,sn)" |
    1.47 +Faccess:
    1.48 +"me \<turnstile> (e,c) \<Rightarrow> (Ref a,ve',s',n') \<Longrightarrow>
    1.49 + me \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" |
    1.50 +Vassign:
    1.51 +"me \<turnstile> (e,c) \<Rightarrow> (r,ve',sn') \<Longrightarrow>
    1.52 + me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" |
    1.53 +Fassign:
    1.54 +"\<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>
    1.55 + me \<turnstile> (oe\<bullet>f ::= e,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3(a,f := r),n\<^isub>3)" |
    1.56 +Mcall:
    1.57 +"\<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);
    1.58 +   ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
    1.59 +   me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
    1.60 +  \<Longrightarrow>
    1.61 + me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
    1.62 +Semi:
    1.63 +"\<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>
    1.64 + me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
    1.65 +IfTrue:
    1.66 +"\<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>
    1.67 + me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
    1.68 +IfFalse:
    1.69 +"\<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>
    1.70 + me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
    1.71 +
    1.72 +"me \<turnstile> (B bv,c) \<rightarrow> (bv,c)" |
    1.73 +
    1.74 +"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)" |
    1.75 +
    1.76 +"\<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>
    1.77 + me \<turnstile> (And b\<^isub>1 b\<^isub>2,c\<^isub>1) \<rightarrow> (bv\<^isub>1\<and>bv\<^isub>2,c\<^isub>3)" |
    1.78 +
    1.79 +"\<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>
    1.80 + me \<turnstile> (Eq e\<^isub>1 e\<^isub>2,c\<^isub>1) \<rightarrow> (r\<^isub>1=r\<^isub>2,c\<^isub>3)"
    1.81 +
    1.82 +
    1.83 +code_pred (modes: i => i => o => bool) big_step .
    1.84 +
    1.85 +text{* Example: natural numbers encoded as objects with a predecessor
    1.86 +field. Null is zero. Method succ adds an object in front, method add
    1.87 +adds as many objects in front as the parameter specifies.
    1.88 +
    1.89 +First, the method bodies: *}
    1.90 +
    1.91 +definition
    1.92 +"m_succ  =  (''s'' ::= New)\<bullet>''pred'' ::= V ''this''; V ''s''"
    1.93 +
    1.94 +definition "m_add =
    1.95 +  IF Eq (V ''param'') Null
    1.96 +  THEN V ''this''
    1.97 +  ELSE V ''this''\<bullet>''succ''<Null>\<bullet>''add''<V ''param''\<bullet>''pred''>"
    1.98 +
    1.99 +text{* The method environment: *}
   1.100 +definition
   1.101 +"menv = (\<lambda>m. Null)(''succ'' := m_succ, ''add'' := m_add)"
   1.102 +
   1.103 +text{* The main code, adding 1 and 2: *}
   1.104 +definition "main =
   1.105 +  ''1'' ::= Null\<bullet>''succ''<Null>;
   1.106 +  ''2'' ::= V ''1''\<bullet>''succ''<Null>;
   1.107 +  V ''2'' \<bullet> ''add'' <V ''1''>"
   1.108 +
   1.109 +text{* Execution of semantics. The final variable environment and store are
   1.110 +converted into lists of references based on given lists of variable and field
   1.111 +names to extract. *}
   1.112 +
   1.113 +values
   1.114 + "{(r, map ve' [''1'',''2''], map (\<lambda>n. map (s' n)[''pred'']) [0..<n])|
   1.115 +    r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}"
   1.116 +
   1.117 +end