more abstract names
authornipkow
Wed Jun 13 11:53:25 2018 +0200 (10 months ago)
changeset 68439c8101022e52a
parent 68438 f04d0e75e439
child 68440 6826718f732d
more abstract names
src/HOL/Data_Structures/Set_Specs.thy
     1.1 --- a/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 10:52:47 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 11:53:25 2018 +0200
     1.3 @@ -47,23 +47,29 @@
     1.4  
     1.5  text \<open>It implements the traditional specification:\<close>
     1.6  
     1.7 +definition set :: "'t \<Rightarrow> 'a set" where
     1.8 +"set == List.set o inorder"
     1.9 +
    1.10 +definition invar :: "'t \<Rightarrow> bool" where
    1.11 +"invar t == inv t \<and> sorted (inorder t)"
    1.12 +
    1.13  sublocale Set
    1.14 -  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    1.15 +  empty insert delete isin set invar
    1.16  proof(standard, goal_cases)
    1.17 -  case 1 show ?case by (auto simp: empty)
    1.18 +  case 1 show ?case by (auto simp: empty set_def)
    1.19  next
    1.20 -  case 2 thus ?case by(simp add: isin)
    1.21 +  case 2 thus ?case by(simp add: isin invar_def set_def)
    1.22  next
    1.23 -  case 3 thus ?case by(simp add: insert set_ins_list)
    1.24 +  case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def)
    1.25  next
    1.26    case (4 s x) thus ?case
    1.27 -    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
    1.28 +    by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def)
    1.29  next
    1.30 -  case 5 thus ?case by(simp add: empty inv_empty)
    1.31 +  case 5 thus ?case by(simp add: empty inv_empty invar_def)
    1.32  next
    1.33 -  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
    1.34 +  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def)
    1.35  next
    1.36 -  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
    1.37 +  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def)
    1.38  qed
    1.39  
    1.40  end