equal
deleted
inserted
replaced
33 |
33 |
34 |
34 |
35 subsection "Functional Correctness Proofs" |
35 subsection "Functional Correctness Proofs" |
36 |
36 |
37 lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))" |
37 lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))" |
38 by (induction t) (auto simp: elems_simps) |
38 by (induction t) (auto simp: elems_simps1) |
39 |
39 |
40 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))" |
40 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))" |
41 by (induction t) (auto simp: elems_simps0 dest: sortedD) |
41 by (induction t) (auto simp: elems_simps2) |
42 |
42 |
43 |
43 |
44 lemma inorder_insert: |
44 lemma inorder_insert: |
45 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
45 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
46 by(induction t) (auto simp: ins_simps) |
46 by(induction t) (auto simp: ins_simps) |