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.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.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.28  lemma iterate_some:
{"ft_lang_label":"__label__en","ft_lang_prob":0.51427037,"math_prob":0.73017305,"size":1792,"snap":"2019-43-2019-47","text_gpt3_token_len":548,"char_repetition_ratio":0.15100671,"word_repetition_ratio":0.017857144,"special_character_ratio":0.35044643,"punctuation_ratio":0.16666667,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.96328,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-22T04:08:35Z\",\"WARC-Record-ID\":\"<urn:uuid:8ae405f2-4dad-4425-95d8-4d4fe4316bf4>\",\"Content-Length\":\"7042\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:de2508b3-aee2-47d0-82c9-5ee1286eeac3>\",\"WARC-Concurrent-To\":\"<urn:uuid:5c0dc841-9aa8-4e79-938c-66ecba886c62>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"http://isabelle.in.tum.de/repos/isabelle/diff/1c0b99f950d9/src/HOL/Multivariate_Analysis/Integration.thy\",\"WARC-Payload-Digest\":\"sha1:3ZXSCYPPCVYIAUJOG6AHF352BGKMSTAY\",\"WARC-Block-Digest\":\"sha1:TOQKHU5RFOUBWPQHA7BEIPIRMY3JGCA4\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570987798619.84_warc_CC-MAIN-20191022030805-20191022054305-00332.warc.gz\"}"}