avoid name clashes
authornipkow
Sat Dec 05 16:33:20 2015 +0100 (2015-12-05)
changeset 617900494964bb226
parent 61789 9ce1a397410a
child 61791 21502fb1ff0a
avoid name clashes
src/HOL/Data_Structures/AVL_Map.thy
src/HOL/Data_Structures/Lookup2.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree_Map.thy
     1.1 --- a/src/HOL/Data_Structures/AVL_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  proof (standard, goal_cases)
     1.5    case 1 show ?case by simp
     1.6  next
     1.7 -  case 2 thus ?case by(simp add: lookup_eq)
     1.8 +  case 2 thus ?case by(simp add: lookup_map_of)
     1.9  next
    1.10    case 3 thus ?case by(simp add: inorder_update)
    1.11  next
     2.1 --- a/src/HOL/Data_Structures/Lookup2.thy	Sat Dec 05 16:13:28 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/Lookup2.thy	Sat Dec 05 16:33:20 2015 +0100
     2.3 @@ -14,7 +14,8 @@
     2.4  "lookup (Node _ l (a,b) r) x =
     2.5    (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
     2.6  
     2.7 -lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     2.8 +lemma lookup_map_of:
     2.9 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    2.10  by(induction t) (auto simp: map_of_simps split: option.split)
    2.11  
    2.12  end
    2.13 \ No newline at end of file
     3.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     3.3 @@ -70,7 +70,7 @@
     3.4  proof (standard, goal_cases)
     3.5    case 1 show ?case by simp
     3.6  next
     3.7 -  case 2 thus ?case by(simp add: lookup_eq)
     3.8 +  case 2 thus ?case by(simp add: lookup_map_of)
     3.9  next
    3.10    case 3 thus ?case by(simp add: inorder_update)
    3.11  next
     4.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     4.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     4.3 @@ -113,7 +113,8 @@
     4.4  
     4.5  subsection "Functional correctness"
     4.6  
     4.7 -lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     4.8 +lemma lookup_map_of:
     4.9 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    4.10  by (induction t) (auto simp: map_of_simps split: option.split)
    4.11  
    4.12  
    4.13 @@ -163,11 +164,11 @@
    4.14  
    4.15  subsection \<open>Overall Correctness\<close>
    4.16  
    4.17 -interpretation T234_Map: Map_by_Ordered
    4.18 +interpretation Map_by_Ordered
    4.19  where empty = Leaf and lookup = lookup and update = update and delete = delete
    4.20  and inorder = inorder and inv = bal
    4.21  proof (standard, goal_cases)
    4.22 -  case 2 thus ?case by(simp add: lookup)
    4.23 +  case 2 thus ?case by(simp add: lookup_map_of)
    4.24  next
    4.25    case 3 thus ?case by(simp add: inorder_update)
    4.26  next
     5.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     5.3 @@ -72,7 +72,8 @@
     5.4  
     5.5  subsection \<open>Functional Correctness\<close>
     5.6  
     5.7 -lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     5.8 +lemma lookup_map_of:
     5.9 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    5.10  by (induction t) (auto simp: map_of_simps split: option.split)
    5.11  
    5.12  
    5.13 @@ -118,11 +119,11 @@
    5.14  
    5.15  subsection \<open>Overall Correctness\<close>
    5.16  
    5.17 -interpretation T23_Map: Map_by_Ordered
    5.18 +interpretation Map_by_Ordered
    5.19  where empty = Leaf and lookup = lookup and update = update and delete = delete
    5.20  and inorder = inorder and inv = bal
    5.21  proof (standard, goal_cases)
    5.22 -  case 2 thus ?case by(simp add: lookup)
    5.23 +  case 2 thus ?case by(simp add: lookup_map_of)
    5.24  next
    5.25    case 3 thus ?case by(simp add: inorder_update)
    5.26  next
     6.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     6.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Sat Dec 05 16:33:20 2015 +0100
     6.3 @@ -30,7 +30,7 @@
     6.4  
     6.5  subsection "Functional Correctness Proofs"
     6.6  
     6.7 -lemma lookup_eq:
     6.8 +lemma lookup_map_of:
     6.9    "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    6.10  by (induction t) (auto simp: map_of_simps split: option.split)
    6.11  
    6.12 @@ -48,7 +48,7 @@
    6.13  proof (standard, goal_cases)
    6.14    case 1 show ?case by simp
    6.15  next
    6.16 -  case 2 thus ?case by(simp add: lookup_eq)
    6.17 +  case 2 thus ?case by(simp add: lookup_map_of)
    6.18  next
    6.19    case 3 thus ?case by(simp add: inorder_update)
    6.20  next