nipkow@63411: (* Author: Tobias Nipkow, Daniel StÃ¼we *) nipkow@61784: nipkow@62130: section \1-2 Brother Tree Implementation of Sets\ nipkow@61784: nipkow@61784: theory Brother12_Set nipkow@61784: imports nipkow@61784: Cmp nipkow@67965: Set_Specs wenzelm@66453: "HOL-Number_Theory.Fib" nipkow@61784: begin nipkow@61784: nipkow@61784: subsection \Data Type and Operations\ nipkow@61784: nipkow@61784: datatype 'a bro = nipkow@61784: N0 | nipkow@61784: N1 "'a bro" | nipkow@61784: N2 "'a bro" 'a "'a bro" | nipkow@61784: (* auxiliary constructors: *) nipkow@61784: L2 'a | nipkow@61784: N3 "'a bro" 'a "'a bro" 'a "'a bro" nipkow@61784: nipkow@61784: fun inorder :: "'a bro \ 'a list" where nipkow@61784: "inorder N0 = []" | nipkow@61784: "inorder (N1 t) = inorder t" | nipkow@61784: "inorder (N2 l a r) = inorder l @ a # inorder r" | nipkow@61784: "inorder (L2 a) = [a]" | nipkow@61784: "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3" nipkow@61784: nipkow@63411: fun isin :: "'a bro \ 'a::linorder \ bool" where nipkow@61784: "isin N0 x = False" | nipkow@61784: "isin (N1 t) x = isin t x" | nipkow@61784: "isin (N2 l a r) x = nipkow@61784: (case cmp x a of nipkow@61784: LT \ isin l x | nipkow@61784: EQ \ True | nipkow@61784: GT \ isin r x)" nipkow@61784: nipkow@61784: fun n1 :: "'a bro \ 'a bro" where nipkow@61784: "n1 (L2 a) = N2 N0 a N0" | nipkow@61784: "n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | nipkow@61784: "n1 t = N1 t" nipkow@61784: nipkow@61784: hide_const (open) insert nipkow@61784: nipkow@61784: locale insert nipkow@61784: begin nipkow@61784: nipkow@61784: fun n2 :: "'a bro \ 'a \ 'a bro \ 'a bro" where nipkow@61784: "n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" | nipkow@61784: "n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" | nipkow@61784: "n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" | nipkow@61784: "n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" | nipkow@61784: "n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" | nipkow@61784: "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" | nipkow@61784: "n2 t1 a t2 = N2 t1 a t2" nipkow@61784: nipkow@63411: fun ins :: "'a::linorder \ 'a bro \ 'a bro" where nipkow@61789: "ins x N0 = L2 x" | nipkow@61789: "ins x (N1 t) = n1 (ins x t)" | nipkow@61789: "ins x (N2 l a r) = nipkow@61789: (case cmp x a of nipkow@61789: LT \ n2 (ins x l) a r | nipkow@61789: EQ \ N2 l a r | nipkow@61789: GT \ n2 l a (ins x r))" nipkow@61784: nipkow@61784: fun tree :: "'a bro \ 'a bro" where nipkow@61784: "tree (L2 a) = N2 N0 a N0" | nipkow@61784: "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | nipkow@61784: "tree t = t" nipkow@61784: nipkow@63411: definition insert :: "'a::linorder \ 'a bro \ 'a bro" where nipkow@61784: "insert x t = tree(ins x t)" nipkow@61784: nipkow@61784: end nipkow@61784: nipkow@61784: locale delete nipkow@61784: begin nipkow@61784: nipkow@61784: fun n2 :: "'a bro \ 'a \ 'a bro \ 'a bro" where nipkow@61784: "n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" | nipkow@61784: "n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) = nipkow@61784: N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784: "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) = nipkow@61784: N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784: "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) = nipkow@61784: N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" | nipkow@61784: "n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) = nipkow@61784: N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784: "n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) = nipkow@61784: N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784: "n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) = nipkow@61784: N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" | nipkow@61784: "n2 t1 a1 t2 = N2 t1 a1 t2" nipkow@61784: nipkow@68020: fun split_min :: "'a bro \ ('a \ 'a bro) option" where nipkow@68020: "split_min N0 = None" | nipkow@68020: "split_min (N1 t) = nipkow@68020: (case split_min t of nipkow@61784: None \ None | nipkow@61784: Some (a, t') \ Some (a, N1 t'))" | nipkow@68020: "split_min (N2 t1 a t2) = nipkow@68020: (case split_min t1 of nipkow@61784: None \ Some (a, N1 t2) | nipkow@61784: Some (b, t1') \ Some (b, n2 t1' a t2))" nipkow@61784: nipkow@63411: fun del :: "'a::linorder \ 'a bro \ 'a bro" where nipkow@61784: "del _ N0 = N0" | nipkow@61784: "del x (N1 t) = N1 (del x t)" | nipkow@61784: "del x (N2 l a r) = nipkow@61784: (case cmp x a of nipkow@61784: LT \ n2 (del x l) a r | nipkow@61784: GT \ n2 l a (del x r) | nipkow@68020: EQ \ (case split_min r of nipkow@61784: None \ N1 l | nipkow@61784: Some (b, r') \ n2 l b r'))" nipkow@61784: nipkow@61784: fun tree :: "'a bro \ 'a bro" where nipkow@61784: "tree (N1 t) = t" | nipkow@61784: "tree t = t" nipkow@61784: nipkow@63411: definition delete :: "'a::linorder \ 'a bro \ 'a bro" where nipkow@61784: "delete a t = tree (del a t)" nipkow@61784: nipkow@61784: end nipkow@61784: nipkow@61784: subsection \Invariants\ nipkow@61784: nipkow@61784: fun B :: "nat \ 'a bro set" nipkow@61784: and U :: "nat \ 'a bro set" where nipkow@61784: "B 0 = {N0}" | nipkow@61784: "B (Suc h) = { N2 t1 a t2 | t1 a t2. nipkow@61784: t1 \ B h \ U h \ t2 \ B h \ t1 \ B h \ t2 \ B h \ U h}" | nipkow@61784: "U 0 = {}" | nipkow@61784: "U (Suc h) = N1 ` B h" nipkow@61784: nipkow@61784: abbreviation "T h \ B h \ U h" nipkow@61784: nipkow@61784: fun Bp :: "nat \ 'a bro set" where nipkow@61784: "Bp 0 = B 0 \ L2 ` UNIV" | nipkow@61784: "Bp (Suc 0) = B (Suc 0) \ {N3 N0 a N0 b N0|a b. True}" | nipkow@61784: "Bp (Suc(Suc h)) = B (Suc(Suc h)) \ nipkow@61784: {N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \ B (Suc h) \ t2 \ U (Suc h) \ t3 \ B (Suc h)}" nipkow@61784: nipkow@61784: fun Um :: "nat \ 'a bro set" where nipkow@61784: "Um 0 = {}" | nipkow@61784: "Um (Suc h) = N1 ` T h" nipkow@61784: nipkow@61784: nipkow@61784: subsection "Functional Correctness Proofs" nipkow@61784: nipkow@61784: subsubsection "Proofs for isin" nipkow@61784: nipkow@67929: lemma isin_set: nipkow@67929: "t \ T h \ sorted(inorder t) \ isin t x = (x \ set(inorder t))" nipkow@67929: by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+ nipkow@61784: nipkow@61784: subsubsection "Proofs for insertion" nipkow@61784: nipkow@61784: lemma inorder_n1: "inorder(n1 t) = inorder t" nipkow@62526: by(cases t rule: n1.cases) (auto simp: sorted_lems) nipkow@61784: nipkow@61784: context insert nipkow@61784: begin nipkow@61784: nipkow@61784: lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r" nipkow@61784: by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems) nipkow@61784: nipkow@61784: lemma inorder_tree: "inorder(tree t) = inorder t" nipkow@61784: by(cases t) auto nipkow@61784: nipkow@61784: lemma inorder_ins: "t \ T h \ nipkow@61784: sorted(inorder t) \ inorder(ins a t) = ins_list a (inorder t)" nipkow@61784: by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2) nipkow@61784: nipkow@61784: lemma inorder_insert: "t \ T h \ nipkow@61784: sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" nipkow@61784: by(simp add: insert_def inorder_ins inorder_tree) nipkow@61784: nipkow@61784: end nipkow@61784: nipkow@61784: subsubsection \Proofs for deletion\ nipkow@61784: nipkow@61784: context delete nipkow@61784: begin nipkow@61784: nipkow@61784: lemma inorder_tree: "inorder(tree t) = inorder t" nipkow@61784: by(cases t) auto nipkow@61784: nipkow@61784: lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r" nipkow@62526: by(cases "(l,a,r)" rule: n2.cases) (auto) nipkow@61784: nipkow@68020: lemma inorder_split_min: nipkow@68020: "t \ T h \ (split_min t = None \ inorder t = []) \ nipkow@68020: (split_min t = Some(a,t') \ inorder t = a # inorder t')" nipkow@61784: by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits) nipkow@61784: nipkow@61784: lemma inorder_del: nipkow@61792: "t \ T h \ sorted(inorder t) \ inorder(del x t) = del_list x (inorder t)" nipkow@61792: by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2 nipkow@68020: inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits) nipkow@61792: nipkow@61792: lemma inorder_delete: nipkow@61792: "t \ T h \ sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" nipkow@61792: by(simp add: delete_def inorder_del inorder_tree) nipkow@61784: nipkow@61784: end nipkow@61784: nipkow@61784: nipkow@61784: subsection \Invariant Proofs\ nipkow@61784: nipkow@61789: subsubsection \Proofs for insertion\ nipkow@61784: nipkow@61784: lemma n1_type: "t \ Bp h \ n1 t \ T (Suc h)" nipkow@61784: by(cases h rule: Bp.cases) auto nipkow@61784: nipkow@61784: context insert nipkow@61784: begin nipkow@61784: nipkow@61809: lemma tree_type: "t \ Bp h \ tree t \ B h \ B (Suc h)" nipkow@61784: by(cases h rule: Bp.cases) auto nipkow@61784: nipkow@61784: lemma n2_type: nipkow@61784: "(t1 \ Bp h \ t2 \ T h \ n2 t1 a t2 \ Bp (Suc h)) \ nipkow@61784: (t1 \ T h \ t2 \ Bp h \ n2 t1 a t2 \ Bp (Suc h))" nipkow@61784: apply(cases h rule: Bp.cases) nipkow@61784: apply (auto)[2] nipkow@61784: apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+ nipkow@61784: done nipkow@61784: nipkow@61784: lemma Bp_if_B: "t \ B h \ t \ Bp h" nipkow@61784: by (cases h rule: Bp.cases) simp_all nipkow@61784: wenzelm@67406: text\An automatic proof:\ nipkow@61784: nipkow@61784: lemma nipkow@61784: "(t \ B h \ ins x t \ Bp h) \ (t \ U h \ ins x t \ T h)" nipkow@61784: apply(induction h arbitrary: t) nipkow@61784: apply (simp) nipkow@61784: apply (fastforce simp: Bp_if_B n2_type dest: n1_type) nipkow@61784: done nipkow@61784: wenzelm@67406: text\A detailed proof:\ nipkow@61784: nipkow@61784: lemma ins_type: nipkow@61784: shows "t \ B h \ ins x t \ Bp h" and "t \ U h \ ins x t \ T h" nipkow@61784: proof(induction h arbitrary: t) nipkow@61784: case 0 nipkow@61784: { case 1 thus ?case by simp nipkow@61784: next nipkow@61784: case 2 thus ?case by simp } nipkow@61784: next nipkow@61784: case (Suc h) nipkow@61784: { case 1 nipkow@61784: then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and nipkow@61784: t1: "t1 \ T h" and t2: "t2 \ T h" and t12: "t1 \ B h \ t2 \ B h" nipkow@61784: by auto nipkow@67040: have ?case if "x < a" nipkow@67040: proof - nipkow@67040: have "n2 (ins x t1) a t2 \ Bp (Suc h)" nipkow@61784: proof cases nipkow@61784: assume "t1 \ B h" nipkow@61784: with t2 show ?thesis by (simp add: Suc.IH(1) n2_type) nipkow@61784: next nipkow@61784: assume "t1 \ B h" nipkow@61784: hence 1: "t1 \ U h" and 2: "t2 \ B h" using t1 t12 by auto nipkow@61784: show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type) nipkow@61784: qed wenzelm@67406: with \x < a\ show ?case by simp nipkow@67040: qed nipkow@61784: moreover nipkow@67040: have ?case if "a < x" nipkow@67040: proof - nipkow@67040: have "n2 t1 a (ins x t2) \ Bp (Suc h)" nipkow@61784: proof cases nipkow@61784: assume "t2 \ B h" nipkow@61784: with t1 show ?thesis by (simp add: Suc.IH(1) n2_type) nipkow@61784: next nipkow@61784: assume "t2 \ B h" nipkow@61784: hence 1: "t1 \ B h" and 2: "t2 \ U h" using t2 t12 by auto nipkow@61784: show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type) nipkow@61784: qed wenzelm@67406: with \a < x\ show ?case by simp nipkow@67040: qed nipkow@67040: moreover nipkow@67040: have ?case if "x = a" nipkow@67040: proof - nipkow@61784: from 1 have "t \ Bp (Suc h)" by(rule Bp_if_B) wenzelm@67406: thus "?case" using \x = a\ by simp nipkow@67040: qed nipkow@61784: ultimately show ?case by auto nipkow@61784: next nipkow@61784: case 2 thus ?case using Suc(1) n1_type by fastforce } nipkow@61784: qed nipkow@61784: nipkow@61784: lemma insert_type: nipkow@61809: "t \ B h \ insert x t \ B h \ B (Suc h)" nipkow@61809: unfolding insert_def by (metis ins_type(1) tree_type) nipkow@61784: nipkow@61784: end nipkow@61784: nipkow@61789: subsubsection "Proofs for deletion" nipkow@61784: nipkow@61784: lemma B_simps[simp]: nipkow@61784: "N1 t \ B h = False" nipkow@61784: "L2 y \ B h = False" nipkow@61784: "(N3 t1 a1 t2 a2 t3) \ B h = False" nipkow@61784: "N0 \ B h \ h = 0" nipkow@61784: by (cases h, auto)+ nipkow@61784: nipkow@61784: context delete nipkow@61784: begin nipkow@61784: nipkow@61784: lemma n2_type1: nipkow@61784: "\t1 \ Um h; t2 \ B h\ \ n2 t1 a t2 \ T (Suc h)" nipkow@61784: apply(cases h rule: Bp.cases) nipkow@61784: apply auto[2] nipkow@61784: apply(erule exE bexE conjE imageE | simp | erule disjE)+ nipkow@61784: done nipkow@61784: nipkow@61784: lemma n2_type2: nipkow@61784: "\t1 \ B h ; t2 \ Um h \ \ n2 t1 a t2 \ T (Suc h)" nipkow@61784: apply(cases h rule: Bp.cases) nipkow@61784: apply auto[2] nipkow@61784: apply(erule exE bexE conjE imageE | simp | erule disjE)+ nipkow@61784: done nipkow@61784: nipkow@61784: lemma n2_type3: nipkow@61784: "\t1 \ T h ; t2 \ T h \ \ n2 t1 a t2 \ T (Suc h)" nipkow@61784: apply(cases h rule: Bp.cases) nipkow@61784: apply auto[2] nipkow@61784: apply(erule exE bexE conjE imageE | simp | erule disjE)+ nipkow@61784: done nipkow@61784: nipkow@68020: lemma split_minNoneN0: "\t \ B h; split_min t = None\ \ t = N0" nipkow@61784: by (cases t) (auto split: option.splits) nipkow@61784: nipkow@68020: lemma split_minNoneN1 : "\t \ U h; split_min t = None\ \ t = N1 N0" nipkow@68020: by (cases h) (auto simp: split_minNoneN0 split: option.splits) nipkow@61784: nipkow@68020: lemma split_min_type: nipkow@68020: "t \ B h \ split_min t = Some (a, t') \ t' \ T h" nipkow@68020: "t \ U h \ split_min t = Some (a, t') \ t' \ Um h" nipkow@61784: proof (induction h arbitrary: t a t') nipkow@61784: case (Suc h) nipkow@61784: { case 1 nipkow@61784: then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and nipkow@61784: t12: "t1 \ T h" "t2 \ T h" "t1 \ B h \ t2 \ B h" nipkow@61784: by auto nipkow@61784: show ?case nipkow@68020: proof (cases "split_min t1") nipkow@61784: case None nipkow@61784: show ?thesis nipkow@61784: proof cases nipkow@61784: assume "t1 \ B h" nipkow@68020: with split_minNoneN0[OF this None] 1 show ?thesis by(auto) nipkow@61784: next nipkow@61784: assume "t1 \ B h" nipkow@61784: thus ?thesis using 1 None by (auto) nipkow@61784: qed nipkow@61784: next nipkow@61784: case [simp]: (Some bt') nipkow@61784: obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce nipkow@61784: show ?thesis nipkow@61784: proof cases nipkow@61784: assume "t1 \ B h" nipkow@61784: from Suc.IH(1)[OF this] 1 have "t1' \ T h" by simp nipkow@61784: from n2_type3[OF this t12(2)] 1 show ?thesis by auto nipkow@61784: next nipkow@61784: assume "t1 \ B h" nipkow@61784: hence t1: "t1 \ U h" and t2: "t2 \ B h" using t12 by auto nipkow@61784: from Suc.IH(2)[OF t1] have "t1' \ Um h" by simp nipkow@61784: from n2_type1[OF this t2] 1 show ?thesis by auto nipkow@61784: qed nipkow@61784: qed nipkow@61784: } nipkow@61784: { case 2 nipkow@61784: then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \ B h" by auto nipkow@61784: show ?case nipkow@68020: proof (cases "split_min t1") nipkow@61784: case None nipkow@68020: with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto) nipkow@61784: next nipkow@61784: case [simp]: (Some bt') nipkow@61784: obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce nipkow@61784: from Suc.IH(1)[OF t1] have "t1' \ T h" by simp nipkow@61784: thus ?thesis using 2 by auto nipkow@61784: qed nipkow@61784: } nipkow@61784: qed auto nipkow@61784: nipkow@61784: lemma del_type: nipkow@61784: "t \ B h \ del x t \ T h" nipkow@61784: "t \ U h \ del x t \ Um h" nipkow@61784: proof (induction h arbitrary: x t) nipkow@61784: case (Suc h) nipkow@61784: { case 1 nipkow@61784: then obtain l a r where [simp]: "t = N2 l a r" and nipkow@61784: lr: "l \ T h" "r \ T h" "l \ B h \ r \ B h" by auto nipkow@67040: have ?case if "x < a" nipkow@67040: proof cases nipkow@67040: assume "l \ B h" nipkow@67040: from n2_type3[OF Suc.IH(1)[OF this] lr(2)] wenzelm@67406: show ?thesis using \x by(simp) nipkow@67040: next nipkow@67040: assume "l \ B h" nipkow@67040: hence "l \ U h" "r \ B h" using lr by auto nipkow@67040: from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)] wenzelm@67406: show ?thesis using \x by(simp) nipkow@67040: qed nipkow@67040: moreover nipkow@67040: have ?case if "x > a" nipkow@67040: proof cases nipkow@67040: assume "r \ B h" nipkow@67040: from n2_type3[OF lr(1) Suc.IH(1)[OF this]] wenzelm@67406: show ?thesis using \x>a\ by(simp) nipkow@67040: next nipkow@67040: assume "r \ B h" nipkow@67040: hence "l \ B h" "r \ U h" using lr by auto nipkow@67040: from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]] wenzelm@67406: show ?thesis using \x>a\ by(simp) nipkow@67040: qed nipkow@67040: moreover nipkow@67040: have ?case if [simp]: "x=a" nipkow@68020: proof (cases "split_min r") nipkow@67040: case None nipkow@67040: show ?thesis nipkow@61784: proof cases nipkow@61784: assume "r \ B h" nipkow@68020: with split_minNoneN0[OF this None] lr show ?thesis by(simp) nipkow@61784: next nipkow@61784: assume "r \ B h" nipkow@67040: hence "r \ U h" using lr by auto nipkow@68020: with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp) nipkow@61784: qed nipkow@67040: next nipkow@67040: case [simp]: (Some br') nipkow@67040: obtain b r' where [simp]: "br' = (b,r')" by fastforce nipkow@67040: show ?thesis nipkow@67040: proof cases nipkow@67040: assume "r \ B h" nipkow@68020: from split_min_type(1)[OF this] n2_type3[OF lr(1)] nipkow@67040: show ?thesis by simp nipkow@61784: next nipkow@67040: assume "r \ B h" nipkow@67040: hence "l \ B h" and "r \ U h" using lr by auto nipkow@68020: from split_min_type(2)[OF this(2)] n2_type2[OF this(1)] nipkow@67040: show ?thesis by simp nipkow@61784: qed nipkow@67040: qed nipkow@67040: ultimately show ?case by auto nipkow@61784: } nipkow@61784: { case 2 with Suc.IH(1) show ?case by auto } nipkow@61784: qed auto nipkow@61784: wenzelm@67613: lemma tree_type: "t \ T (h+1) \ tree t \ B (h+1) \ B h" nipkow@61784: by(auto) nipkow@61784: nipkow@61809: lemma delete_type: "t \ B h \ delete x t \ B h \ B(h-1)" nipkow@61784: unfolding delete_def nipkow@61809: by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1) nipkow@61784: nipkow@61784: end nipkow@61784: nipkow@61789: nipkow@61784: subsection "Overall correctness" nipkow@61784: nipkow@61784: interpretation Set_by_Ordered nipkow@61789: where empty = N0 and isin = isin and insert = insert.insert nipkow@61809: and delete = delete.delete and inorder = inorder and inv = "\t. \h. t \ B h" nipkow@61784: proof (standard, goal_cases) nipkow@61784: case 2 thus ?case by(auto intro!: isin_set) nipkow@61784: next nipkow@61784: case 3 thus ?case by(auto intro!: insert.inorder_insert) nipkow@61784: next nipkow@61792: case 4 thus ?case by(auto intro!: delete.inorder_delete) nipkow@61784: next nipkow@61784: case 6 thus ?case using insert.insert_type by blast nipkow@61784: next nipkow@61784: case 7 thus ?case using delete.delete_type by blast nipkow@61784: qed auto nipkow@61784: nipkow@63411: nipkow@63411: subsection \Height-Size Relation\ nipkow@63411: nipkow@63411: text \By Daniel St\"uwe\ nipkow@63411: nipkow@63411: fun fib_tree :: "nat \ unit bro" where nipkow@63411: "fib_tree 0 = N0" nipkow@63411: | "fib_tree (Suc 0) = N2 N0 () N0" nipkow@63411: | "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))" nipkow@63411: nipkow@63411: fun fib' :: "nat \ nat" where nipkow@63411: "fib' 0 = 0" nipkow@63411: | "fib' (Suc 0) = 1" nipkow@63411: | "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h" nipkow@63411: nipkow@63411: fun size :: "'a bro \ nat" where nipkow@63411: "size N0 = 0" nipkow@63411: | "size (N1 t) = size t" nipkow@63411: | "size (N2 t1 _ t2) = 1 + size t1 + size t2" nipkow@63411: nipkow@63411: lemma fib_tree_B: "fib_tree h \ B h" nipkow@63411: by (induction h rule: fib_tree.induct) auto nipkow@63411: nipkow@63411: declare [[names_short]] nipkow@63411: nipkow@63411: lemma size_fib': "size (fib_tree h) = fib' h" nipkow@63411: by (induction h rule: fib_tree.induct) auto nipkow@63411: nipkow@63411: lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))" nipkow@63411: by (induction h rule: fib_tree.induct) auto nipkow@63411: nipkow@63411: lemma B_N2_cases[consumes 1]: nipkow@63411: assumes "N2 t1 a t2 \ B (Suc n)" nipkow@63411: obtains nipkow@63411: (BB) "t1 \ B n" and "t2 \ B n" | nipkow@63411: (UB) "t1 \ U n" and "t2 \ B n" | nipkow@63411: (BU) "t1 \ B n" and "t2 \ U n" nipkow@63411: using assms by auto nipkow@63411: nipkow@63411: lemma size_bounded: "t \ B h \ size t \ size (fib_tree h)" nipkow@63411: unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct) nipkow@63411: case (3 h t') nipkow@63411: note main = 3 nipkow@63411: then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto nipkow@63411: with main have "N2 t1 a t2 \ B (Suc (Suc h))" by auto nipkow@63411: thus ?case proof (cases rule: B_N2_cases) nipkow@63411: case BB nipkow@63411: then obtain x y z where t2: "t2 = N2 x y z \ t2 = N2 z y x" "x \ B h" by auto nipkow@63411: show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto nipkow@63411: next nipkow@63411: case UB nipkow@63411: then obtain t11 where t1: "t1 = N1 t11" "t11 \ B h" by auto nipkow@63411: show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp nipkow@63411: next nipkow@63411: case BU nipkow@63411: then obtain t22 where t2: "t2 = N1 t22" "t22 \ B h" by auto nipkow@63411: show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp nipkow@63411: qed nipkow@63411: qed auto nipkow@63411: nipkow@63411: theorem "t \ B h \ fib (h + 2) \ size t + 1" nipkow@63411: using size_bounded nipkow@63411: by (simp add: size_fib' fibfib[symmetric] del: fib.simps) nipkow@63411: nipkow@61784: end