src/HOL/List.thy
changeset 51489 f738e6dbd844
parent 51315 536a5603a138
child 51540 eea5c4ca4a0e
     1.1 --- a/src/HOL/List.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -2734,51 +2734,11 @@
     1.4  
     1.5  lemma (in comp_fun_commute) fold_set_fold_remdups:
     1.6    "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
     1.7 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
     1.8 -
     1.9 -lemma (in ab_semigroup_mult) fold1_distinct_set_fold:
    1.10 -  assumes "xs \<noteq> []"
    1.11 -  assumes d: "distinct xs"
    1.12 -  shows "Finite_Set.fold1 times (set xs) = List.fold times (tl xs) (hd xs)"
    1.13 -proof -
    1.14 -  interpret comp_fun_commute times by (fact comp_fun_commute)
    1.15 -  from assms obtain y ys where xs: "xs = y # ys"
    1.16 -    by (cases xs) auto
    1.17 -  then have *: "y \<notin> set ys" using assms by simp
    1.18 -  from xs d have **: "remdups ys = ys"  by safe (induct ys, auto)
    1.19 -  show ?thesis
    1.20 -  proof (cases "set ys = {}")
    1.21 -    case True with xs show ?thesis by simp
    1.22 -  next
    1.23 -    case False
    1.24 -    then have "fold1 times (Set.insert y (set ys)) = Finite_Set.fold times y (set ys)"
    1.25 -      by (simp_all add: fold1_eq_fold *)
    1.26 -    with xs show ?thesis
    1.27 -      by (simp add: fold_set_fold_remdups **)
    1.28 -  qed
    1.29 -qed
    1.30 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb)
    1.31  
    1.32  lemma (in comp_fun_idem) fold_set_fold:
    1.33    "Finite_Set.fold f y (set xs) = fold f xs y"
    1.34 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
    1.35 -
    1.36 -lemma (in ab_semigroup_idem_mult) fold1_set_fold:
    1.37 -  assumes "xs \<noteq> []"
    1.38 -  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
    1.39 -proof -
    1.40 -  interpret comp_fun_idem times by (fact comp_fun_idem)
    1.41 -  from assms obtain y ys where xs: "xs = y # ys"
    1.42 -    by (cases xs) auto
    1.43 -  show ?thesis
    1.44 -  proof (cases "set ys = {}")
    1.45 -    case True with xs show ?thesis by simp
    1.46 -  next
    1.47 -    case False
    1.48 -    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
    1.49 -      by (simp only: finite_set fold1_eq_fold_idem)
    1.50 -    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
    1.51 -  qed
    1.52 -qed
    1.53 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
    1.54  
    1.55  lemma union_set_fold [code]:
    1.56    "set xs \<union> A = fold Set.insert xs A"
    1.57 @@ -2813,49 +2773,18 @@
    1.58    "A \<inter> List.coset xs = fold Set.remove xs A"
    1.59    by (simp add: Diff_eq [symmetric] minus_set_fold)
    1.60  
    1.61 -lemma (in lattice) Inf_fin_set_fold:
    1.62 -  "Inf_fin (set (x # xs)) = fold inf xs x"
    1.63 +lemma (in semilattice_set) set_eq_fold:
    1.64 +  "F (set (x # xs)) = fold f xs x"
    1.65  proof -
    1.66 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.67 -    by (fact ab_semigroup_idem_mult_inf)
    1.68 -  show ?thesis
    1.69 -    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
    1.70 -qed
    1.71 -
    1.72 -declare Inf_fin_set_fold [code]
    1.73 -
    1.74 -lemma (in lattice) Sup_fin_set_fold:
    1.75 -  "Sup_fin (set (x # xs)) = fold sup xs x"
    1.76 -proof -
    1.77 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.78 -    by (fact ab_semigroup_idem_mult_sup)
    1.79 -  show ?thesis
    1.80 -    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
    1.81 +  interpret comp_fun_idem f
    1.82 +    by default (simp_all add: fun_eq_iff left_commute)
    1.83 +  show ?thesis by (simp add: eq_fold fold_set_fold)
    1.84  qed
    1.85  
    1.86 -declare Sup_fin_set_fold [code]
    1.87 -
    1.88 -lemma (in linorder) Min_fin_set_fold:
    1.89 -  "Min (set (x # xs)) = fold min xs x"
    1.90 -proof -
    1.91 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.92 -    by (fact ab_semigroup_idem_mult_min)
    1.93 -  show ?thesis
    1.94 -    by (simp add: Min_def fold1_set_fold del: set.simps)
    1.95 -qed
    1.96 -
    1.97 -declare Min_fin_set_fold [code]
    1.98 -
    1.99 -lemma (in linorder) Max_fin_set_fold:
   1.100 -  "Max (set (x # xs)) = fold max xs x"
   1.101 -proof -
   1.102 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.103 -    by (fact ab_semigroup_idem_mult_max)
   1.104 -  show ?thesis
   1.105 -    by (simp add: Max_def fold1_set_fold del: set.simps)
   1.106 -qed
   1.107 -
   1.108 -declare Max_fin_set_fold [code]
   1.109 +declare Inf_fin.set_eq_fold [code]
   1.110 +declare Sup_fin.set_eq_fold [code]
   1.111 +declare min_max.Inf_fin.set_eq_fold [code]
   1.112 +declare min_max.Sup_fin.set_eq_fold [code]
   1.113  
   1.114  lemma (in complete_lattice) Inf_set_fold:
   1.115    "Inf (set xs) = fold inf xs top"
   1.116 @@ -4915,24 +4844,36 @@
   1.117  sets to lists but one should convert in the other direction (via
   1.118  @{const set}). *}
   1.119  
   1.120 +subsubsection {* @{text sorted_list_of_set} *}
   1.121 +
   1.122 +text{* This function maps (finite) linearly ordered sets to sorted
   1.123 +lists. Warning: in most cases it is not a good idea to convert from
   1.124 +sets to lists but one should convert in the other direction (via
   1.125 +@{const set}). *}
   1.126 +
   1.127 +definition (in linorder) sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   1.128 +  "sorted_list_of_set = folding.F insort []"
   1.129 +
   1.130 +sublocale linorder < sorted_list_of_set!: folding insort Nil
   1.131 +where
   1.132 +  "folding.F insort [] = sorted_list_of_set"
   1.133 +proof -
   1.134 +  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   1.135 +  show "folding insort" by default (fact comp_fun_commute)
   1.136 +  show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
   1.137 +qed
   1.138 +
   1.139  context linorder
   1.140  begin
   1.141  
   1.142 -definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   1.143 -"sorted_list_of_set = Finite_Set.fold insort []"
   1.144 -
   1.145 -lemma sorted_list_of_set_empty [simp]:
   1.146 +lemma sorted_list_of_set_empty:
   1.147    "sorted_list_of_set {} = []"
   1.148 -  by (simp add: sorted_list_of_set_def)
   1.149 +  by (fact sorted_list_of_set.empty)
   1.150  
   1.151  lemma sorted_list_of_set_insert [simp]:
   1.152    assumes "finite A"
   1.153    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
   1.154 -proof -
   1.155 -  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   1.156 -  from assms show ?thesis
   1.157 -    by (simp add: sorted_list_of_set_def fold_insert_remove)
   1.158 -qed
   1.159 +  using assms by (fact sorted_list_of_set.insert_remove)
   1.160  
   1.161  lemma sorted_list_of_set [simp]:
   1.162    "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
   1.163 @@ -4943,7 +4884,7 @@
   1.164    "sorted_list_of_set (set xs) = sort (remdups xs)"
   1.165  proof -
   1.166    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   1.167 -  show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
   1.168 +  show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)
   1.169  qed
   1.170  
   1.171  lemma sorted_list_of_set_remove: