--- a/src/HOL/Data_Structures/Brother12_Set.thy Fri Aug 25 09:56:45 2023 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Sat Aug 26 11:36:25 2023 +0100
@@ -3,10 +3,10 @@
section \<open>1-2 Brother Tree Implementation of Sets\<close>
theory Brother12_Set
-imports
- Cmp
- Set_Specs
- "HOL-Number_Theory.Fib"
+ imports
+ Cmp
+ Set_Specs
+ "HOL-Number_Theory.Fib"
begin
subsection \<open>Data Type and Operations\<close>
@@ -20,28 +20,28 @@
N3 "'a bro" 'a "'a bro" 'a "'a bro"
definition empty :: "'a bro" where
-"empty = N0"
+ "empty = N0"
fun inorder :: "'a bro \<Rightarrow> 'a list" where
-"inorder N0 = []" |
-"inorder (N1 t) = inorder t" |
-"inorder (N2 l a r) = inorder l @ a # inorder r" |
-"inorder (L2 a) = [a]" |
-"inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
+ "inorder N0 = []" |
+ "inorder (N1 t) = inorder t" |
+ "inorder (N2 l a r) = inorder l @ a # inorder r" |
+ "inorder (L2 a) = [a]" |
+ "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
-"isin N0 x = False" |
-"isin (N1 t) x = isin t x" |
-"isin (N2 l a r) x =
+ "isin N0 x = False" |
+ "isin (N1 t) x = isin t x" |
+ "isin (N2 l a r) x =
(case cmp x a of
LT \<Rightarrow> isin l x |
EQ \<Rightarrow> True |
GT \<Rightarrow> isin r x)"
fun n1 :: "'a bro \<Rightarrow> 'a bro" where
-"n1 (L2 a) = N2 N0 a N0" |
-"n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
-"n1 t = N1 t"
+ "n1 (L2 a) = N2 N0 a N0" |
+ "n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
+ "n1 t = N1 t"
hide_const (open) insert
@@ -49,30 +49,30 @@
begin
fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
-"n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
-"n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
-"n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
-"n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
-"n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
-"n2 t1 a t2 = N2 t1 a t2"
+ "n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
+ "n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
+ "n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
+ "n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
+ "n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
+ "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
+ "n2 t1 a t2 = N2 t1 a t2"
fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"ins x N0 = L2 x" |
-"ins x (N1 t) = n1 (ins x t)" |
-"ins x (N2 l a r) =
+ "ins x N0 = L2 x" |
+ "ins x (N1 t) = n1 (ins x t)" |
+ "ins x (N2 l a r) =
(case cmp x a of
LT \<Rightarrow> n2 (ins x l) a r |
EQ \<Rightarrow> N2 l a r |
GT \<Rightarrow> n2 l a (ins x r))"
fun tree :: "'a bro \<Rightarrow> 'a bro" where
-"tree (L2 a) = N2 N0 a N0" |
-"tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
-"tree t = t"
+ "tree (L2 a) = N2 N0 a N0" |
+ "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
+ "tree t = t"
definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"insert x t = tree(ins x t)"
+ "insert x t = tree(ins x t)"
end
@@ -80,36 +80,36 @@
begin
fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
-"n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
+ "n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
+ "n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
+ "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
+ "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
-"n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
+ "n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
+ "n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
+ "n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
-"n2 t1 a1 t2 = N2 t1 a1 t2"
+ "n2 t1 a1 t2 = N2 t1 a1 t2"
fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
-"split_min N0 = None" |
-"split_min (N1 t) =
+ "split_min N0 = None" |
+ "split_min (N1 t) =
(case split_min t of
None \<Rightarrow> None |
Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
-"split_min (N2 t1 a t2) =
+ "split_min (N2 t1 a t2) =
(case split_min t1 of
None \<Rightarrow> Some (a, N1 t2) |
Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"del _ N0 = N0" |
-"del x (N1 t) = N1 (del x t)" |
-"del x (N2 l a r) =
+ "del _ N0 = N0" |
+ "del x (N1 t) = N1 (del x t)" |
+ "del x (N2 l a r) =
(case cmp x a of
LT \<Rightarrow> n2 (del x l) a r |
GT \<Rightarrow> n2 l a (del x r) |
@@ -118,35 +118,35 @@
Some (b, r') \<Rightarrow> n2 l b r'))"
fun tree :: "'a bro \<Rightarrow> 'a bro" where
-"tree (N1 t) = t" |
-"tree t = t"
+ "tree (N1 t) = t" |
+ "tree t = t"
definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"delete a t = tree (del a t)"
+ "delete a t = tree (del a t)"
end
subsection \<open>Invariants\<close>
fun B :: "nat \<Rightarrow> 'a bro set"
-and U :: "nat \<Rightarrow> 'a bro set" where
-"B 0 = {N0}" |
-"B (Suc h) = { N2 t1 a t2 | t1 a t2.
+ and U :: "nat \<Rightarrow> 'a bro set" where
+ "B 0 = {N0}" |
+ "B (Suc h) = { N2 t1 a t2 | t1 a t2.
t1 \<in> B h \<union> U h \<and> t2 \<in> B h \<or> t1 \<in> B h \<and> t2 \<in> B h \<union> U h}" |
-"U 0 = {}" |
-"U (Suc h) = N1 ` B h"
+ "U 0 = {}" |
+ "U (Suc h) = N1 ` B h"
abbreviation "T h \<equiv> B h \<union> U h"
fun Bp :: "nat \<Rightarrow> 'a bro set" where
-"Bp 0 = B 0 \<union> L2 ` UNIV" |
-"Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
-"Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
+ "Bp 0 = B 0 \<union> L2 ` UNIV" |
+ "Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
+ "Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
{N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \<in> B (Suc h) \<and> t2 \<in> U (Suc h) \<and> t3 \<in> B (Suc h)}"
fun Um :: "nat \<Rightarrow> 'a bro set" where
-"Um 0 = {}" |
-"Um (Suc h) = N1 ` T h"
+ "Um 0 = {}" |
+ "Um (Suc h) = N1 ` T h"
subsection "Functional Correctness Proofs"
@@ -155,29 +155,29 @@
lemma isin_set:
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
-by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
+ by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
subsubsection "Proofs for insertion"
lemma inorder_n1: "inorder(n1 t) = inorder t"
-by(cases t rule: n1.cases) (auto simp: sorted_lems)
+ by(cases t rule: n1.cases) (auto simp: sorted_lems)
context insert
begin
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
+ by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
lemma inorder_tree: "inorder(tree t) = inorder t"
-by(cases t) auto
+ by(cases t) auto
lemma inorder_ins: "t \<in> T h \<Longrightarrow>
sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)"
-by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
+ by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
lemma inorder_insert: "t \<in> T h \<Longrightarrow>
sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
-by(simp add: insert_def inorder_ins inorder_tree)
+ by(simp add: insert_def inorder_ins inorder_tree)
end
@@ -187,27 +187,27 @@
begin
lemma inorder_tree: "inorder(tree t) = inorder t"
-by(cases t) auto
+ by(cases t) auto
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: n2.cases) (auto)
+ by(cases "(l,a,r)" rule: n2.cases) (auto)
lemma inorder_split_min:
"t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and>
(split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
-by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
+ by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
lemma inorder_del:
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
apply (induction h arbitrary: t)
apply (auto simp: del_list_simps inorder_n2 split: option.splits)
apply (auto simp: del_list_simps inorder_n2
- inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
+ inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
done
lemma inorder_delete:
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(simp add: delete_def inorder_del inorder_tree)
+ by(simp add: delete_def inorder_del inorder_tree)
end
@@ -217,38 +217,41 @@
subsubsection \<open>Proofs for insertion\<close>
lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
-by(cases h rule: Bp.cases) auto
+ by(cases h rule: Bp.cases) auto
context insert
begin
lemma tree_type: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
-by(cases h rule: Bp.cases) auto
+ by(cases h rule: Bp.cases) auto
lemma n2_type:
"(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and>
(t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
-apply(cases h rule: Bp.cases)
-apply (auto)[2]
-apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
-done
+ apply(cases h rule: Bp.cases)
+ apply (auto)[2]
+ apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
+ done
lemma Bp_if_B: "t \<in> B h \<Longrightarrow> t \<in> Bp h"
-by (cases h rule: Bp.cases) simp_all
+ by (cases h rule: Bp.cases) simp_all
text\<open>An automatic proof:\<close>
lemma
"(t \<in> B h \<longrightarrow> ins x t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> ins x t \<in> T h)"
-apply(induction h arbitrary: t)
- apply (simp)
-apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
-done
+proof (induction h arbitrary: t)
+ case 0
+ then show ?case by simp
+next
+ case (Suc h)
+ then show ?case by (fastforce simp: Bp_if_B n2_type dest: n1_type)
+qed
text\<open>A detailed proof:\<close>
lemma ins_type:
-shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
+ shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
proof(induction h arbitrary: t)
case 0
{ case 1 thus ?case by simp
@@ -300,7 +303,7 @@
lemma insert_type:
"t \<in> B h \<Longrightarrow> insert x t \<in> B h \<union> B (Suc h)"
-unfolding insert_def by (metis ins_type(1) tree_type)
+ unfolding insert_def by (metis ins_type(1) tree_type)
end
@@ -311,37 +314,38 @@
"L2 y \<in> B h = False"
"(N3 t1 a1 t2 a2 t3) \<in> B h = False"
"N0 \<in> B h \<longleftrightarrow> h = 0"
-by (cases h, auto)+
+ by (cases h, auto)+
context delete
begin
lemma n2_type1:
"\<lbrakk>t1 \<in> Um h; t2 \<in> B h\<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
-apply(cases h rule: Bp.cases)
-apply auto[2]
-apply(erule exE bexE conjE imageE | simp | erule disjE)+
-done
+ apply(cases h rule: Bp.cases)
+ apply auto[2]
+ apply(erule exE bexE conjE imageE | simp | erule disjE)+
+ done
lemma n2_type2:
"\<lbrakk>t1 \<in> B h ; t2 \<in> Um h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
-apply(cases h rule: Bp.cases)
-apply auto[2]
-apply(erule exE bexE conjE imageE | simp | erule disjE)+
-done
+ apply(cases h rule: Bp.cases)
+ using Um.simps(1) apply blast
+ apply force
+ apply(erule exE bexE conjE imageE | simp | erule disjE)+
+ done
lemma n2_type3:
"\<lbrakk>t1 \<in> T h ; t2 \<in> T h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
-apply(cases h rule: Bp.cases)
-apply auto[2]
-apply(erule exE bexE conjE imageE | simp | erule disjE)+
-done
+ apply(cases h rule: Bp.cases)
+ apply auto[2]
+ apply(erule exE bexE conjE imageE | simp | erule disjE)+
+ done
lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow> t = N0"
-by (cases t) (auto split: option.splits)
+ by (cases t) (auto split: option.splits)
lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
-by (cases h) (auto simp: split_minNoneN0 split: option.splits)
+ by (cases h) (auto simp: split_minNoneN0 split: option.splits)
lemma split_min_type:
"t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
@@ -459,11 +463,11 @@
qed auto
lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t \<in> B (h+1) \<union> B h"
-by(auto)
+ by(auto)
lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
-unfolding delete_def
-by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
+ unfolding delete_def
+ by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
end
@@ -471,8 +475,8 @@
subsection "Overall correctness"
interpretation Set_by_Ordered
-where empty = empty and isin = isin and insert = insert.insert
-and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
+ where empty = empty and isin = isin and insert = insert.insert
+ and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
proof (standard, goal_cases)
case 2 thus ?case by(auto intro!: isin_set)
next
@@ -506,27 +510,27 @@
| "size (N2 t1 _ t2) = 1 + size t1 + size t2"
lemma fib_tree_B: "fib_tree h \<in> B h"
-by (induction h rule: fib_tree.induct) auto
+ by (induction h rule: fib_tree.induct) auto
declare [[names_short]]
lemma size_fib': "size (fib_tree h) = fib' h"
-by (induction h rule: fib_tree.induct) auto
+ by (induction h rule: fib_tree.induct) auto
lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))"
-by (induction h rule: fib_tree.induct) auto
+ by (induction h rule: fib_tree.induct) auto
lemma B_N2_cases[consumes 1]:
-assumes "N2 t1 a t2 \<in> B (Suc n)"
-obtains
- (BB) "t1 \<in> B n" and "t2 \<in> B n" |
- (UB) "t1 \<in> U n" and "t2 \<in> B n" |
- (BU) "t1 \<in> B n" and "t2 \<in> U n"
-using assms by auto
+ assumes "N2 t1 a t2 \<in> B (Suc n)"
+ obtains
+ (BB) "t1 \<in> B n" and "t2 \<in> B n" |
+ (UB) "t1 \<in> U n" and "t2 \<in> B n" |
+ (BU) "t1 \<in> B n" and "t2 \<in> U n"
+ using assms by auto
lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> size (fib_tree h)"
-unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
-case (3 h t')
+ unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
+ case (3 h t')
note main = 3
then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto
with main have "N2 t1 a t2 \<in> B (Suc (Suc h))" by auto
@@ -546,7 +550,7 @@
qed auto
theorem "t \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1"
-using size_bounded
-by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
+ using size_bounded
+ by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
end