names of fold_set locales resemble name of characteristic property more closely
authorhaftmann
Fri May 20 11:44:16 2011 +0200 (2011-05-20)
changeset 428711c0b99f950d9
parent 42869 43b0f61f56d0
child 42872 585c8333b0da
names of fold_set locales resemble name of characteristic property more closely
src/HOL/Big_Operators.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Library/More_List.thy
src/HOL/Library/More_Set.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Fri May 20 08:16:56 2011 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Fri May 20 11:44:16 2011 +0200
     1.3 @@ -1205,7 +1205,7 @@
     1.4  proof qed (rule inf_assoc inf_commute inf_idem)+
     1.5  
     1.6  lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
     1.7 -by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
     1.8 +by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
     1.9  
    1.10  lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
    1.11  by (induct pred: finite) (auto intro: le_infI1)
     2.1 --- a/src/HOL/Finite_Set.thy	Fri May 20 08:16:56 2011 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Fri May 20 11:44:16 2011 +0200
     2.3 @@ -532,13 +532,13 @@
     2.4  if @{text f} is ``left-commutative'':
     2.5  *}
     2.6  
     2.7 -locale fun_left_comm =
     2.8 +locale comp_fun_commute =
     2.9    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
    2.10 -  assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
    2.11 +  assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
    2.12  begin
    2.13  
    2.14  lemma fun_left_comm: "f x (f y z) = f y (f x z)"
    2.15 -  using commute_comp by (simp add: fun_eq_iff)
    2.16 +  using comp_fun_commute by (simp add: fun_eq_iff)
    2.17  
    2.18  end
    2.19  
    2.20 @@ -565,7 +565,7 @@
    2.21  
    2.22  subsubsection{*From @{const fold_graph} to @{term fold}*}
    2.23  
    2.24 -context fun_left_comm
    2.25 +context comp_fun_commute
    2.26  begin
    2.27  
    2.28  lemma fold_graph_insertE_aux:
    2.29 @@ -671,12 +671,12 @@
    2.30  
    2.31  text{* A simplified version for idempotent functions: *}
    2.32  
    2.33 -locale fun_left_comm_idem = fun_left_comm +
    2.34 -  assumes fun_comp_idem: "f x o f x = f x"
    2.35 +locale comp_fun_idem = comp_fun_commute +
    2.36 +  assumes comp_fun_idem: "f x o f x = f x"
    2.37  begin
    2.38  
    2.39  lemma fun_left_idem: "f x (f x z) = f x z"
    2.40 -  using fun_comp_idem by (simp add: fun_eq_iff)
    2.41 +  using comp_fun_idem by (simp add: fun_eq_iff)
    2.42  
    2.43  lemma fold_insert_idem:
    2.44    assumes fin: "finite A"
    2.45 @@ -700,33 +700,33 @@
    2.46  
    2.47  subsubsection {* Expressing set operations via @{const fold} *}
    2.48  
    2.49 -lemma (in fun_left_comm) comp_comp_fun_commute:
    2.50 -  "fun_left_comm (f \<circ> g)"
    2.51 +lemma (in comp_fun_commute) comp_comp_fun_commute:
    2.52 +  "comp_fun_commute (f \<circ> g)"
    2.53  proof
    2.54 -qed (simp_all add: commute_comp)
    2.55 +qed (simp_all add: comp_fun_commute)
    2.56  
    2.57 -lemma (in fun_left_comm_idem) comp_comp_fun_idem:
    2.58 -  "fun_left_comm_idem (f \<circ> g)"
    2.59 -  by (rule fun_left_comm_idem.intro, rule comp_comp_fun_commute, unfold_locales)
    2.60 -    (simp_all add: fun_comp_idem)
    2.61 +lemma (in comp_fun_idem) comp_comp_fun_idem:
    2.62 +  "comp_fun_idem (f \<circ> g)"
    2.63 +  by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
    2.64 +    (simp_all add: comp_fun_idem)
    2.65  
    2.66 -lemma fun_left_comm_idem_insert:
    2.67 -  "fun_left_comm_idem insert"
    2.68 +lemma comp_fun_idem_insert:
    2.69 +  "comp_fun_idem insert"
    2.70  proof
    2.71  qed auto
    2.72  
    2.73 -lemma fun_left_comm_idem_remove:
    2.74 -  "fun_left_comm_idem (\<lambda>x A. A - {x})"
    2.75 +lemma comp_fun_idem_remove:
    2.76 +  "comp_fun_idem (\<lambda>x A. A - {x})"
    2.77  proof
    2.78  qed auto
    2.79  
    2.80 -lemma (in semilattice_inf) fun_left_comm_idem_inf:
    2.81 -  "fun_left_comm_idem inf"
    2.82 +lemma (in semilattice_inf) comp_fun_idem_inf:
    2.83 +  "comp_fun_idem inf"
    2.84  proof
    2.85  qed (auto simp add: inf_left_commute)
    2.86  
    2.87 -lemma (in semilattice_sup) fun_left_comm_idem_sup:
    2.88 -  "fun_left_comm_idem sup"
    2.89 +lemma (in semilattice_sup) comp_fun_idem_sup:
    2.90 +  "comp_fun_idem sup"
    2.91  proof
    2.92  qed (auto simp add: sup_left_commute)
    2.93  
    2.94 @@ -734,7 +734,7 @@
    2.95    assumes "finite A"
    2.96    shows "A \<union> B = fold insert B A"
    2.97  proof -
    2.98 -  interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
    2.99 +  interpret comp_fun_idem insert by (fact comp_fun_idem_insert)
   2.100    from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
   2.101  qed
   2.102  
   2.103 @@ -742,7 +742,7 @@
   2.104    assumes "finite A"
   2.105    shows "B - A = fold (\<lambda>x A. A - {x}) B A"
   2.106  proof -
   2.107 -  interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
   2.108 +  interpret comp_fun_idem "\<lambda>x A. A - {x}" by (fact comp_fun_idem_remove)
   2.109    from `finite A` show ?thesis by (induct A arbitrary: B) auto
   2.110  qed
   2.111  
   2.112 @@ -753,7 +753,7 @@
   2.113    assumes "finite A"
   2.114    shows "inf B (Inf A) = fold inf B A"
   2.115  proof -
   2.116 -  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
   2.117 +  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   2.118    from `finite A` show ?thesis by (induct A arbitrary: B)
   2.119      (simp_all add: Inf_insert inf_commute fold_fun_comm)
   2.120  qed
   2.121 @@ -762,7 +762,7 @@
   2.122    assumes "finite A"
   2.123    shows "sup B (Sup A) = fold sup B A"
   2.124  proof -
   2.125 -  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
   2.126 +  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   2.127    from `finite A` show ?thesis by (induct A arbitrary: B)
   2.128      (simp_all add: Sup_insert sup_commute fold_fun_comm)
   2.129  qed
   2.130 @@ -781,8 +781,8 @@
   2.131    assumes "finite A"
   2.132    shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
   2.133  proof (rule sym)
   2.134 -  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
   2.135 -  interpret fun_left_comm_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
   2.136 +  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   2.137 +  interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
   2.138    from `finite A` have "fold (inf \<circ> f) B A = ?inf"
   2.139      by (induct A arbitrary: B)
   2.140        (simp_all add: INFI_def Inf_insert inf_left_commute)
   2.141 @@ -793,8 +793,8 @@
   2.142    assumes "finite A"
   2.143    shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
   2.144  proof (rule sym)
   2.145 -  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
   2.146 -  interpret fun_left_comm_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
   2.147 +  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   2.148 +  interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
   2.149    from `finite A` have "fold (sup \<circ> f) B A = ?sup"
   2.150      by (induct A arbitrary: B)
   2.151        (simp_all add: SUPR_def Sup_insert sup_left_commute)
   2.152 @@ -829,7 +829,7 @@
   2.153  assumes "finite A" and "a \<notin> A"
   2.154  shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
   2.155  proof -
   2.156 -  interpret I: fun_left_comm "%x y. (g x) * y" proof
   2.157 +  interpret I: comp_fun_commute "%x y. (g x) * y" proof
   2.158    qed (simp add: fun_eq_iff mult_ac)
   2.159    show ?thesis using assms by (simp add: fold_image_def)
   2.160  qed
   2.161 @@ -1052,14 +1052,14 @@
   2.162  context ab_semigroup_mult
   2.163  begin
   2.164  
   2.165 -lemma fun_left_comm: "fun_left_comm (op *)" proof
   2.166 +lemma comp_fun_commute: "comp_fun_commute (op *)" proof
   2.167  qed (simp add: fun_eq_iff mult_ac)
   2.168  
   2.169  lemma fold_graph_insert_swap:
   2.170  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
   2.171  shows "fold_graph times z (insert b A) (z * y)"
   2.172  proof -
   2.173 -  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   2.174 +  interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute)
   2.175  from assms show ?thesis
   2.176  proof (induct rule: fold_graph.induct)
   2.177    case emptyI show ?case by (subst mult_commute [of z b], fast)
   2.178 @@ -1099,7 +1099,7 @@
   2.179  lemma fold1_eq_fold:
   2.180  assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
   2.181  proof -
   2.182 -  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   2.183 +  interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute)
   2.184    from assms show ?thesis
   2.185  apply (simp add: fold1_def fold_def)
   2.186  apply (rule the_equality)
   2.187 @@ -1126,7 +1126,7 @@
   2.188    assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
   2.189    shows "fold1 times (insert x A) = x * fold1 times A"
   2.190  proof -
   2.191 -  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   2.192 +  interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute)
   2.193    from nonempty obtain a A' where "A = insert a A' & a ~: A'"
   2.194      by (auto simp add: nonempty_iff)
   2.195    with A show ?thesis
   2.196 @@ -1138,15 +1138,15 @@
   2.197  context ab_semigroup_idem_mult
   2.198  begin
   2.199  
   2.200 -lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof
   2.201 +lemma comp_fun_idem: "comp_fun_idem (op *)" proof
   2.202  qed (simp_all add: fun_eq_iff mult_left_commute)
   2.203  
   2.204  lemma fold1_insert_idem [simp]:
   2.205    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   2.206    shows "fold1 times (insert x A) = x * fold1 times A"
   2.207  proof -
   2.208 -  interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
   2.209 -    by (rule fun_left_comm_idem)
   2.210 +  interpret comp_fun_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
   2.211 +    by (rule comp_fun_idem)
   2.212    from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
   2.213      by (auto simp add: nonempty_iff)
   2.214    show ?thesis
   2.215 @@ -1191,7 +1191,7 @@
   2.216    case False
   2.217    with assms show ?thesis by (simp add: fold1_eq_fold)
   2.218  next
   2.219 -  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
   2.220 +  interpret comp_fun_idem times by (fact comp_fun_idem)
   2.221    case True then obtain b B
   2.222      where A: "A = insert a B" and "a \<notin> B" by (rule set_insert)
   2.223    with assms have "finite B" by auto
   2.224 @@ -1315,7 +1315,7 @@
   2.225  locale folding =
   2.226    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   2.227    fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
   2.228 -  assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
   2.229 +  assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
   2.230    assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A"
   2.231  begin
   2.232  
   2.233 @@ -1327,8 +1327,8 @@
   2.234    assumes "finite A" and "x \<notin> A"
   2.235    shows "F (insert x A) = F A \<circ> f x"
   2.236  proof -
   2.237 -  interpret fun_left_comm f proof
   2.238 -  qed (insert commute_comp, simp add: fun_eq_iff)
   2.239 +  interpret comp_fun_commute f proof
   2.240 +  qed (insert comp_fun_commute, simp add: fun_eq_iff)
   2.241    from fold_insert2 assms
   2.242    have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
   2.243    with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
   2.244 @@ -1351,38 +1351,38 @@
   2.245  
   2.246  lemma commute_left_comp:
   2.247    "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
   2.248 -  by (simp add: o_assoc commute_comp)
   2.249 +  by (simp add: o_assoc comp_fun_commute)
   2.250  
   2.251 -lemma commute_comp':
   2.252 +lemma comp_fun_commute':
   2.253    assumes "finite A"
   2.254    shows "f x \<circ> F A = F A \<circ> f x"
   2.255    using assms by (induct A)
   2.256 -    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] commute_comp)
   2.257 +    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute)
   2.258  
   2.259  lemma commute_left_comp':
   2.260    assumes "finite A"
   2.261    shows "f x \<circ> (F A \<circ> g) = F A \<circ> (f x \<circ> g)"
   2.262 -  using assms by (simp add: o_assoc commute_comp')
   2.263 +  using assms by (simp add: o_assoc comp_fun_commute')
   2.264  
   2.265 -lemma commute_comp'':
   2.266 +lemma comp_fun_commute'':
   2.267    assumes "finite A" and "finite B"
   2.268    shows "F B \<circ> F A = F A \<circ> F B"
   2.269    using assms by (induct A)
   2.270 -    (simp_all add: o_assoc, simp add: o_assoc [symmetric] commute_comp')
   2.271 +    (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute')
   2.272  
   2.273  lemma commute_left_comp'':
   2.274    assumes "finite A" and "finite B"
   2.275    shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
   2.276 -  using assms by (simp add: o_assoc commute_comp'')
   2.277 +  using assms by (simp add: o_assoc comp_fun_commute'')
   2.278  
   2.279 -lemmas commute_comps = o_assoc [symmetric] commute_comp commute_left_comp
   2.280 -  commute_comp' commute_left_comp' commute_comp'' commute_left_comp''
   2.281 +lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp
   2.282 +  comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''
   2.283  
   2.284  lemma union_inter:
   2.285    assumes "finite A" and "finite B"
   2.286    shows "F (A \<union> B) \<circ> F (A \<inter> B) = F A \<circ> F B"
   2.287    using assms by (induct A)
   2.288 -    (simp_all del: o_apply add: insert_absorb Int_insert_left commute_comps,
   2.289 +    (simp_all del: o_apply add: insert_absorb Int_insert_left comp_fun_commutes,
   2.290        simp add: o_assoc)
   2.291  
   2.292  lemma union:
   2.293 @@ -1411,7 +1411,7 @@
   2.294    assumes "finite A" and "x \<in> A"
   2.295    shows "F A \<circ> f x = F A"
   2.296  using assms by (induct A)
   2.297 -  (auto simp add: commute_comps idem_comp, simp add: commute_left_comp' [symmetric] commute_comp')
   2.298 +  (auto simp add: comp_fun_commutes idem_comp, simp add: commute_left_comp' [symmetric] comp_fun_commute')
   2.299  
   2.300  lemma subset_comp_idem:
   2.301    assumes "finite A" and "B \<subseteq> A"
   2.302 @@ -1460,7 +1460,7 @@
   2.303    assumes "finite A" and "x \<notin> A"
   2.304    shows "F (insert x A) = g x * F A"
   2.305  proof -
   2.306 -  interpret fun_left_comm "%x y. (g x) * y" proof
   2.307 +  interpret comp_fun_commute "%x y. (g x) * y" proof
   2.308    qed (simp add: ac_simps fun_eq_iff)
   2.309    with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
   2.310      by (simp add: fold_image_def)
   2.311 @@ -1697,8 +1697,8 @@
   2.312    with `finite A` have "finite B" by simp
   2.313    interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
   2.314    qed (simp_all add: fun_eq_iff ac_simps)
   2.315 -  thm fold.commute_comp' [of B b, simplified fun_eq_iff, simplified]
   2.316 -  from `finite B` fold.commute_comp' [of B x]
   2.317 +  thm fold.comp_fun_commute' [of B b, simplified fun_eq_iff, simplified]
   2.318 +  from `finite B` fold.comp_fun_commute' [of B x]
   2.319      have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
   2.320    then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)
   2.321    from `finite B` * fold.insert [of B b]
     3.1 --- a/src/HOL/GCD.thy	Fri May 20 08:16:56 2011 +0200
     3.2 +++ b/src/HOL/GCD.thy	Fri May 20 11:44:16 2011 +0200
     3.3 @@ -1436,16 +1436,16 @@
     3.4  lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
     3.5  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
     3.6  
     3.7 -lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
     3.8 +lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
     3.9  proof qed (auto simp add: gcd_ac_nat)
    3.10  
    3.11 -lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
    3.12 +lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
    3.13  proof qed (auto simp add: gcd_ac_int)
    3.14  
    3.15 -lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
    3.16 +lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
    3.17  proof qed (auto simp add: lcm_ac_nat)
    3.18  
    3.19 -lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
    3.20 +lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
    3.21  proof qed (auto simp add: lcm_ac_int)
    3.22  
    3.23  
    3.24 @@ -1516,8 +1516,8 @@
    3.25    assumes "finite N"
    3.26    shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
    3.27  proof -
    3.28 -  interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
    3.29 -    by (rule fun_left_comm_idem_lcm_nat)
    3.30 +  interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
    3.31 +    by (rule comp_fun_idem_lcm_nat)
    3.32    from assms show ?thesis by(simp add: Lcm_def)
    3.33  qed
    3.34  
    3.35 @@ -1525,8 +1525,8 @@
    3.36    assumes "finite N"
    3.37    shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
    3.38  proof -
    3.39 -  interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
    3.40 -    by (rule fun_left_comm_idem_lcm_int)
    3.41 +  interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
    3.42 +    by (rule comp_fun_idem_lcm_int)
    3.43    from assms show ?thesis by(simp add: Lcm_def)
    3.44  qed
    3.45  
    3.46 @@ -1534,8 +1534,8 @@
    3.47    assumes "finite N"
    3.48    shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
    3.49  proof -
    3.50 -  interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
    3.51 -    by (rule fun_left_comm_idem_gcd_nat)
    3.52 +  interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
    3.53 +    by (rule comp_fun_idem_gcd_nat)
    3.54    from assms show ?thesis by(simp add: Gcd_def)
    3.55  qed
    3.56  
    3.57 @@ -1543,8 +1543,8 @@
    3.58    assumes "finite N"
    3.59    shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
    3.60  proof -
    3.61 -  interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
    3.62 -    by (rule fun_left_comm_idem_gcd_int)
    3.63 +  interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
    3.64 +    by (rule comp_fun_idem_gcd_int)
    3.65    from assms show ?thesis by(simp add: Gcd_def)
    3.66  qed
    3.67  
    3.68 @@ -1685,28 +1685,28 @@
    3.69  lemma Lcm_set_nat [code_unfold]:
    3.70    "Lcm (set ns) = foldl lcm (1::nat) ns"
    3.71  proof -
    3.72 -  interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
    3.73 +  interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_lcm_nat)
    3.74    show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
    3.75  qed
    3.76  
    3.77  lemma Lcm_set_int [code_unfold]:
    3.78    "Lcm (set is) = foldl lcm (1::int) is"
    3.79  proof -
    3.80 -  interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
    3.81 +  interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_lcm_int)
    3.82    show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
    3.83  qed
    3.84  
    3.85  lemma Gcd_set_nat [code_unfold]:
    3.86    "Gcd (set ns) = foldl gcd (0::nat) ns"
    3.87  proof -
    3.88 -  interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
    3.89 +  interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_gcd_nat)
    3.90    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
    3.91  qed
    3.92  
    3.93  lemma Gcd_set_int [code_unfold]:
    3.94    "Gcd (set ns) = foldl gcd (0::int) ns"
    3.95  proof -
    3.96 -  interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
    3.97 +  interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_gcd_int)
    3.98    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
    3.99  qed
   3.100  
     4.1 --- a/src/HOL/Library/More_List.thy	Fri May 20 08:16:56 2011 +0200
     4.2 +++ b/src/HOL/Library/More_List.thy	Fri May 20 11:44:16 2011 +0200
     4.3 @@ -158,11 +158,11 @@
     4.4  
     4.5  text {* @{const Finite_Set.fold} and @{const fold} *}
     4.6  
     4.7 -lemma (in fun_left_comm) fold_set_remdups:
     4.8 +lemma (in comp_fun_commute) fold_set_remdups:
     4.9    "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
    4.10    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
    4.11  
    4.12 -lemma (in fun_left_comm_idem) fold_set:
    4.13 +lemma (in comp_fun_idem) fold_set:
    4.14    "Finite_Set.fold f y (set xs) = fold f xs y"
    4.15    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
    4.16  
    4.17 @@ -170,7 +170,7 @@
    4.18    assumes "xs \<noteq> []"
    4.19    shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
    4.20  proof -
    4.21 -  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
    4.22 +  interpret comp_fun_idem times by (fact comp_fun_idem)
    4.23    from assms obtain y ys where xs: "xs = y # ys"
    4.24      by (cases xs) auto
    4.25    show ?thesis
    4.26 @@ -239,8 +239,8 @@
    4.27  lemma (in complete_lattice) Inf_set_fold:
    4.28    "Inf (set xs) = fold inf xs top"
    4.29  proof -
    4.30 -  interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.31 -    by (fact fun_left_comm_idem_inf)
    4.32 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.33 +    by (fact comp_fun_idem_inf)
    4.34    show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
    4.35  qed
    4.36  
    4.37 @@ -251,8 +251,8 @@
    4.38  lemma (in complete_lattice) Sup_set_fold:
    4.39    "Sup (set xs) = fold sup xs bot"
    4.40  proof -
    4.41 -  interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.42 -    by (fact fun_left_comm_idem_sup)
    4.43 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.44 +    by (fact comp_fun_idem_sup)
    4.45    show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
    4.46  qed
    4.47  
     5.1 --- a/src/HOL/Library/More_Set.thy	Fri May 20 08:16:56 2011 +0200
     5.2 +++ b/src/HOL/Library/More_Set.thy	Fri May 20 11:44:16 2011 +0200
     5.3 @@ -15,11 +15,11 @@
     5.4  definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     5.5    "remove x A = A - {x}"
     5.6  
     5.7 -lemma fun_left_comm_idem_remove:
     5.8 -  "fun_left_comm_idem remove"
     5.9 +lemma comp_fun_idem_remove:
    5.10 +  "comp_fun_idem remove"
    5.11  proof -
    5.12    have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
    5.13 -  show ?thesis by (simp only: fun_left_comm_idem_remove rem)
    5.14 +  show ?thesis by (simp only: comp_fun_idem_remove rem)
    5.15  qed
    5.16  
    5.17  lemma minus_fold_remove:
    5.18 @@ -66,8 +66,8 @@
    5.19  lemma union_set:
    5.20    "set xs \<union> A = fold Set.insert xs A"
    5.21  proof -
    5.22 -  interpret fun_left_comm_idem Set.insert
    5.23 -    by (fact fun_left_comm_idem_insert)
    5.24 +  interpret comp_fun_idem Set.insert
    5.25 +    by (fact comp_fun_idem_insert)
    5.26    show ?thesis by (simp add: union_fold_insert fold_set)
    5.27  qed
    5.28  
    5.29 @@ -82,8 +82,8 @@
    5.30  lemma minus_set:
    5.31    "A - set xs = fold remove xs A"
    5.32  proof -
    5.33 -  interpret fun_left_comm_idem remove
    5.34 -    by (fact fun_left_comm_idem_remove)
    5.35 +  interpret comp_fun_idem remove
    5.36 +    by (fact comp_fun_idem_remove)
    5.37    show ?thesis
    5.38      by (simp add: minus_fold_remove [of _ A] fold_set)
    5.39  qed
     6.1 --- a/src/HOL/Library/Multiset.thy	Fri May 20 08:16:56 2011 +0200
     6.2 +++ b/src/HOL/Library/Multiset.thy	Fri May 20 11:44:16 2011 +0200
     6.3 @@ -1457,7 +1457,7 @@
     6.4  lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
     6.5  unfolding fold_mset_def by blast
     6.6  
     6.7 -context fun_left_comm
     6.8 +context comp_fun_commute
     6.9  begin
    6.10  
    6.11  lemma fold_msetG_determ:
    6.12 @@ -1563,10 +1563,10 @@
    6.13  qed
    6.14  
    6.15  lemma fold_mset_fusion:
    6.16 -  assumes "fun_left_comm g"
    6.17 +  assumes "comp_fun_commute g"
    6.18    shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
    6.19  proof -
    6.20 -  interpret fun_left_comm g by (fact assms)
    6.21 +  interpret comp_fun_commute g by (fact assms)
    6.22    show "PROP ?P" by (induct A) auto
    6.23  qed
    6.24  
    6.25 @@ -1598,7 +1598,7 @@
    6.26  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
    6.27    "image_mset f = fold_mset (op + o single o f) {#}"
    6.28  
    6.29 -interpretation image_left_comm: fun_left_comm "op + o single o f"
    6.30 +interpretation image_fun_commute: comp_fun_commute "op + o single o f"
    6.31  proof qed (simp add: add_ac fun_eq_iff)
    6.32  
    6.33  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
     7.1 --- a/src/HOL/List.thy	Fri May 20 08:16:56 2011 +0200
     7.2 +++ b/src/HOL/List.thy	Fri May 20 11:44:16 2011 +0200
     7.3 @@ -2478,11 +2478,11 @@
     7.4  
     7.5  text {* @{const Finite_Set.fold} and @{const foldl} *}
     7.6  
     7.7 -lemma (in fun_left_comm) fold_set_remdups:
     7.8 +lemma (in comp_fun_commute) fold_set_remdups:
     7.9    "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
    7.10    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
    7.11  
    7.12 -lemma (in fun_left_comm_idem) fold_set:
    7.13 +lemma (in comp_fun_idem) fold_set:
    7.14    "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
    7.15    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
    7.16  
    7.17 @@ -2490,7 +2490,7 @@
    7.18    assumes "xs \<noteq> []"
    7.19    shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
    7.20  proof -
    7.21 -  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
    7.22 +  interpret comp_fun_idem times by (fact comp_fun_idem)
    7.23    from assms obtain y ys where xs: "xs = y # ys"
    7.24      by (cases xs) auto
    7.25    show ?thesis
    7.26 @@ -2543,16 +2543,16 @@
    7.27  lemma (in complete_lattice) Inf_set_fold [code_unfold]:
    7.28    "Inf (set xs) = foldl inf top xs"
    7.29  proof -
    7.30 -  interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    7.31 -    by (fact fun_left_comm_idem_inf)
    7.32 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    7.33 +    by (fact comp_fun_idem_inf)
    7.34    show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
    7.35  qed
    7.36  
    7.37  lemma (in complete_lattice) Sup_set_fold [code_unfold]:
    7.38    "Sup (set xs) = foldl sup bot xs"
    7.39  proof -
    7.40 -  interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    7.41 -    by (fact fun_left_comm_idem_sup)
    7.42 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    7.43 +    by (fact comp_fun_idem_sup)
    7.44    show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
    7.45  qed
    7.46  
    7.47 @@ -3762,8 +3762,8 @@
    7.48    "insort x (insort y xs) = insort y (insort x xs)"
    7.49    by (cases "x = y") (auto intro: insort_key_left_comm)
    7.50  
    7.51 -lemma fun_left_comm_insort:
    7.52 -  "fun_left_comm insort"
    7.53 +lemma comp_fun_commute_insort:
    7.54 +  "comp_fun_commute insort"
    7.55  proof
    7.56  qed (simp add: insort_left_comm fun_eq_iff)
    7.57  
    7.58 @@ -4249,7 +4249,7 @@
    7.59    assumes "finite A"
    7.60    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
    7.61  proof -
    7.62 -  interpret fun_left_comm insort by (fact fun_left_comm_insort)
    7.63 +  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
    7.64    with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
    7.65  qed
    7.66  
    7.67 @@ -4261,7 +4261,7 @@
    7.68  lemma sorted_list_of_set_sort_remdups:
    7.69    "sorted_list_of_set (set xs) = sort (remdups xs)"
    7.70  proof -
    7.71 -  interpret fun_left_comm insort by (fact fun_left_comm_insort)
    7.72 +  interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
    7.73    show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
    7.74  qed
    7.75  
     8.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:56 2011 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 11:44:16 2011 +0200
     8.3 @@ -1826,8 +1826,8 @@
     8.4  lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
     8.5  lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto
     8.6  
     8.7 -lemma fun_left_comm_monoidal[intro]: assumes "monoidal opp" shows "fun_left_comm opp"
     8.8 -  unfolding fun_left_comm_def using monoidal_ac[OF assms] by auto
     8.9 +lemma comp_fun_commute_monoidal[intro]: assumes "monoidal opp" shows "comp_fun_commute opp"
    8.10 +  unfolding comp_fun_commute_def using monoidal_ac[OF assms] by auto
    8.11  
    8.12  lemma support_clauses:
    8.13    "\<And>f g s. support opp f {} = {}"
    8.14 @@ -1850,12 +1850,12 @@
    8.15  proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
    8.16    show ?thesis unfolding iterate_def if_P[OF True] * by auto
    8.17  next case False note x=this
    8.18 -  note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]]
    8.19 +  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
    8.20    show ?thesis proof(cases "f x = neutral opp")
    8.21      case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
    8.22        unfolding True monoidal_simps[OF assms(1)] by auto
    8.23    next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
    8.24 -      apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def])
    8.25 +      apply(subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
    8.26        using `finite s` unfolding support_def using False x by auto qed qed 
    8.27  
    8.28  lemma iterate_some: