canonical argument order for present
authorhaftmann
Tue Jul 13 15:37:31 2010 +0200 (2010-07-13 ago)
changeset 37803582d0fbd201e
parent 37802 f2e9c104cebd
child 37804 0145e59c1f6c
child 37809 6c87cdad912d
canonical argument order for present
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Ref.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 15:34:02 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 15:37:31 2010 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4  
     1.5  subsection {* Primitives *}
     1.6  
     1.7 -definition (*FIXME present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where*)
     1.8 -  array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
     1.9 -  "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
    1.10 +definition (*FIXME present *)
    1.11 +  array_present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
    1.12 +  "array_present h a \<longleftrightarrow> addr_of_array a < lim h"
    1.13  
    1.14  definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*)
    1.15    get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
    1.16 @@ -90,7 +90,7 @@
    1.17  lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
    1.18    unfolding noteq_arrs_def by auto
    1.19  
    1.20 -lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
    1.21 +lemma present_new_arr: "array_present h a \<Longrightarrow> a =!!= fst (array xs h)"
    1.22    by (simp add: array_present_def noteq_arrs_def array_def Let_def)
    1.23  
    1.24  lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
    1.25 @@ -150,15 +150,15 @@
    1.26    by (simp add: Let_def split_def array_def)
    1.27  
    1.28  lemma array_present_update [simp]: 
    1.29 -  "array_present a (update b i v h) = array_present a h"
    1.30 -  by (simp add: update_def array_present_def set_array_def get_array_def)
    1.31 +  "array_present (update b i v h) = array_present h"
    1.32 +  by (simp add: update_def array_present_def set_array_def get_array_def expand_fun_eq)
    1.33  
    1.34  lemma array_present_array [simp]:
    1.35 -  "array_present (fst (array xs h)) (snd (array xs h))"
    1.36 +  "array_present (snd (array xs h)) (fst (array xs h))"
    1.37    by (simp add: array_present_def array_def set_array_def Let_def)
    1.38  
    1.39  lemma not_array_present_array [simp]:
    1.40 -  "\<not> array_present (fst (array xs h)) h"
    1.41 +  "\<not> array_present h (fst (array xs h))"
    1.42    by (simp add: array_present_def array_def Let_def)
    1.43  
    1.44  
    1.45 @@ -180,7 +180,7 @@
    1.46  lemma crel_newE [crel_elims]:
    1.47    assumes "crel (new n x) h h' r"
    1.48    obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
    1.49 -    "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
    1.50 +    "get_array r h' = replicate n x" "array_present h' r" "\<not> array_present h r"
    1.51    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.52  
    1.53  lemma execute_of_list [execute_simps]:
    1.54 @@ -199,7 +199,7 @@
    1.55  lemma crel_of_listE [crel_elims]:
    1.56    assumes "crel (of_list xs) h h' r"
    1.57    obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
    1.58 -    "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
    1.59 +    "get_array r h' = xs" "array_present h' r" "\<not> array_present h r"
    1.60    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.61  
    1.62  lemma execute_make [execute_simps]:
    1.63 @@ -218,7 +218,7 @@
    1.64  lemma crel_makeE [crel_elims]:
    1.65    assumes "crel (make n f) h h' r"
    1.66    obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
    1.67 -    "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
    1.68 +    "get_array r h' = map f [0 ..< n]" "array_present h' r" "\<not> array_present h r"
    1.69    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.70  
    1.71  lemma execute_len [execute_simps]:
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 15:34:02 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 15:37:31 2010 +0200
     2.3 @@ -251,11 +251,11 @@
     2.4    by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
     2.5  
     2.6  lemma array_present_set [simp]:
     2.7 -  "array_present a (set r v h) = array_present a h"
     2.8 -  by (simp add: array_present_def set_def)
     2.9 +  "array_present (set r v h) = array_present h"
    2.10 +  by (simp add: array_present_def set_def expand_fun_eq)
    2.11  
    2.12  lemma array_present_alloc [simp]:
    2.13 -  "array_present a h \<Longrightarrow> array_present a (snd (alloc v h))"
    2.14 +  "array_present h a \<Longrightarrow> array_present (snd (alloc v h)) a"
    2.15    by (simp add: array_present_def alloc_def Let_def)
    2.16  
    2.17  lemma set_array_set_swap: