src/HOL/Library/RBT_Set.thy
changeset 51489 f738e6dbd844
parent 51115 7dbd6832a689
child 51540 eea5c4ca4a0e
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -316,11 +316,10 @@
     1.4    assumes "is_rbt t"
     1.5    shows "rbt_min t = rbt_min_opt t"
     1.6  proof -
     1.7 -  interpret ab_semigroup_idem_mult "(min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_min
     1.8 -    unfolding class.ab_semigroup_idem_mult_def by blast
     1.9 -  show ?thesis
    1.10 -    by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric]
    1.11 -      non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def)
    1.12 +  from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
    1.13 +  with assms show ?thesis
    1.14 +    by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
    1.15 +      min_max.Inf_fin.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
    1.16  qed
    1.17  
    1.18  (* maximum *)
    1.19 @@ -337,12 +336,7 @@
    1.20    fixes xs :: "('a :: linorder) list"
    1.21    assumes "xs \<noteq> []"
    1.22    shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
    1.23 -proof -
    1.24 -  interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
    1.25 -    unfolding class.ab_semigroup_idem_mult_def by blast
    1.26 -  show ?thesis
    1.27 -  using assms by (auto simp add: fold1_set_fold[symmetric])
    1.28 -qed
    1.29 +  using assms by (simp add: min_max.Sup_fin.set_eq_fold [symmetric])
    1.30  
    1.31  lemma rbt_max_simps:
    1.32    assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
    1.33 @@ -416,11 +410,10 @@
    1.34    assumes "is_rbt t"
    1.35    shows "rbt_max t = rbt_max_opt t"
    1.36  proof -
    1.37 -  interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
    1.38 -    unfolding class.ab_semigroup_idem_mult_def by blast
    1.39 -  show ?thesis
    1.40 -    by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric]
    1.41 -      non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def)
    1.42 +  from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
    1.43 +  with assms show ?thesis
    1.44 +    by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
    1.45 +      min_max.Sup_fin.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
    1.46  qed
    1.47  
    1.48  
    1.49 @@ -434,13 +427,13 @@
    1.50    by transfer (simp add: rbt_fold1_keys_def)
    1.51  
    1.52  lemma finite_fold1_fold1_keys:
    1.53 -  assumes "class.ab_semigroup_mult f"
    1.54 -  assumes "\<not> (is_empty t)"
    1.55 -  shows "Finite_Set.fold1 f (Set t) = fold1_keys f t"
    1.56 +  assumes "semilattice f"
    1.57 +  assumes "\<not> is_empty t"
    1.58 +  shows "semilattice_set.F f (Set t) = fold1_keys f t"
    1.59  proof -
    1.60 -  interpret ab_semigroup_mult f by fact
    1.61 +  from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
    1.62    show ?thesis using assms 
    1.63 -    by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys)
    1.64 +    by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
    1.65  qed
    1.66  
    1.67  (* minimum *)
    1.68 @@ -658,14 +651,14 @@
    1.69  
    1.70  lemma card_Set [code]:
    1.71    "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
    1.72 -by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp) 
    1.73 +  by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
    1.74  
    1.75  lemma setsum_Set [code]:
    1.76    "setsum f (Set xs) = fold_keys (plus o f) xs 0"
    1.77  proof -
    1.78    have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
    1.79    then show ?thesis 
    1.80 -    by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def)
    1.81 +    by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
    1.82  qed
    1.83  
    1.84  definition not_a_singleton_tree  where [code del]: "not_a_singleton_tree x y = x y"
    1.85 @@ -743,11 +736,10 @@
    1.86  lemma Min_fin_set_fold [code]:
    1.87    "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)"
    1.88  proof -
    1.89 -  have *:"(class.ab_semigroup_mult (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_min
    1.90 -    unfolding class.ab_semigroup_idem_mult_def by blast
    1.91 +  have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
    1.92 +  with finite_fold1_fold1_keys [OF *, folded Min_def]
    1.93    show ?thesis
    1.94 -    by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def 
    1.95 -      r_min_eq_r_min_opt[symmetric])  
    1.96 +    by (simp add: not_non_empty_tree_def r_min_alt_def r_min_eq_r_min_opt [symmetric])  
    1.97  qed
    1.98  
    1.99  lemma Inf_fin_set_fold [code]:
   1.100 @@ -781,11 +773,10 @@
   1.101  lemma Max_fin_set_fold [code]:
   1.102    "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)"
   1.103  proof -
   1.104 -  have *:"(class.ab_semigroup_mult (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_max
   1.105 -    unfolding class.ab_semigroup_idem_mult_def by blast
   1.106 +  have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
   1.107 +  with finite_fold1_fold1_keys [OF *, folded Max_def]
   1.108    show ?thesis
   1.109 -    by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def 
   1.110 -      r_max_eq_r_max_opt[symmetric])  
   1.111 +    by (simp add: not_non_empty_tree_def r_max_alt_def r_max_eq_r_max_opt [symmetric])  
   1.112  qed
   1.113  
   1.114  lemma Sup_fin_set_fold [code]: