src/HOL/NanoJava/State.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 67443 3abf6a722518
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/NanoJava/State.thy
     2     Author:     David von Oheimb
     3     Copyright   2001 Technische Universitaet Muenchen
     4 *)
     5 
     6 section "Program State"
     7 
     8 theory State imports TypeRel begin
     9 
    10 definition body :: "cname \<times> mname => stmt" where
    11  "body \<equiv> \<lambda>(C,m). bdy (the (method C m))"
    12 
    13 text \<open>Locations, i.e.\ abstract references to objects\<close>
    14 typedecl loc 
    15 
    16 datatype val
    17   = Null        \<comment>\<open>null reference\<close>
    18   | Addr loc    \<comment>\<open>address, i.e. location of object\<close>
    19 
    20 type_synonym fields
    21         = "(fname \<rightharpoonup> val)"
    22 
    23 type_synonym
    24         obj = "cname \<times> fields"
    25 
    26 translations
    27   (type) "fields" \<leftharpoondown> (type) "fname => val option"
    28   (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"
    29 
    30 definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
    31  "init_vars m == map_option (\<lambda>T. Null) o m"
    32   
    33 text \<open>private:\<close>
    34 type_synonym heap = "loc   \<rightharpoonup> obj"
    35 type_synonym locals = "vname \<rightharpoonup> val"  
    36 
    37 text \<open>private:\<close>
    38 record  state
    39         = heap   :: heap
    40           locals :: locals
    41 
    42 translations
    43   (type) "heap" \<leftharpoondown> (type) "loc => obj option"
    44   (type) "locals" \<leftharpoondown> (type) "vname => val option"
    45   (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
    46 
    47 definition del_locs :: "state => state" where
    48  "del_locs s \<equiv> s (| locals := empty |)"
    49 
    50 definition init_locs     :: "cname => mname => state => state" where
    51  "init_locs C m s \<equiv> s (| locals := locals s ++ 
    52                          init_vars (map_of (lcl (the (method C m)))) |)"
    53 
    54 text \<open>The first parameter of @{term set_locs} is of type @{typ state} 
    55         rather than @{typ locals} in order to keep @{typ locals} private.\<close>
    56 definition set_locs :: "state => state => state" where
    57  "set_locs s s' \<equiv> s' (| locals := locals s |)"
    58 
    59 definition get_local     :: "state => vname => val" ("_<_>" [99,0] 99) where
    60  "get_local s x  \<equiv> the (locals s x)"
    61 
    62 \<comment>\<open>local function:\<close>
    63 definition get_obj       :: "state => loc => obj" where
    64  "get_obj s a \<equiv> the (heap s a)"
    65 
    66 definition obj_class     :: "state => loc => cname" where
    67  "obj_class s a \<equiv> fst (get_obj s a)"
    68 
    69 definition get_field     :: "state => loc => fname => val" where
    70  "get_field s a f \<equiv> the (snd (get_obj s a) f)"
    71 
    72 \<comment>\<open>local function:\<close>
    73 definition hupd       :: "loc => obj => state => state"   ("hupd'(_\<mapsto>_')" [10,10] 1000) where
    74  "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
    75 
    76 definition lupd       :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000) where
    77  "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
    78 
    79 definition new_obj :: "loc => cname => state => state" where
    80  "new_obj a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
    81 
    82 definition upd_obj    :: "loc => fname => val => state => state" where
    83  "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"
    84 
    85 definition new_Addr      :: "state => val" where
    86  "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"
    87 
    88 
    89 subsection "Properties not used in the meta theory"
    90 
    91 lemma locals_upd_id [simp]: "s\<lparr>locals := locals s\<rparr> = s" 
    92 by simp
    93 
    94 lemma lupd_get_local_same [simp]: "lupd(x\<mapsto>v) s<x> = v"
    95 by (simp add: lupd_def get_local_def)
    96 
    97 lemma lupd_get_local_other [simp]: "x \<noteq> y \<Longrightarrow> lupd(x\<mapsto>v) s<y> = s<y>"
    98 apply (drule not_sym)
    99 by (simp add: lupd_def get_local_def)
   100 
   101 lemma get_field_lupd [simp]:
   102   "get_field (lupd(x\<mapsto>y) s) a f = get_field s a f"
   103 by (simp add: lupd_def get_field_def get_obj_def)
   104 
   105 lemma get_field_set_locs [simp]:
   106   "get_field (set_locs l s) a f = get_field s a f"
   107 by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
   108 
   109 lemma get_field_del_locs [simp]:
   110   "get_field (del_locs s) a f = get_field s a f"
   111 by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
   112 
   113 lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>"
   114 by (simp add: new_obj_def hupd_def get_local_def)
   115 
   116 lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s"
   117 by (simp add: lupd_def)
   118 
   119 lemma heap_hupd_same [simp]: "heap (hupd(a\<mapsto>obj) s) a = Some obj"
   120 by (simp add: hupd_def)
   121 
   122 lemma heap_hupd_other [simp]: "aa \<noteq> a  \<Longrightarrow> heap (hupd(aa\<mapsto>obj) s) a = heap s a"
   123 apply (drule not_sym)
   124 by (simp add: hupd_def)
   125 
   126 lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s"
   127 by (simp add: hupd_def)
   128 
   129 lemma heap_del_locs [simp]: "heap (del_locs s) = heap s"
   130 by (simp add: del_locs_def)
   131 
   132 lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s"
   133 by (simp add: set_locs_def)
   134 
   135 lemma hupd_lupd [simp]: 
   136   "hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)"
   137 by (simp add: hupd_def lupd_def)
   138 
   139 lemma hupd_del_locs [simp]: 
   140   "hupd(a\<mapsto>obj) (del_locs s) = del_locs (hupd(a\<mapsto>obj) s)"
   141 by (simp add: hupd_def del_locs_def)
   142 
   143 lemma new_obj_lupd [simp]: 
   144   "new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (new_obj a C s)"
   145 by (simp add: new_obj_def)
   146 
   147 lemma new_obj_del_locs [simp]: 
   148   "new_obj a C (del_locs s) = del_locs (new_obj a C s)"
   149 by (simp add: new_obj_def)
   150 
   151 lemma upd_obj_lupd [simp]: 
   152   "upd_obj a f v (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (upd_obj a f v s)"
   153 by (simp add: upd_obj_def Let_def split_beta)
   154 
   155 lemma upd_obj_del_locs [simp]: 
   156   "upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)"
   157 by (simp add: upd_obj_def Let_def split_beta)
   158 
   159 lemma get_field_hupd_same [simp]:
   160  "get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs"
   161 apply (rule ext)
   162 by (simp add: get_field_def get_obj_def)
   163 
   164 lemma get_field_hupd_other [simp]:
   165  "aa \<noteq> a  \<Longrightarrow> get_field (hupd(aa\<mapsto>obj) s) a = get_field s a"
   166 apply (rule ext)
   167 by (simp add: get_field_def get_obj_def)
   168 
   169 lemma new_AddrD: 
   170 "new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null"
   171 apply (unfold new_Addr_def)
   172 apply (erule subst)
   173 apply (rule someI)
   174 apply (rule disjI2)
   175 apply (rule HOL.refl)
   176 done
   177 
   178 end