# HG changeset patch # User haftmann # Date 1278944610 -7200 # Node ID 786ecb1af09ba2b98508dd4a78b136e30fe8f3b6 # Parent 026ed2fc15d4263c7e5639f8609635b34c9f57da dropped unused lemmas of dubious value diff -r 026ed2fc15d4 -r 786ecb1af09b src/HOL/Imperative_HOL/Relational.thy --- 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 "\h h'. P f [] h h' []" - assumes "\h h1 h' x xs y ys. \ crel (f x) h h1 y; crel (Heap_Monad.fold_map f xs) h1 h' ys; P f xs h1 h' ys \ \ 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 \ b" - shows "[b - Suc a.. Array.length a h" - shows "h = h' \ 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..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a h - n.. Array.length a h" - assumes "i \ 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..n. map_entry n f a) [Array.length a h - n.. i \ Array.length a ?h1 - n" by arith - from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [Array.length a h - n.. 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..n. map_entry n f a) [Array.length a h - n..n. map_entry n f a) [Array.length a ?h1 - n..n. map_entry n f a) [0..n. map_entry n f a) [Array.length a h - Array.length a h.. Array.length a h" - shows "success (Heap_Monad.fold_map (\n. map_entry n f a) [Array.length a h - n..