src/HOL/Multivariate_Analysis/Integration.thy
changeset 42871 1c0b99f950d9
parent 42869 43b0f61f56d0
child 44125 230a8665c919
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 08:16:56 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 20 11:44:16 2011 +0200
     1.3 @@ -1826,8 +1826,8 @@
     1.4  lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
     1.5  lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto
     1.6  
     1.7 -lemma fun_left_comm_monoidal[intro]: assumes "monoidal opp" shows "fun_left_comm opp"
     1.8 -  unfolding fun_left_comm_def using monoidal_ac[OF assms] by auto
     1.9 +lemma comp_fun_commute_monoidal[intro]: assumes "monoidal opp" shows "comp_fun_commute opp"
    1.10 +  unfolding comp_fun_commute_def using monoidal_ac[OF assms] by auto
    1.11  
    1.12  lemma support_clauses:
    1.13    "\<And>f g s. support opp f {} = {}"
    1.14 @@ -1850,12 +1850,12 @@
    1.15  proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
    1.16    show ?thesis unfolding iterate_def if_P[OF True] * by auto
    1.17  next case False note x=this
    1.18 -  note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]]
    1.19 +  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
    1.20    show ?thesis proof(cases "f x = neutral opp")
    1.21      case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
    1.22        unfolding True monoidal_simps[OF assms(1)] by auto
    1.23    next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
    1.24 -      apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def])
    1.25 +      apply(subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
    1.26        using `finite s` unfolding support_def using False x by auto qed qed 
    1.27  
    1.28  lemma iterate_some: