author | krauss |
Tue, 13 Jul 2010 12:00:11 +0200 | |
changeset 37792 | ba0bc31b90d7 |
parent 37771 | 1bec64044b5e |
child 37797 | 96551d6b1414 |
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 |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
36098
diff
changeset
|
11 |
hide_const (open) swap rev |
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
|
12 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
13 |
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
37792 | 14 |
"swap a i j = 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
|
15 |
x \<leftarrow> nth a i; |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
16 |
y \<leftarrow> nth a 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
|
17 |
upd i y a; |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
18 |
upd j x a; |
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 |
return () |
37792 | 20 |
}" |
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
|
21 |
|
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 |
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
37792 | 23 |
"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
|
24 |
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
|
25 |
rev a (i + 1) (j - 1) |
37792 | 26 |
} |
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
|
27 |
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
|
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 |
notation (output) swap ("swap") |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
30 |
notation (output) rev ("rev") |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
31 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
32 |
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
|
33 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
34 |
lemma swap_pointwise: assumes "crel (swap a i j) h h' r" |
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
35 |
shows "get_array a h' ! k = (if k = i then get_array a h ! 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
|
36 |
else if k = j then get_array a h ! i |
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 |
else get_array a h ! 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
|
38 |
using assms unfolding swap.simps |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
39 |
by (elim crel_elims) |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
40 |
(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
|
41 |
|
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 |
lemma rev_pointwise: assumes "crel (rev a i j) h h' r" |
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 |
shows "get_array a h' ! k = (if k < i then get_array a h ! 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
|
44 |
else if j < k then get_array a h ! 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
|
45 |
else get_array a h ! (j - (k - i)))" (is "?P 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
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
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
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
|
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 |
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
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
show ?thesis |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
|
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 |
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
|
71 |
assumes "crel (rev a i j) h h' r" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
72 |
shows "Array.length a h = Array.length a 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
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
unfolding swap.simps |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
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
|
90 |
show ?thesis |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
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
|
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 |
lemma rev2_rev': assumes "crel (rev a i j) h h' u" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
96 |
assumes "j < Array.length a 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
|
97 |
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
|
98 |
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
|
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 |
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
|
101 |
assume "k < Suc j - i" |
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 |
with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - 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
|
103 |
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
|
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 |
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
|
106 |
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
|
107 |
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
|
108 |
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
|
109 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
110 |
lemma rev2_rev: |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
111 |
assumes "crel (rev a 0 (Array.length a h - 1)) h h' u" |
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 |
shows "get_array a h' = List.rev (get_array 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
|
113 |
using rev2_rev'[OF assms] rev_length[OF assms] assms |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset
|
114 |
by (cases "Array.length a h = 0", auto simp add: Array.length_def |
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset
|
115 |
subarray_def sublist'_all rev.simps[where j=0] 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
|
116 |
(drule sym[of "List.length (get_array a h)"], simp) |
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 |
|
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset
|
118 |
end |