# HG changeset patch
# User nipkow
# Date 1722514054 -7200
# Node ID 06350a8745c99ab17cf2c795254a94dd1621c185
# Parent  161286c9d426dd80b2d2545794aad016c0d3e8a3
tuned names

diff -r 161286c9d426 -r 06350a8745c9 src/HOL/Data_Structures/Trie_Fun.thy
--- a/src/HOL/Data_Structures/Trie_Fun.thy	Wed Jul 31 10:36:28 2024 +0200
+++ b/src/HOL/Data_Structures/Trie_Fun.thy	Thu Aug 01 14:07:34 2024 +0200
@@ -37,31 +37,31 @@
    x # ys \<Rightarrow> (case m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t ys))"
 by(cases xs)auto
 
-definition set :: "'a trie \<Rightarrow> 'a list set" where
-[simp]: "set t = {xs. isin t xs}"
+definition set_trie :: "'a trie \<Rightarrow> 'a list set" where
+[simp]: "set_trie t = {xs. isin t xs}"
 
-lemma isin_set: "isin t xs = (xs \<in> set t)"
+lemma isin_set_trie: "isin t xs = (xs \<in> set_trie t)"
 by simp
 
-lemma set_insert: "set (insert xs t) = set t \<union> {xs}"
+lemma set_trie_insert: "set_trie (insert xs t) = set_trie t \<union> {xs}"
 by (induction xs t rule: insert.induct)
    (auto simp: isin_case split!: if_splits option.splits list.splits)
 
-lemma set_delete: "set (delete xs t) = set t - {xs}"
+lemma set_trie_delete: "set_trie (delete xs t) = set_trie t - {xs}"
 by (induction xs t rule: delete.induct)
    (auto simp: isin_case split!: if_splits option.splits list.splits)
 
 interpretation S: Set
 where empty = empty and isin = isin and insert = insert and delete = delete
-and set = set and invar = "\<lambda>_. True"
+and set = set_trie and invar = "\<lambda>_. True"
 proof (standard, goal_cases)
   case 1 show ?case by (simp add: isin_case split: list.split)
 next
-  case 2 show ?case by(rule isin_set)
+  case 2 show ?case by(rule isin_set_trie)
 next
-  case 3 show ?case by(rule set_insert)
+  case 3 show ?case by(rule set_trie_insert)
 next
-  case 4 show ?case by(rule set_delete)
+  case 4 show ?case by(rule set_trie_delete)
 qed (rule TrueI)+
 
 end
diff -r 161286c9d426 -r 06350a8745c9 src/HOL/Data_Structures/Trie_Ternary.thy
--- a/src/HOL/Data_Structures/Trie_Ternary.thy	Wed Jul 31 10:36:28 2024 +0200
+++ b/src/HOL/Data_Structures/Trie_Ternary.thy	Thu Aug 01 14:07:34 2024 +0200
@@ -103,15 +103,15 @@
 
 interpretation S2: Set
 where empty = empty3 and isin = isin3 and insert = insert3 and delete = delete3
-and set = "set o abs3" and invar = invar3
+and set = "set_trie o abs3" and invar = invar3
 proof (standard, goal_cases)
   case 1 show ?case by (simp add: isin_case split: list.split)
 next
   case 2 thus ?case by (simp add: isin_abs3)
 next
-  case 3 thus ?case by (simp add: set_insert abs3_insert3 del: set_def)
+  case 3 thus ?case by (simp add: set_trie_insert abs3_insert3 del: set_trie_def)
 next
-  case 4 thus ?case by (simp add: set_delete abs3_delete3 del: set_def)
+  case 4 thus ?case by (simp add: set_trie_delete abs3_delete3 del: set_trie_def)
 next
   case 5 thus ?case by (simp add: M.map_specs Tree_Set.empty_def[symmetric])
 next