--- a/src/HOL/Imperative_HOL/Relational.thy Mon Jul 12 16:19:15 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy Mon Jul 12 16:23:30 2010 +0200
@@ -35,162 +35,4 @@
| y where "x = Some y" "crel (s y) h h' r"
using assms unfolding crel_def by (auto split: option.splits)
-lemma crel_fold_map:
- assumes "crel (Heap_Monad.fold_map f xs) h h' r"
- assumes "\<And>h h'. P f [] h h' []"
- assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (Heap_Monad.fold_map f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
- shows "P f xs h h' r"
-using assms(1)
-proof (induct xs arbitrary: h h' r)
- case Nil with assms(2) show ?case
- by (auto elim: crel_returnE)
-next
- case (Cons x xs)
- from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
- and crel_fold_map: "crel (Heap_Monad.fold_map f xs) h1 h' ys"
- and r_def: "r = y#ys"
- unfolding fold_map.simps
- by (auto elim!: crel_bindE crel_returnE)
- from Cons(1)[OF crel_fold_map] crel_fold_map crel_f assms(3) r_def
- show ?case by auto
-qed
-
-lemma upt_conv_Cons':
- assumes "Suc a \<le> b"
- shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
-proof -
- from assms have l: "b - Suc a < b" by arith
- from assms have "Suc (b - Suc a) = b - a" by arith
- with l show ?thesis by (simp add: upt_conv_Cons)
-qed
-
-lemma crel_fold_map_nth:
- assumes
- "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
- assumes "n \<le> Array.length a h"
- shows "h = h' \<and> xs = drop (Array.length a h - n) (get_array a h)"
-using assms
-proof (induct n arbitrary: xs h h')
- case 0 thus ?case
- by (auto elim!: crel_returnE simp add: Array.length_def)
-next
- case (Suc n)
- from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
- by (simp add: upt_conv_Cons')
- with Suc(2) obtain r where
- crel_fold_map: "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
- and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
- by (auto elim!: crel_bindE crel_nthE crel_returnE)
- from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)"
- by arith
- with Suc.hyps[OF crel_fold_map] xs_def show ?case
- unfolding Array.length_def
- by (auto simp add: nth_drop')
-qed
-
-lemma crel_fold_map_map_entry_remains:
- assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
- assumes "i < Array.length a h - n"
- shows "get_array a h ! i = get_array a h' ! i"
-using assms
-proof (induct n arbitrary: h h' r)
- case 0
- thus ?case
- by (auto elim: crel_returnE)
-next
- case (Suc n)
- let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
- from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
- by (simp add: upt_conv_Cons')
- from Suc(2) this obtain r where
- crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
- by (auto simp add: elim!: crel_bindE crel_map_entryE crel_returnE)
- have length_remains: "Array.length a ?h1 = Array.length a h" by simp
- from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
- by simp
- from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
-qed
-
-lemma crel_fold_map_map_entry_changes:
- assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
- assumes "n \<le> Array.length a h"
- assumes "i \<ge> Array.length a h - n"
- assumes "i < Array.length a h"
- shows "get_array a h' ! i = f (get_array a h ! i)"
-using assms
-proof (induct n arbitrary: h h' r)
- case 0
- thus ?case
- by (auto elim!: crel_returnE)
-next
- case (Suc n)
- let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
- from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
- by (simp add: upt_conv_Cons')
- from Suc(2) this obtain r where
- crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
- by (auto simp add: elim!: crel_bindE crel_map_entryE crel_returnE)
- have length_remains: "Array.length a ?h1 = Array.length a h" by simp
- from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
- from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
- from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
- from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
- by simp
- from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
- crel_fold_map_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
- show ?case
- by (auto simp add: nth_list_update_eq Array.length_def)
-qed
-
-lemma crel_fold_map_map_entry_length:
- assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
- assumes "n \<le> Array.length a h"
- shows "Array.length a h' = Array.length a h"
-using assms
-proof (induct n arbitrary: h h' r)
- case 0
- thus ?case by (auto elim!: crel_returnE)
-next
- case (Suc n)
- let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
- from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
- by (simp add: upt_conv_Cons')
- from Suc(2) this obtain r where
- crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
- by (auto elim!: crel_bindE crel_map_entryE crel_returnE)
- have length_remains: "Array.length a ?h1 = Array.length a h" by simp
- from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
- by simp
- from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
-qed
-
-lemma crel_fold_map_map_entry:
-assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
- shows "get_array a h' = List.map f (get_array a h)"
-proof -
- from assms have "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
- from crel_fold_map_map_entry_length[OF this]
- crel_fold_map_map_entry_changes[OF this] show ?thesis
- unfolding Array.length_def
- by (auto intro: nth_equalityI)
-qed
-
-lemma success_fold_map_map_entry:
- assumes "n \<le> Array.length a h"
- shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
-using assms
-proof (induct n arbitrary: h)
- case 0
- thus ?case by (auto intro: success_returnI)
-next
- case (Suc n)
- from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] =
- (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
- by (simp add: upt_conv_Cons')
- with Suc.hyps [of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case apply -
- apply (auto simp add: execute_simps execute_bind_success intro!: successI success_returnI success_map_entryI elim: crel_map_entryE)
- apply (subst execute_bind) apply (auto simp add: execute_simps execute_bind_success intro: execute_bind)
- done
-qed
-
end