equal
deleted
inserted
replaced
45 |
45 |
46 |
46 |
47 subsection "Functional Correctness Proofs" |
47 subsection "Functional Correctness Proofs" |
48 |
48 |
49 lemma inorder_paint: "inorder(paint c t) = inorder t" |
49 lemma inorder_paint: "inorder(paint c t) = inorder t" |
50 by(induction t) (auto) |
50 by(cases t) (auto) |
51 |
51 |
52 lemma inorder_bal: |
52 lemma inorder_bal: |
53 "inorder(bal l a r) = inorder l @ a # inorder r" |
53 "inorder(bal l a r) = inorder l @ a # inorder r" |
54 by(induction l a r rule: bal.induct) (auto) |
54 by(cases "(l,a,r)" rule: bal.cases) (auto) |
55 |
55 |
56 lemma inorder_ins: |
56 lemma inorder_ins: |
57 "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)" |
57 "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)" |
58 by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal) |
58 by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal) |
59 |
59 |
61 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
61 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
62 by (simp add: insert_def inorder_ins inorder_paint) |
62 by (simp add: insert_def inorder_ins inorder_paint) |
63 |
63 |
64 lemma inorder_balL: |
64 lemma inorder_balL: |
65 "inorder(balL l a r) = inorder l @ a # inorder r" |
65 "inorder(balL l a r) = inorder l @ a # inorder r" |
66 by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_paint) |
66 by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint) |
67 |
67 |
68 lemma inorder_balR: |
68 lemma inorder_balR: |
69 "inorder(balR l a r) = inorder l @ a # inorder r" |
69 "inorder(balR l a r) = inorder l @ a # inorder r" |
70 by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_paint) |
70 by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint) |
71 |
71 |
72 lemma inorder_combine: |
72 lemma inorder_combine: |
73 "inorder(combine l r) = inorder l @ inorder r" |
73 "inorder(combine l r) = inorder l @ inorder r" |
74 by(induction l r rule: combine.induct) |
74 by(induction l r rule: combine.induct) |
75 (auto simp: inorder_balL inorder_balR split: tree.split color.split) |
75 (auto simp: inorder_balL inorder_balR split: tree.split color.split) |