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