tuned names
authornipkow
Mon Nov 16 13:08:52 2015 +0100 (2015-11-16)
changeset 61686e6784939d645
parent 61685 2b3772ecfdec
child 61687 95a57e288fd4
tuned names
src/HOL/Data_Structures/AVL_Map.thy
src/HOL/Data_Structures/Map_by_Ordered.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/Splay_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	Mon Nov 16 12:37:46 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  interpretation Map_by_Ordered
     1.6  where empty = Leaf and lookup = lookup and update = update and delete = delete
     1.7 -and inorder = inorder and wf = "\<lambda>_. True"
     1.8 +and inorder = inorder and inv = "\<lambda>_. True"
     1.9  proof (standard, goal_cases)
    1.10    case 1 show ?case by simp
    1.11  next
    1.12 @@ -47,6 +47,6 @@
    1.13    case 3 thus ?case by(simp add: inorder_update)
    1.14  next
    1.15    case 4 thus ?case by(simp add: inorder_delete)
    1.16 -qed (rule TrueI)+
    1.17 +qed auto
    1.18  
    1.19  end
     2.1 --- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Mon Nov 16 12:37:46 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Mon Nov 16 13:08:52 2015 +0100
     2.3 @@ -12,12 +12,12 @@
     2.4  fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
     2.5  fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
     2.6  fixes invar :: "'m \<Rightarrow> bool"
     2.7 -assumes "map_of empty = (\<lambda>_. None)"
     2.8 -assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
     2.9 -assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
    2.10 -assumes "invar empty"
    2.11 -assumes "invar m \<Longrightarrow> invar(update a b m)"
    2.12 -assumes "invar m \<Longrightarrow> invar(delete a m)"
    2.13 +assumes map_empty: "map_of empty = (\<lambda>_. None)"
    2.14 +and map_update: "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
    2.15 +and map_delete: "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
    2.16 +and invar_empty: "invar empty"
    2.17 +and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
    2.18 +and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"
    2.19  
    2.20  locale Map_by_Ordered =
    2.21  fixes empty :: "'t"
    2.22 @@ -25,21 +25,21 @@
    2.23  fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    2.24  fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
    2.25  fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
    2.26 -fixes wf :: "'t \<Rightarrow> bool"
    2.27 +fixes inv :: "'t \<Rightarrow> bool"
    2.28  assumes empty: "inorder empty = []"
    2.29 -assumes lookup: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.30 +and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.31    lookup t a = map_of (inorder t) a"
    2.32 -assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.33 +and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.34    inorder(update a b t) = upd_list a b (inorder t)"
    2.35 -assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.36 +and delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.37    inorder(delete a t) = del_list a (inorder t)"
    2.38 -assumes wf_empty:  "wf empty"
    2.39 -assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
    2.40 -assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
    2.41 +and inv_empty:  "inv empty"
    2.42 +and inv_insert: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
    2.43 +and inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
    2.44  begin
    2.45  
    2.46  sublocale Map
    2.47 -  empty update delete "map_of o inorder" "\<lambda>t. wf t \<and> sorted1 (inorder t)"
    2.48 +  empty update delete "map_of o inorder" "\<lambda>t. inv t \<and> sorted1 (inorder t)"
    2.49  proof(standard, goal_cases)
    2.50    case 1 show ?case by (auto simp: empty)
    2.51  next
    2.52 @@ -47,11 +47,11 @@
    2.53  next
    2.54    case 3 thus ?case by(simp add: delete map_of_del_list)
    2.55  next
    2.56 -  case 4 thus ?case by(simp add: empty wf_empty)
    2.57 +  case 4 thus ?case by(simp add: empty inv_empty)
    2.58  next
    2.59 -  case 5 thus ?case by(simp add: update wf_insert sorted_upd_list)
    2.60 +  case 5 thus ?case by(simp add: update inv_insert sorted_upd_list)
    2.61  next
    2.62 -  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    2.63 +  case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    2.64  qed
    2.65  
    2.66  end
     3.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Mon Nov 16 12:37:46 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     3.3 @@ -53,7 +53,7 @@
     3.4  
     3.5  interpretation Map_by_Ordered
     3.6  where empty = Leaf and lookup = lookup and update = update and delete = delete
     3.7 -and inorder = inorder and wf = "\<lambda>_. True"
     3.8 +and inorder = inorder and inv = "\<lambda>_. True"
     3.9  proof (standard, goal_cases)
    3.10    case 1 show ?case by simp
    3.11  next
    3.12 @@ -62,6 +62,6 @@
    3.13    case 3 thus ?case by(simp add: inorder_update)
    3.14  next
    3.15    case 4 thus ?case by(simp add: inorder_delete)
    3.16 -qed (rule TrueI)+
    3.17 +qed auto
    3.18  
    3.19  end
     4.1 --- a/src/HOL/Data_Structures/Splay_Map.thy	Mon Nov 16 12:37:46 2015 +0100
     4.2 +++ b/src/HOL/Data_Structures/Splay_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     4.3 @@ -163,7 +163,7 @@
     4.4  
     4.5  interpretation Map_by_Ordered
     4.6  where empty = Leaf and lookup = lookup and update = update
     4.7 -and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
     4.8 +and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
     4.9  proof (standard, goal_cases)
    4.10    case 2 thus ?case by(simp add: lookup_eq)
    4.11  next
     5.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Mon Nov 16 12:37:46 2015 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     5.3 @@ -165,7 +165,7 @@
     5.4  
     5.5  interpretation T234_Map: Map_by_Ordered
     5.6  where empty = Leaf and lookup = lookup and update = update and delete = delete
     5.7 -and inorder = inorder and wf = bal
     5.8 +and inorder = inorder and inv = bal
     5.9  proof (standard, goal_cases)
    5.10    case 2 thus ?case by(simp add: lookup)
    5.11  next
     6.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Mon Nov 16 12:37:46 2015 +0100
     6.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     6.3 @@ -120,7 +120,7 @@
     6.4  
     6.5  interpretation T23_Map: Map_by_Ordered
     6.6  where empty = Leaf and lookup = lookup and update = update and delete = delete
     6.7 -and inorder = inorder and wf = bal
     6.8 +and inorder = inorder and inv = bal
     6.9  proof (standard, goal_cases)
    6.10    case 2 thus ?case by(simp add: lookup)
    6.11  next
     7.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 16 12:37:46 2015 +0100
     7.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     7.3 @@ -44,7 +44,7 @@
     7.4  
     7.5  interpretation Map_by_Ordered
     7.6  where empty = Leaf and lookup = lookup and update = update and delete = delete
     7.7 -and inorder = inorder and wf = "\<lambda>_. True"
     7.8 +and inorder = inorder and inv = "\<lambda>_. True"
     7.9  proof (standard, goal_cases)
    7.10    case 1 show ?case by simp
    7.11  next
    7.12 @@ -53,6 +53,6 @@
    7.13    case 3 thus ?case by(simp add: inorder_update)
    7.14  next
    7.15    case 4 thus ?case by(simp add: inorder_delete)
    7.16 -qed (rule TrueI)+
    7.17 +qed auto
    7.18  
    7.19  end