author  haftmann 
Wed, 14 Jul 2010 16:13:14 +0200  
changeset 37826  4c0a5e35931a 
parent 37806  a7679be14442 
child 37845  b70d7a347964 
permissions  rwrr 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
35041
diff
changeset

1 
(* Title: HOL/Imperative_HOL/ex/Imperative_Quicksort.thy 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
35041
diff
changeset

2 
Author: Lukas Bulwahn, TU Muenchen 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
35041
diff
changeset

3 
*) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
35041
diff
changeset

4 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
35041
diff
changeset

5 
header {* An imperative implementation of Quicksort on arrays *} 
30689
b14b2cc4e25e
moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents:
29793
diff
changeset

6 

b14b2cc4e25e
moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents:
29793
diff
changeset

7 
theory Imperative_Quicksort 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

8 
imports Imperative_HOL Subarray Multiset Efficient_Nat 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

9 
begin 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

10 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

11 
text {* We prove QuickSort correct in the Relational Calculus. *} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

12 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

13 
definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

14 
where 
37792  15 
"swap arr i j = 
16 
do { 

37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

17 
x \<leftarrow> Array.nth arr i; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

18 
y \<leftarrow> Array.nth arr j; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

19 
Array.upd i y arr; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

20 
Array.upd j x arr; 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

21 
return () 
37792  22 
}" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

23 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

24 
lemma crel_swapI [crel_intros]: 
37802  25 
assumes "i < Array.length h a" "j < Array.length h a" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

26 
"x = Array.get h a ! i" "y = Array.get h a ! j" 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

27 
"h' = Array.update a j x (Array.update a i y h)" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

28 
shows "crel (swap a i j) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

29 
unfolding swap_def using assms by (auto intro!: crel_intros) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

30 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

31 
lemma swap_permutes: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

32 
assumes "crel (swap a i j) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

33 
shows "multiset_of (Array.get h' a) 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

34 
= multiset_of (Array.get h a)" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

35 
using assms 
28145  36 
unfolding swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

37 
by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

38 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

39 
function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

40 
where 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

41 
"part1 a left right p = ( 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

42 
if (right \<le> left) then return right 
37792  43 
else do { 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

44 
v \<leftarrow> Array.nth a left; 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

45 
(if (v \<le> p) then (part1 a (left + 1) right p) 
37792  46 
else (do { swap a left right; 
47 
part1 a left (right  1) p })) 

48 
})" 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

49 
by pat_completeness auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

50 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

51 
termination 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

52 
by (relation "measure (\<lambda>(_,l,r,_). r  l )") auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

53 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

54 
declare part1.simps[simp del] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

55 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

56 
lemma part_permutes: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

57 
assumes "crel (part1 a l r p) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

58 
shows "multiset_of (Array.get h' a) 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

59 
= multiset_of (Array.get h a)" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

60 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

