author | haftmann |
Fri, 28 Dec 2012 10:25:59 +0100 | |
changeset 50630 | 1ea90e8046dc |
parent 47108 | 2a1953f0d20d |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset
|
1 |
(* Title: HOL/Imperative_HOL/ex/Imperative_Reverse.thy |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset
|
3 |
*) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset
|
4 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset
|
5 |
header {* An imperative in-place reversal on arrays *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset
|
6 |
|
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
7 |
theory Imperative_Reverse |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44890
diff
changeset
|
8 |
imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
9 |
begin |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
10 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
11 |
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
37792 | 12 |
"swap a i j = do { |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
13 |
x \<leftarrow> Array.nth a i; |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
14 |
y \<leftarrow> Array.nth a j; |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
15 |
Array.upd i y a; |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
16 |
Array.upd j x a; |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
17 |
return () |
37792 | 18 |
}" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
19 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
20 |
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
37792 | 21 |
"rev a i j = (if (i < j) then do { |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
22 |
swap a i j; |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
23 |
rev a (i + 1) (j - 1) |
37792 | 24 |
} |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
25 |
else return ())" |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
26 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
27 |
declare swap.simps [simp del] rev.simps [simp del] |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
28 |
|
40671 | 29 |
lemma swap_pointwise: assumes "effect (swap a i j) h h' r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
30 |
shows "Array.get h' a ! k = (if k = i then Array.get h a ! j |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
31 |
else if k = j then Array.get h a ! i |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
32 |
else Array.get h a ! k)" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
33 |
using assms unfolding swap.simps |
40671 | 34 |
by (elim effect_elims) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
35 |
(auto simp: length_def) |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
36 |
|
40671 | 37 |
lemma rev_pointwise: assumes "effect (rev a i j) h h' r" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
38 |
shows "Array.get h' a ! k = (if k < i then Array.get h a ! k |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
39 |
else if j < k then Array.get h a ! k |
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
40 |
else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'") |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
41 |
using assms proof (induct a i j arbitrary: h h' rule: rev.induct) |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
42 |
case (1 a i j h h'') |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
43 |
thus ?case |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
44 |
proof (cases "i < j") |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
45 |
case True |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
46 |
with 1[unfolded rev.simps[of a i j]] |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
47 |
obtain h' where |
40671 | 48 |
swp: "effect (swap a i j) h h' ()" |
49 |
and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()" |
|
50 |
by (auto elim: effect_elims) |
|
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
51 |
from rev 1 True |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
52 |
have eq: "?P a (i + 1) (j - 1) h' h''" by auto |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
53 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
54 |
have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
55 |
with True show ?thesis |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
56 |
by (elim disjE) (auto simp: eq swap_pointwise[OF swp]) |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
57 |
next |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
58 |
case False |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
59 |
with 1[unfolded rev.simps[of a i j]] |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
60 |
show ?thesis |
40671 | 61 |
by (cases "k = j") (auto elim: effect_elims) |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
62 |
qed |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
63 |
qed |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
64 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
65 |
lemma rev_length: |
40671 | 66 |
assumes "effect (rev a i j) h h' r" |
37802 | 67 |
shows "Array.length h a = Array.length h' a" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
68 |
using assms |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
69 |
proof (induct a i j arbitrary: h h' rule: rev.induct) |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
70 |
case (1 a i j h h'') |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
71 |
thus ?case |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
72 |
proof (cases "i < j") |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
73 |
case True |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
74 |
with 1[unfolded rev.simps[of a i j]] |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
75 |
obtain h' where |
40671 | 76 |
swp: "effect (swap a i j) h h' ()" |
77 |
and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()" |
|
78 |
by (auto elim: effect_elims) |
|
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
79 |
from swp rev 1 True show ?thesis |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
80 |
unfolding swap.simps |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
40671
diff
changeset
|
81 |
by (elim effect_elims) fastforce |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
82 |
next |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
83 |
case False |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
84 |
with 1[unfolded rev.simps[of a i j]] |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
85 |
show ?thesis |
40671 | 86 |
by (auto elim: effect_elims) |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
87 |
qed |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
88 |
qed |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
89 |
|
40671 | 90 |
lemma rev2_rev': assumes "effect (rev a i j) h h' u" |
37802 | 91 |
assumes "j < Array.length h a" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
92 |
shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)" |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
93 |
proof - |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
94 |
{ |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
95 |
fix k |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
96 |
assume "k < Suc j - i" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
97 |
with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
98 |
by auto |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
99 |
} |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
100 |
with assms(2) rev_length[OF assms(1)] show ?thesis |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
101 |
unfolding subarray_def Array.length_def |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
102 |
by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI) |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
103 |
qed |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
104 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
105 |
lemma rev2_rev: |
40671 | 106 |
assumes "effect (rev a 0 (Array.length h a - 1)) h h' u" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
107 |
shows "Array.get h' a = List.rev (Array.get h a)" |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
108 |
using rev2_rev'[OF assms] rev_length[OF assms] assms |
37802 | 109 |
by (cases "Array.length h a = 0", auto simp add: Array.length_def |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44890
diff
changeset
|
110 |
subarray_def rev.simps[where j=0] elim!: effect_elims) |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
111 |
(drule sym[of "List.length (Array.get h a)"], simp) |
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
112 |
|
38069 | 113 |
definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))" |
38058 | 114 |
|
50630
1ea90e8046dc
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
haftmann
parents:
47108
diff
changeset
|
115 |
export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp |
37826 | 116 |
|
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
117 |
end |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44890
diff
changeset
|
118 |