qualify interpretations to avoid clashes
authornipkow
Wed Jun 13 15:24:20 2018 +0200 (11 days ago)
changeset 684406826718f732d
parent 68439 c8101022e52a
child 68441 3b11d48a711a
qualify interpretations to avoid clashes
src/HOL/Data_Structures/AA_Set.thy
src/HOL/Data_Structures/AVL_Map.thy
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Set_Specs.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     1.3 @@ -485,7 +485,7 @@
     1.4    (auto simp: del_list_simps inorder_adjust pre_adj_if_postL pre_adj_if_postR 
     1.5                post_split_max post_delete split_maxD split: prod.splits)
     1.6  
     1.7 -interpretation I: Set_by_Ordered
     1.8 +interpretation S: Set_by_Ordered
     1.9  where empty = empty and isin = isin and insert = insert and delete = delete
    1.10  and inorder = inorder and inv = invar
    1.11  proof (standard, goal_cases)
     2.1 --- a/src/HOL/Data_Structures/AVL_Map.thy	Wed Jun 13 11:53:25 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Wed Jun 13 15:24:20 2018 +0200
     2.3 @@ -25,12 +25,12 @@
     2.4  
     2.5  subsection \<open>Functional Correctness\<close>
     2.6  
     2.7 -theorem inorder_update_avl:
     2.8 +theorem inorder_update:
     2.9    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    2.10  by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR)
    2.11  
    2.12  
    2.13 -theorem inorder_delete_avl:
    2.14 +theorem inorder_delete:
    2.15    "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
    2.16  by(induction t)
    2.17    (auto simp: del_list_simps inorder_balL inorder_balR
    2.18 @@ -180,7 +180,7 @@
    2.19  qed simp_all
    2.20  
    2.21  
    2.22 -interpretation Map_by_Ordered
    2.23 +interpretation M: Map_by_Ordered
    2.24  where empty = empty and lookup = lookup and update = update and delete = delete
    2.25  and inorder = inorder and inv = avl
    2.26  proof (standard, goal_cases)
    2.27 @@ -188,9 +188,9 @@
    2.28  next
    2.29    case 2 thus ?case by(simp add: lookup_map_of)
    2.30  next
    2.31 -  case 3 thus ?case by(simp add: inorder_update_avl)
    2.32 +  case 3 thus ?case by(simp add: inorder_update)
    2.33  next
    2.34 -  case 4 thus ?case by(simp add: inorder_delete_avl)
    2.35 +  case 4 thus ?case by(simp add: inorder_delete)
    2.36  next
    2.37    case 5 show ?case by (simp add: empty_def)
    2.38  next
     3.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     3.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     3.3 @@ -423,7 +423,7 @@
     3.4  
     3.5  subsection "Overall correctness"
     3.6  
     3.7 -interpretation Set_by_Ordered
     3.8 +interpretation S: Set_by_Ordered
     3.9  where empty = empty and isin = isin and insert = insert and delete = delete
    3.10  and inorder = inorder and inv = avl
    3.11  proof (standard, goal_cases)
     4.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Wed Jun 13 11:53:25 2018 +0200
     4.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Wed Jun 13 15:24:20 2018 +0200
     4.3 @@ -42,7 +42,7 @@
     4.4  by(induction x y t rule: upd.induct)
     4.5    (auto simp: upd_list_simps inorder_baliL inorder_baliR)
     4.6  
     4.7 -lemma inorder_update_rbt:
     4.8 +lemma inorder_update:
     4.9    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    4.10  by(simp add: update_def inorder_upd inorder_paint)
    4.11  
    4.12 @@ -51,7 +51,7 @@
    4.13  by(induction x t rule: del.induct)
    4.14    (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
    4.15  
    4.16 -lemma inorder_delete_rbt:
    4.17 +lemma inorder_delete:
    4.18    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    4.19  by(simp add: delete_def inorder_del inorder_paint)
    4.20  
    4.21 @@ -104,7 +104,7 @@
    4.22  theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
    4.23  by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
    4.24  
    4.25 -interpretation Map_by_Ordered
    4.26 +interpretation M: Map_by_Ordered
    4.27  where empty = empty and lookup = lookup and update = update and delete = delete
    4.28  and inorder = inorder and inv = rbt
    4.29  proof (standard, goal_cases)
    4.30 @@ -112,9 +112,9 @@
    4.31  next
    4.32    case 2 thus ?case by(simp add: lookup_map_of)
    4.33  next
    4.34 -  case 3 thus ?case by(simp add: inorder_update_rbt)
    4.35 +  case 3 thus ?case by(simp add: inorder_update)
    4.36  next
    4.37 -  case 4 thus ?case by(simp add: inorder_delete_rbt)
    4.38 +  case 4 thus ?case by(simp add: inorder_delete)
    4.39  next
    4.40    case 5 thus ?case by (simp add: rbt_def empty_def) 
    4.41  next
     5.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     5.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     5.3 @@ -256,7 +256,7 @@
     5.4  
     5.5  text \<open>Overall correctness:\<close>
     5.6  
     5.7 -interpretation Set_by_Ordered
     5.8 +interpretation S: Set_by_Ordered
     5.9  where empty = empty and isin = isin and insert = insert and delete = delete
    5.10  and inorder = inorder and inv = rbt
    5.11  proof (standard, goal_cases)
     6.1 --- a/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 11:53:25 2018 +0200
     6.2 +++ b/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 15:24:20 2018 +0200
     6.3 @@ -33,16 +33,16 @@
     6.4  fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
     6.5  fixes inorder :: "'t \<Rightarrow> 'a list"
     6.6  fixes inv :: "'t \<Rightarrow> bool"
     6.7 -assumes empty: "inorder empty = []"
     6.8 +assumes inorder_empty: "inorder empty = []"
     6.9  assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    6.10    isin t x = (x \<in> set (inorder t))"
    6.11 -assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    6.12 +assumes inorder_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    6.13    inorder(insert x t) = ins_list x (inorder t)"
    6.14 -assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    6.15 +assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    6.16    inorder(delete x t) = del_list x (inorder t)"
    6.17 -assumes inv_empty:  "inv empty"
    6.18 -assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    6.19 -assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    6.20 +assumes inorder_inv_empty:  "inv empty"
    6.21 +assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    6.22 +assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    6.23  begin
    6.24  
    6.25  text \<open>It implements the traditional specification:\<close>
    6.26 @@ -56,20 +56,20 @@
    6.27  sublocale Set
    6.28    empty insert delete isin set invar
    6.29  proof(standard, goal_cases)
    6.30 -  case 1 show ?case by (auto simp: empty set_def)
    6.31 +  case 1 show ?case by (auto simp: inorder_empty set_def)
    6.32  next
    6.33    case 2 thus ?case by(simp add: isin invar_def set_def)
    6.34  next
    6.35 -  case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def)
    6.36 +  case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
    6.37  next
    6.38    case (4 s x) thus ?case
    6.39 -    by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def)
    6.40 +    by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
    6.41  next
    6.42 -  case 5 thus ?case by(simp add: empty inv_empty invar_def)
    6.43 +  case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
    6.44  next
    6.45 -  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def)
    6.46 +  case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def)
    6.47  next
    6.48 -  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def)
    6.49 +  case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
    6.50  qed
    6.51  
    6.52  end
     7.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Wed Jun 13 11:53:25 2018 +0200
     7.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Wed Jun 13 15:24:20 2018 +0200
     7.3 @@ -123,7 +123,7 @@
     7.4  by(induction t)
     7.5    (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
     7.6  
     7.7 -lemma inorder_update_234:
     7.8 +lemma inorder_update:
     7.9    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
    7.10  by(simp add: update_def inorder_upd)
    7.11  
    7.12 @@ -133,7 +133,7 @@
    7.13    (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits)
    7.14  (* 30 secs (2016) *)
    7.15  
    7.16 -lemma inorder_delete_234: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    7.17 +lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    7.18    inorder(delete x t) = del_list x (inorder t)"
    7.19  by(simp add: delete_def inorder_del)
    7.20  
    7.21 @@ -160,15 +160,15 @@
    7.22  
    7.23  subsection \<open>Overall Correctness\<close>
    7.24  
    7.25 -interpretation Map_by_Ordered
    7.26 +interpretation M: Map_by_Ordered
    7.27  where empty = empty and lookup = lookup and update = update and delete = delete
    7.28  and inorder = inorder and inv = bal
    7.29  proof (standard, goal_cases)
    7.30    case 2 thus ?case by(simp add: lookup_map_of)
    7.31  next
    7.32 -  case 3 thus ?case by(simp add: inorder_update_234)
    7.33 +  case 3 thus ?case by(simp add: inorder_update)
    7.34  next
    7.35 -  case 4 thus ?case by(simp add: inorder_delete_234)
    7.36 +  case 4 thus ?case by(simp add: inorder_delete)
    7.37  next
    7.38    case 6 thus ?case by(simp add: bal_update)
    7.39  next
     8.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Wed Jun 13 11:53:25 2018 +0200
     8.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Wed Jun 13 15:24:20 2018 +0200
     8.3 @@ -504,7 +504,7 @@
     8.4  
     8.5  subsection \<open>Overall Correctness\<close>
     8.6  
     8.7 -interpretation Set_by_Ordered
     8.8 +interpretation S: Set_by_Ordered
     8.9  where empty = empty and isin = isin and insert = insert and delete = delete
    8.10  and inorder = inorder and inv = bal
    8.11  proof (standard, goal_cases)
     9.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Wed Jun 13 11:53:25 2018 +0200
     9.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Wed Jun 13 15:24:20 2018 +0200
     9.3 @@ -81,7 +81,7 @@
     9.4    "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
     9.5  by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
     9.6  
     9.7 -corollary inorder_update_23:
     9.8 +corollary inorder_update:
     9.9    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    9.10  by(simp add: update_def inorder_upd)
    9.11  
    9.12 @@ -91,7 +91,7 @@
    9.13  by(induction t rule: del.induct)
    9.14    (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
    9.15  
    9.16 -corollary inorder_delete_23: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    9.17 +corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    9.18    inorder(delete x t) = del_list x (inorder t)"
    9.19  by(simp add: delete_def inorder_del)
    9.20  
    9.21 @@ -119,7 +119,7 @@
    9.22  
    9.23  subsection \<open>Overall Correctness\<close>
    9.24  
    9.25 -interpretation Map_by_Ordered
    9.26 +interpretation M: Map_by_Ordered
    9.27  where empty = empty and lookup = lookup and update = update and delete = delete
    9.28  and inorder = inorder and inv = bal
    9.29  proof (standard, goal_cases)
    9.30 @@ -127,9 +127,9 @@
    9.31  next
    9.32    case 2 thus ?case by(simp add: lookup_map_of)
    9.33  next
    9.34 -  case 3 thus ?case by(simp add: inorder_update_23)
    9.35 +  case 3 thus ?case by(simp add: inorder_update)
    9.36  next
    9.37 -  case 4 thus ?case by(simp add: inorder_delete_23)
    9.38 +  case 4 thus ?case by(simp add: inorder_delete)
    9.39  next
    9.40    case 5 thus ?case by(simp add: empty_def)
    9.41  next
    10.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed Jun 13 11:53:25 2018 +0200
    10.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Wed Jun 13 15:24:20 2018 +0200
    10.3 @@ -379,7 +379,7 @@
    10.4  
    10.5  subsection \<open>Overall Correctness\<close>
    10.6  
    10.7 -interpretation Set_by_Ordered
    10.8 +interpretation S: Set_by_Ordered
    10.9  where empty = empty and isin = isin and insert = insert and delete = delete
   10.10  and inorder = inorder and inv = bal
   10.11  proof (standard, goal_cases)
    11.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Wed Jun 13 11:53:25 2018 +0200
    11.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Wed Jun 13 15:24:20 2018 +0200
    11.3 @@ -34,15 +34,15 @@
    11.4    "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    11.5  by (induction t) (auto simp: map_of_simps split: option.split)
    11.6  
    11.7 -lemma inorder_update_tree:
    11.8 +lemma inorder_update:
    11.9    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
   11.10  by(induction t) (auto simp: upd_list_simps)
   11.11  
   11.12 -lemma inorder_delete_tree:
   11.13 +lemma inorder_delete:
   11.14    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
   11.15  by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
   11.16  
   11.17 -interpretation Map_by_Ordered
   11.18 +interpretation M: Map_by_Ordered
   11.19  where empty = empty and lookup = lookup and update = update and delete = delete
   11.20  and inorder = inorder and inv = "\<lambda>_. True"
   11.21  proof (standard, goal_cases)
   11.22 @@ -50,9 +50,9 @@
   11.23  next
   11.24    case 2 thus ?case by(simp add: lookup_map_of)
   11.25  next
   11.26 -  case 3 thus ?case by(simp add: inorder_update_tree)
   11.27 +  case 3 thus ?case by(simp add: inorder_update)
   11.28  next
   11.29 -  case 4 thus ?case by(simp add: inorder_delete_tree)
   11.30 +  case 4 thus ?case by(simp add: inorder_delete)
   11.31  qed auto
   11.32  
   11.33  end
    12.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Wed Jun 13 11:53:25 2018 +0200
    12.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Wed Jun 13 15:24:20 2018 +0200
    12.3 @@ -62,7 +62,7 @@
    12.4    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    12.5  by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
    12.6  
    12.7 -interpretation Set_by_Ordered
    12.8 +interpretation S: Set_by_Ordered
    12.9  where empty = empty and isin = isin and insert = insert and delete = delete
   12.10  and inorder = inorder and inv = "\<lambda>_. True"
   12.11  proof (standard, goal_cases)