equal
deleted
inserted
replaced
146 subsection "Functional Correctness" |
146 subsection "Functional Correctness" |
147 |
147 |
148 subsubsection "Proofs for isin" |
148 subsubsection "Proofs for isin" |
149 |
149 |
150 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))" |
150 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))" |
151 by (induction t) (auto simp: isin_simps ball_Un) |
151 by (induction t) (auto simp: isin_simps) |
152 |
152 |
153 |
153 |
154 subsubsection "Proofs for insert" |
154 subsubsection "Proofs for insert" |
155 |
155 |
156 lemma inorder_ins: |
156 lemma inorder_ins: |