equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* An imperative in-place reversal on arrays *} |
5 header {* An imperative in-place reversal on arrays *} |
6 |
6 |
7 theory Imperative_Reverse |
7 theory Imperative_Reverse |
8 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray |
8 imports Imperative_HOL Subarray |
9 begin |
9 begin |
10 |
10 |
11 hide_const (open) swap rev |
11 hide_const (open) swap rev |
12 |
12 |
13 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
13 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
34 lemma swap_pointwise: assumes "crel (swap a i j) h h' r" |
34 lemma swap_pointwise: assumes "crel (swap a i j) h h' r" |
35 shows "get_array a h' ! k = (if k = i then get_array a h ! j |
35 shows "get_array a h' ! k = (if k = i then get_array a h ! j |
36 else if k = j then get_array a h ! i |
36 else if k = j then get_array a h ! i |
37 else get_array a h ! k)" |
37 else get_array a h ! k)" |
38 using assms unfolding swap.simps |
38 using assms unfolding swap.simps |
39 by (elim crel_elim_all) |
39 by (elim crel_elims) |
40 (auto simp: length_def) |
40 (auto simp: length_def) |
41 |
41 |
42 lemma rev_pointwise: assumes "crel (rev a i j) h h' r" |
42 lemma rev_pointwise: assumes "crel (rev a i j) h h' r" |
43 shows "get_array a h' ! k = (if k < i then get_array a h ! k |
43 shows "get_array a h' ! k = (if k < i then get_array a h ! k |
44 else if j < k then get_array a h ! k |
44 else if j < k then get_array a h ! k |
50 case True |
50 case True |
51 with 1[unfolded rev.simps[of a i j]] |
51 with 1[unfolded rev.simps[of a i j]] |
52 obtain h' where |
52 obtain h' where |
53 swp: "crel (swap a i j) h h' ()" |
53 swp: "crel (swap a i j) h h' ()" |
54 and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
54 and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
55 by (auto elim: crel_elim_all) |
55 by (auto elim: crel_elims) |
56 from rev 1 True |
56 from rev 1 True |
57 have eq: "?P a (i + 1) (j - 1) h' h''" by auto |
57 have eq: "?P a (i + 1) (j - 1) h' h''" by auto |
58 |
58 |
59 have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith |
59 have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith |
60 with True show ?thesis |
60 with True show ?thesis |
61 by (elim disjE) (auto simp: eq swap_pointwise[OF swp]) |
61 by (elim disjE) (auto simp: eq swap_pointwise[OF swp]) |
62 next |
62 next |
63 case False |
63 case False |
64 with 1[unfolded rev.simps[of a i j]] |
64 with 1[unfolded rev.simps[of a i j]] |
65 show ?thesis |
65 show ?thesis |
66 by (cases "k = j") (auto elim: crel_elim_all) |
66 by (cases "k = j") (auto elim: crel_elims) |
67 qed |
67 qed |
68 qed |
68 qed |
69 |
69 |
70 lemma rev_length: |
70 lemma rev_length: |
71 assumes "crel (rev a i j) h h' r" |
71 assumes "crel (rev a i j) h h' r" |
78 case True |
78 case True |
79 with 1[unfolded rev.simps[of a i j]] |
79 with 1[unfolded rev.simps[of a i j]] |
80 obtain h' where |
80 obtain h' where |
81 swp: "crel (swap a i j) h h' ()" |
81 swp: "crel (swap a i j) h h' ()" |
82 and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
82 and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
83 by (auto elim: crel_elim_all) |
83 by (auto elim: crel_elims) |
84 from swp rev 1 True show ?thesis |
84 from swp rev 1 True show ?thesis |
85 unfolding swap.simps |
85 unfolding swap.simps |
86 by (elim crel_elim_all) fastsimp |
86 by (elim crel_elims) fastsimp |
87 next |
87 next |
88 case False |
88 case False |
89 with 1[unfolded rev.simps[of a i j]] |
89 with 1[unfolded rev.simps[of a i j]] |
90 show ?thesis |
90 show ?thesis |
91 by (auto elim: crel_elim_all) |
91 by (auto elim: crel_elims) |
92 qed |
92 qed |
93 qed |
93 qed |
94 |
94 |
95 lemma rev2_rev': assumes "crel (rev a i j) h h' u" |
95 lemma rev2_rev': assumes "crel (rev a i j) h h' u" |
96 assumes "j < Array.length a h" |
96 assumes "j < Array.length a h" |
110 lemma rev2_rev: |
110 lemma rev2_rev: |
111 assumes "crel (rev a 0 (Array.length a h - 1)) h h' u" |
111 assumes "crel (rev a 0 (Array.length a h - 1)) h h' u" |
112 shows "get_array a h' = List.rev (get_array a h)" |
112 shows "get_array a h' = List.rev (get_array a h)" |
113 using rev2_rev'[OF assms] rev_length[OF assms] assms |
113 using rev2_rev'[OF assms] rev_length[OF assms] assms |
114 by (cases "Array.length a h = 0", auto simp add: Array.length_def |
114 by (cases "Array.length a h = 0", auto simp add: Array.length_def |
115 subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all) |
115 subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims) |
116 (drule sym[of "List.length (get_array a h)"], simp) |
116 (drule sym[of "List.length (get_array a h)"], simp) |
117 |
117 |
118 end |
118 end |