merged
authorhaftmann
Tue Jul 13 12:05:20 2010 +0200 (2010-07-13 ago)
changeset 3779796551d6b1414
parent 37794 46c21c1f8cb0
parent 37796 08bd610b2583
child 37798 0b0570445a2a
merged
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:01:12 2010 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 12:05:20 2010 +0200
     2.3 @@ -150,7 +150,7 @@
     2.4  
     2.5  lemma crel_refE [crel_elims]:
     2.6    assumes "crel (ref v) h h' r"
     2.7 -  obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
     2.8 +  obtains "get h' r = v" and "present h' r" and "\<not> present h r"
     2.9    using assms by (rule crelE) (simp add: execute_simps)
    2.10  
    2.11  lemma execute_lookup [execute_simps]:
    2.12 @@ -162,13 +162,13 @@
    2.13    by (auto intro: success_intros  simp add: lookup_def)
    2.14  
    2.15  lemma crel_lookupI [crel_intros]:
    2.16 -  assumes "h' = h" "x = Ref.get h r"
    2.17 +  assumes "h' = h" "x = get h r"
    2.18    shows "crel (!r) h h' x"
    2.19    by (rule crelI) (insert assms, simp add: execute_simps)
    2.20  
    2.21  lemma crel_lookupE [crel_elims]:
    2.22    assumes "crel (!r) h h' x"
    2.23 -  obtains "h' = h" "x = Ref.get h r"
    2.24 +  obtains "h' = h" "x = get h r"
    2.25    using assms by (rule crelE) (simp add: execute_simps)
    2.26  
    2.27  lemma execute_update [execute_simps]:
    2.28 @@ -180,13 +180,13 @@
    2.29    by (auto intro: success_intros  simp add: update_def)
    2.30  
    2.31  lemma crel_updateI [crel_intros]:
    2.32 -  assumes "h' = Ref.set r v h"
    2.33 +  assumes "h' = set r v h"
    2.34    shows "crel (r := v) h h' x"
    2.35    by (rule crelI) (insert assms, simp add: execute_simps)
    2.36  
    2.37  lemma crel_updateE [crel_elims]:
    2.38    assumes "crel (r' := v) h h' r"
    2.39 -  obtains "h' = Ref.set r' v h"
    2.40 +  obtains "h' = set r' v h"
    2.41    using assms by (rule crelE) (simp add: execute_simps)
    2.42  
    2.43  lemma execute_change [execute_simps]:
    2.44 @@ -198,13 +198,13 @@
    2.45    by (auto intro!: success_intros crel_intros simp add: change_def)
    2.46  
    2.47  lemma crel_changeI [crel_intros]: 
    2.48 -  assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
    2.49 -  shows "crel (Ref.change f r) h h' x"
    2.50 +  assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
    2.51 +  shows "crel (change f r) h h' x"
    2.52    by (rule crelI) (insert assms, simp add: execute_simps)  
    2.53  
    2.54  lemma crel_changeE [crel_elims]:
    2.55 -  assumes "crel (Ref.change f r') h h' r"
    2.56 -  obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
    2.57 +  assumes "crel (change f r') h h' r"
    2.58 +  obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
    2.59    using assms by (rule crelE) (simp add: execute_simps)
    2.60  
    2.61  lemma lookup_chain:
    2.62 @@ -226,17 +226,17 @@
    2.63    "get_array a (set r v h) ! i = get_array a h ! i"
    2.64    by simp
    2.65  
    2.66 -lemma get_change [simp]:
    2.67 -  "get (Array.change a i v h) r  = get h r"
    2.68 -  by (simp add: get_def Array.change_def set_array_def)
    2.69 +lemma get_update [simp]:
    2.70 +  "get (Array.update a i v h) r  = get h r"
    2.71 +  by (simp add: get_def Array.update_def set_array_def)
    2.72  
    2.73 -lemma alloc_change:
    2.74 -  "fst (alloc v (Array.change a i v' h)) = fst (alloc v h)"
    2.75 -  by (simp add: Array.change_def get_array_def set_array_def alloc_def Let_def)
    2.76 +lemma alloc_update:
    2.77 +  "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
    2.78 +  by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
    2.79  
    2.80 -lemma change_set_swap:
    2.81 -  "Array.change a i v (set r v' h) = set r v' (Array.change a i v h)"
    2.82 -  by (simp add: Array.change_def get_array_def set_array_def set_def)
    2.83 +lemma update_set_swap:
    2.84 +  "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
    2.85 +  by (simp add: Array.update_def get_array_def set_array_def set_def)
    2.86  
    2.87  lemma length_alloc [simp]: 
    2.88    "Array.length a (snd (alloc v h)) = Array.length a h"
    2.89 @@ -246,9 +246,9 @@
    2.90    "get_array a (snd (alloc v h)) = get_array a h"
    2.91    by (simp add: get_array_def alloc_def set_def Let_def)
    2.92  
    2.93 -lemma present_change [simp]: 
    2.94 -  "present (Array.change a i v h) = present h"
    2.95 -  by (simp add: Array.change_def set_array_def expand_fun_eq present_def)
    2.96 +lemma present_update [simp]: 
    2.97 +  "present (Array.update a i v h) = present h"
    2.98 +  by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
    2.99  
   2.100  lemma array_present_set [simp]:
   2.101    "array_present a (set r v h) = array_present a h"
   2.102 @@ -262,7 +262,7 @@
   2.103    "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
   2.104    by (simp add: set_array_def set_def)
   2.105  
   2.106 -hide_const (open) present get set alloc lookup update change
   2.107 +hide_const (open) present get set alloc noteq lookup update change
   2.108  
   2.109  
   2.110  subsection {* Code generator setup *}
     6.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 11:01:12 2010 +0100
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 12:05:20 2010 +0200
     6.3 @@ -11,20 +11,20 @@
     6.4  definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
     6.5    "subarray n m a h \<equiv> sublist' n m (get_array a h)"
     6.6  
     6.7 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
     6.8 -apply (simp add: subarray_def Array.change_def)
     6.9 +lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    6.10 +apply (simp add: subarray_def Array.update_def)
    6.11  apply (simp add: sublist'_update1)
    6.12  done
    6.13  
    6.14 -lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
    6.15 -apply (simp add: subarray_def Array.change_def)
    6.16 +lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    6.17 +apply (simp add: subarray_def Array.update_def)
    6.18  apply (subst sublist'_update2)
    6.19  apply fastsimp
    6.20  apply simp
    6.21  done
    6.22  
    6.23 -lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h[i - n := v]"
    6.24 -unfolding subarray_def Array.change_def
    6.25 +lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
    6.26 +unfolding subarray_def Array.update_def
    6.27  by (simp add: sublist'_update3)
    6.28  
    6.29  lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"