equal
deleted
inserted
replaced
31 if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')" |
31 if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')" |
32 |
32 |
33 |
33 |
34 subsection "Functional Correctness Proofs" |
34 subsection "Functional Correctness Proofs" |
35 |
35 |
36 lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
36 lemma lookup_eq: |
|
37 "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
37 apply (induction t) |
38 apply (induction t) |
38 apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split) |
39 apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split) |
39 done |
40 done |
40 |
41 |
41 |
42 |
42 lemma inorder_update: |
43 lemma inorder_update: |
43 "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
44 "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
44 by(induction t) (auto simp: upd_list_sorteds sorted_lems) |
45 by(induction t) (auto simp: upd_list_simps) |
45 |
46 |
46 |
47 |
47 lemma del_minD: |
48 lemma del_minD: |
48 "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> |
49 "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> |
49 x # inorder t' = inorder t" |
50 x # inorder t' = inorder t" |