simplified types
authornipkow
Sat May 11 15:27:11 2019 +0200 (6 months ago)
changeset 70262e12779b8f5b6
parent 70261 efbdfcaa6258
child 70263 805250bb7363
simplified types
src/HOL/Data_Structures/Trie_Fun.thy
src/HOL/Data_Structures/Trie_Map.thy
     1.1 --- a/src/HOL/Data_Structures/Trie_Fun.thy	Fri May 10 11:20:02 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Trie_Fun.thy	Sat May 11 15:27:11 2019 +0200
     1.3 @@ -8,33 +8,33 @@
     1.4  text \<open>A trie where each node maps a key to sub-tries via a function.
     1.5  Nice abstract model. Not efficient because of the function space.\<close>
     1.6  
     1.7 -datatype 'a trie = Lf | Nd bool "'a \<Rightarrow> 'a trie option"
     1.8 +datatype 'a trie = Nd bool "'a \<Rightarrow> 'a trie option"
     1.9  
    1.10  fun isin :: "'a trie \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.11 -"isin Lf xs = False" |
    1.12  "isin (Nd b m) [] = b" |
    1.13  "isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
    1.14  
    1.15  fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
    1.16 -"insert [] Lf = Nd True (\<lambda>x. None)" |
    1.17  "insert [] (Nd b m) = Nd True m" |
    1.18 -"insert (x#xs) Lf = Nd False ((\<lambda>x. None)(x := Some(insert xs Lf)))" |
    1.19  "insert (x#xs) (Nd b m) =
    1.20 -   Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> Lf | Some t \<Rightarrow> t))))"
    1.21 +   Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> Nd False (\<lambda>_. None) | Some t \<Rightarrow> t))))"
    1.22  
    1.23  fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
    1.24 -"delete xs Lf = Lf" |
    1.25  "delete [] (Nd b m) = Nd False m" |
    1.26  "delete (x#xs) (Nd b m) = Nd b
    1.27     (case m x of
    1.28        None \<Rightarrow> m |
    1.29        Some t \<Rightarrow> m(x := Some(delete xs t)))"
    1.30  
    1.31 +text \<open>The actual definition of \<open>set\<close> is a bit cryptic but canonical, to enable
    1.32 +primrec to prove termination:\<close>
    1.33 +
    1.34  primrec set :: "'a trie \<Rightarrow> 'a list set" where
    1.35 -"set Lf = {}" |
    1.36  "set (Nd b m) = (if b then {[]} else {}) \<union>
    1.37      (\<Union>a. case (map_option set o m) a of None \<Rightarrow> {} | Some t \<Rightarrow> (#) a ` t)"
    1.38  
    1.39 +text \<open>This is the more human-readable version:\<close>
    1.40 +
    1.41  lemma set_Nd:
    1.42    "set (Nd b m) =
    1.43       (if b then {[]} else {}) \<union>
    1.44 @@ -50,11 +50,7 @@
    1.45  proof(induction xs t rule: insert.induct)
    1.46    case 1 thus ?case by simp
    1.47  next
    1.48 -  case 2 thus ?case by simp
    1.49 -next
    1.50 -  case 3 thus ?case by simp (subst set_eq_iff, simp)
    1.51 -next
    1.52 -  case 4
    1.53 +  case 2
    1.54    thus ?case
    1.55      apply(simp)
    1.56      apply(subst set_eq_iff)
    1.57 @@ -65,11 +61,9 @@
    1.58  
    1.59  lemma set_delete: "set (delete xs t) = set t - {xs}"
    1.60  proof(induction xs t rule: delete.induct)
    1.61 -  case 1 thus ?case by simp
    1.62 +  case 1 thus ?case by (force split: option.splits)
    1.63  next
    1.64 -  case 2 thus ?case by (force split: option.splits)
    1.65 -next
    1.66 -  case 3
    1.67 +  case 2
    1.68    thus ?case
    1.69      apply (auto simp add: image_iff split!: if_splits option.splits)
    1.70         apply blast
    1.71 @@ -79,7 +73,7 @@
    1.72  qed
    1.73  
    1.74  interpretation S: Set
    1.75 -where empty = Lf and isin = isin and insert = insert and delete = delete
    1.76 +where empty = "Nd False (\<lambda>_. None)" and isin = isin and insert = insert and delete = delete
    1.77  and set = set and invar = "\<lambda>_. True"
    1.78  proof (standard, goal_cases)
    1.79    case 1 show ?case by (simp)
     2.1 --- a/src/HOL/Data_Structures/Trie_Map.thy	Fri May 10 11:20:02 2019 +0200
     2.2 +++ b/src/HOL/Data_Structures/Trie_Map.thy	Sat May 11 15:27:11 2019 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  type_synonym 'a mapi = "'a rbt"
     2.6  
     2.7 -datatype 'a trie_map = Lf | Nd bool "('a * 'a trie_map) mapi"
     2.8 +datatype 'a trie_map = Nd bool "('a * 'a trie_map) mapi"
     2.9  
    2.10  text \<open>In principle one should be able to given an implementation of tries
    2.11  once and for all for any map implementation and not just for a specific one (RBT) as done here.
    2.12 @@ -30,19 +30,15 @@
    2.13  done
    2.14  
    2.15  fun isin :: "('a::linorder) trie_map \<Rightarrow> 'a list \<Rightarrow> bool" where
    2.16 -"isin Lf xs = False" |
    2.17  "isin (Nd b m) [] = b" |
    2.18  "isin (Nd b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
    2.19  
    2.20  fun insert :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
    2.21 -"insert [] Lf = Nd True empty" |
    2.22  "insert [] (Nd b m) = Nd True m" |
    2.23 -"insert (x#xs) Lf = Nd False (update x (insert xs Lf) empty)" |
    2.24  "insert (x#xs) (Nd b m) =
    2.25 -  Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> Lf | Some t \<Rightarrow> t)) m)"
    2.26 +  Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> Nd False Leaf | Some t \<Rightarrow> t)) m)"
    2.27  
    2.28  fun delete :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
    2.29 -"delete xs Lf = Lf" |
    2.30  "delete [] (Nd b m) = Nd False m" |
    2.31  "delete (x#xs) (Nd b m) = Nd b
    2.32     (case lookup m x of
    2.33 @@ -55,31 +51,29 @@
    2.34  text \<open>Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\<close>
    2.35  
    2.36  fun abs :: "'a::linorder trie_map \<Rightarrow> 'a trie" where
    2.37 -"abs Lf = Trie_Fun.Lf" |
    2.38 -"abs (Nd b t) = Trie_Fun.Nd b (\<lambda>a. map_option abs (lookup t a))"
    2.39 +"abs (Nd b t) = Trie_Fun0.Nd b (\<lambda>a. map_option abs (lookup t a))"
    2.40  
    2.41  fun invar :: "('a::linorder)trie_map \<Rightarrow> bool" where
    2.42 -"invar Lf = True" |
    2.43  "invar (Nd b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar t))"
    2.44  
    2.45 -lemma isin_abs: "isin t xs = Trie_Fun.isin (abs t) xs"
    2.46 +lemma isin_abs: "isin t xs = Trie_Fun0.isin (abs t) xs"
    2.47  apply(induction t xs rule: isin.induct)
    2.48  apply(auto split: option.split)
    2.49  done
    2.50  
    2.51 -lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun.insert xs (abs t)"
    2.52 +lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun0.insert xs (abs t)"
    2.53  apply(induction xs t rule: insert.induct)
    2.54 -apply(auto simp: M.map_specs split: option.split)
    2.55 +apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split)
    2.56  done
    2.57  
    2.58 -lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun.delete xs (abs t)"
    2.59 +lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun0.delete xs (abs t)"
    2.60  apply(induction xs t rule: delete.induct)
    2.61  apply(auto simp: M.map_specs split: option.split)
    2.62  done
    2.63  
    2.64  lemma invar_insert: "invar t \<Longrightarrow> invar (insert xs t)"
    2.65  apply(induction xs t rule: insert.induct)
    2.66 -apply(auto simp: M.map_specs split: option.split)
    2.67 +apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split)
    2.68  done
    2.69  
    2.70  lemma invar_delete: "invar t \<Longrightarrow> invar (delete xs t)"
    2.71 @@ -90,7 +84,7 @@
    2.72  text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close>
    2.73  
    2.74  interpretation S2: Set
    2.75 -where empty = Lf and isin = isin and insert = insert and delete = delete
    2.76 +where empty = "Nd False Leaf" and isin = isin and insert = insert and delete = delete
    2.77  and set = "set o abs" and invar = invar
    2.78  proof (standard, goal_cases)
    2.79    case 1 show ?case by (simp)
    2.80 @@ -101,7 +95,7 @@
    2.81  next
    2.82    case 4 thus ?case by (simp add: set_delete abs_delete)
    2.83  next
    2.84 -  case 5 thus ?case by (simp)
    2.85 +  case 5 thus ?case by (simp add: M.map_specs RBT_Set.empty_def[symmetric])
    2.86  next
    2.87    case 6 thus ?case by (simp add: invar_insert)
    2.88  next