# HG changeset patch # User nipkow # Date 1528896260 -7200 # Node ID 6826718f732dfa65da75d45e5d7819ea2abe9e9a # Parent c8101022e52af153e5dbe2a1af0aca62f7e4f836 qualify interpretations to avoid clashes diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/AA_Set.thy --- a/src/HOL/Data_Structures/AA_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/AA_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -485,7 +485,7 @@ (auto simp: del_list_simps inorder_adjust pre_adj_if_postL pre_adj_if_postR post_split_max post_delete split_maxD split: prod.splits) -interpretation I: Set_by_Ordered +interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = invar proof (standard, goal_cases) diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/AVL_Map.thy --- a/src/HOL/Data_Structures/AVL_Map.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/AVL_Map.thy Wed Jun 13 15:24:20 2018 +0200 @@ -25,12 +25,12 @@ subsection \Functional Correctness\ -theorem inorder_update_avl: +theorem inorder_update: "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR) -theorem inorder_delete_avl: +theorem inorder_delete: "sorted1(inorder t) \ inorder (delete x t) = del_list x (inorder t)" by(induction t) (auto simp: del_list_simps inorder_balL inorder_balR @@ -180,7 +180,7 @@ qed simp_all -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 = avl proof (standard, goal_cases) @@ -188,9 +188,9 @@ next case 2 thus ?case by(simp add: lookup_map_of) next - case 3 thus ?case by(simp add: inorder_update_avl) + case 3 thus ?case by(simp add: inorder_update) next - case 4 thus ?case by(simp add: inorder_delete_avl) + case 4 thus ?case by(simp add: inorder_delete) next case 5 show ?case by (simp add: empty_def) next diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/AVL_Set.thy --- a/src/HOL/Data_Structures/AVL_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/AVL_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -423,7 +423,7 @@ subsection "Overall correctness" -interpretation Set_by_Ordered +interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = avl proof (standard, goal_cases) diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/RBT_Map.thy --- a/src/HOL/Data_Structures/RBT_Map.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/RBT_Map.thy Wed Jun 13 15:24:20 2018 +0200 @@ -42,7 +42,7 @@ by(induction x y t rule: upd.induct) (auto simp: upd_list_simps inorder_baliL inorder_baliR) -lemma inorder_update_rbt: +lemma inorder_update: "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" by(simp add: update_def inorder_upd inorder_paint) @@ -51,7 +51,7 @@ by(induction x t rule: del.induct) (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) -lemma inorder_delete_rbt: +lemma inorder_delete: "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)" by(simp add: delete_def inorder_del inorder_paint) @@ -104,7 +104,7 @@ theorem rbt_delete: "rbt t \ rbt (delete k t)" by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint) -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 = rbt proof (standard, goal_cases) @@ -112,9 +112,9 @@ next case 2 thus ?case by(simp add: lookup_map_of) next - case 3 thus ?case by(simp add: inorder_update_rbt) + case 3 thus ?case by(simp add: inorder_update) next - case 4 thus ?case by(simp add: inorder_delete_rbt) + case 4 thus ?case by(simp add: inorder_delete) next case 5 thus ?case by (simp add: rbt_def empty_def) next diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/RBT_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -256,7 +256,7 @@ text \Overall correctness:\ -interpretation Set_by_Ordered +interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = rbt proof (standard, goal_cases) diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Set_Specs.thy --- a/src/HOL/Data_Structures/Set_Specs.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/Set_Specs.thy Wed Jun 13 15:24:20 2018 +0200 @@ -33,16 +33,16 @@ fixes isin :: "'t \ 'a \ bool" fixes inorder :: "'t \ 'a list" fixes inv :: "'t \ bool" -assumes empty: "inorder empty = []" +assumes inorder_empty: "inorder empty = []" assumes isin: "inv t \ sorted(inorder t) \ isin t x = (x \ set (inorder t))" -assumes insert: "inv t \ sorted(inorder t) \ +assumes inorder_insert: "inv t \ sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" -assumes delete: "inv t \ sorted(inorder t) \ +assumes inorder_delete: "inv t \ sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" -assumes inv_empty: "inv empty" -assumes inv_insert: "inv t \ sorted(inorder t) \ inv(insert x t)" -assumes inv_delete: "inv t \ sorted(inorder t) \ inv(delete x t)" +assumes inorder_inv_empty: "inv empty" +assumes inorder_inv_insert: "inv t \ sorted(inorder t) \ inv(insert x t)" +assumes inorder_inv_delete: "inv t \ sorted(inorder t) \ inv(delete x t)" begin text \It implements the traditional specification:\ @@ -56,20 +56,20 @@ sublocale Set empty insert delete isin set invar proof(standard, goal_cases) - case 1 show ?case by (auto simp: empty set_def) + case 1 show ?case by (auto simp: inorder_empty set_def) next case 2 thus ?case by(simp add: isin invar_def set_def) next - case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def) + case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def) next case (4 s x) thus ?case - by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def) + by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def) next - case 5 thus ?case by(simp add: empty inv_empty invar_def) + case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def) next - case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def) + case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def) next - case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def) + case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def) qed end diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree234_Map.thy --- a/src/HOL/Data_Structures/Tree234_Map.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/Tree234_Map.thy Wed Jun 13 15:24:20 2018 +0200 @@ -123,7 +123,7 @@ by(induction t) (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits) -lemma inorder_update_234: +lemma inorder_update: "sorted1(inorder t) \ inorder(update a b t) = upd_list a b (inorder t)" by(simp add: update_def inorder_upd) @@ -133,7 +133,7 @@ (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits) (* 30 secs (2016) *) -lemma inorder_delete_234: "\ bal t ; sorted1(inorder t) \ \ +lemma inorder_delete: "\ bal t ; sorted1(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" by(simp add: delete_def inorder_del) @@ -160,15 +160,15 @@ subsection \Overall Correctness\ -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 = bal proof (standard, goal_cases) case 2 thus ?case by(simp add: lookup_map_of) next - case 3 thus ?case by(simp add: inorder_update_234) + case 3 thus ?case by(simp add: inorder_update) next - case 4 thus ?case by(simp add: inorder_delete_234) + case 4 thus ?case by(simp add: inorder_delete) next case 6 thus ?case by(simp add: bal_update) next diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree234_Set.thy --- a/src/HOL/Data_Structures/Tree234_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/Tree234_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -504,7 +504,7 @@ subsection \Overall Correctness\ -interpretation Set_by_Ordered +interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = bal proof (standard, goal_cases) diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree23_Map.thy --- a/src/HOL/Data_Structures/Tree23_Map.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/Tree23_Map.thy Wed Jun 13 15:24:20 2018 +0200 @@ -81,7 +81,7 @@ "sorted1(inorder t) \ inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)" by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits) -corollary inorder_update_23: +corollary inorder_update: "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" by(simp add: update_def inorder_upd) @@ -91,7 +91,7 @@ by(induction t rule: del.induct) (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) -corollary inorder_delete_23: "\ bal t ; sorted1(inorder t) \ \ +corollary inorder_delete: "\ bal t ; sorted1(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" by(simp add: delete_def inorder_del) @@ -119,7 +119,7 @@ subsection \Overall Correctness\ -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 = bal proof (standard, goal_cases) @@ -127,9 +127,9 @@ next case 2 thus ?case by(simp add: lookup_map_of) next - case 3 thus ?case by(simp add: inorder_update_23) + case 3 thus ?case by(simp add: inorder_update) next - case 4 thus ?case by(simp add: inorder_delete_23) + case 4 thus ?case by(simp add: inorder_delete) next case 5 thus ?case by(simp add: empty_def) next diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree23_Set.thy --- a/src/HOL/Data_Structures/Tree23_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/Tree23_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -379,7 +379,7 @@ subsection \Overall Correctness\ -interpretation Set_by_Ordered +interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = bal proof (standard, goal_cases) diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree_Map.thy --- 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) \ 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) \ 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) \ 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 = "\_. 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 diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree_Set.thy --- a/src/HOL/Data_Structures/Tree_Set.thy Wed Jun 13 11:53:25 2018 +0200 +++ b/src/HOL/Data_Structures/Tree_Set.thy Wed Jun 13 15:24:20 2018 +0200 @@ -62,7 +62,7 @@ "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" by(induction t) (auto simp: del_list_simps split_minD split: prod.splits) -interpretation Set_by_Ordered +interpretation S: Set_by_Ordered where empty = empty and isin = isin and insert = insert and delete = delete and inorder = inorder and inv = "\_. True" proof (standard, goal_cases)