src/HOL/Data_Structures/Set_Specs.thy
changeset 68440 6826718f732d
parent 68439 c8101022e52a
child 68492 c7e0a7bcacaf
     1.1 --- a/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 11:53:25 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 15:24:20 2018 +0200
     1.3 @@ -33,16 +33,16 @@
     1.4  fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
     1.5  fixes inorder :: "'t \<Rightarrow> 'a list"
     1.6  fixes inv :: "'t \<Rightarrow> bool"
     1.7 -assumes empty: "inorder empty = []"
     1.8 +assumes inorder_empty: "inorder empty = []"
     1.9  assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    1.10    isin t x = (x \<in> set (inorder t))"
    1.11 -assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    1.12 +assumes inorder_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    1.13    inorder(insert x t) = ins_list x (inorder t)"
    1.14 -assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    1.15 +assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    1.16    inorder(delete x t) = del_list x (inorder t)"
    1.17 -assumes inv_empty:  "inv empty"
    1.18 -assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    1.19 -assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    1.20 +assumes inorder_inv_empty:  "inv empty"
    1.21 +assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
    1.22 +assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
    1.23  begin
    1.24  
    1.25  text \<open>It implements the traditional specification:\<close>
    1.26 @@ -56,20 +56,20 @@
    1.27  sublocale Set
    1.28    empty insert delete isin set invar
    1.29  proof(standard, goal_cases)
    1.30 -  case 1 show ?case by (auto simp: empty set_def)
    1.31 +  case 1 show ?case by (auto simp: inorder_empty set_def)
    1.32  next
    1.33    case 2 thus ?case by(simp add: isin invar_def set_def)
    1.34  next
    1.35 -  case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def)
    1.36 +  case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
    1.37  next
    1.38    case (4 s x) thus ?case
    1.39 -    by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def)
    1.40 +    by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
    1.41  next
    1.42 -  case 5 thus ?case by(simp add: empty inv_empty invar_def)
    1.43 +  case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
    1.44  next
    1.45 -  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def)
    1.46 +  case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def)
    1.47  next
    1.48 -  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def)
    1.49 +  case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
    1.50  qed
    1.51  
    1.52  end