Commit 5a90575b authored by Niels Mündler's avatar Niels Mündler
Browse files

Formatting, remove wrongly added file

parent 943298de494d
......@@ -5,7 +5,7 @@ begin
(* Resolves TODO by Peter Lammich *)
(* OCaml handles the case of len=0 correctly (i.e.
as specified by the Hoare Triple in Array_Blit
not generating an exception if si+len \<le> array length and such) *)
not generating an exception if si+len \<le> array length and such) *)
code_printing code_module "array_blit" \<rightharpoonup> (OCaml)
\<open>
let array_blit src si dst di len = (
......@@ -17,7 +17,7 @@ code_printing code_module "array_blit" \<rightharpoonup> (OCaml)
\<close>
code_printing constant blit' \<rightharpoonup>
(OCaml) "(fun () -> /array'_blit _ _ _ _ _)"
(OCaml) "(fun () -> /array'_blit _ _ _ _ _)"
export_code blit checking OCaml
......@@ -50,14 +50,14 @@ lemma sblit_rule[sep_heap_rules]:
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "\<And>x. lsrc ! si # take len (drop (Suc si) lsrc) @ x
= take (Suc len) (drop si lsrc) @ x"
apply simp
by (metis Suc.prems(1) add_Suc_right Cons_nth_drop_Suc
less_Suc_eq_le add.commute not_less_eq take_Suc_Cons
less_Suc_eq_le add.commute not_less_eq take_Suc_Cons
Nat.trans_le_add2)
from Suc.prems show ?case
......@@ -83,17 +83,17 @@ text "For separated arrays it is equivalent to normal blit.
lemma rblit_rule[sep_heap_rules]:
assumes LEN: "si+len \<le> length lsrc" "di+len \<le> length ldst"
shows
"< src \<mapsto>\<^sub>a lsrc
"< src \<mapsto>\<^sub>a lsrc
* dst \<mapsto>\<^sub>a ldst >
rblit src si dst di len
<\<lambda>_. src \<mapsto>\<^sub>a lsrc
<\<lambda>_. src \<mapsto>\<^sub>a lsrc
* dst \<mapsto>\<^sub>a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst)
>"
using LEN
proof (induction len arbitrary: ldst)
case 0 thus ?case by sep_auto
next
case (Suc len)
case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "drop (di + len) (ldst[di + len := lsrc ! (si + len)])
......@@ -132,7 +132,7 @@ lemma srblit_rule[sep_heap_rules]:
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
case (Suc len)
case (Suc len)
note [sep_heap_rules] = Suc.IH
have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)]))
......@@ -160,7 +160,7 @@ subsection "Modeling target language blit"
text "For convenience, a function that is oblivious to the direction of the shift
is defined."
definition "safe_sblit a s d l \<equiv>
definition "safe_sblit a s d l \<equiv>
if s > d then
sblit a s d l
else
......@@ -219,13 +219,13 @@ code_printing code_module "array_sblit" \<rightharpoonup> (OCaml)
\<close>
definition safe_sblit' where
[code del]: "safe_sblit' src si di len
= safe_sblit src (nat_of_integer si) (nat_of_integer di)
[code del]: "safe_sblit' src si di len
= safe_sblit src (nat_of_integer si) (nat_of_integer di)
(nat_of_integer len)"
lemma [code]:
"safe_sblit src si di len
= safe_sblit' src (integer_of_nat si) (integer_of_nat di)
"safe_sblit src si di len
= safe_sblit' src (integer_of_nat si) (integer_of_nat di)
(integer_of_nat len)" by (simp add: safe_sblit'_def)
(* TODO: Export to other languages: Haskell *)
......@@ -242,7 +242,7 @@ code_printing constant safe_sblit' \<rightharpoonup>
}"
code_printing constant safe_sblit' \<rightharpoonup>
(OCaml) "(fun () -> /array'_sblit _ _ _ _)"
(OCaml) "(fun () -> /array'_sblit _ _ _ _)"
export_code safe_sblit checking SML Scala OCaml
......
theory BTree
theory BTree
imports Main "HOL-Data_Structures.Sorted_Less" "HOL-Data_Structures.Cmp"
begin
......@@ -135,11 +135,11 @@ lemma height_btree_order:
"height (Node (ls@[a]) t) = height (Node (a#ls) t)"
by simp
lemma height_btree_sub:
lemma height_btree_sub:
"height (Node ((sub,x)#ls) t) = max (height (Node ls t)) (Suc (height sub))"
by simp
lemma height_btree_last:
lemma height_btree_last:
"height (Node ((sub,x)#ts) t) = max (height (Node ts sub)) (Suc (height t))"
by (induction ts) auto
......@@ -155,11 +155,11 @@ lemma child_subset: "p \<in> set t \<Longrightarrow> set_btree (fst p) \<subsete
apply(auto)
done
lemma some_child_sub:
lemma some_child_sub:
assumes "(sub,sep) \<in> set t"
shows "sub \<in> set (subtrees t)"
and "sep \<in> set (separators t)"
using assms by force+
using assms by force+
(* balancedness lemmas *)
......@@ -178,14 +178,14 @@ lemma height_bal_tree: "bal (Node ts t) \<Longrightarrow> height (Node ts t) = S
lemma bal_split_last:
lemma bal_split_last:
assumes "bal (Node (ls@(sub,sep)#rs) t)"
shows "bal (Node (ls@rs) t)"
and "height (Node (ls@(sub,sep)#rs) t) = height (Node (ls@rs) t)"
using assms by auto
lemma bal_split_right:
lemma bal_split_right:
assumes "bal (Node (ls@rs) t)"
shows "bal (Node rs t)"
and "height (Node rs t) = height (Node (ls@rs) t)"
......
......@@ -40,7 +40,7 @@ lemma sum_list_replicate: "sum_list (replicate n c) = n*c"
abbreviation "bound k h \<equiv> ((k+1)^h - 1)"
lemma nodes_height_upper_bound:
lemma nodes_height_upper_bound:
"\<lbrakk>order k t; bal t\<rbrakk> \<Longrightarrow> nodes t * (2*k) \<le> bound (2*k) (height t)"
proof(induction t rule: nodes.induct)
case (2 ts t)
......@@ -64,7 +64,7 @@ proof(induction t rule: nodes.induct)
by simp
moreover have "(nodes t)*(2*k) \<le> ?sub_height"
using 2 by simp
ultimately have "(nodes (Node ts t))*(2*k) \<le>
ultimately have "(nodes (Node ts t))*(2*k) \<le>
2*k
+ ?sub_height * (2*k)
+ ?sub_height"
......@@ -130,7 +130,7 @@ lemma upper_bound_sharp_node:
subsection "Maximum height for a given number of nodes"
lemma nodes_height_lower_bound:
lemma nodes_height_lower_bound:
"\<lbrakk>order k t; bal t\<rbrakk> \<Longrightarrow> bound k (height t) \<le> nodes t * k"
proof(induction t rule: nodes.induct)
case (2 ts t)
......@@ -144,7 +144,7 @@ proof(induction t rule: nodes.induct)
using map_replicate_const[of ?sub_height "subtrees ts"] length_map
by simp
also have "\<dots> \<le> sum_list (map (\<lambda>t. nodes t * k) (subtrees ts))"
using 2
using 2
using sum_list_mono[of "subtrees ts" "\<lambda>x. bound k (height t)" "\<lambda>t. nodes t * k"]
by (metis bal.simps(2) order.simps(2))
also have "\<dots> = sum_list (map nodes (subtrees ts)) * k"
......@@ -153,14 +153,14 @@ proof(induction t rule: nodes.induct)
by simp
moreover have "(nodes t)*k \<ge> ?sub_height"
using 2 by simp
ultimately have "(nodes (Node ts t))*k \<ge>
ultimately have "(nodes (Node ts t))*k \<ge>
k
+ ?sub_height * k
+ ?sub_height"
unfolding nodes.simps add_mult_distrib
by linarith
also have
"k + ?sub_height * k + ?sub_height =
"k + ?sub_height * k + ?sub_height =
k + k*((k + 1) ^ height t) - k + (k + 1) ^ height t - 1"
by (simp add: diff_mult_distrib2 mult.assoc mult.commute)
also have "\<dots> = k*((k + 1) ^ height t) + (k + 1) ^ height t - 1"
......@@ -238,7 +238,7 @@ proof (cases t)
moreover have "(nodes t)*k \<ge> ?sub_height"
using Node assms nodes_height_lower_bound
by auto
ultimately have "(nodes (Node ts t))*k \<ge>
ultimately have "(nodes (Node ts t))*k \<ge>
?sub_height
+ ?sub_height + k"
unfolding nodes.simps add_mult_distrib
......@@ -247,7 +247,7 @@ proof (cases t)
using Node assms(2) height_bal_tree by fastforce
qed simp
lemma nodes_root_height_upper_bound:
lemma nodes_root_height_upper_bound:
assumes "root_order k t"
and "bal t"
shows "nodes t * (2*k) \<le> (2*k+1)^(height t) - 1"
......@@ -275,7 +275,7 @@ proof(cases t)
moreover have "(nodes t)*(2*k) \<le> ?sub_height"
using Node assms nodes_height_upper_bound
by auto
ultimately have "(nodes (Node ts t))*(2*k) \<le>
ultimately have "(nodes (Node ts t))*(2*k) \<le>
2*k
+ ?sub_height * (2*k)
+ ?sub_height"
......@@ -301,7 +301,7 @@ lemma nodes_root_height_lower_bound_simp:
shows "(2*((k+1)^(height t - 1) - 1)) div k + (of_bool (t \<noteq> Leaf)) \<le> nodes t"
proof (cases t)
case Node
have "(2*((k+1)^(height t - 1) - 1)) div k + (of_bool (t \<noteq> Leaf)) =
have "(2*((k+1)^(height t - 1) - 1)) div k + (of_bool (t \<noteq> Leaf)) =
(2*((k+1)^(height t - 1) - 1) + (of_bool (t \<noteq> Leaf))*k) div k"
using Node assms
using div_plus_div_distrib_dvd_left[of k k "(2 * Suc k ^ (height t - Suc 0) - Suc (Suc 0))"]
......
......@@ -39,7 +39,7 @@ text "The refinement relationship to abstract B-trees."
fun btree_assn :: "nat \<Rightarrow> 'a::heap btree \<Rightarrow> 'a btnode ref option \<Rightarrow> assn" where
"btree_assn k Leaf None = emp" |
"btree_assn k (Node ts t) (Some a) =
"btree_assn k (Node ts t) (Some a) =
(\<exists>\<^sub>A tsi ti tsi'.
a \<mapsto>\<^sub>r Btnode tsi ti
* btree_assn k t ti
......@@ -53,7 +53,7 @@ also need to directly reason on nodes and not only on references
to them."
fun btnode_assn :: "nat \<Rightarrow> 'a::heap btree \<Rightarrow> 'a btnode \<Rightarrow> assn" where
"btnode_assn k (Node ts t) (Btnode tsi ti) =
"btnode_assn k (Node ts t) (Btnode tsi ti) =
(\<exists>\<^sub>A tsi'.
btree_assn k t ti
* is_pfa (2*k) tsi' tsi
......
......@@ -11,7 +11,7 @@ subsection "Auxiliary operations"
definition "split_relation xs \<equiv>
\<lambda>(as,bs) i. i \<le> length xs \<and> as = take i xs \<and> bs = drop i xs"
lemma split_relation_alt:
lemma split_relation_alt:
"split_relation as (ls,rs) i = (as = ls@rs \<and> i = length ls)"
by (auto simp add: split_relation_def)
......@@ -70,9 +70,9 @@ definition split_half :: "('a::heap \<times> 'b::{heap}) pfarray \<Rightarrow> n
lemma split_half_rule[sep_heap_rules]: "<
is_pfa c tsi a
* list_assn R ts tsi>
* list_assn R ts tsi>
split_half a
<\<lambda>i.
<\<lambda>i.
is_pfa c tsi a
* list_assn R ts tsi
* \<up>(i = length ts div 2 \<and> split_relation ts (BTree_Set.split_half ts) i)>"
......@@ -95,9 +95,9 @@ locale imp_split = abs_split: BTree_Set.split split
fixes imp_split:: "('a btnode ref option \<times> 'a::{heap,default,linorder}) pfarray \<Rightarrow> 'a \<Rightarrow> nat Heap"
assumes imp_split_rule [sep_heap_rules]:"sorted_less (separators ts) \<Longrightarrow>
<is_pfa c tsi (a,n)
* blist_assn k ts tsi>
imp_split (a,n) p
<\<lambda>i.
* blist_assn k ts tsi>
imp_split (a,n) p
<\<lambda>i.
is_pfa c tsi (a,n)
* blist_assn k ts tsi
* \<up>(split_relation ts (split ts p) i)>\<^sub>t"
......@@ -107,7 +107,7 @@ subsection "Membership"
partial_function (heap) isin :: "'a btnode ref option \<Rightarrow> 'a \<Rightarrow> bool Heap"
where
"isin p x =
"isin p x =
(case p of
None \<Rightarrow> return False |
(Some a) \<Rightarrow> do {
......@@ -129,7 +129,7 @@ partial_function (heap) isin :: "'a btnode ref option \<Rightarrow> 'a \<Rightar
subsection "Insertion"
datatype 'b btupi =
datatype 'b btupi =
T\<^sub>i "'b btnode ref option" |
Up\<^sub>i "'b btnode ref option" "'b" "'b btnode ref option"
......@@ -169,7 +169,7 @@ definition node\<^sub>i :: "nat \<Rightarrow> ('a btnode ref option \<times> 'a)
partial_function (heap) ins :: "nat \<Rightarrow> 'a \<Rightarrow> 'a btnode ref option \<Rightarrow> 'a btupi Heap"
where
"ins k x apo = (case apo of
None \<Rightarrow>
None \<Rightarrow>
return (Up\<^sub>i None x None) |
(Some ap) \<Rightarrow> do {
a \<leftarrow> !ap;
......@@ -182,7 +182,7 @@ partial_function (heap) ins :: "nat \<Rightarrow> 'a \<Rightarrow> 'a btnode ref
return (T\<^sub>i apo)
else do {
r \<leftarrow> ins k x sub;
case r of
case r of
(T\<^sub>i lp) \<Rightarrow> do {
pfa_set (kvs a) i (lp,sep);
return (T\<^sub>i apo)
......@@ -202,12 +202,12 @@ partial_function (heap) ins :: "nat \<Rightarrow> 'a \<Rightarrow> 'a btnode ref
}
else do {
r \<leftarrow> ins k x (last a);
case r of
case r of
(T\<^sub>i lp) \<Rightarrow> do {
ap := (Btnode (kvs a) lp);
return (T\<^sub>i apo)
} |
(Up\<^sub>i lp x' rp) \<Rightarrow>
(Up\<^sub>i lp x' rp) \<Rightarrow>
if tsl < 2*k then do {
kvs' \<leftarrow> pfa_append (kvs a) (lp,x');
ap := (Btnode kvs' rp);
......@@ -223,7 +223,7 @@ partial_function (heap) ins :: "nat \<Rightarrow> 'a \<Rightarrow> 'a btnode ref
(*fun tree\<^sub>i::"'a up\<^sub>i \<Rightarrow> 'a btree" where
"tree\<^sub>i (T\<^sub>i sub) = sub" |
"tree\<^sub>i (Up\<^sub>i l a r) = (Node [(l,a)] r)"
"tree\<^sub>i (Up\<^sub>i l a r) = (Node [(l,a)] r)"
fun insert::"nat \<Rightarrow> 'a \<Rightarrow> 'a btree \<Rightarrow> 'a btree" where
"insert k x t = tree\<^sub>i (ins k x t)"
......@@ -288,7 +288,7 @@ definition rebalance_middle_tree:: "nat \<Rightarrow> (('a::{default,heap,linord
res_node\<^sub>i \<leftarrow> node\<^sub>i k mts' (last rsub);
case res_node\<^sub>i of
T\<^sub>i u \<Rightarrow> do {
tsi' \<leftarrow> pfa_set tsi i (u,rsep);
tsi' \<leftarrow> pfa_set tsi i (u,rsep);
tsi'' \<leftarrow> pfa_delete tsi' (i+1);
return (Btnode tsi'' r_ti)
} |
......@@ -375,7 +375,7 @@ next
apply safe
using False apply simp
apply(subst isin.simps)
using "2.prems" sorted_inorder_separators
using "2.prems" sorted_inorder_separators
apply(sep_auto)
(*eliminate vacuous case*)
apply(auto simp add: split_relation_alt list_assn_append_Cons_left dest!: mod_starD list_assn_len)[]
......@@ -569,13 +569,13 @@ next
apply(sep_auto)
subgoal for p tsil tsin tti
using Nil list_split
by (simp add: list_assn_aux_ineq_len split_relation_alt)
by (simp add: list_assn_aux_ineq_len split_relation_alt)
subgoal for p tsil tsin tti tsi' i tsin' _ sub sep
using Nil list_split
using Nil list_split
by (simp add: list_assn_aux_ineq_len split_relation_alt)
subgoal for p tsil tsin tti tsi' i tsin'
thm "2.IH"(1)[of ls rrs tti]
using Nil list_split Up\<^sub>i apply(sep_auto split!: list.splits
using Nil list_split Up\<^sub>i apply(sep_auto split!: list.splits
simp add: split_relation_alt
heap add: "2.IH"(1)[of ls rrs tti])
subgoal for ai
......@@ -798,7 +798,7 @@ lemma insert_rule':
shows "<btree_assn (Suc k) t ti * \<up>(abs_split.invar_inorder (Suc k) t \<and> sorted_less (inorder t))>
insert (Suc k) x ti
<\<lambda>ri.\<exists>\<^sub>Ar. btree_assn (Suc k) r ri * \<up>(abs_split.invar_inorder (Suc k) r \<and> sorted_less (inorder r) \<and> inorder r = (ins_list x (inorder t)))>\<^sub>t"
using abs_split.insert_bal abs_split.insert_order abs_split.insert_inorder
using abs_split.insert_bal abs_split.insert_order abs_split.insert_inorder
by (sep_auto heap: insert_rule simp add: sorted_ins_list)
lemma list_update_length2 [simp]:
......@@ -839,7 +839,7 @@ lemma second_last_access:"(xs@a#b#ys) ! Suc(length xs) = b"
lemma pfa_assn_len:"h \<Turnstile> is_pfa k ls (a,n) \<Longrightarrow> n \<le> k \<and> length ls = n"
by (auto simp add: is_pfa_def)
(*declare "impCE"[rule del]*)
(*declare "impCE"[rule del]*)
lemma rebalance_middle_tree_rule:
assumes "height t = height sub"
and "case rs of (rsub,rsep) # list \<Rightarrow> height rsub = height t | [] \<Rightarrow> True"
......@@ -851,10 +851,10 @@ lemma rebalance_middle_tree_rule:
apply(rule norm_pre_ex_rule)+
proof(goal_cases)
case (1 lsi z rsi)
then show ?case
then show ?case
proof(cases z)
case z_split: (Pair subi sepi)
then show ?thesis
then show ?thesis
proof(cases sub)
case sub_leaf[simp]: Leaf
then have t_leaf[simp]: "t = Leaf" using assms
......@@ -873,7 +873,7 @@ proof(goal_cases)
case sub_node[simp]: (Node mts mt)
then obtain tts tt where t_node[simp]: "t = Node tts tt" using assms
by (cases t) auto
then show ?thesis
then show ?thesis
proof(cases "length mts \<ge> k \<and> length tts \<ge> k")
case True
then show ?thesis
......@@ -885,7 +885,7 @@ proof(goal_cases)
using assms apply(sep_auto split!: prod.splits)
using assms apply (auto simp del: height_btree.simps dest!: mod_starD list_assn_len)[]
using z_split apply(auto)[]
subgoal for _ _ _ _ _ _ _ _ tp tsia' tsin' _ _ _ _ _ _ _ _ _ _ tsia tsin tti ttsi sepi subp
subgoal for _ _ _ _ _ _ _ _ tp tsia' tsin' _ _ _ _ _ _ _ _ _ _ tsia tsin tti ttsi sepi subp
apply(auto dest!: mod_starD list_assn_len simp: prod_assn_def)[]
apply(vcg)
apply(auto)[]
......@@ -900,7 +900,7 @@ proof(goal_cases)
done
next
case False
then show ?thesis
then show ?thesis
proof(cases rs)
case Nil
then show ?thesis
......@@ -912,7 +912,7 @@ proof(goal_cases)
apply(sep_auto split!: prod.splits)
using assms apply (auto simp del: height_btree.simps dest!: mod_starD list_assn_len)[]
using z_split apply(auto)[]
subgoal for _ _ _ _ _ _ _ _ tp tsia' tsin' _ _ _ _ _ _ _ _ _ _ tsia tsin tti ttsi
subgoal for _ _ _ _ _ _ _ _ tp tsia' tsin' _ _ _ _ _ _ _ _ _ _ tsia tsin tti ttsi
apply(auto dest!: mod_starD list_assn_len simp: prod_assn_def)[]
apply(vcg)
using False apply(auto dest!: mod_starD list_assn_len)
......@@ -973,7 +973,7 @@ proof(goal_cases)
apply(sep_auto split!: prod.splits)
using assms apply (auto simp del: height_btree.simps dest!: mod_starD list_assn_len)[]
apply(auto)[]
subgoal for _ _ _ _ _ _ _ _ tp tsia' tsin' _ _ _ _ _ _ _ _ _ _ tsia tsin tti ttsi
subgoal for _ _ _ _ _ _ _ _ tp tsia' tsin' _ _ _ _ _ _ _ _ _ _ tsia tsin tti ttsi
apply(auto dest!: mod_starD list_assn_len simp: prod_assn_def)[]
apply(vcg)
using False apply(auto dest!: mod_starD list_assn_len)
......@@ -1073,7 +1073,7 @@ proof(goal_cases)
apply (drule btupi_assn_T mod_starD | erule conjE exE)+
apply vcg
apply simp
subgoal for rsubtsi ai tsian
subgoal for rsubtsi ai tsian
apply(cases tsian)
apply simp
apply(rule P_imp_Q_implies_P)
......@@ -1132,8 +1132,8 @@ lemma rebalance_last_tree_rule:
prefer 2
apply(auto dest!: list_assn_len)[]
using assms apply(sep_auto)
supply R = rebalance_middle_tree_rule[where
ls="list" and
supply R = rebalance_middle_tree_rule[where
ls="list" and
rs="[]" and
i="length tsi - 1", simplified]
apply(cases tsia)
......@@ -1263,7 +1263,7 @@ tt \<noteq> Leaf \<Longrightarrow>
apply (simp add: prod_assn_def)
apply vcg
apply(subst abs_split.split_max.simps)
using "1.prems" apply(auto dest!: mod_starD split!: prod.splits btree.splits)
using "1.prems" apply(auto dest!: mod_starD split!: prod.splits btree.splits)
subgoal for _ _ _ _ _ _ _ _ _ _ tp'
apply(cases "abs_split.rebalance_last_tree k (butlasttsi' @ [(lasttssubi, lasttssepi)]) ttsub"; cases tp')
apply auto
......@@ -1354,14 +1354,14 @@ next
obtain ls rs where split_ts[simp]: "split ts x = (ls, rs)"
by (cases "split ts x")
obtain tss lastts_sub lastts_sep where last_ts: "ts = tss@[(lastts_sub, lastts_sep)]"
using "2.prems" apply auto
using "2.prems" apply auto
by (metis abs_split.isin.cases neq_Nil_rev_conv)
show ?case
proof(cases "rs")
case Nil
then show ?thesis
apply(subst del.simps)
apply sep_auto
apply sep_auto
using "2.prems"(2) sorted_inorder_separators apply blast
apply(rule hoare_triple_preI)
apply (sep_auto)
......@@ -1385,7 +1385,7 @@ next
apply (sep_auto)
apply(cases "abs_split.rebalance_last_tree k ts (abs_split.del k x tt)")
apply(auto simp add: split_relation_alt dest!: mod_starD list_assn_len)
subgoal for tnode
subgoal for tnode
apply (cases tnode; sep_auto)
done
done
......@@ -1395,7 +1395,7 @@ next
then obtain sub sep where [simp]: "rrs = (sub, sep)"
by (cases rrs)
consider (sep_n_x) "sep \<noteq> x" |
(sep_x_Leaf) "sep = x \<and> sub = Leaf" |
(sep_x_Leaf) "sep = x \<and> sub = Leaf" |
(sep_x_Node) "sep = x \<and> (\<exists>ts t. sub = Node ts t)"
using btree.exhaust by blast
then show ?thesis
......@@ -1403,7 +1403,7 @@ next
case sep_n_x
then show ?thesis
apply(subst del.simps)
apply sep_auto
apply sep_auto
using "2.prems"(2) sorted_inorder_separators apply blast
apply(vcg (ss))
apply(vcg (ss))
......@@ -1448,7 +1448,7 @@ next
apply(vcg (ss); simp)
apply(cases tsi; simp)
subgoal for subi' _ tsia' tsin'
supply R = rebalance_middle_tree_update_rule
supply R = rebalance_middle_tree_update_rule
thm R
(* TODO create a new heap rule, in the node_i style *)
apply(auto dest!: list_assn_len)[]
......@@ -1487,7 +1487,7 @@ next
apply(vcg (ss); simp)
apply(cases tsi; simp)
subgoal for x' xab a n
supply R = rebalance_middle_tree_update_rule
supply R = rebalance_middle_tree_update_rule
thm R
(* TODO create a new heap rule, in the node_i style *)
apply(auto dest!: list_assn_len)[]
......@@ -1512,7 +1512,7 @@ next
case sep_x_Leaf
then show ?thesis
apply(subst del.simps)
apply sep_auto
apply sep_auto
using "2.prems"(2) sorted_inorder_separators apply blast
apply(vcg (ss))
apply(vcg (ss))
......@@ -1562,7 +1562,7 @@ next
case sep_x_Node
then show ?thesis
apply(subst del.simps)
apply sep_auto
apply sep_auto
using "2.prems"(2) sorted_inorder_separators apply blast
apply(vcg (ss))
apply(vcg (ss))
......@@ -1621,7 +1621,7 @@ next
apply(cases split_res; simp)
subgoal for split_subi split_sepi
supply R = rebalance_middle_tree_update_rule[
of tt split_sub rss "length lsi" ls k lsi split_subi split_sep rsi tsi ti
of tt split_sub rss "length lsi" ls k lsi split_subi split_sep rsi tsi ti
]
thm R
(* id_assn split_sepi doesnt match yet... *)
......
......@@ -22,15 +22,15 @@ text "The linear split is the most simple split function for binary trees.
definition lin_split :: "('a::heap \<times> 'b::{heap,linorder}) pfarray \<Rightarrow> 'b \<Rightarrow> nat Heap"
where
"lin_split \<equiv> \<lambda> (a,n) p. do {
i \<leftarrow> heap_WHILET
i \<leftarrow> heap_WHILET
(\<lambda>i. if i<n then do {
(_,s) \<leftarrow> Array.nth a i;
return (s<p)
} else return False)
(\<lambda>i. return (i+1))
} else return False)
(\<lambda>i. return (i+1))
0;
return i
}"
......@@ -41,7 +41,7 @@ lemma lin_split_rule: "
<\<lambda>i. is_pfa c xs (a,n) * \<up>(i\<le>n \<and> (\<forall>j<i. snd (xs!j) < p) \<and> (i<n \<longrightarrow> snd (xs!i)\<ge>p))>\<^sub>t"
unfolding lin_split_def
supply R = heap_WHILET_rule''[where
supply R = heap_WHILET_rule''[where
R = "measure (\<lambda>i. n - i)"
and I = "\<lambda>i. is_pfa c xs (a,n) * \<up>(i\<le>n \<and> (\<forall>j<i. snd (xs!j) < p))"
and b = "\<lambda>i. i<n \<and> snd (xs!i) < p"
......@@ -53,10 +53,10 @@ lemma lin_split_rule: "
apply (metis nth_take snd_eqD)
apply (metis nth_take snd_eqD)
apply (sep_auto simp: is_pfa_def less_Suc_eq)+
apply (metis nth_take)
apply (metis nth_take)
apply(sep_auto simp: is_pfa_def)
apply (metis le_simps(3) less_Suc_eq less_le_trans nth_take)
apply(sep_auto simp: is_pfa_def)+
apply (metis le_simps(3) less_Suc_eq less_le_trans nth_take)
apply(sep_auto simp: is_pfa_def)+
done
subsection "Binary split"
......@@ -69,8 +69,8 @@ and the resulting proof, we first implement the split on singleton arrays."
definition bin'_split :: "'b::{heap,linorder} array_list \<Rightarrow> 'b \<Rightarrow> nat Heap"
where
"bin'_split \<equiv> \<lambda>(a,n) p. do {
(low',high') \<leftarrow> heap_WHILET
(\<lambda>(low,high). return (low < high))
(low',high') \<leftarrow> heap_WHILET
(\<lambda>(low,high). return (low < high))
(\<lambda>(low,high). let mid = ((low + high) div 2) in
do {
s \<leftarrow> Array.nth a mid;
......@@ -79,7 +79,7 @@ definition bin'_split :: "'b::{heap,linorder} array_list \<Rightarrow> 'b \<Righ
else if p > s then
return (mid+1, high)
else return (mid,mid)
})
})
(0::nat,n);
return low'
}"
......@@ -95,7 +95,7 @@ sorted_less xs \<Longrightarrow>
<\<lambda>l. is_pfa c xs (a,n) * \<up>(l \<le> n \<and> (\<forall>j<l. xs!j < p) \<and> (l<n \<longrightarrow> xs!l\<ge>p)) >\<^sub>t"
unfolding bin'_split_def
supply R = heap_WHILET_rule''[where
supply R = heap_WHILET_rule''[where
R = "measure (\<lambda>(l,h). h-l)"
and I = "\<lambda>(l,h). is_pfa c xs (a,n) * \<up>(l\<le>h \<and> h \<le> n \<and> (\<forall>j<l. xs!j < p) \<and> (h<n \<longrightarrow> xs!h\<ge>p))"
and b = "\<lambda>(l,h). l<h"
......@@ -184,8 +184,8 @@ is derived in a straightforward manner."
definition bin_split :: "('a::heap \<times> 'b::{heap,linorder}) pfarray \<Rightarrow> 'b \<Rightarrow> nat Heap"
where
"bin_split \<equiv> \<lambda>(a,n) p. do {
(low',high') \<leftarrow> heap_WHILET
(\<lambda>(low,high). return (low < high))
(low',high') \<leftarrow> heap_WHILET
(\<lambda>(low,high). return (low < high))
(\<lambda>(low,high). let mid = ((low + high) div 2) in
do {
(_,s) \<leftarrow> Array.nth a mid;
......@@ -194,7 +194,7 @@ definition bin_split :: "('a::heap \<times> 'b::{heap,linorder}) pfarray \<Right
else if p > s then
return (mid+1, high)
else return (mid,mid)
})
})
(0::nat,n);
return low'
}"
......@@ -221,7 +221,7 @@ sorted_less (map snd xs) \<Longrightarrow>
(* this works in principle, as demonstrated above *)
unfolding bin_split_def
supply R = heap_WHILET_rule''[where
supply R = heap_WHILET_rule''[where
R = "measure (\<lambda>(l,h). h-l)"
and I = "\<lambda>(l,h). is_pfa c xs (a,n) * \<up>(l\<le>h \<and> h \<le> n \<and> (\<forall>j<l. snd (xs!j) < p) \<and> (h<n \<longrightarrow> snd (xs!h)\<ge>p))"
and b = "\<lambda>(l,h). l<h"
......@@ -235,21 +235,21 @@ sorted_less (map snd xs) \<Longrightarrow>
apply(auto dest!: sndI nth_take_eq[of n _ _ "(_ + _) div 2"])[]
apply (sep_auto dest!: sndI )
subgoal for ls i ls' _ _ j
using map_snd_sorted_lesseq[of "take n ls'" j "(i + n) div 2"]
using map_snd_sorted_lesseq[of "take n ls'" j "(i + n) div 2"]
less_mult_imp_div_less apply(auto)[]
done
subgoal for ls i j ls' _ _ j'