# HG changeset patch # User nipkow # Date 1557397967 -7200 # Node ID 20d819b0a29de52f83ae32faee0f2017c310662a # Parent 4ce07be8ba17d020f2ae3c0a1db17e83042baba8 New version of tries diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/Data_Structures/Base_FDS.thy --- a/src/HOL/Data_Structures/Base_FDS.thy Wed May 08 21:28:34 2019 +0200 +++ b/src/HOL/Data_Structures/Base_FDS.thy Thu May 09 12:32:47 2019 +0200 @@ -1,3 +1,5 @@ +section "Common Basis Theory" + theory Base_FDS imports "HOL-Library.Pattern_Aliases" begin diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Wed May 08 21:28:34 2019 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Thu May 09 12:32:47 2019 +0200 @@ -1,5 +1,7 @@ (* Author: Tobias Nipkow *) +section "Sorting" + theory Sorting imports Complex_Main diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/Data_Structures/Trie.thy --- a/src/HOL/Data_Structures/Trie.thy Wed May 08 21:28:34 2019 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,278 +0,0 @@ -(* Author: Tobias Nipkow *) - -section \Trie and Patricia Trie Implementations of \mbox{\bool list set\}\ - -theory Trie -imports Set_Specs -begin - -hide_const (open) insert - -declare Let_def[simp] - - -subsection "Trie" - -datatype trie = Leaf | Node bool "trie * trie" - -text \The pairing allows things like \Node b (if \ then (l,r) else (r,l))\.\ - -fun isin :: "trie \ bool list \ bool" where -"isin Leaf ks = False" | -"isin (Node b (l,r)) ks = - (case ks of - [] \ b | - k#ks \ isin (if k then r else l) ks)" - -fun insert :: "bool list \ trie \ 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 \ trie * trie \ trie" where -"shrink_Node b lr = (if \ b \ lr = (Leaf,Leaf) then Leaf else Node b lr)" - -fun delete :: "bool list \ trie \ trie" where -"delete ks Leaf = Leaf" | -"delete ks (Node b (l,r)) = - (case ks of - [] \ shrink_Node False (l,r) | - k#ks' \ shrink_Node b (if k then (l, delete ks' r) else (delete ks' l, r)))" - -fun invar :: "trie \ bool" where -"invar Leaf = True" | -"invar (Node b (l,r)) = ((\ b \ l \ Leaf \ r \ Leaf) \ invar l \ invar r)" - - -subsubsection \Functional Correctness\ - -lemma isin_insert: "isin (insert as t) bs = (as = bs \ 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 \ bs \ 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 \ Leaf" -by(cases "(ks,t)" rule: insert.cases) auto - -lemma invar_insert: "invar t \ invar (insert ks t)" -by(induction ks t rule: insert.induct)(auto simp: insert_not_Leaf) - -lemma invar_delete: "invar t \ 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 = "\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 \ bool list \ 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 [] \ b | k#ks' \ isinP (if k then r else l) ks' - else False)" - -text \\split xs ys = (zs, xs', ys')\ iff - \zs\ is the longest common prefix of \xs\ and \ys\ and - \xs = zs @ xs'\ and \ys = zs @ ys'\\ -fun split where -"split [] ys = ([],[],ys)" | -"split xs [] = ([],xs,[])" | -"split (x#xs) (y#ys) = - (if x\y then ([],x#xs,y#ys) - else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))" - -fun insertP :: "bool list \ trieP \ 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') \ - 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',[]) \ - NodeP ps b (if k then (l,insertP ks' r) else (insertP ks' l, r)) | - (qs,[],p#ps') \ - let t = NodeP ps' b (l,r) - in NodeP qs True (if p then (LeafP, t) else (t, LeafP)) | - (qs,[],[]) \ 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) \ LeafP | - (LeafP, NodeP ps' b' lr') \ NodeP (ps @ True # ps') b' lr' | - (NodeP ps' b' lr', LeafP) \ NodeP (ps @ False # ps') b' lr' | - _ \ NodeP ps b lr)" - -fun deleteP :: "bool list \ trieP \ trieP" where -"deleteP ks LeafP = LeafP" | -"deleteP ks (NodeP ps b (l,r)) = - (case split ks ps of - (qs,_,p#ps') \ NodeP ps b (l,r) | - (qs,k#ks',[]) \ - shrink_NodeP ps b (if k then (l, deleteP ks' r) else (deleteP ks' l, r)) | - (qs,[],[]) \ shrink_NodeP ps False (l,r))" - -fun invarP :: "trieP \ bool" where -"invarP LeafP = True" | -"invarP (NodeP ps b (l,r)) = ((\b \ l \ LeafP \ r \ LeafP) \ invarP l \ invarP r)" - -text \The abstraction function(s):\ - -fun prefix_trie :: "bool list \ trie \ 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 \ 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 \Functional Correctness\ - -text \IsinP:\ - -lemma isin_prefix_trie: "isin (prefix_trie ps t) ks = - (length ks \ length ps \ - (let n = length ps in ps = take n ks \ 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 \Insert:\ - -lemma prefix_trie_Leaf_iff: "prefix_trie ps t = Leaf \ 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') \ - xs = zs @ xs' \ ys = zs @ ys' \ (xs' \ [] \ ys' \ [] \ hd xs' \ 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' \ isinP t ks')" -by (simp add: isin_insert isinP abs_trieP_insertP) - -lemma insertP_not_LeafP: "insertP ks t \ LeafP" -apply(induction ks t rule: insertP.induct) -apply(auto split: prod.split list.split) -done - -lemma invarP_insertP: "invarP t \ invarP (insertP ks t)" -apply(induction ks t rule: insertP.induct) -apply(auto simp: insertP_not_LeafP split: prod.split list.split) -done - -text \Delete:\ - -lemma invar_shrink_NodeP: "\ invarP l; invarP r \ \ invarP (shrink_NodeP ps b (l,r))" -by(auto split: trieP.split) - -lemma invarP_deleteP: "invarP t \ 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\ks' \ 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 = "\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 diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/Data_Structures/Trie_Fun.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Trie_Fun.thy Thu May 09 12:32:47 2019 +0200 @@ -0,0 +1,94 @@ +section \Tries via Functions\ + +theory Trie_Fun +imports + Set_Specs +begin + +text \A trie where each node maps a key to sub-tries via a function. +Nice abstract model. Not efficient because of the function space.\ + +datatype 'a trie = Lf | Nd bool "'a \ 'a trie option" + +fun isin :: "'a trie \ 'a list \ bool" where +"isin Lf xs = False" | +"isin (Nd b m) [] = b" | +"isin (Nd b m) (k # xs) = (case m k of None \ False | Some t \ isin t xs)" + +fun insert :: "('a::linorder) list \ 'a trie \ 'a trie" where +"insert [] Lf = Nd True (\x. None)" | +"insert [] (Nd b m) = Nd True m" | +"insert (x#xs) Lf = Nd False ((\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 \ Lf | Some t \ t))))" + +fun delete :: "('a::linorder) list \ 'a trie \ '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 \ m | + Some t \ m(x := Some(delete xs t)))" + +primrec set :: "'a trie \ 'a list set" where +"set Lf = {}" | +"set (Nd b m) = (if b then {[]} else {}) \ + (\a. case (map_option set o m) a of None \ {} | Some t \ (#) a ` t)" + +lemma set_Nd: + "set (Nd b m) = + (if b then {[]} else {}) \ + (\a. case m a of None \ {} | Some t \ (#) a ` set t)" +by (auto simp: split: option.splits) + +lemma isin_set: "isin t xs = (xs \ set t)" +apply(induction t xs rule: isin.induct) +apply (auto split: option.split) +done + +lemma set_insert: "set (insert xs t) = set t \ {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 = "\_. 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 diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/Data_Structures/Trie_Map.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Trie_Map.thy Thu May 09 12:32:47 2019 +0200 @@ -0,0 +1,112 @@ +section "Tries via Search Trees" + +theory Trie_Map +imports + RBT_Map + Trie_Fun +begin + +text \An implementation of tries based on maps implemented by red-black trees. +Works for any kind of search tree.\ + +text \Implementation of map:\ + +type_synonym 'a mapi = "'a rbt" + +datatype 'a trie_map = Lf | Nd bool "('a * 'a trie_map) mapi" + +text \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 \Tree_Map\, +and not just \RBT_Map\, except for the termination lemma \lookup_size\.\ + +lemma lookup_size[termination_simp]: + fixes t :: "('a::linorder * 'a trie_map) rbt" + shows "lookup t a = Some b \ size b < Suc (size_tree (\ab. Suc (size (snd ab))) (\x. 0) t)" +apply(induction t a rule: lookup.induct) +apply(auto split: if_splits) +done + +fun isin :: "('a::linorder) trie_map \ 'a list \ bool" where +"isin Lf xs = False" | +"isin (Nd b m) [] = b" | +"isin (Nd b m) (x # xs) = (case lookup m x of None \ False | Some t \ isin t xs)" + +fun insert :: "('a::linorder) list \ 'a trie_map \ '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 \ Lf | Some t \ t)) m)" + +fun delete :: "('a::linorder) list \ 'a trie_map \ '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 \ m | + Some t \ update x (delete xs t) m)" + + +subsection "Correctness" + +text \Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\ + +fun abs :: "'a::linorder trie_map \ 'a trie" where +"abs Lf = Trie_Fun.Lf" | +"abs (Nd b t) = Trie_Fun.Nd b (\a. map_option abs (lookup t a))" + +fun invar :: "('a::linorder)trie_map \ bool" where +"invar Lf = True" | +"invar (Nd b m) = (M.invar m \ (\a t. lookup m a = Some t \ 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 \ 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 \ 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 \ 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 \ invar (delete xs t)" +apply(induction xs t rule: delete.induct) +apply(auto simp: M.map_specs split: option.split) +done + +text \Overall correctness w.r.t. the \Set\ ADT:\ + +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 diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/Data_Structures/Tries_Binary.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Tries_Binary.thy Thu May 09 12:32:47 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 \ 'a * 'a \ 'a" where +"sel2 b (a1,a2) = (if b then a2 else a1)" + +fun mod2 :: "('a \ 'a) \ bool \ 'a * 'a \ '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 \ bool list \ bool" where +"isin Lf ks = False" | +"isin (Nd b lr) ks = + (case ks of + [] \ b | + k#ks \ isin (sel2 k lr) ks)" + +fun insert :: "bool list \ trie \ 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 \ isin t bs)" +apply(induction as t arbitrary: bs rule: insert.induct) +apply (auto split: list.splits if_splits) +done + +text \A simple implementation of delete; does not shrink the trie!\ + +fun delete0 :: "bool list \ trie \ trie" where +"delete0 ks Lf = Lf" | +"delete0 ks (Nd b lr) = + (case ks of + [] \ Nd False lr | + k#ks' \ Nd b (mod2 (delete0 ks') k lr))" + +lemma isin_delete0: "isin (delete0 as t) bs = (as \ bs \ isin t bs)" +apply(induction as t arbitrary: bs rule: delete0.induct) +apply (auto split: list.splits if_splits) +done + +text \Now deletion with shrinking:\ + +fun node :: "bool \ trie * trie \ trie" where +"node b lr = (if \ b \ lr = (Lf,Lf) then Lf else Nd b lr)" + +fun delete :: "bool list \ trie \ trie" where +"delete ks Lf = Lf" | +"delete ks (Nd b lr) = + (case ks of + [] \ node False lr | + k#ks' \ node b (mod2 (delete ks') k lr))" + +lemma isin_delete: "isin (delete as t) bs = (as \ bs \ 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 \ bool list set" where +"set_trie t = {xs. isin t xs}" + +lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \ {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 = "\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 \ bool list \ 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 [] \ b | k#ks' \ isinP (sel2 k lr) ks' + else False)" + +fun split where +"split [] ys = ([],[],ys)" | +"split xs [] = ([],xs,[])" | +"split (x#xs) (y#ys) = + (if x\y then ([],x#xs,y#ys) + else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))" + + +lemma mod2_cong[fundef_cong]: + "\ lr = lr'; k = k'; \a b. lr'=(a,b) \ f (a) = f' (a) ; \a b. lr'=(a,b) \ f (b) = f' (b) \ + \ mod2 f k lr= mod2 f' k' lr'" +by(cases lr, cases lr', auto) + +fun insertP :: "bool list \ ptrie \ 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') \ + 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',[]) \ + NdP ps b (mod2 (insertP ks') k lr) | + (qs,[],p#ps') \ + let t = NdP ps' b lr in + NdP qs True (if p then (LfP,t) else (t,LfP)) | + (qs,[],[]) \ NdP ps True lr)" + + +fun nodeP :: "bool list \ bool \ ptrie * ptrie \ ptrie" where +"nodeP ps b lr = (if \ b \ lr = (LfP,LfP) then LfP else NdP ps b lr)" + +fun deleteP :: "bool list \ ptrie \ ptrie" where +"deleteP ks LfP = LfP" | +"deleteP ks (NdP ps b lr) = + (case split ks ps of + (qs,ks',p#ps') \ NdP ps b lr | + (qs,k#ks',[]) \ nodeP ps b (mod2 (deleteP ks') k lr) | + (qs,[],[]) \ nodeP ps False lr)" + + +subsubsection \Functional Correctness\ + +text \First step: @{typ ptrie} implements @{typ trie} via the abstraction function \abs_ptrie\:\ + +fun prefix_trie :: "bool list \ trie \ 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 \ 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 \Correctness of @{const isinP}:\ + +lemma isin_prefix_trie: + "isin (prefix_trie ps t) ks + = (ps = take (length ps) ks \ 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 \Correctness of @{const insertP}:\ + +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') \ + ks = qs @ ks' \ ps = qs @ ps' \ (ks' \ [] \ ps' \ [] \ hd ks' \ 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 \Correctness of @{const deleteP}:\ + +lemma prefix_trie_Lf: "prefix_trie xs t = Lf \ xs = [] \ t = Lf" +by(cases xs)(auto) + +lemma abs_ptrie_Lf: "abs_ptrie t = Lf \ 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 \The overall correctness proof. Simply composes correctness lemmas.\ + +definition set_ptrie :: "ptrie \ bool list set" where +"set_ptrie = set_trie o abs_ptrie" + +lemma set_ptrie_insertP: "set_ptrie (insertP xs t) = set_ptrie t \ {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 = "\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 diff -r 4ce07be8ba17 -r 20d819b0a29d src/HOL/ROOT --- a/src/HOL/ROOT Wed May 08 21:28:34 2019 +0200 +++ b/src/HOL/ROOT Thu May 09 12:32:47 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"