author | nipkow |
Mon, 12 Sep 2011 07:55:43 +0200 | |
changeset 44890 | 22f665a2e91c |
parent 41842 | d8f76db6a207 |
child 45129 | 1fce03e3e8ad |
permissions | -rw-r--r-- |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
32960
diff
changeset
|
1 |
(* Title: HOL/Imperative_HOL/ex/Sublist.thy |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
32960
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
32960
diff
changeset
|
3 |
*) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
4 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
5 |
header {* Slices of lists *} |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
6 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
7 |
theory Sublist |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
36098
diff
changeset
|
8 |
imports "~~/src/HOL/Library/Multiset" |
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 |
lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
12 |
apply (induct xs arbitrary: i j k) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
13 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
14 |
apply (simp only: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
15 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
16 |
apply safe |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
17 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
18 |
apply (erule_tac x="0" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
19 |
apply (erule_tac x="j - 1" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
20 |
apply (erule_tac x="k - 1" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
21 |
apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
22 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
23 |
apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
24 |
apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
25 |
apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
26 |
apply simp |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
27 |
apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
28 |
apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
29 |
apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
30 |
apply fastforce |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
31 |
apply (erule_tac x="i - 1" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
32 |
apply (erule_tac x="j - 1" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
33 |
apply (erule_tac x="k - 1" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
34 |
apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
35 |
apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
36 |
apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
37 |
apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
38 |
apply simp |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
39 |
apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
40 |
apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
41 |
apply fastforce |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
42 |
apply fastforce |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
43 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
44 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
45 |
lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
46 |
apply (induct xs arbitrary: i inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
47 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
48 |
apply (case_tac i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
49 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
50 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
51 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
52 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
53 |
lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
54 |
proof (induct xs arbitrary: i inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
55 |
case Nil thus ?case by simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
56 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
57 |
case (Cons x xs) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
58 |
thus ?case |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
59 |
proof (cases i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
60 |
case 0 with Cons show ?thesis by (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
61 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
62 |
case (Suc i') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
63 |
with Cons show ?thesis |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
64 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
65 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
66 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
67 |
apply (auto simp add: nat.split) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
68 |
apply (simp add: card_less_Suc[symmetric]) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
69 |
apply (simp add: card_less_Suc2) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
70 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
71 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
72 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
73 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
74 |
lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
75 |
by (simp add: sublist_update1 sublist_update2) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
76 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
77 |
lemma sublist_take: "sublist xs {j. j < m} = take m xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
78 |
apply (induct xs arbitrary: m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
79 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
80 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
81 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
82 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
83 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
84 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
85 |
lemma sublist_take': "sublist xs {0..<m} = take m xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
86 |
apply (induct xs arbitrary: m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
87 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
88 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
89 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
90 |
apply (simp add: sublist_Cons sublist_take) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
91 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
92 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
93 |
lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
94 |
apply (induct xs) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
95 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
96 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
97 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
98 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
99 |
lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
100 |
apply (induct xs) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
101 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
102 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
103 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
104 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
105 |
lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
106 |
apply (induct xs arbitrary: a) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
107 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
108 |
apply(case_tac aa) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
109 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
110 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
111 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
112 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
113 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
114 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
115 |
lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
116 |
apply (induct xs arbitrary: inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
117 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
118 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
119 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
120 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
121 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
122 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
123 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
124 |
lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
125 |
apply (induct xs arbitrary: inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
126 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
127 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
128 |
apply (auto split: if_splits) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
129 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
130 |
apply (case_tac x, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
131 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
132 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
133 |
lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
134 |
apply (induct xs arbitrary: inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
135 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
136 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
137 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
138 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
139 |
apply (case_tac x, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
140 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
141 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
142 |
lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
143 |
apply (induct xs arbitrary: ys inds inds') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
144 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
145 |
apply (drule sym, rule sym) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
146 |
apply (simp add: sublist_Nil, fastforce) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
147 |
apply (case_tac ys) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
148 |
apply (simp add: sublist_Nil, fastforce) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
149 |
apply (auto simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
150 |
apply (erule_tac x="list" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
151 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
152 |
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
153 |
apply fastforce |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
154 |
apply (erule_tac x="list" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
155 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
156 |
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
157 |
apply fastforce |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
158 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
159 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
160 |
lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
161 |
apply (induct xs arbitrary: ys inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
162 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
163 |
apply (rule sym, simp add: sublist_Nil) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
164 |
apply (case_tac ys) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
165 |
apply (simp add: sublist_Nil) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
166 |
apply (auto simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
167 |
apply (erule_tac x="list" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
168 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
169 |
apply fastforce |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
170 |
apply (erule_tac x="list" in meta_allE) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
171 |
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
172 |
apply fastforce |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
173 |
done |
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 sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
176 |
by (rule sublist_eq, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
177 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
178 |
lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
179 |
apply (induct xs arbitrary: ys inds) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
180 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
181 |
apply (rule sym, simp add: sublist_Nil) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
182 |
apply (case_tac ys) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
183 |
apply (simp add: sublist_Nil) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
184 |
apply (auto simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
185 |
apply (case_tac i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
186 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
187 |
apply (case_tac i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
188 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
189 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
190 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
191 |
section {* Another sublist function *} |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
192 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
193 |
function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
194 |
where |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
195 |
"sublist' n m [] = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
196 |
| "sublist' n 0 xs = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
197 |
| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
198 |
| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
199 |
by pat_completeness auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
200 |
termination by lexicographic_order |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
201 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
202 |
subsection {* Proving equivalence to the other sublist command *} |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
203 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
204 |
lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
205 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
206 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
207 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
208 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
209 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
210 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
211 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
212 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
213 |
apply (simp add: sublist_Cons) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
214 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
215 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
216 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
217 |
lemma "sublist' n m xs = sublist xs {n..<m}" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
218 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
219 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
220 |
apply (case_tac n, case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
221 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
222 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
223 |
apply (simp add: sublist_take') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
224 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
225 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
226 |
apply (simp add: sublist_Cons sublist'_sublist) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
227 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
228 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
229 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
230 |
subsection {* Showing equivalence to use of drop and take for definition *} |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
231 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
232 |
lemma "sublist' n m xs = take (m - n) (drop n xs)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
233 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
234 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
235 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
236 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
237 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
238 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
239 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
240 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
241 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
242 |
subsection {* General lemma about sublist *} |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
243 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
244 |
lemma sublist'_Nil[simp]: "sublist' i j [] = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
245 |
by simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
246 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
247 |
lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow> sublist' i' j xs)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
248 |
by (cases i) auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
249 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
250 |
lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
251 |
apply (cases j) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
252 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
253 |
apply (cases i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
254 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
255 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
256 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
257 |
lemma sublist_n_0: "sublist' n 0 xs = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
258 |
by (induct xs, auto) |
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 sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
261 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
262 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
263 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
264 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
265 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
266 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
267 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
268 |
done |
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 sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
271 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
272 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
273 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
274 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
275 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
276 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
277 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
278 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
279 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
280 |
lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
281 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
282 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
283 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
284 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
285 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
286 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
287 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
288 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
289 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
290 |
lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
291 |
apply (induct xs arbitrary: n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
292 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
293 |
apply (case_tac m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
294 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
295 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
296 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
297 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
298 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
299 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
300 |
lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
301 |
apply (induct xs arbitrary: n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
302 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
303 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
304 |
apply (case_tac n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
305 |
apply (simp add: sublist_n_0) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
306 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
307 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
308 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
309 |
lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
310 |
apply (induct xs arbitrary: n m i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
311 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
312 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
313 |
apply (case_tac i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
314 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
315 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
316 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
317 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
318 |
lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
319 |
apply (induct xs arbitrary: n m i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
320 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
321 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
322 |
apply (case_tac i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
323 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
324 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
325 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
326 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
327 |
lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
328 |
proof (induct xs arbitrary: n m i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
329 |
case Nil thus ?case by auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
330 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
331 |
case (Cons x xs) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
332 |
thus ?case |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
333 |
apply - |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
334 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
335 |
apply (cases i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
336 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
337 |
apply (cases i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
338 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
339 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
340 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
341 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
342 |
lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
343 |
proof (induct xs arbitrary: i j ys n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
344 |
case Nil |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
345 |
thus ?case |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
346 |
apply - |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
347 |
apply (rule sym, drule sym) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
348 |
apply (simp add: sublist'_Nil) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
349 |
apply (simp add: sublist'_Nil3) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
350 |
apply arith |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
351 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
352 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
353 |
case (Cons x xs i j ys n m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
354 |
note c = this |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
355 |
thus ?case |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
356 |
proof (cases m) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
357 |
case 0 thus ?thesis by (simp add: sublist_n_0) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
358 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
359 |
case (Suc m') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
360 |
note a = this |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
361 |
thus ?thesis |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
362 |
proof (cases n) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
363 |
case 0 note b = this |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
364 |
show ?thesis |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
365 |
proof (cases ys) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
366 |
case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
367 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
368 |
case (Cons y ys) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
369 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
370 |
proof (cases j) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
371 |
case 0 with a b Cons.prems show ?thesis by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
372 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
373 |
case (Suc j') with a b Cons.prems Cons show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
374 |
apply - |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
375 |
apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
376 |
done |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
377 |
qed |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
378 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
379 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
380 |
case (Suc n') |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
381 |
show ?thesis |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
382 |
proof (cases ys) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
383 |
case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3) |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
384 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
385 |
case (Cons y ys) with Suc a Cons.prems show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
386 |
apply - |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
387 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
388 |
apply (cases j) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
389 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
390 |
apply (cases i) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
391 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
392 |
apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"]) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
393 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
394 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
395 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
396 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
397 |
apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"]) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
398 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
399 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
400 |
apply simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32580
diff
changeset
|
401 |
done |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
402 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
403 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
404 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
405 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
406 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
407 |
lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
408 |
by (induct xs arbitrary: i j, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
409 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
410 |
lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
411 |
apply (induct xs arbitrary: a i j) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
412 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
413 |
apply (case_tac j) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
414 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
415 |
apply (case_tac i) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
416 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
417 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
418 |
done |
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 |
lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
421 |
apply (induct xs arbitrary: a i j) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
422 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
423 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
424 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
425 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
426 |
(* suffices that j \<le> length xs and length ys *) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
427 |
lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
428 |
proof (induct xs arbitrary: ys i j) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
429 |
case Nil thus ?case by simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
430 |
next |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
431 |
case (Cons x xs) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
432 |
thus ?case |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
433 |
apply - |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
434 |
apply (cases ys) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
435 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
436 |
apply simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
437 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
438 |
apply (case_tac i', auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
439 |
apply (erule_tac x="Suc i'" in allE, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
440 |
apply (erule_tac x="i' - 1" in allE, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
441 |
apply (erule_tac x="Suc i'" in allE, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
442 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
443 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
444 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
445 |
lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
446 |
by (induct xs, auto) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
447 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
448 |
lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
449 |
by (induct xs arbitrary: i j n m) (auto simp add: min_diff) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
450 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
451 |
lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
452 |
by (induct xs arbitrary: i j k) auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
453 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
454 |
lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
455 |
apply (induct xs arbitrary: i j k) |
41842 | 456 |
apply simp |
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
457 |
apply (case_tac k) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
458 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
459 |
done |
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 |
lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
462 |
apply (simp add: sublist'_sublist) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
463 |
apply (simp add: set_sublist) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
464 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
465 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
466 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
467 |
lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
468 |
unfolding set_sublist' by blast |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
469 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
470 |
lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
471 |
unfolding set_sublist' by blast |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
472 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
473 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
474 |
lemma multiset_of_sublist: |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
475 |
assumes l_r: "l \<le> r \<and> r \<le> List.length xs" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
476 |
assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
477 |
assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
478 |
assumes multiset: "multiset_of xs = multiset_of ys" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
479 |
shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
480 |
proof - |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
481 |
from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
482 |
by (simp add: sublist'_append) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
483 |
from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
484 |
with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
485 |
by (simp add: sublist'_append) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
486 |
from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
487 |
moreover |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
488 |
from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
489 |
by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
490 |
moreover |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
491 |
from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
492 |
by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
493 |
moreover |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
494 |
ultimately show ?thesis by (simp add: multiset_of_append) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
495 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
496 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
497 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
diff
changeset
|
498 |
end |