equal
deleted
inserted
replaced
108 LT \<Rightarrow> baldL (delete x l) a ba r | |
108 LT \<Rightarrow> baldL (delete x l) a ba r | |
109 GT \<Rightarrow> baldR l a ba (delete x r))" |
109 GT \<Rightarrow> baldR l a ba (delete x r))" |
110 |
110 |
111 lemmas split_max_induct = split_max.induct[case_names Node Leaf] |
111 lemmas split_max_induct = split_max.induct[case_names Node Leaf] |
112 |
112 |
113 lemmas splits = if_splits tree.splits tree.splits tree_bal2.splits bal.splits |
113 lemmas splits = if_splits tree.splits tree_bal2.splits bal.splits |
114 |
114 |
115 subsection \<open>Proofs\<close> |
115 subsection \<open>Proofs\<close> |
116 |
116 |
117 lemma insert_Diff1[simp]: "insert x t \<noteq> Diff Leaf" |
117 lemma insert_Diff1[simp]: "insert x t \<noteq> Diff Leaf" |
118 by (cases t)(auto split!: splits) |
118 by (cases t)(auto split!: splits) |