61 
proof (induct a l r p arbitrary: h h' rs rule:part1.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

62 
case (1 a l r p h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

63 
thus ?case 
28145  64 
unfolding part1.simps [of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

65 
by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

66 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

67 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

68 
lemma part_returns_index_in_bounds: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

69 
assumes "crel (part1 a l r p) h h' rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

70 
assumes "l \<le> r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

71 
shows "l \<le> rs \<and> rs \<le> r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

72 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

73 
proof (induct a l r p arbitrary: h h' rs rule:part1.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

74 
case (1 a l r p h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

75 
note cr = `crel (part1 a l r p) h h' rs` 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

76 
show ?case 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

77 
proof (cases "r \<le> l") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

78 
case True (* Terminating case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

79 
with cr `l \<le> r` show ?thesis 
28145  80 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

81 
by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

82 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

83 
case False (* recursive case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

84 
note rec_condition = this 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

85 
let ?v = "Array.get h a ! l" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

86 
show ?thesis 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

87 
proof (cases "?v \<le> p") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

88 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

89 
with cr False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

90 
have rec1: "crel (part1 a (l + 1) r p) h h' rs" 
28145  91 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

92 
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

93 
from rec_condition have "l + 1 \<le> r" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

94 
from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

95 
show ?thesis by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

96 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

97 
case False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

98 
with rec_condition cr 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

99 
obtain h1 where swp: "crel (swap a l r) h h1 ()" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

100 
and rec2: "crel (part1 a l (r  1) p) h1 h' rs" 
28145  101 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

102 
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

103 
from rec_condition have "l \<le> r  1" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

104 
from 1(2) [OF rec_condition False rec2 `l \<le> r  1`] show ?thesis by fastsimp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

105 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

106 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

107 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

108 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

109 
lemma part_length_remains: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

110 
assumes "crel (part1 a l r p) h h' rs" 
37802  111 
shows "Array.length h a = Array.length h' a" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

112 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

113 
proof (induct a l r p arbitrary: h h' rs rule:part1.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

114 
case (1 a l r p h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

115 
note cr = `crel (part1 a l r p) h h' rs` 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

116 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

117 
show ?case 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

118 
proof (cases "r \<le> l") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

119 
case True (* Terminating case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

120 
with cr show ?thesis 
28145  121 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

122 
by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

123 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

124 
case False (* recursive case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

125 
with cr 1 show ?thesis 
28145  126 
unfolding part1.simps [of a l r p] swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

127 
by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

128 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

129 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

130 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

131 
lemma part_outer_remains: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

132 
assumes "crel (part1 a l r p) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

133 
shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

134 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

135 
proof (induct a l r p arbitrary: h h' rs rule:part1.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

136 
case (1 a l r p h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

137 
note cr = `crel (part1 a l r p) h h' rs` 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

138 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

139 
show ?case 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

140 
proof (cases "r \<le> l") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

141 
case True (* Terminating case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

142 
with cr show ?thesis 
28145  143 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

144 
by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

145 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

146 
case False (* recursive case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

147 
note rec_condition = this 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

148 
let ?v = "Array.get h a ! l" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

149 
show ?thesis 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

150 
proof (cases "?v \<le> p") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

151 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

152 
with cr False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

153 
have rec1: "crel (part1 a (l + 1) r p) h h' rs" 
28145  154 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

155 
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

156 
from 1(1)[OF rec_condition True rec1] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

157 
show ?thesis by fastsimp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

158 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

159 
case False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

160 
with rec_condition cr 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

161 
obtain h1 where swp: "crel (swap a l r) h h1 ()" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

162 
and rec2: "crel (part1 a l (r  1) p) h1 h' rs" 
28145  163 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

164 
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

165 
from swp rec_condition have 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

166 
"\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

167 
unfolding swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

168 
by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

169 
with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

170 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

171 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

172 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

173 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

174 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

175 
lemma part_partitions: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

176 
assumes "crel (part1 a l r p) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

177 
shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p) 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

178 
\<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

179 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

180 
proof (induct a l r p arbitrary: h h' rs rule:part1.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

181 
case (1 a l r p h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

182 
note cr = `crel (part1 a l r p) h h' rs` 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

183 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

184 
show ?case 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

185 
proof (cases "r \<le> l") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

186 
case True (* Terminating case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

187 
with cr have "rs = r" 
28145  188 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

189 
by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

190 
with True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

191 
show ?thesis by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

192 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

193 
case False (* recursive case *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

194 
note lr = this 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

195 
let ?v = "Array.get h a ! l" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

196 
show ?thesis 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

197 
proof (cases "?v \<le> p") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

198 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

199 
with lr cr 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

200 
have rec1: "crel (part1 a (l + 1) r p) h h' rs" 
28145  201 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

202 
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

203 
from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

204 
by fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

205 
have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

206 
with 1(1)[OF False True rec1] a_l show ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

207 
by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

208 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

209 
case False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

210 
with lr cr 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

211 
obtain h1 where swp: "crel (swap a l r) h h1 ()" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

212 
and rec2: "crel (part1 a l (r  1) p) h1 h' rs" 
28145  213 
unfolding part1.simps[of a l r p] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

214 
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

215 
from swp False have "Array.get h1 a ! r \<ge> p" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

216 
unfolding swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

217 
by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE) 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

218 
with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

219 
by fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

220 
have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r  1))" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

221 
with 1(2)[OF lr False rec2] a_r show ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

222 
by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

223 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

224 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

225 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

226 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

227 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

228 
fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

229 
where 
37792  230 
"partition a left right = do { 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

231 
pivot \<leftarrow> Array.nth a right; 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

232 
middle \<leftarrow> part1 a left (right  1) pivot; 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

233 
v \<leftarrow> Array.nth a middle; 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

234 
m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle); 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

235 
swap a m right; 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

236 
return m 
37792  237 
}" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

238 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

239 
declare partition.simps[simp del] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

240 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

241 
lemma partition_permutes: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

242 
assumes "crel (partition a l r) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

243 
shows "multiset_of (Array.get h' a) 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

244 
= multiset_of (Array.get h a)" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

245 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

246 
from assms part_permutes swap_permutes show ?thesis 
28145  247 
unfolding partition.simps 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

248 
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

249 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

250 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

251 
lemma partition_length_remains: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

252 
assumes "crel (partition a l r) h h' rs" 
37802  253 
shows "Array.length h a = Array.length h' a" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

254 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

255 
from assms part_length_remains show ?thesis 
28145  256 
unfolding partition.simps swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

257 
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

258 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

259 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

260 
lemma partition_outer_remains: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

261 
assumes "crel (partition a l r) h h' rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

262 
assumes "l < r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

263 
shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

264 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

265 
from assms part_outer_remains part_returns_index_in_bounds show ?thesis 
28145  266 
unfolding partition.simps swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

267 
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

268 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

269 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

270 
lemma partition_returns_index_in_bounds: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

271 
assumes crel: "crel (partition a l r) h h' rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

272 
assumes "l < r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

273 
shows "l \<le> rs \<and> rs \<le> r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

274 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

275 
from crel obtain middle h'' p where part: "crel (part1 a l (r  1) p) h h'' middle" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

276 
and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

277 
else middle)" 
28145  278 
unfolding partition.simps 
37805  279 
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

280 
from `l < r` have "l \<le> r  1" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

281 
from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

282 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

283 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

284 
lemma partition_partitions: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

285 
assumes crel: "crel (partition a l r) h h' rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

286 
assumes "l < r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

287 
shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and> 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

288 
(\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

289 
proof  
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

290 
let ?pivot = "Array.get h a ! r" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

291 
from crel obtain middle h1 where part: "crel (part1 a l (r  1) ?pivot) h h1 middle" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

292 
and swap: "crel (swap a rs r) h1 h' ()" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

293 
and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

294 
else middle)" 
28145  295 
unfolding partition.simps 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

296 
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

297 
from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs) 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

298 
(Array.update a rs (Array.get h1 a ! r) h1)" 
28145  299 
unfolding swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

300 
by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp 
37802  301 
from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a" 
28145  302 
unfolding swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

303 
by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp 
37802  304 
from swap have swap_length_remains: "Array.length h1 a = Array.length h' a" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

305 
unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

306 
from `l < r` have "l \<le> r  1" by simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

307 
note middle_in_bounds = part_returns_index_in_bounds[OF part this] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

308 
from part_outer_remains[OF part] `l < r` 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

309 
have "Array.get h a ! r = Array.get h1 a ! r" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

310 
by fastsimp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

311 
with swap 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

312 
have right_remains: "Array.get h a ! r = Array.get h' a ! rs" 
28145  313 
unfolding swap_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

314 
by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

315 
from part_partitions [OF part] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

316 
show ?thesis 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

317 
proof (cases "Array.get h1 a ! middle \<le> ?pivot") 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

318 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

319 
with rs_equals have rs_equals: "rs = middle + 1" by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

320 
{ 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

321 
fix i 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

322 
assume i_is_left: "l \<le> i \<and> i < rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

323 
with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r` 
37802  324 
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

325 
from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

326 
with part_partitions[OF part] right_remains True 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

327 
have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

328 
with i_props h'_def in_bounds have "Array.get h' a ! i \<le> Array.get h' a ! rs" 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

329 
unfolding Array.update_def Array.length_def by simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

330 
} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

331 
moreover 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

332 
{ 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

333 
fix i 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

334 
assume "rs < i \<and> i \<le> r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

335 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

336 
hence "(rs < i \<and> i \<le> r  1) \<or> (rs < i \<and> i = r)" by arith 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

337 
hence "Array.get h' a ! rs \<le> Array.get h' a ! i" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

338 
proof 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

339 
assume i_is: "rs < i \<and> i \<le> r  1" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

340 
with swap_length_remains in_bounds middle_in_bounds rs_equals 
37802  341 
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

342 
from part_partitions[OF part] rs_equals right_remains i_is 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

343 
have "Array.get h' a ! rs \<le> Array.get h1 a ! i" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

344 
by fastsimp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

345 
with i_props h'_def show ?thesis by fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

346 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

347 
assume i_is: "rs < i \<and> i = r" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

348 
with rs_equals have "Suc middle \<noteq> r" by arith 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

349 
with middle_in_bounds `l < r` have "Suc middle \<le> r  1" by arith 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

350 
with part_partitions[OF part] right_remains 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

351 
have "Array.get h' a ! rs \<le> Array.get h1 a ! (Suc middle)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

352 
by fastsimp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

353 
with i_is True rs_equals right_remains h'_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

354 
show ?thesis using in_bounds 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

355 
unfolding Array.update_def Array.length_def 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

356 
by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

357 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

358 
} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

359 
ultimately show ?thesis by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

360 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

361 
case False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

362 
with rs_equals have rs_equals: "middle = rs" by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

363 
{ 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

364 
fix i 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

365 
assume i_is_left: "l \<le> i \<and> i < rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

366 
with swap_length_remains in_bounds middle_in_bounds rs_equals 
37802  367 
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

368 
from part_partitions[OF part] rs_equals right_remains i_is_left 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

369 
have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

370 
with i_props h'_def have "Array.get h' a ! i \<le> Array.get h' a ! rs" 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

371 
unfolding Array.update_def by simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

372 
} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

373 
moreover 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

374 
{ 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

375 
fix i 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

376 
assume "rs < i \<and> i \<le> r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

377 
hence "(rs < i \<and> i \<le> r  1) \<or> i = r" by arith 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

378 
hence "Array.get h' a ! rs \<le> Array.get h' a ! i" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

379 
proof 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

380 
assume i_is: "rs < i \<and> i \<le> r  1" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

381 
with swap_length_remains in_bounds middle_in_bounds rs_equals 
37802  382 
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

383 
from part_partitions[OF part] rs_equals right_remains i_is 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

384 
have "Array.get h' a ! rs \<le> Array.get h1 a ! i" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

385 
by fastsimp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

386 
with i_props h'_def show ?thesis by fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

387 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

388 
assume i_is: "i = r" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

389 
from i_is False rs_equals right_remains h'_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

390 
show ?thesis using in_bounds 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

391 
unfolding Array.update_def Array.length_def 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

392 
by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

393 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

394 
} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

395 
ultimately 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

396 
show ?thesis by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

397 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

398 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

399 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

400 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

401 
function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

402 
where 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

403 
"quicksort arr left right = 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

404 
(if (right > left) then 
37792  405 
do { 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

406 
pivotNewIndex \<leftarrow> partition arr left right; 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

407 
pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex; 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

408 
quicksort arr left (pivotNewIndex  1); 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

409 
quicksort arr (pivotNewIndex + 1) right 
37792  410 
} 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

411 
else return ())" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

412 
by pat_completeness auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

413 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

414 
(* For termination, we must show that the pivotNewIndex is between left and right *) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

415 
termination 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

416 
by (relation "measure (\<lambda>(a, l, r). (r  l))") auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

417 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

418 
declare quicksort.simps[simp del] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

419 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

420 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

421 
lemma quicksort_permutes: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

422 
assumes "crel (quicksort a l r) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

423 
shows "multiset_of (Array.get h' a) 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

424 
= multiset_of (Array.get h a)" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

425 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

426 
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

427 
case (1 a l r h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

428 
with partition_permutes show ?case 
28145  429 
unfolding quicksort.simps [of a l r] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

430 
by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

431 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

432 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

433 
lemma length_remains: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

434 
assumes "crel (quicksort a l r) h h' rs" 
37802  435 
shows "Array.length h a = Array.length h' a" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

436 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

437 
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

438 
case (1 a l r h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

439 
with partition_length_remains show ?case 
28145  440 
unfolding quicksort.simps [of a l r] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

441 
by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

442 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

443 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

444 
lemma quicksort_outer_remains: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

445 
assumes "crel (quicksort a l r) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

446 
shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

447 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

448 
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

449 
case (1 a l r h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

450 
note cr = `crel (quicksort a l r) h h' rs` 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

451 
thus ?case 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

452 
proof (cases "r > l") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

453 
case False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

454 
with cr have "h' = h" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

455 
unfolding quicksort.simps [of a l r] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

456 
by (elim crel_ifE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

457 
thus ?thesis by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

458 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

459 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

460 
{ 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

461 
fix h1 h2 p ret1 ret2 i 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

462 
assume part: "crel (partition a l r) h h1 p" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

463 
assume qs1: "crel (quicksort a l (p  1)) h1 h2 ret1" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

464 
assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

465 
assume pivot: "l \<le> p \<and> p \<le> r" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

466 
assume i_outer: "i < l \<or> r < i" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

467 
from partition_outer_remains [OF part True] i_outer 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

468 
have "Array.get h a !i = Array.get h1 a ! i" by fastsimp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

469 
moreover 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

470 
with 1(1) [OF True pivot qs1] pivot i_outer 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

471 
have "Array.get h1 a ! i = Array.get h2 a ! i" by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

472 
moreover 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

473 
with qs2 1(2) [of p h2 h' ret2] True pivot i_outer 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

474 
have "Array.get h2 a ! i = Array.get h' a ! i" by auto 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

475 
ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

476 
} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

477 
with cr show ?thesis 
28145  478 
unfolding quicksort.simps [of a l r] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

479 
by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

480 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

481 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

482 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

483 
lemma quicksort_is_skip: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

484 
assumes "crel (quicksort a l r) h h' rs" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

485 
shows "r \<le> l \<longrightarrow> h = h'" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

486 
using assms 
28145  487 
unfolding quicksort.simps [of a l r] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

488 
by (elim crel_ifE crel_returnE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

489 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

490 
lemma quicksort_sorts: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

491 
assumes "crel (quicksort a l r) h h' rs" 
37802  492 
assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

493 
shows "sorted (subarray l (r + 1) a h')" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

494 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

495 
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

496 
case (1 a l r h h' rs) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

497 
note cr = `crel (quicksort a l r) h h' rs` 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

498 
thus ?case 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

499 
proof (cases "r > l") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

500 
case False 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

501 
hence "l \<ge> r + 1 \<or> l = r" by arith 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

502 
with length_remains[OF cr] 1(5) show ?thesis 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

503 
by (auto simp add: subarray_Nil subarray_single) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

504 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

505 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

506 
{ 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

507 
fix h1 h2 p 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

508 
assume part: "crel (partition a l r) h h1 p" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

509 
assume qs1: "crel (quicksort a l (p  1)) h1 h2 ()" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

510 
assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

511 
from partition_returns_index_in_bounds [OF part True] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

512 
have pivot: "l\<le> p \<and> p \<le> r" . 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

513 
note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part] 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

514 
from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1] 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

515 
have pivot_unchanged: "Array.get h1 a ! p = Array.get h' a ! p" by (cases p, auto) 
28013  516 
(* First of all, by induction hypothesis both sublists are sorted. *) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

517 
from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

518 
have IH1: "sorted (subarray l p a h2)" by (cases p, auto simp add: subarray_Nil) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

519 
from quicksort_outer_remains [OF qs2] length_remains 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

520 
have left_subarray_remains: "subarray l p a h2 = subarray l p a h'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

521 
by (simp add: subarray_eq_samelength_iff) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

522 
with IH1 have IH1': "sorted (subarray l p a h')" by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

523 
from 1(2)[OF True pivot qs2] pivot 1(5) length_remains 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

524 
have IH2: "sorted (subarray (p + 1) (r + 1) a h')" 
28013  525 
by (cases "Suc p \<le> r", auto simp add: subarray_Nil) 
526 
(*  Secondly, both sublists remain partitioned. *) 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

527 
from partition_partitions[OF part True] 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

528 
have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> Array.get h1 a ! p " 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

529 
and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j" 
28013  530 
by (auto simp add: all_in_set_subarray_conv) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

531 
from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

532 
length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"] 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

533 
have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset

534 
unfolding Array.length_def subarray_def by (cases p, auto) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

535 
with left_subarray_remains part_conds1 pivot_unchanged 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

536 
have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p" 
28013  537 
by (simp, subst set_of_multiset_of[symmetric], simp) 
538 
(*  These steps are the analogous for the right sublist \<dots> *) 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

539 
from quicksort_outer_remains [OF qs1] length_remains 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

540 
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

541 
by (auto simp add: subarray_eq_samelength_iff) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

542 
from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

543 
length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"] 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

544 
have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset

545 
unfolding Array.length_def subarray_def by auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

546 
with right_subarray_remains part_conds2 pivot_unchanged 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

547 
have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j" 
28013  548 
by (simp, subst set_of_multiset_of[symmetric], simp) 
549 
(*  Thirdly and finally, we show that the array is sorted 

550 
following from the facts above. *) 

37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

551 
from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

552 
by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

553 
with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

554 
unfolding subarray_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31887
diff
changeset

555 
apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv) 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

556 
by (auto simp add: set_sublist' dest: le_trans [of _ "Array.get h' a ! p"]) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

557 
} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

558 
with True cr show ?thesis 
28145  559 
unfolding quicksort.simps [of a l r] 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

560 
by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

561 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

562 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

563 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

564 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

565 
lemma quicksort_is_sort: 
37802  566 
assumes crel: "crel (quicksort a 0 (Array.length h a  1)) h h' rs" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

567 
shows "Array.get h' a = sort (Array.get h a)" 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

568 
proof (cases "Array.get h a = []") 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

569 
case True 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

570 
with quicksort_is_skip[OF crel] show ?thesis 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset

571 
unfolding Array.length_def by simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

572 
next 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

573 
case False 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

574 
from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset

575 
unfolding Array.length_def subarray_def by auto 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

576 
with length_remains[OF crel] have "sorted (Array.get h' a)" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36098
diff
changeset

577 
unfolding Array.length_def by simp 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

578 
with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

579 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

580 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

581 
subsection {* No Errors in quicksort *} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

582 
text {* We have proved that quicksort sorts (if no exceptions occur). 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

583 
We will now show that exceptions do not occur. *} 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

584 

37758  585 
lemma success_part1I: 
37802  586 
assumes "l < Array.length h a" "r < Array.length h a" 
37758  587 
shows "success (part1 a l r p) h" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

588 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

589 
proof (induct a l r p arbitrary: h rule: part1.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

590 
case (1 a l r p) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

591 
thus ?case unfolding part1.simps [of a l r] 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

592 
apply (auto intro!: success_intros del: success_ifI simp add: not_le) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

593 
apply (auto intro!: crel_intros crel_swapI) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

594 
done 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

595 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

596 

37758  597 
lemma success_bindI' [success_intros]: (*FIXME move*) 
598 
assumes "success f h" 

599 
assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'" 

600 
shows "success (f \<guillemotright>= g) h" 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

601 
using assms(1) proof (rule success_crelE) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

602 
fix h' r 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

603 
assume "crel f h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

604 
moreover with assms(2) have "success (g r) h'" . 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

605 
ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

606 
qed 
37758  607 

608 
lemma success_partitionI: 

37802  609 
assumes "l < r" "l < Array.length h a" "r < Array.length h a" 
37758  610 
shows "success (partition a l r) h" 
611 
using assms unfolding partition.simps swap_def 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

612 
apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

613 
apply (frule part_length_remains) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

614 
apply (frule part_returns_index_in_bounds) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

615 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

616 
apply (frule part_length_remains) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

617 
apply (frule part_returns_index_in_bounds) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

618 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

619 
apply (frule part_length_remains) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

620 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

621 
done 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

622 

37758  623 
lemma success_quicksortI: 
37802  624 
assumes "l < Array.length h a" "r < Array.length h a" 
37758  625 
shows "success (quicksort a l r) h" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

626 
using assms 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

627 
proof (induct a l r arbitrary: h rule: quicksort.induct) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

628 
case (1 a l ri h) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

629 
thus ?case 
28145  630 
unfolding quicksort.simps [of a l ri] 
37758  631 
apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

632 
apply (frule partition_returns_index_in_bounds) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

633 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

634 
apply (frule partition_returns_index_in_bounds) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

635 
apply auto 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

636 
apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

637 
apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

638 
apply (erule disjE) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

639 
apply auto 
28145  640 
unfolding quicksort.simps [of a "Suc ri" ri] 
37758  641 
apply (auto intro!: success_ifI success_returnI) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

642 
done 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

643 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

644 

27674  645 

646 
subsection {* Example *} 

647 

37792  648 
definition "qsort a = do { 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

649 
k \<leftarrow> Array.len a; 
27674  650 
quicksort a 0 (k  1); 
651 
return a 

37792  652 
}" 
27674  653 

35041
6eb917794a5c
avoid upto in generated code (is infix operator in library.ML)
haftmann
parents:
32960
diff
changeset

654 
code_reserved SML upto 
6eb917794a5c
avoid upto in generated code (is infix operator in library.ML)
haftmann
parents:
32960
diff
changeset

655 

27674  656 
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} 
657 

37826  658 
export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? 
27674  659 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset

660 
end 