diff -r 140addd19343 -r f11e974b47e0 src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Fri Jan 27 12:32:49 2017 +0100 +++ b/src/HOL/Data_Structures/RBT_Set.thy Fri Jan 27 17:28:10 2017 +0100 @@ -91,7 +91,7 @@ subsection \Structural invariants\ -text\The proofs are due to Markus Reiter and Alexander Krauss,\ +text\The proofs are due to Markus Reiter and Alexander Krauss.\ fun color :: "'a rbt \ color" where "color Leaf = Black" | @@ -135,7 +135,8 @@ lemma invh_paint: "invh t \ invh (paint c t)" by (cases t) auto -lemma invc_bal: "\invc_sons l; invc_sons r\ \ invc (bal l a r)" +lemma invc_bal: + "\invc l \ invc_sons r \ invc_sons l \ invc r\ \ invc (bal l a r)" by (induct l a r rule: bal.induct) auto lemma bheight_bal: @@ -314,224 +315,4 @@ thus ?thesis by simp qed -text \By Daniel St\"uwe\ - -lemma color_RedE:"color t = Red \ invc t = - (\ l a r . t = R l a r \ color l = Black \ color r = Black \ invc l \ invc r)" -by (cases t) auto - -lemma rbt_induct[consumes 1]: - assumes "rbt t" - assumes [simp]: "P Leaf" - assumes "\ t l a r. \t = B l a r; invc t; invh t; Q(l); Q(r)\ \ P t" - assumes "\ t l a r. \t = R l a r; invc t; invh t; P(l); P(r)\ \ Q t" - assumes "\ t . P(t) \ Q(t)" - shows "P t" -using assms(1) unfolding rbt_def apply safe -proof (induction t rule: measure_induct[of size]) -case (1 t) - note * = 1 assms - show ?case proof (cases t) - case [simp]: (Node c l a r) - show ?thesis proof (cases c) - case Red thus ?thesis using 1 by simp - next - case [simp]: Black - show ?thesis - proof (cases "color l") - case Red - thus ?thesis using * by (cases "color r") (auto simp: color_RedE) - next - case Black - thus ?thesis using * by (cases "color r") (auto simp: color_RedE) - qed - qed - qed simp -qed - -lemma rbt_b_height: "rbt t \ bheight t * 2 \ height t" -by (induction t rule: rbt_induct[where Q="\ t. bheight t * 2 + 1 \ height t"]) auto - -lemma red_b_height: "invc t \ invh t \ bheight t * 2 + 1 \ height t" -apply (cases t) apply simp - using rbt_b_height unfolding rbt_def - by (cases "color t") fastforce+ - -lemma red_b_height2: "invc t \ invh t \ bheight t \ height t div 2" -using red_b_height by fastforce - -lemma rbt_b_height2: "bheight t \ height t" -by (induction t) auto - -lemma "rbt t \ size1 t \ 4 ^ (bheight t)" -by(induction t rule: rbt_induct[where Q="\ t. size1 t \ 2 * 4 ^ (bheight t)"]) auto - -text \Balanced red-balck tree with all black nodes:\ -inductive balB :: "nat \ unit rbt \ bool" where -"balB 0 Leaf" | -"balB h t \ balB (Suc h) (B t () t)" - -inductive_cases [elim!]: "balB 0 t" -inductive_cases [elim]: "balB (Suc h) t" - -lemma balB_hs: "balB h t \ bheight t = height t" -by (induction h t rule: "balB.induct") auto - -lemma balB_h: "balB h t \ h = height t" -by (induction h t rule: "balB.induct") auto - -lemma "rbt t \ balB (bheight t) t' \ size t' \ size t" -by (induction t arbitrary: t' - rule: rbt_induct[where Q="\ t . \ h t'. balB (bheight t) t' \ size t' \ size t"]) - fastforce+ - -lemma balB_bh: "invc t \ invh t \ balB (bheight t) t' \ size t' \ size t" -by (induction t arbitrary: t') (fastforce split: if_split_asm)+ - -lemma balB_bh3:"\ balB h t; balB (h' + h) t' \ \ size t \ size t'" -by (induction h t arbitrary: t' h' rule: balB.induct) fastforce+ - -corollary balB_bh3': "\ balB h t; balB h' t'; h \ h' \ \ size t \ size t'" -using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps) - -lemma exist_pt: "\ t . balB h t" -by (induction h) (auto intro: balB.intros) - -corollary compact_pt: - assumes "invc t" "invh t" "h \ bheight t" "balB h t'" - shows "size t' \ size t" -proof - - obtain t'' where "balB (bheight t) t''" using exist_pt by blast - thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto -qed - -lemma balB_bh2: "balB (bheight t) t'\ invc t \ invh t \ height t' \ height t" -apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct) -using balB_h rbt_b_height2 by auto - -lemma balB_rbt: "balB h t \ rbt t" -unfolding rbt_def -by (induction h t rule: balB.induct) auto - -lemma balB_size[simp]: "balB h t \ size1 t = 2^h" -by (induction h t rule: balB.induct) auto - -text \Red-black tree (except that the root may be red) of minimal size -for a given height:\ - -inductive RB :: "nat \ unit rbt \ bool" where -"RB 0 Leaf" | -"balB (h div 2) t \ RB h t' \ color t' = Red \ RB (Suc h) (B t' () t)" | -"balB (h div 2) t \ RB h t' \ color t' = Black \ RB (Suc h) (R t' () t)" - -lemmas RB.intros[intro] - -lemma RB_invc: "RB h t \ invc t" -apply (induction h t rule: RB.induct) -using balB_rbt unfolding rbt_def by auto - -lemma RB_h: "RB h t \ h = height t" -apply (induction h t rule: RB.induct) -using balB_h by auto - -lemma RB_mod: "RB h t \ (color t = Black \ h mod 2 = 0)" -apply (induction h t rule: RB.induct) -apply auto -by presburger - -lemma RB_b_height: "RB h t \ height t div 2 = bheight t" -proof (induction h t rule: RB.induct) - case 1 - thus ?case by auto -next - case (2 h t t') - with RB_mod obtain n where "2*n + 1 = h" - by (metis color.distinct(1) mult_div_mod_eq parity) - with 2 balB_h RB_h show ?case by auto -next - case (3 h t t') - with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast - with 3 balB_h RB_h show ?case by auto -qed - -lemma weak_RB_induct[consumes 1]: - "RB h t \ P 0 \\ \ (\h t t' c . balB (h div 2) t \ RB h t' \ - P h t' \ P (Suc h) (Node c t' () t)) \ P h t" -using RB.induct by metis - -lemma RB_invh: "RB h t \ invh t" -apply (induction h t rule: weak_RB_induct) - using balB_h balB_hs RB_h balB_rbt RB_b_height - unfolding rbt_def -by auto - -lemma RB_bheight_minimal: - "\RB (height t') t; invc t'; invh t'\ \ bheight t \ bheight t'" -using RB_b_height RB_h red_b_height2 by fastforce - -lemma RB_minimal: "RB (height t') t \ invh t \ invc t' \ invh t' \ size t \ size t'" -proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct) - case 1 thus ?case by auto -next - case (2 h t t'') - have ***: "size (Node c t'' () t) \ size t'" - if assms: - "\ (t' :: 'a rbt) . \ h = height t'; invh t''; invc t'; invh t' \ - \ size t'' \ size t'" - "Suc h = height t'" "balB (h div 2) t" "RB h t''" - "invc t'" "invh t'" "height l \ height r" - and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)" - for t' :: "'a rbt" and c l a r - proof - - from assms have inv: "invc r" "invh r" by auto - from assms have "height l = h" using max_def by auto - with RB_bheight_minimal[of l t''] have - "bheight t \ bheight r" using assms last by auto - with compact_pt[OF inv] balB_h balB_hs have - "size t \ size r" using assms(3) by auto moreover - have "size t'' \ size l" using assms last by auto ultimately - show ?thesis by simp - qed - - from 2 obtain c l a r where - t': "t' = Node c l a r" by (cases t') auto - with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto - show ?case proof (cases "height r \ height l") - case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto - next - case False - obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto - have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto - thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto - qed -qed - -lemma RB_size: "RB h t \ size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)" -by (induction h t rule: "RB.induct" ) auto - -lemma RB_exist: "\ t . RB h t" -proof (induction h) - case (Suc n) - obtain r where r: "balB (n div 2) r" using exist_pt by blast - obtain l where l: "RB n l" using Suc by blast - obtain t where - "color l = Red \ t = B l () r" - "color l = Black \ t = R l () r" by auto - with l and r have "RB (Suc n) t" by (cases "color l") auto - thus ?case by auto -qed auto - -lemma bound: - assumes "invc t" "invh t" and [simp]:"height t = h" - shows "size t \ 2^((h+1) div 2) + 2^(h div 2) - 2" -proof - - obtain t' where t': "RB h t'" using RB_exist by auto - show ?thesis using RB_size[OF t'] - RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t' - unfolding size1_def by auto -qed - -corollary "rbt t \ h = height t \ size t \ 2^((h+1) div 2) + 2^(h div 2) - 2" -using bound unfolding rbt_def by blast - end