src/HOL/Library/RBT_Set.thy
changeset 60679 ade12ef2773c
parent 60580 7e741e22d7fc
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -621,14 +621,17 @@
     1.4  lemma image_Set [code]:
     1.5    "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
     1.6  proof -
     1.7 -  have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
     1.8 -  then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
     1.9 +  have "comp_fun_commute (\<lambda>k. Set.insert (f k))"
    1.10 +    by standard auto
    1.11 +  then show ?thesis
    1.12 +    by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
    1.13  qed
    1.14  
    1.15  lemma Ball_Set [code]:
    1.16    "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
    1.17  proof -
    1.18 -  have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
    1.19 +  have "comp_fun_commute (\<lambda>k s. s \<and> P k)"
    1.20 +    by standard auto
    1.21    then show ?thesis 
    1.22      by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
    1.23  qed
    1.24 @@ -636,7 +639,8 @@
    1.25  lemma Bex_Set [code]:
    1.26    "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
    1.27  proof -
    1.28 -  have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
    1.29 +  have "comp_fun_commute (\<lambda>k s. s \<or> P k)"
    1.30 +    by standard auto
    1.31    then show ?thesis 
    1.32      by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
    1.33  qed
    1.34 @@ -670,7 +674,8 @@
    1.35  lemma setsum_Set [code]:
    1.36    "setsum f (Set xs) = fold_keys (plus o f) xs 0"
    1.37  proof -
    1.38 -  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
    1.39 +  have "comp_fun_commute (\<lambda>x. op + (f x))"
    1.40 +    by standard (auto simp: ac_simps)
    1.41    then show ?thesis 
    1.42      by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
    1.43  qed
    1.44 @@ -695,23 +700,23 @@
    1.45      by(auto split: rbt.split unit.split color.split)
    1.46  qed
    1.47  
    1.48 -lemma Pow_Set [code]:
    1.49 -  "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
    1.50 -by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
    1.51 +lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
    1.52 +  by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
    1.53  
    1.54  lemma product_Set [code]:
    1.55    "Product_Type.product (Set t1) (Set t2) = 
    1.56      fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
    1.57  proof -
    1.58 -  have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
    1.59 +  have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x
    1.60 +    by standard auto
    1.61    show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
    1.62      by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
    1.63  qed
    1.64  
    1.65 -lemma Id_on_Set [code]:
    1.66 -  "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
    1.67 +lemma Id_on_Set [code]: "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
    1.68  proof -
    1.69 -  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
    1.70 +  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))"
    1.71 +    by standard auto
    1.72    then show ?thesis
    1.73      by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
    1.74  qed
    1.75 @@ -728,10 +733,12 @@
    1.76    "(Set t1) O (Set t2) = fold_keys 
    1.77      (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
    1.78  proof -
    1.79 -  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
    1.80 +  interpret comp_fun_idem Set.insert
    1.81 +    by (fact comp_fun_idem_insert)
    1.82    have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
    1.83 -    by default (auto simp add: fun_eq_iff)
    1.84 -  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
    1.85 +    by standard (auto simp add: fun_eq_iff)
    1.86 +  show ?thesis
    1.87 +    using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
    1.88      by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
    1.89  qed
    1.90  
    1.91 @@ -759,11 +766,13 @@
    1.92    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
    1.93    shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
    1.94  proof -
    1.95 -  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
    1.96 +  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.97 +    by standard (simp add: fun_eq_iff ac_simps)
    1.98    then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
    1.99      by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   1.100    then show ?thesis 
   1.101 -    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   1.102 +    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric]
   1.103 +      r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   1.104  qed
   1.105  
   1.106  definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
   1.107 @@ -775,7 +784,7 @@
   1.108    shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
   1.109  proof -
   1.110    have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   1.111 -    by default (auto simp add: fun_eq_iff ac_simps)
   1.112 +    by standard (auto simp add: fun_eq_iff ac_simps)
   1.113    then show ?thesis
   1.114      by (auto simp: INF_fold_inf finite_fold_fold_keys)
   1.115  qed
   1.116 @@ -800,14 +809,17 @@
   1.117    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   1.118    shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   1.119  proof -
   1.120 -  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   1.121 +  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.122 +    by standard (simp add: fun_eq_iff ac_simps)
   1.123    then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   1.124      by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   1.125    then show ?thesis 
   1.126 -    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   1.127 +    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric]
   1.128 +      r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   1.129  qed
   1.130  
   1.131 -definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
   1.132 +definition Sup' :: "'a :: {linorder,complete_lattice} set \<Rightarrow> 'a"
   1.133 +  where [code del]: "Sup' x = Sup x"
   1.134  declare Sup'_def[symmetric, code_unfold]
   1.135  declare Sup_Set_fold[folded Sup'_def, code]
   1.136  
   1.137 @@ -816,30 +828,34 @@
   1.138    shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
   1.139  proof -
   1.140    have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
   1.141 -    by default (auto simp add: fun_eq_iff ac_simps)
   1.142 +    by standard (auto simp add: fun_eq_iff ac_simps)
   1.143    then show ?thesis
   1.144      by (auto simp: SUP_fold_sup finite_fold_fold_keys)
   1.145  qed
   1.146  
   1.147 -lemma sorted_list_set[code]:
   1.148 -  "sorted_list_of_set (Set t) = RBT.keys t"
   1.149 -by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   1.150 +lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
   1.151 +  by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   1.152  
   1.153  lemma Bleast_code [code]:
   1.154 - "Bleast (Set t) P = (case filter P (RBT.keys t) of
   1.155 -    x#xs \<Rightarrow> x |
   1.156 -    [] \<Rightarrow> abort_Bleast (Set t) P)"
   1.157 +  "Bleast (Set t) P =
   1.158 +    (case filter P (RBT.keys t) of
   1.159 +      x # xs \<Rightarrow> x
   1.160 +    | [] \<Rightarrow> abort_Bleast (Set t) P)"
   1.161  proof (cases "filter P (RBT.keys t)")
   1.162 -  case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   1.163 +  case Nil
   1.164 +  thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   1.165  next
   1.166    case (Cons x ys)
   1.167    have "(LEAST x. x \<in> Set t \<and> P x) = x"
   1.168    proof (rule Least_equality)
   1.169 -    show "x \<in> Set t \<and> P x" using Cons[symmetric]
   1.170 -      by(auto simp add: set_keys Cons_eq_filter_iff)
   1.171 +    show "x \<in> Set t \<and> P x"
   1.172 +      using Cons[symmetric]
   1.173 +      by (auto simp add: set_keys Cons_eq_filter_iff)
   1.174      next
   1.175 -      fix y assume "y : Set t \<and> P y"
   1.176 -      then show "x \<le> y" using Cons[symmetric]
   1.177 +      fix y
   1.178 +      assume "y \<in> Set t \<and> P y"
   1.179 +      then show "x \<le> y"
   1.180 +        using Cons[symmetric]
   1.181          by(auto simp add: set_keys Cons_eq_filter_iff)
   1.182            (metis sorted_Cons sorted_append sorted_keys)
   1.183    qed