src/HOL/Data_Structures/Map_Specs.thy
changeset 68431 b294e095f64c
parent 67965 aaa31cd0caef
child 68492 c7e0a7bcacaf
     1.1 --- a/src/HOL/Data_Structures/Map_Specs.thy	Tue Jun 12 07:18:18 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Map_Specs.thy	Tue Jun 12 17:18:40 2018 +0200
     1.3 @@ -31,36 +31,41 @@
     1.4  fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
     1.5  fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
     1.6  fixes inv :: "'t \<Rightarrow> bool"
     1.7 -assumes empty: "inorder empty = []"
     1.8 -and lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
     1.9 +assumes inorder_empty: "inorder empty = []"
    1.10 +and inorder_lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    1.11    lookup t a = map_of (inorder t) a"
    1.12 -and update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    1.13 +and inorder_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    1.14    inorder(update a b t) = upd_list a b (inorder t)"
    1.15 -and delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    1.16 +and inorder_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow>
    1.17    inorder(delete a t) = del_list a (inorder t)"
    1.18 -and inv_empty:  "inv empty"
    1.19 -and inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
    1.20 -and inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
    1.21 +and inorder_inv_empty:  "inv empty"
    1.22 +and inorder_inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
    1.23 +and inorder_inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
    1.24  begin
    1.25  
    1.26  text \<open>It implements the traditional specification:\<close>
    1.27  
    1.28 +definition invar :: "'t \<Rightarrow> bool" where
    1.29 +"invar t == inv t \<and> sorted1 (inorder t)"
    1.30 +
    1.31  sublocale Map
    1.32 -  empty update delete lookup "\<lambda>t. inv t \<and> sorted1 (inorder t)"
    1.33 +  empty update delete lookup invar
    1.34  proof(standard, goal_cases)
    1.35 -  case 1 show ?case by (auto simp: lookup empty inv_empty)
    1.36 +  case 1 show ?case by (auto simp: inorder_lookup inorder_empty inorder_inv_empty)
    1.37  next
    1.38    case 2 thus ?case
    1.39 -    by(simp add: fun_eq_iff update inv_update map_of_ins_list lookup sorted_upd_list)
    1.40 +    by(simp add: fun_eq_iff inorder_update inorder_inv_update map_of_ins_list inorder_lookup
    1.41 +         sorted_upd_list invar_def)
    1.42  next
    1.43    case 3 thus ?case
    1.44 -    by(simp add: fun_eq_iff delete inv_delete map_of_del_list lookup sorted_del_list)
    1.45 -next
    1.46 -  case 4 thus ?case by(simp add: empty inv_empty)
    1.47 +    by(simp add: fun_eq_iff inorder_delete inorder_inv_delete map_of_del_list inorder_lookup
    1.48 +         sorted_del_list invar_def)
    1.49  next
    1.50 -  case 5 thus ?case by(simp add: update inv_update sorted_upd_list)
    1.51 +  case 4 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
    1.52  next
    1.53 -  case 6 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    1.54 +  case 5 thus ?case by(simp add: inorder_update inorder_inv_update sorted_upd_list invar_def)
    1.55 +next
    1.56 +  case 6 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
    1.57  qed
    1.58  
    1.59  end