6 begin |
6 begin |
7 |
7 |
8 text \<open>A trie where each node maps a key to sub-tries via a function. |
8 text \<open>A trie where each node maps a key to sub-tries via a function. |
9 Nice abstract model. Not efficient because of the function space.\<close> |
9 Nice abstract model. Not efficient because of the function space.\<close> |
10 |
10 |
11 datatype 'a trie = Lf | Nd bool "'a \<Rightarrow> 'a trie option" |
11 datatype 'a trie = Nd bool "'a \<Rightarrow> 'a trie option" |
12 |
12 |
13 fun isin :: "'a trie \<Rightarrow> 'a list \<Rightarrow> bool" where |
13 fun isin :: "'a trie \<Rightarrow> 'a list \<Rightarrow> bool" where |
14 "isin Lf xs = False" | |
|
15 "isin (Nd b m) [] = b" | |
14 "isin (Nd b m) [] = b" | |
16 "isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)" |
15 "isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)" |
17 |
16 |
18 fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where |
17 fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where |
19 "insert [] Lf = Nd True (\<lambda>x. None)" | |
|
20 "insert [] (Nd b m) = Nd True m" | |
18 "insert [] (Nd b m) = Nd True m" | |
21 "insert (x#xs) Lf = Nd False ((\<lambda>x. None)(x := Some(insert xs Lf)))" | |
|
22 "insert (x#xs) (Nd b m) = |
19 "insert (x#xs) (Nd b m) = |
23 Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> Lf | Some t \<Rightarrow> t))))" |
20 Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> Nd False (\<lambda>_. None) | Some t \<Rightarrow> t))))" |
24 |
21 |
25 fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where |
22 fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where |
26 "delete xs Lf = Lf" | |
|
27 "delete [] (Nd b m) = Nd False m" | |
23 "delete [] (Nd b m) = Nd False m" | |
28 "delete (x#xs) (Nd b m) = Nd b |
24 "delete (x#xs) (Nd b m) = Nd b |
29 (case m x of |
25 (case m x of |
30 None \<Rightarrow> m | |
26 None \<Rightarrow> m | |
31 Some t \<Rightarrow> m(x := Some(delete xs t)))" |
27 Some t \<Rightarrow> m(x := Some(delete xs t)))" |
32 |
28 |
|
29 text \<open>The actual definition of \<open>set\<close> is a bit cryptic but canonical, to enable |
|
30 primrec to prove termination:\<close> |
|
31 |
33 primrec set :: "'a trie \<Rightarrow> 'a list set" where |
32 primrec set :: "'a trie \<Rightarrow> 'a list set" where |
34 "set Lf = {}" | |
|
35 "set (Nd b m) = (if b then {[]} else {}) \<union> |
33 "set (Nd b m) = (if b then {[]} else {}) \<union> |
36 (\<Union>a. case (map_option set o m) a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` t)" |
34 (\<Union>a. case (map_option set o m) a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` t)" |
|
35 |
|
36 text \<open>This is the more human-readable version:\<close> |
37 |
37 |
38 lemma set_Nd: |
38 lemma set_Nd: |
39 "set (Nd b m) = |
39 "set (Nd b m) = |
40 (if b then {[]} else {}) \<union> |
40 (if b then {[]} else {}) \<union> |
41 (\<Union>a. case m a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` set t)" |
41 (\<Union>a. case m a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` set t)" |
48 |
48 |
49 lemma set_insert: "set (insert xs t) = set t \<union> {xs}" |
49 lemma set_insert: "set (insert xs t) = set t \<union> {xs}" |
50 proof(induction xs t rule: insert.induct) |
50 proof(induction xs t rule: insert.induct) |
51 case 1 thus ?case by simp |
51 case 1 thus ?case by simp |
52 next |
52 next |
53 case 2 thus ?case by simp |
53 case 2 |
54 next |
|
55 case 3 thus ?case by simp (subst set_eq_iff, simp) |
|
56 next |
|
57 case 4 |
|
58 thus ?case |
54 thus ?case |
59 apply(simp) |
55 apply(simp) |
60 apply(subst set_eq_iff) |
56 apply(subst set_eq_iff) |
61 apply(auto split!: if_splits option.splits) |
57 apply(auto split!: if_splits option.splits) |
62 apply fastforce |
58 apply fastforce |
63 by (metis imageI option.sel) |
59 by (metis imageI option.sel) |
64 qed |
60 qed |
65 |
61 |
66 lemma set_delete: "set (delete xs t) = set t - {xs}" |
62 lemma set_delete: "set (delete xs t) = set t - {xs}" |
67 proof(induction xs t rule: delete.induct) |
63 proof(induction xs t rule: delete.induct) |
68 case 1 thus ?case by simp |
64 case 1 thus ?case by (force split: option.splits) |
69 next |
65 next |
70 case 2 thus ?case by (force split: option.splits) |
66 case 2 |
71 next |
|
72 case 3 |
|
73 thus ?case |
67 thus ?case |
74 apply (auto simp add: image_iff split!: if_splits option.splits) |
68 apply (auto simp add: image_iff split!: if_splits option.splits) |
75 apply blast |
69 apply blast |
76 apply (metis insertE insertI2 insert_Diff_single option.inject) |
70 apply (metis insertE insertI2 insert_Diff_single option.inject) |
77 apply blast |
71 apply blast |
78 by (metis insertE insertI2 insert_Diff_single option.inject) |
72 by (metis insertE insertI2 insert_Diff_single option.inject) |
79 qed |
73 qed |
80 |
74 |
81 interpretation S: Set |
75 interpretation S: Set |
82 where empty = Lf and isin = isin and insert = insert and delete = delete |
76 where empty = "Nd False (\<lambda>_. None)" and isin = isin and insert = insert and delete = delete |
83 and set = set and invar = "\<lambda>_. True" |
77 and set = set and invar = "\<lambda>_. True" |
84 proof (standard, goal_cases) |
78 proof (standard, goal_cases) |
85 case 1 show ?case by (simp) |
79 case 1 show ?case by (simp) |
86 next |
80 next |
87 case 2 thus ?case by(simp add: isin_set) |
81 case 2 thus ?case by(simp add: isin_set) |