src/HOL/Imperative_HOL/Ref.thy
changeset 37797 96551d6b1414
parent 37792 ba0bc31b90d7
parent 37796 08bd610b2583
child 37802 f2e9c104cebd
equal deleted inserted replaced
37794:46c21c1f8cb0 37797:96551d6b1414
   148   shows "crel (ref v) h h' r"
   148   shows "crel (ref v) h h' r"
   149   by (rule crelI) (insert assms, simp add: execute_simps)
   149   by (rule crelI) (insert assms, simp add: execute_simps)
   150 
   150 
   151 lemma crel_refE [crel_elims]:
   151 lemma crel_refE [crel_elims]:
   152   assumes "crel (ref v) h h' r"
   152   assumes "crel (ref v) h h' r"
   153   obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
   153   obtains "get h' r = v" and "present h' r" and "\<not> present h r"
   154   using assms by (rule crelE) (simp add: execute_simps)
   154   using assms by (rule crelE) (simp add: execute_simps)
   155 
   155 
   156 lemma execute_lookup [execute_simps]:
   156 lemma execute_lookup [execute_simps]:
   157   "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
   157   "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
   158   by (simp add: lookup_def execute_simps)
   158   by (simp add: lookup_def execute_simps)
   160 lemma success_lookupI [success_intros]:
   160 lemma success_lookupI [success_intros]:
   161   "success (lookup r) h"
   161   "success (lookup r) h"
   162   by (auto intro: success_intros  simp add: lookup_def)
   162   by (auto intro: success_intros  simp add: lookup_def)
   163 
   163 
   164 lemma crel_lookupI [crel_intros]:
   164 lemma crel_lookupI [crel_intros]:
   165   assumes "h' = h" "x = Ref.get h r"
   165   assumes "h' = h" "x = get h r"
   166   shows "crel (!r) h h' x"
   166   shows "crel (!r) h h' x"
   167   by (rule crelI) (insert assms, simp add: execute_simps)
   167   by (rule crelI) (insert assms, simp add: execute_simps)
   168 
   168 
   169 lemma crel_lookupE [crel_elims]:
   169 lemma crel_lookupE [crel_elims]:
   170   assumes "crel (!r) h h' x"
   170   assumes "crel (!r) h h' x"
   171   obtains "h' = h" "x = Ref.get h r"
   171   obtains "h' = h" "x = get h r"
   172   using assms by (rule crelE) (simp add: execute_simps)
   172   using assms by (rule crelE) (simp add: execute_simps)
   173 
   173 
   174 lemma execute_update [execute_simps]:
   174 lemma execute_update [execute_simps]:
   175   "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
   175   "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
   176   by (simp add: update_def execute_simps)
   176   by (simp add: update_def execute_simps)
   178 lemma success_updateI [success_intros]:
   178 lemma success_updateI [success_intros]:
   179   "success (update r v) h"
   179   "success (update r v) h"
   180   by (auto intro: success_intros  simp add: update_def)
   180   by (auto intro: success_intros  simp add: update_def)
   181 
   181 
   182 lemma crel_updateI [crel_intros]:
   182 lemma crel_updateI [crel_intros]:
   183   assumes "h' = Ref.set r v h"
   183   assumes "h' = set r v h"
   184   shows "crel (r := v) h h' x"
   184   shows "crel (r := v) h h' x"
   185   by (rule crelI) (insert assms, simp add: execute_simps)
   185   by (rule crelI) (insert assms, simp add: execute_simps)
   186 
   186 
   187 lemma crel_updateE [crel_elims]:
   187 lemma crel_updateE [crel_elims]:
   188   assumes "crel (r' := v) h h' r"
   188   assumes "crel (r' := v) h h' r"
   189   obtains "h' = Ref.set r' v h"
   189   obtains "h' = set r' v h"
   190   using assms by (rule crelE) (simp add: execute_simps)
   190   using assms by (rule crelE) (simp add: execute_simps)
   191 
   191 
   192 lemma execute_change [execute_simps]:
   192 lemma execute_change [execute_simps]:
   193   "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
   193   "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
   194   by (simp add: change_def bind_def Let_def execute_simps)
   194   by (simp add: change_def bind_def Let_def execute_simps)
   196 lemma success_changeI [success_intros]:
   196 lemma success_changeI [success_intros]:
   197   "success (change f r) h"
   197   "success (change f r) h"
   198   by (auto intro!: success_intros crel_intros simp add: change_def)
   198   by (auto intro!: success_intros crel_intros simp add: change_def)
   199 
   199 
   200 lemma crel_changeI [crel_intros]: 
   200 lemma crel_changeI [crel_intros]: 
   201   assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
   201   assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
   202   shows "crel (Ref.change f r) h h' x"
   202   shows "crel (change f r) h h' x"
   203   by (rule crelI) (insert assms, simp add: execute_simps)  
   203   by (rule crelI) (insert assms, simp add: execute_simps)  
   204 
   204 
   205 lemma crel_changeE [crel_elims]:
   205 lemma crel_changeE [crel_elims]:
   206   assumes "crel (Ref.change f r') h h' r"
   206   assumes "crel (change f r') h h' r"
   207   obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
   207   obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
   208   using assms by (rule crelE) (simp add: execute_simps)
   208   using assms by (rule crelE) (simp add: execute_simps)
   209 
   209 
   210 lemma lookup_chain:
   210 lemma lookup_chain:
   211   "(!r \<guillemotright> f) = f"
   211   "(!r \<guillemotright> f) = f"
   212   by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
   212   by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
   224 
   224 
   225 lemma nth_set [simp]:
   225 lemma nth_set [simp]:
   226   "get_array a (set r v h) ! i = get_array a h ! i"
   226   "get_array a (set r v h) ! i = get_array a h ! i"
   227   by simp
   227   by simp
   228 
   228 
   229 lemma get_change [simp]:
   229 lemma get_update [simp]:
   230   "get (Array.change a i v h) r  = get h r"
   230   "get (Array.update a i v h) r  = get h r"
   231   by (simp add: get_def Array.change_def set_array_def)
   231   by (simp add: get_def Array.update_def set_array_def)
   232 
   232 
   233 lemma alloc_change:
   233 lemma alloc_update:
   234   "fst (alloc v (Array.change a i v' h)) = fst (alloc v h)"
   234   "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
   235   by (simp add: Array.change_def get_array_def set_array_def alloc_def Let_def)
   235   by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
   236 
   236 
   237 lemma change_set_swap:
   237 lemma update_set_swap:
   238   "Array.change a i v (set r v' h) = set r v' (Array.change a i v h)"
   238   "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
   239   by (simp add: Array.change_def get_array_def set_array_def set_def)
   239   by (simp add: Array.update_def get_array_def set_array_def set_def)
   240 
   240 
   241 lemma length_alloc [simp]: 
   241 lemma length_alloc [simp]: 
   242   "Array.length a (snd (alloc v h)) = Array.length a h"
   242   "Array.length a (snd (alloc v h)) = Array.length a h"
   243   by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
   243   by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
   244 
   244 
   245 lemma get_array_alloc [simp]: 
   245 lemma get_array_alloc [simp]: 
   246   "get_array a (snd (alloc v h)) = get_array a h"
   246   "get_array a (snd (alloc v h)) = get_array a h"
   247   by (simp add: get_array_def alloc_def set_def Let_def)
   247   by (simp add: get_array_def alloc_def set_def Let_def)
   248 
   248 
   249 lemma present_change [simp]: 
   249 lemma present_update [simp]: 
   250   "present (Array.change a i v h) = present h"
   250   "present (Array.update a i v h) = present h"
   251   by (simp add: Array.change_def set_array_def expand_fun_eq present_def)
   251   by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
   252 
   252 
   253 lemma array_present_set [simp]:
   253 lemma array_present_set [simp]:
   254   "array_present a (set r v h) = array_present a h"
   254   "array_present a (set r v h) = array_present a h"
   255   by (simp add: array_present_def set_def)
   255   by (simp add: array_present_def set_def)
   256 
   256 
   260 
   260 
   261 lemma set_array_set_swap:
   261 lemma set_array_set_swap:
   262   "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
   262   "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
   263   by (simp add: set_array_def set_def)
   263   by (simp add: set_array_def set_def)
   264 
   264 
   265 hide_const (open) present get set alloc lookup update change
   265 hide_const (open) present get set alloc noteq lookup update change
   266 
   266 
   267 
   267 
   268 subsection {* Code generator setup *}
   268 subsection {* Code generator setup *}
   269 
   269 
   270 text {* SML *}
   270 text {* SML *}