equal
deleted
inserted
replaced
28 EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')" |
28 EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')" |
29 |
29 |
30 |
30 |
31 subsection "Functional Correctness Proofs" |
31 subsection "Functional Correctness Proofs" |
32 |
32 |
33 lemma lookup_eq: |
33 lemma lookup_map_of: |
34 "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
34 "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
35 by (induction t) (auto simp: map_of_simps split: option.split) |
35 by (induction t) (auto simp: map_of_simps split: option.split) |
36 |
36 |
37 lemma inorder_update: |
37 lemma inorder_update: |
38 "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
38 "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
46 where empty = Leaf and lookup = lookup and update = update and delete = delete |
46 where empty = Leaf and lookup = lookup and update = update and delete = delete |
47 and inorder = inorder and inv = "\<lambda>_. True" |
47 and inorder = inorder and inv = "\<lambda>_. True" |
48 proof (standard, goal_cases) |
48 proof (standard, goal_cases) |
49 case 1 show ?case by simp |
49 case 1 show ?case by simp |
50 next |
50 next |
51 case 2 thus ?case by(simp add: lookup_eq) |
51 case 2 thus ?case by(simp add: lookup_map_of) |
52 next |
52 next |
53 case 3 thus ?case by(simp add: inorder_update) |
53 case 3 thus ?case by(simp add: inorder_update) |
54 next |
54 next |
55 case 4 thus ?case by(simp add: inorder_delete) |
55 case 4 thus ?case by(simp add: inorder_delete) |
56 qed auto |
56 qed auto |