author | haftmann |
Fri, 23 Jul 2010 10:58:13 +0200 | |
changeset 37947 | 844977c7abeb |
parent 37845 | b70d7a347964 |
child 37959 | 6fe5fa827f18 |
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 |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
8 |
imports Imperative_HOL Subarray |
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 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
29 |
lemma swap_pointwise: assumes "crel (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 |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
34 |
by (elim crel_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 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
37 |
lemma rev_pointwise: assumes "crel (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 |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
48 |
swp: "crel (swap 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
|
49 |
and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
50 |
by (auto elim: crel_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 |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
61 |
by (cases "k = j") (auto elim: crel_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: |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
66 |
assumes "crel (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 |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
76 |
swp: "crel (swap 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
|
77 |
and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()" |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
78 |
by (auto elim: crel_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 |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
81 |
by (elim crel_elims) fastsimp |
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 |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
86 |
by (auto elim: crel_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 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
90 |
lemma rev2_rev': assumes "crel (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: |
37802 | 106 |
assumes "crel (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 |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
110 |
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_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 |
|
37845
b70d7a347964
first roughly working version of Imperative HOL for Scala
haftmann
parents:
37826
diff
changeset
|
113 |
export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? |
37826 | 114 |
|
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
|
115 |
end |