|
1 theory Imperative_Reverse |
|
2 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray |
|
3 begin |
|
4 |
|
5 hide (open) const swap rev |
|
6 |
|
7 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
|
8 "swap a i j = (do |
|
9 x \<leftarrow> nth a i; |
|
10 y \<leftarrow> nth a j; |
|
11 upd i y a; |
|
12 upd j x a; |
|
13 return () |
|
14 done)" |
|
15 |
|
16 fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
|
17 "rev a i j = (if (i < j) then (do |
|
18 swap a i j; |
|
19 rev a (i + 1) (j - 1) |
|
20 done) |
|
21 else return ())" |
|
22 |
|
23 notation (output) swap ("swap") |
|
24 notation (output) rev ("rev") |
|
25 |
|
26 declare swap.simps [simp del] rev.simps [simp del] |
|
27 |
|
28 lemma swap_pointwise: assumes "crel (swap a i j) h h' r" |
|
29 shows "get_array a h' ! k = (if k = i then get_array a h ! j |
|
30 else if k = j then get_array a h ! i |
|
31 else get_array a h ! k)" |
|
32 using assms unfolding swap.simps |
|
33 by (elim crel_elim_all) |
|
34 (auto simp: Heap.length_def) |
|
35 |
|
36 lemma rev_pointwise: assumes "crel (rev a i j) h h' r" |
|
37 shows "get_array a h' ! k = (if k < i then get_array a h ! k |
|
38 else if j < k then get_array a h ! k |
|
39 else get_array a h ! (j - (k - i)))" (is "?P a i j h h'") |
|
40 using assms proof (induct a i j arbitrary: h h' rule: rev.induct) |
|
41 case (1 a i j h h'') |
|
42 thus ?case |
|
43 proof (cases "i < j") |
|
44 case True |
|
45 with 1[unfolded rev.simps[of a i j]] |
|
46 obtain h' where |
|
47 swp: "crel (swap a i j) h h' ()" |
|
48 and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
|
49 by (auto elim: crel_elim_all) |
|
50 from rev 1 True |
|
51 have eq: "?P a (i + 1) (j - 1) h' h''" by auto |
|
52 |
|
53 have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith |
|
54 with True show ?thesis |
|
55 by (elim disjE) (auto simp: eq swap_pointwise[OF swp]) |
|
56 next |
|
57 case False |
|
58 with 1[unfolded rev.simps[of a i j]] |
|
59 show ?thesis |
|
60 by (cases "k = j") (auto elim: crel_elim_all) |
|
61 qed |
|
62 qed |
|
63 |
|
64 lemma rev_length: |
|
65 assumes "crel (rev a i j) h h' r" |
|
66 shows "Heap.length a h = Heap.length a h'" |
|
67 using assms |
|
68 proof (induct a i j arbitrary: h h' rule: rev.induct) |
|
69 case (1 a i j h h'') |
|
70 thus ?case |
|
71 proof (cases "i < j") |
|
72 case True |
|
73 with 1[unfolded rev.simps[of a i j]] |
|
74 obtain h' where |
|
75 swp: "crel (swap a i j) h h' ()" |
|
76 and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
|
77 by (auto elim: crel_elim_all) |
|
78 from swp rev 1 True show ?thesis |
|
79 unfolding swap.simps |
|
80 by (elim crel_elim_all) fastsimp |
|
81 next |
|
82 case False |
|
83 with 1[unfolded rev.simps[of a i j]] |
|
84 show ?thesis |
|
85 by (auto elim: crel_elim_all) |
|
86 qed |
|
87 qed |
|
88 |
|
89 lemma rev2_rev': assumes "crel (rev a i j) h h' u" |
|
90 assumes "j < Heap.length a h" |
|
91 shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)" |
|
92 proof - |
|
93 { |
|
94 fix k |
|
95 assume "k < Suc j - i" |
|
96 with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)" |
|
97 by auto |
|
98 } |
|
99 with assms(2) rev_length[OF assms(1)] show ?thesis |
|
100 unfolding subarray_def Heap.length_def |
|
101 by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI) |
|
102 qed |
|
103 |
|
104 lemma rev2_rev: |
|
105 assumes "crel (rev a 0 (Heap.length a h - 1)) h h' u" |
|
106 shows "get_array a h' = List.rev (get_array a h)" |
|
107 using rev2_rev'[OF assms] rev_length[OF assms] assms |
|
108 by (cases "Heap.length a h = 0", auto simp add: Heap.length_def |
|
109 subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all) |
|
110 (drule sym[of "List.length (get_array a h)"], simp) |
|
111 |
|
112 end |