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