Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Data_Structures/Tree_Map.thy
changeset 68440 6826718f732d
parent 68431 b294e095f64c 
--- a/src/HOL/Data_Structures/Tree_Map.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -34,15 +34,15 @@
   "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
 by (induction t) (auto simp: map_of_simps split: option.split)
 
-lemma inorder_update_tree:
+lemma inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
 by(induction t) (auto simp: upd_list_simps)
 
-lemma inorder_delete_tree:
+lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
 
-interpretation Map_by_Ordered
+interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
@@ -50,9 +50,9 @@
 next
   case 2 thus ?case by(simp add: lookup_map_of)
 next
-  case 3 thus ?case by(simp add: inorder_update_tree)
+  case 3 thus ?case by(simp add: inorder_update)
 next
-  case 4 thus ?case by(simp add: inorder_delete_tree)
+  case 4 thus ?case by(simp add: inorder_delete)
 qed auto
 
 end
isabelle