--- a/src/HOL/Data_Structures/Base_FDS.thy Thu May 09 16:40:58 2019 +0200
+++ b/src/HOL/Data_Structures/Base_FDS.thy Thu May 09 16:48:25 2019 +0200
@@ -1,3 +1,5 @@
+section "Common Basis Theory"
+
theory Base_FDS
imports "HOL-Library.Pattern_Aliases"
begin
--- a/src/HOL/Data_Structures/Sorting.thy Thu May 09 16:40:58 2019 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy Thu May 09 16:48:25 2019 +0200
@@ -1,5 +1,7 @@
(* Author: Tobias Nipkow *)
+section "Sorting"
+
theory Sorting
imports
Complex_Main
--- a/src/HOL/Data_Structures/Trie.thy Thu May 09 16:40:58 2019 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section \<open>Trie and Patricia Trie Implementations of \mbox{\<open>bool list set\<close>}\<close>
-
-theory Trie
-imports Set_Specs
-begin
-
-hide_const (open) insert
-
-declare Let_def[simp]
-
-
-subsection "Trie"
-
-datatype trie = Leaf | Node bool "trie * trie"
-
-text \<open>The pairing allows things like \<open>Node b (if \<dots> then (l,r) else (r,l))\<close>.\<close>
-
-fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
-"isin Leaf ks = False" |
-"isin (Node b (l,r)) ks =
- (case ks of
- [] \<Rightarrow> b |
- k#ks \<Rightarrow> isin (if k then r else l) ks)"
-
-fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"insert [] Leaf = Node True (Leaf,Leaf)" |
-"insert [] (Node b lr) = Node True lr" |
-"insert (k#ks) Leaf =
- Node False (if k then (Leaf, insert ks Leaf)
- else (insert ks Leaf, Leaf))" |
-"insert (k#ks) (Node b (l,r)) =
- Node b (if k then (l, insert ks r)
- else (insert ks l, r))"
-
-fun shrink_Node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
-"shrink_Node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)"
-
-fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"delete ks Leaf = Leaf" |
-"delete ks (Node b (l,r)) =
- (case ks of
- [] \<Rightarrow> shrink_Node False (l,r) |
- k#ks' \<Rightarrow> shrink_Node b (if k then (l, delete ks' r) else (delete ks' l, r)))"
-
-fun invar :: "trie \<Rightarrow> bool" where
-"invar Leaf = True" |
-"invar (Node b (l,r)) = ((\<not> b \<longrightarrow> l \<noteq> Leaf \<or> r \<noteq> Leaf) \<and> invar l \<and> invar r)"
-
-
-subsubsection \<open>Functional Correctness\<close>
-
-lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
-apply(induction as t arbitrary: bs rule: insert.induct)
-apply(auto split: list.splits)
-done
-
-lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
-apply(induction as t arbitrary: bs rule: delete.induct)
- apply simp
-apply (auto split: list.splits; fastforce)
-done
-
-lemma insert_not_Leaf: "insert ks t \<noteq> Leaf"
-by(cases "(ks,t)" rule: insert.cases) auto
-
-lemma invar_insert: "invar t \<Longrightarrow> invar (insert ks t)"
-by(induction ks t rule: insert.induct)(auto simp: insert_not_Leaf)
-
-lemma invar_delete: "invar t \<Longrightarrow> invar (delete ks t)"
-by(induction ks t rule: delete.induct)(auto split: list.split)
-
-interpretation T: Set
-where empty = Leaf and insert = insert and delete = delete and isin = isin
-and set = "\<lambda>t. {x. isin t x}" and invar = invar
-proof (standard, goal_cases)
- case 1 thus ?case by simp
-next
- case 2 thus ?case by simp
-next
- case 3 thus ?case by (auto simp add: isin_insert)
-next
- case 4 thus ?case by (auto simp add: isin_delete)
-next
- case 5 thus ?case by simp
-next
- case 6 thus ?case by (auto simp add: invar_insert)
-next
- case 7 thus ?case by (auto simp add: invar_delete)
-qed
-
-
-subsection "Patricia Trie"
-
-datatype trieP = LeafP | NodeP "bool list" bool "trieP * trieP"
-
-fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
-"isinP LeafP ks = False" |
-"isinP (NodeP ps b (l,r)) ks =
- (let n = length ps in
- if ps = take n ks
- then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (if k then r else l) ks'
- else False)"
-
-text \<open>\<open>split xs ys = (zs, xs', ys')\<close> iff
- \<open>zs\<close> is the longest common prefix of \<open>xs\<close> and \<open>ys\<close> and
- \<open>xs = zs @ xs'\<close> and \<open>ys = zs @ ys'\<close>\<close>
-fun split where
-"split [] ys = ([],[],ys)" |
-"split xs [] = ([],xs,[])" |
-"split (x#xs) (y#ys) =
- (if x\<noteq>y then ([],x#xs,y#ys)
- else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
-
-fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
-"insertP ks LeafP = NodeP ks True (LeafP,LeafP)" |
-"insertP ks (NodeP ps b (l,r)) =
- (case split ks ps of
- (qs,k#ks',p#ps') \<Rightarrow>
- let tp = NodeP ps' b (l,r); tk = NodeP ks' True (LeafP,LeafP)
- in NodeP qs False (if k then (tp,tk) else (tk,tp)) |
- (qs,k#ks',[]) \<Rightarrow>
- NodeP ps b (if k then (l,insertP ks' r) else (insertP ks' l, r)) |
- (qs,[],p#ps') \<Rightarrow>
- let t = NodeP ps' b (l,r)
- in NodeP qs True (if p then (LeafP, t) else (t, LeafP)) |
- (qs,[],[]) \<Rightarrow> NodeP ps True (l,r))"
-
-fun shrink_NodeP where
-"shrink_NodeP ps b lr = (if b then NodeP ps b lr else
- case lr of
- (LeafP, LeafP) \<Rightarrow> LeafP |
- (LeafP, NodeP ps' b' lr') \<Rightarrow> NodeP (ps @ True # ps') b' lr' |
- (NodeP ps' b' lr', LeafP) \<Rightarrow> NodeP (ps @ False # ps') b' lr' |
- _ \<Rightarrow> NodeP ps b lr)"
-
-fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
-"deleteP ks LeafP = LeafP" |
-"deleteP ks (NodeP ps b (l,r)) =
- (case split ks ps of
- (qs,_,p#ps') \<Rightarrow> NodeP ps b (l,r) |
- (qs,k#ks',[]) \<Rightarrow>
- shrink_NodeP ps b (if k then (l, deleteP ks' r) else (deleteP ks' l, r)) |
- (qs,[],[]) \<Rightarrow> shrink_NodeP ps False (l,r))"
-
-fun invarP :: "trieP \<Rightarrow> bool" where
-"invarP LeafP = True" |
-"invarP (NodeP ps b (l,r)) = ((\<not>b \<longrightarrow> l \<noteq> LeafP \<or> r \<noteq> LeafP) \<and> invarP l \<and> invarP r)"
-
-text \<open>The abstraction function(s):\<close>
-
-fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"prefix_trie [] t = t" |
-"prefix_trie (k#ks) t =
- (let t' = prefix_trie ks t in shrink_Node False (if k then (Leaf,t') else (t',Leaf)))"
-
-fun abs_trieP :: "trieP \<Rightarrow> trie" where
-"abs_trieP LeafP = Leaf" |
-"abs_trieP (NodeP ps b (l,r)) = prefix_trie ps (Node b (abs_trieP l, abs_trieP r))"
-
-
-subsubsection \<open>Functional Correctness\<close>
-
-text \<open>IsinP:\<close>
-
-lemma isin_prefix_trie: "isin (prefix_trie ps t) ks =
- (length ks \<ge> length ps \<and>
- (let n = length ps in ps = take n ks \<and> isin t (drop n ks)))"
-by(induction ps arbitrary: ks)(auto split: list.split)
-
-lemma isinP: "isinP t ks = isin (abs_trieP t) ks"
-apply(induction t arbitrary: ks rule: abs_trieP.induct)
- apply(auto simp: isin_prefix_trie split: list.split)
- using nat_le_linear apply force
-using nat_le_linear apply force
-done
-
-text \<open>Insert:\<close>
-
-lemma prefix_trie_Leaf_iff: "prefix_trie ps t = Leaf \<longleftrightarrow> t = Leaf"
-by (induction ps) auto
-
-lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf"
-by(induction ks) (auto simp: prefix_trie_Leaf_iff)
-
-lemma prefix_trie_Leaf: "prefix_trie ps Leaf = Leaf"
-by(induction ps) auto
-
-lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
-by(induction ks) (auto simp: prefix_trie_Leaf_iff insert_not_Leaf prefix_trie_Leaf)
-
-lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
-by(induction ps) auto
-
-lemma split_iff: "split xs ys = (zs, xs', ys') \<longleftrightarrow>
- xs = zs @ xs' \<and> ys = zs @ ys' \<and> (xs' \<noteq> [] \<and> ys' \<noteq> [] \<longrightarrow> hd xs' \<noteq> hd ys')"
-proof(induction xs ys arbitrary: zs xs' ys' rule: split.induct)
- case 1 thus ?case by auto
-next
- case 2 thus ?case by auto
-next
- case 3 thus ?case by(clarsimp simp: Cons_eq_append_conv split: prod.splits if_splits) auto
-qed
-
-lemma abs_trieP_insertP:
- "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
-apply(induction t arbitrary: ks)
-apply(auto simp: prefix_trie_Leafs insert_append prefix_trie_append
- prefix_trie_Leaf_iff split_iff split: list.split prod.split)
-done
-
-corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' \<or> isinP t ks')"
-by (simp add: isin_insert isinP abs_trieP_insertP)
-
-lemma insertP_not_LeafP: "insertP ks t \<noteq> LeafP"
-apply(induction ks t rule: insertP.induct)
-apply(auto split: prod.split list.split)
-done
-
-lemma invarP_insertP: "invarP t \<Longrightarrow> invarP (insertP ks t)"
-apply(induction ks t rule: insertP.induct)
-apply(auto simp: insertP_not_LeafP split: prod.split list.split)
-done
-
-text \<open>Delete:\<close>
-
-lemma invar_shrink_NodeP: "\<lbrakk> invarP l; invarP r \<rbrakk> \<Longrightarrow> invarP (shrink_NodeP ps b (l,r))"
-by(auto split: trieP.split)
-
-lemma invarP_deleteP: "invarP t \<Longrightarrow> invarP (deleteP ks t)"
-apply(induction t arbitrary: ks)
-apply(auto simp: invar_shrink_NodeP split_iff simp del: shrink_NodeP.simps
- split!: list.splits prod.split if_splits)
-done
-
-lemma delete_append:
- "delete (ks @ ks') (prefix_trie ks t) = prefix_trie ks (delete ks' t)"
-by(induction ks) auto
-
-lemma abs_trieP_shrink_NodeP:
- "abs_trieP (shrink_NodeP ps b (l,r)) = prefix_trie ps (shrink_Node b (abs_trieP l, abs_trieP r))"
-apply(induction ps arbitrary: b l r)
-apply (auto simp: prefix_trie_Leaf prefix_trie_Leaf_iff prefix_trie_append
- split!: trieP.splits if_splits)
-done
-
-lemma abs_trieP_deleteP:
- "abs_trieP (deleteP ks t) = delete ks (abs_trieP t)"
-apply(induction t arbitrary: ks)
-apply(auto simp: prefix_trie_Leafs delete_append prefix_trie_Leaf
- abs_trieP_shrink_NodeP prefix_trie_append split_iff
- simp del: shrink_NodeP.simps split!: list.split prod.split if_splits)
-done
-
-corollary isinP_deleteP: "isinP (deleteP ks t) ks' = (ks\<noteq>ks' \<and> isinP t ks')"
-by (simp add: isin_delete isinP abs_trieP_deleteP)
-
-interpretation PT: Set
-where empty = LeafP and insert = insertP and delete = deleteP
-and isin = isinP and set = "\<lambda>t. {x. isinP t x}" and invar = invarP
-proof (standard, goal_cases)
- case 1 thus ?case by (simp)
-next
- case 2 thus ?case by (simp)
-next
- case 3 thus ?case by (auto simp add: isinP_insertP)
-next
- case 4 thus ?case by (auto simp add: isinP_deleteP)
-next
- case 5 thus ?case by (simp)
-next
- case 6 thus ?case by (simp add: invarP_insertP)
-next
- case 7 thus ?case by (auto simp add: invarP_deleteP)
-qed
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Trie_Fun.thy Thu May 09 16:48:25 2019 +0200
@@ -0,0 +1,94 @@
+section \<open>Tries via Functions\<close>
+
+theory Trie_Fun
+imports
+ Set_Specs
+begin
+
+text \<open>A trie where each node maps a key to sub-tries via a function.
+Nice abstract model. Not efficient because of the function space.\<close>
+
+datatype 'a trie = Lf | Nd bool "'a \<Rightarrow> 'a trie option"
+
+fun isin :: "'a trie \<Rightarrow> 'a list \<Rightarrow> bool" where
+"isin Lf xs = False" |
+"isin (Nd b m) [] = b" |
+"isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
+
+fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+"insert [] Lf = Nd True (\<lambda>x. None)" |
+"insert [] (Nd b m) = Nd True m" |
+"insert (x#xs) Lf = Nd False ((\<lambda>x. None)(x := Some(insert xs Lf)))" |
+"insert (x#xs) (Nd b m) =
+ Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> Lf | Some t \<Rightarrow> t))))"
+
+fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+"delete xs Lf = Lf" |
+"delete [] (Nd b m) = Nd False m" |
+"delete (x#xs) (Nd b m) = Nd b
+ (case m x of
+ None \<Rightarrow> m |
+ Some t \<Rightarrow> m(x := Some(delete xs t)))"
+
+primrec set :: "'a trie \<Rightarrow> 'a list set" where
+"set Lf = {}" |
+"set (Nd b m) = (if b then {[]} else {}) \<union>
+ (\<Union>a. case (map_option set o m) a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` t)"
+
+lemma set_Nd:
+ "set (Nd b m) =
+ (if b then {[]} else {}) \<union>
+ (\<Union>a. case m a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` set t)"
+by (auto simp: split: option.splits)
+
+lemma isin_set: "isin t xs = (xs \<in> set t)"
+apply(induction t xs rule: isin.induct)
+apply (auto split: option.split)
+done
+
+lemma set_insert: "set (insert xs t) = set t \<union> {xs}"
+proof(induction xs t rule: insert.induct)
+ case 1 thus ?case by simp
+next
+ case 2 thus ?case by simp
+next
+ case 3 thus ?case by simp (subst set_eq_iff, simp)
+next
+ case 4
+ thus ?case
+ apply(simp)
+ apply(subst set_eq_iff)
+ apply(auto split!: if_splits option.splits)
+ apply fastforce
+ by (metis imageI option.sel)
+qed
+
+lemma set_delete: "set (delete xs t) = set t - {xs}"
+proof(induction xs t rule: delete.induct)
+ case 1 thus ?case by simp
+next
+ case 2 thus ?case by (force split: option.splits)
+next
+ case 3
+ thus ?case
+ apply (auto simp add: image_iff split!: if_splits option.splits)
+ apply blast
+ apply (metis insertE insertI2 insert_Diff_single option.inject)
+ apply blast
+ by (metis insertE insertI2 insert_Diff_single option.inject)
+qed
+
+interpretation S: Set
+where empty = Lf and isin = isin and insert = insert and delete = delete
+and set = set and invar = "\<lambda>_. True"
+proof (standard, goal_cases)
+ case 1 show ?case by (simp)
+next
+ case 2 thus ?case by(simp add: isin_set)
+next
+ case 3 thus ?case by(simp add: set_insert)
+next
+ case 4 thus ?case by(simp add: set_delete)
+qed (rule TrueI)+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Trie_Map.thy Thu May 09 16:48:25 2019 +0200
@@ -0,0 +1,112 @@
+section "Tries via Search Trees"
+
+theory Trie_Map
+imports
+ RBT_Map
+ Trie_Fun
+begin
+
+text \<open>An implementation of tries based on maps implemented by red-black trees.
+Works for any kind of search tree.\<close>
+
+text \<open>Implementation of map:\<close>
+
+type_synonym 'a mapi = "'a rbt"
+
+datatype 'a trie_map = Lf | Nd bool "('a * 'a trie_map) mapi"
+
+text \<open>In principle one should be able to given an implementation of tries
+once and for all for any map implementation and not just for a specific one (RBT) as done here.
+But because the map (@{typ "'a rbt"}) is used in a datatype, the HOL type system does not support this.
+
+However, the development below works verbatim for any map implementation, eg \<open>Tree_Map\<close>,
+and not just \<open>RBT_Map\<close>, except for the termination lemma \<open>lookup_size\<close>.\<close>
+
+lemma lookup_size[termination_simp]:
+ fixes t :: "('a::linorder * 'a trie_map) rbt"
+ shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc (size (snd ab))) (\<lambda>x. 0) t)"
+apply(induction t a rule: lookup.induct)
+apply(auto split: if_splits)
+done
+
+fun isin :: "('a::linorder) trie_map \<Rightarrow> 'a list \<Rightarrow> bool" where
+"isin Lf xs = False" |
+"isin (Nd b m) [] = b" |
+"isin (Nd b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
+
+fun insert :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
+"insert [] Lf = Nd True empty" |
+"insert [] (Nd b m) = Nd True m" |
+"insert (x#xs) Lf = Nd False (update x (insert xs Lf) empty)" |
+"insert (x#xs) (Nd b m) =
+ Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> Lf | Some t \<Rightarrow> t)) m)"
+
+fun delete :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
+"delete xs Lf = Lf" |
+"delete [] (Nd b m) = Nd False m" |
+"delete (x#xs) (Nd b m) = Nd b
+ (case lookup m x of
+ None \<Rightarrow> m |
+ Some t \<Rightarrow> update x (delete xs t) m)"
+
+
+subsection "Correctness"
+
+text \<open>Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\<close>
+
+fun abs :: "'a::linorder trie_map \<Rightarrow> 'a trie" where
+"abs Lf = Trie_Fun.Lf" |
+"abs (Nd b t) = Trie_Fun.Nd b (\<lambda>a. map_option abs (lookup t a))"
+
+fun invar :: "('a::linorder)trie_map \<Rightarrow> bool" where
+"invar Lf = True" |
+"invar (Nd b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar t))"
+
+lemma isin_abs: "isin t xs = Trie_Fun.isin (abs t) xs"
+apply(induction t xs rule: isin.induct)
+apply(auto split: option.split)
+done
+
+lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun.insert xs (abs t)"
+apply(induction xs t rule: insert.induct)
+apply(auto simp: M.map_specs split: option.split)
+done
+
+lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun.delete xs (abs t)"
+apply(induction xs t rule: delete.induct)
+apply(auto simp: M.map_specs split: option.split)
+done
+
+lemma invar_insert: "invar t \<Longrightarrow> invar (insert xs t)"
+apply(induction xs t rule: insert.induct)
+apply(auto simp: M.map_specs split: option.split)
+done
+
+lemma invar_delete: "invar t \<Longrightarrow> invar (delete xs t)"
+apply(induction xs t rule: delete.induct)
+apply(auto simp: M.map_specs split: option.split)
+done
+
+text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close>
+
+interpretation S2: Set
+where empty = Lf and isin = isin and insert = insert and delete = delete
+and set = "set o abs" and invar = invar
+proof (standard, goal_cases)
+ case 1 show ?case by (simp)
+next
+ case 2 thus ?case by (simp add: isin_set isin_abs)
+next
+ case 3 thus ?case by (simp add: set_insert abs_insert)
+next
+ case 4 thus ?case by (simp add: set_delete abs_delete)
+next
+ case 5 thus ?case by (simp)
+next
+ case 6 thus ?case by (simp add: invar_insert)
+next
+ case 7 thus ?case by (simp add: invar_delete)
+qed
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Tries_Binary.thy Thu May 09 16:48:25 2019 +0200
@@ -0,0 +1,264 @@
+(* Author: Tobias Nipkow *)
+
+section "Binary Tries and Patricia Tries"
+
+theory Tries_Binary
+imports Set_Specs
+begin
+
+hide_const (open) insert
+
+declare Let_def[simp]
+
+fun sel2 :: "bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a" where
+"sel2 b (a1,a2) = (if b then a2 else a1)"
+
+fun mod2 :: "('a \<Rightarrow> 'a) \<Rightarrow> bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a * 'a" where
+"mod2 f b (a1,a2) = (if b then (a1,f a2) else (f a1,a2))"
+
+
+subsection "Trie"
+
+datatype trie = Lf | Nd bool "trie * trie"
+
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
+"isin Lf ks = False" |
+"isin (Nd b lr) ks =
+ (case ks of
+ [] \<Rightarrow> b |
+ k#ks \<Rightarrow> isin (sel2 k lr) ks)"
+
+fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"insert [] Lf = Nd True (Lf,Lf)" |
+"insert [] (Nd b lr) = Nd True lr" |
+"insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
+"insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
+
+lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
+apply(induction as t arbitrary: bs rule: insert.induct)
+apply (auto split: list.splits if_splits)
+done
+
+text \<open>A simple implementation of delete; does not shrink the trie!\<close>
+
+fun delete0 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"delete0 ks Lf = Lf" |
+"delete0 ks (Nd b lr) =
+ (case ks of
+ [] \<Rightarrow> Nd False lr |
+ k#ks' \<Rightarrow> Nd b (mod2 (delete0 ks') k lr))"
+
+lemma isin_delete0: "isin (delete0 as t) bs = (as \<noteq> bs \<and> isin t bs)"
+apply(induction as t arbitrary: bs rule: delete0.induct)
+apply (auto split: list.splits if_splits)
+done
+
+text \<open>Now deletion with shrinking:\<close>
+
+fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
+"node b lr = (if \<not> b \<and> lr = (Lf,Lf) then Lf else Nd b lr)"
+
+fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"delete ks Lf = Lf" |
+"delete ks (Nd b lr) =
+ (case ks of
+ [] \<Rightarrow> node False lr |
+ k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
+
+lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
+apply(induction as t arbitrary: bs rule: delete.induct)
+ apply simp
+apply (auto split: list.splits if_splits)
+ apply (metis isin.simps(1))
+ apply (metis isin.simps(1))
+ done
+
+definition set_trie :: "trie \<Rightarrow> bool list set" where
+"set_trie t = {xs. isin t xs}"
+
+lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
+by(auto simp add: isin_insert set_trie_def)
+
+interpretation S: Set
+where empty = Lf and isin = isin and insert = insert and delete = delete
+and set = set_trie and invar = "\<lambda>t. True"
+proof (standard, goal_cases)
+ case 1 show ?case by (simp add: set_trie_def)
+next
+ case 2 thus ?case by(simp add: set_trie_def)
+next
+ case 3 thus ?case by(auto simp: set_trie_insert)
+next
+ case 4 thus ?case by(auto simp: isin_delete set_trie_def)
+qed (rule TrueI)+
+
+
+subsection "Patricia Trie"
+
+datatype ptrie = LfP | NdP "bool list" bool "ptrie * ptrie"
+
+fun isinP :: "ptrie \<Rightarrow> bool list \<Rightarrow> bool" where
+"isinP LfP ks = False" |
+"isinP (NdP ps b lr) ks =
+ (let n = length ps in
+ if ps = take n ks
+ then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
+ else False)"
+
+fun split where
+"split [] ys = ([],[],ys)" |
+"split xs [] = ([],xs,[])" |
+"split (x#xs) (y#ys) =
+ (if x\<noteq>y then ([],x#xs,y#ys)
+ else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
+
+
+lemma mod2_cong[fundef_cong]:
+ "\<lbrakk> lr = lr'; k = k'; \<And>a b. lr'=(a,b) \<Longrightarrow> f (a) = f' (a) ; \<And>a b. lr'=(a,b) \<Longrightarrow> f (b) = f' (b) \<rbrakk>
+ \<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
+by(cases lr, cases lr', auto)
+
+fun insertP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+"insertP ks LfP = NdP ks True (LfP,LfP)" |
+"insertP ks (NdP ps b lr) =
+ (case split ks ps of
+ (qs,k#ks',p#ps') \<Rightarrow>
+ let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
+ NdP qs False (if k then (tp,tk) else (tk,tp)) |
+ (qs,k#ks',[]) \<Rightarrow>
+ NdP ps b (mod2 (insertP ks') k lr) |
+ (qs,[],p#ps') \<Rightarrow>
+ let t = NdP ps' b lr in
+ NdP qs True (if p then (LfP,t) else (t,LfP)) |
+ (qs,[],[]) \<Rightarrow> NdP ps True lr)"
+
+
+fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> ptrie * ptrie \<Rightarrow> ptrie" where
+"nodeP ps b lr = (if \<not> b \<and> lr = (LfP,LfP) then LfP else NdP ps b lr)"
+
+fun deleteP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+"deleteP ks LfP = LfP" |
+"deleteP ks (NdP ps b lr) =
+ (case split ks ps of
+ (qs,ks',p#ps') \<Rightarrow> NdP ps b lr |
+ (qs,k#ks',[]) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
+ (qs,[],[]) \<Rightarrow> nodeP ps False lr)"
+
+
+subsubsection \<open>Functional Correctness\<close>
+
+text \<open>First step: @{typ ptrie} implements @{typ trie} via the abstraction function \<open>abs_ptrie\<close>:\<close>
+
+fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"prefix_trie [] t = t" |
+"prefix_trie (k#ks) t =
+ (let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"
+
+fun abs_ptrie :: "ptrie \<Rightarrow> trie" where
+"abs_ptrie LfP = Lf" |
+"abs_ptrie (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_ptrie l, abs_ptrie r))"
+
+
+text \<open>Correctness of @{const isinP}:\<close>
+
+lemma isin_prefix_trie:
+ "isin (prefix_trie ps t) ks
+ = (ps = take (length ps) ks \<and> isin t (drop (length ps) ks))"
+apply(induction ps arbitrary: ks)
+apply(auto split: list.split)
+done
+
+lemma isinP:
+ "isinP t ks = isin (abs_ptrie t) ks"
+apply(induction t arbitrary: ks rule: abs_ptrie.induct)
+ apply(auto simp: isin_prefix_trie split: list.split)
+done
+
+
+text \<open>Correctness of @{const insertP}:\<close>
+
+lemma prefix_trie_Lfs: "prefix_trie ks (Nd True (Lf,Lf)) = insert ks Lf"
+apply(induction ks)
+apply auto
+done
+
+lemma insert_prefix_trie_same:
+ "insert ps (prefix_trie ps (Nd b lr)) = prefix_trie ps (Nd True lr)"
+apply(induction ps)
+apply auto
+done
+
+lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
+apply(induction ks)
+apply auto
+done
+
+lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
+apply(induction ps)
+apply auto
+done
+
+lemma split_if: "split ks ps = (qs, ks', ps') \<Longrightarrow>
+ ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
+apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
+apply(auto split: prod.splits if_splits)
+done
+
+lemma abs_ptrie_insertP:
+ "abs_ptrie (insertP ks t) = insert ks (abs_ptrie t)"
+apply(induction t arbitrary: ks)
+apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
+ dest!: split_if split: list.split prod.split if_splits)
+done
+
+
+text \<open>Correctness of @{const deleteP}:\<close>
+
+lemma prefix_trie_Lf: "prefix_trie xs t = Lf \<longleftrightarrow> xs = [] \<and> t = Lf"
+by(cases xs)(auto)
+
+lemma abs_ptrie_Lf: "abs_ptrie t = Lf \<longleftrightarrow> t = LfP"
+by(cases t) (auto simp: prefix_trie_Lf)
+
+lemma delete_prefix_trie:
+ "delete xs (prefix_trie xs (Nd b (l,r)))
+ = (if (l,r) = (Lf,Lf) then Lf else prefix_trie xs (Nd False (l,r)))"
+by(induction xs)(auto simp: prefix_trie_Lf)
+
+lemma delete_append_prefix_trie:
+ "delete (xs @ ys) (prefix_trie xs t)
+ = (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
+by(induction xs)(auto simp: prefix_trie_Lf)
+
+lemma delete_abs_ptrie:
+ "delete ks (abs_ptrie t) = abs_ptrie (deleteP ks t)"
+apply(induction t arbitrary: ks)
+apply(auto simp: delete_prefix_trie delete_append_prefix_trie
+ prefix_trie_append prefix_trie_Lf abs_ptrie_Lf
+ dest!: split_if split: if_splits list.split prod.split)
+done
+
+
+text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
+
+definition set_ptrie :: "ptrie \<Rightarrow> bool list set" where
+"set_ptrie = set_trie o abs_ptrie"
+
+lemma set_ptrie_insertP: "set_ptrie (insertP xs t) = set_ptrie t \<union> {xs}"
+by(simp add: abs_ptrie_insertP set_trie_insert set_ptrie_def)
+
+interpretation SP: Set
+where empty = LfP and isin = isinP and insert = insertP and delete = deleteP
+and set = set_ptrie and invar = "\<lambda>t. True"
+proof (standard, goal_cases)
+ case 1 show ?case by (simp add: set_ptrie_def set_trie_def)
+next
+ case 2 thus ?case by(simp add: isinP set_ptrie_def set_trie_def)
+next
+ case 3 thus ?case by (auto simp: set_ptrie_insertP)
+next
+ case 4 thus ?case
+ by(auto simp: isin_delete set_ptrie_def set_trie_def simp flip: delete_abs_ptrie)
+qed (rule TrueI)+
+
+end
--- a/src/HOL/ROOT Thu May 09 16:40:58 2019 +0200
+++ b/src/HOL/ROOT Thu May 09 16:48:25 2019 +0200
@@ -233,7 +233,9 @@
AA_Map
Set2_Join_RBT
Array_Braun
- Trie
+ Trie_Fun
+ Trie_Map
+ Tries_Binary
Leftist_Heap
Binomial_Heap
document_files "root.tex" "root.bib"