# HG changeset patch # User desharna # Date 1623318854 -7200 # Node ID 77306bf4e1eec88b4da6e47363299764b538ef39 # Parent 58f6b41efe8816b4ad0c0a9a6e027e67c33f1a69# Parent 9447668d1b775e868bc752bc652c8243ba5329c1 merged diff -r 58f6b41efe88 -r 77306bf4e1ee NEWS --- a/NEWS Thu Jun 10 11:21:57 2021 +0200 +++ b/NEWS Thu Jun 10 11:54:14 2021 +0200 @@ -34,6 +34,12 @@ *** Document preparation *** +* More predefined symbols: \ \ (package "stmaryrd"), \ \ (LaTeX package +"pifont"). + +* High-quality blackboard-bold symbols from font "txmia" (LaTeX package +"pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\. + * Document antiquotations for ML text have been refined: "def" and "ref" variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def} (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit @@ -97,16 +103,23 @@ no longer required. +*** Pure *** + +* "global_interpretation" is applicable in instantiation and overloading +targets and in any nested target built on top of a target supporting +"global_interpretation". + + *** HOL *** -* Theory Multiset: dedicated predicate "multiset" is gone, use -explict expression instead. Minor INCOMPATIBILITY. - -* Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem -to empty_mset, member_mset, not_member_mset respectively. Minor -INCOMPATIBILITY. - -* Theory Multiset: consolidated operation and fact names: +* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone, +use explict expression instead. Minor INCOMPATIBILITY. + +* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty, +Melem, not_Melem to empty_mset, member_mset, not_member_mset +respectively. Minor INCOMPATIBILITY. + +* Theory "HOL-Library.Multiset": consolidated operation and fact names: inf_subset_mset ~> inter_mset sup_subset_mset ~> union_mset multiset_inter_def ~> inter_mset_def @@ -114,52 +127,52 @@ multiset_inter_count ~> count_inter_mset sup_subset_mset_count ~> count_union_mset -* Theory Multiset: syntax precendence for membership operations has been -adjusted to match the corresponding precendences on sets. Rare -INCOMPATIBILITY. - -* HOL-Analysis/HOL-Probability: indexed products of discrete -distributions, negative binomial distribution, Hoeffding's inequality, -Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some -more small lemmas. Some theorems that were stated awkwardly before were -corrected. Minor INCOMPATIBILITY. +* Theory "HOL-Library.Multiset": syntax precendence for membership +operations has been adjusted to match the corresponding precendences on +sets. Rare INCOMPATIBILITY. + +* Session "HOL-Analysis" and "HOL-Probability": indexed products of +discrete distributions, negative binomial distribution, Hoeffding's +inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, +and some more small lemmas. Some theorems that were stated awkwardly +before were corrected. Minor INCOMPATIBILITY. * Theorems "antisym" and "eq_iff" in class "order" have been renamed to "order.antisym" and "order.eq_iff", to coexist locally with "antisym" -and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant +and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant potential for change can be avoided if interpretations of type class "order" are replaced or augmented by interpretations of locale "ordering". -* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor +* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor INCOMPATIBILITY; note that for most applications less elementary lemmas exists. -* Dedicated session HOL-Combinatorics. INCOMPATIBILITY: theories +* Theory "HOL-Library.Permutation" has been renamed to the more specific +"HOL-Library.List_Permutation". Note that most notions from that theory +are already present in theory "HOL-Combinatorics.Permutations". +INCOMPATIBILITY. + +* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", "Multiset_Permutations", "Perm" have been moved there from session HOL-Library. -* Theory "Permutation" in HOL-Library has been renamed to the more -specific "List_Permutation". Note that most notions from that -theory are already present in theory "Permutations". INCOMPATIBILITY. - -* Lemma "permutes_induct" has been given stronger -hypotheses and named premises. INCOMPATIBILITY. - -* Theory "Transposition" in HOL-Combinatorics provides elementary -swap operation "transpose". - -* Combinator "Fun.swap" resolved into a mere input abbreviation -in separate theory "Transposition" in HOL-Combinatorics. -INCOMPATIBILITY. +* Theory "HOL-Combinatorics.Transposition" provides elementary swap +operation "transpose". + +* Lemma "permutes_induct" has been given stronger hypotheses and named +premises. INCOMPATIBILITY. + +* Combinator "Fun.swap" resolved into a mere input abbreviation in +separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. * Bit operations set_bit, unset_bit and flip_bit are now class -operations. INCOMPATIBILITY. +operations. INCOMPATIBILITY. * Abbreviation "max_word" has been moved to session Word_Lib in the AFP, as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", -"setBit", "clearBit". See there further the changelog in theory Guide. +"setBit", "clearBit". See there further the changelog in theory Guide. INCOMPATIBILITY. @@ -231,10 +244,27 @@ *** System *** +* ML profiling has been updated and reactivated, after some degration in +Isabelle2021: + + - "isabelle build -o threads=1 -o profiling=..." works properly + within the PIDE session context; + + - "isabelle profiling_report" now uses the session build database + (like "isabelle log"); + + - output uses non-intrusive tracing messages, instead of warnings. + * System option "system_log" specifies an optional log file for internal -messages produced by Output.system_message in Isabelle/ML; "-" refers to -console progress of the build job. This works for "isabelle build" or -any derivative of it. +messages produced by Output.system_message in Isabelle/ML; the value +"true" refers to console progress of the build job. This works for +"isabelle build" or any derivative of it. + +* System options of type string may be set to "true" using the short +notation of type bool. E.g. "isabelle build -o system_log". + +* System option "document=true" is an alias for "document=pdf" and thus +can be used in the short form. E.g. "isabelle build -o document". * Command-line tool "isabelle version" supports repository archives (without full .hg directory). More options. @@ -991,12 +1021,6 @@ *** Document preparation *** -* More predefined symbols: \ \ (package "stmaryrd"), \ \ (package -"pifont"). - -* High-quality blackboard-bold symbols from font "txmia" (package -"pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\. - * Document markers are formal comments of the form \<^marker>\marker_body\ that are stripped from document output: the effect is to modify the semantic presentation context or to emit markup to the PIDE document. Some diff -r 58f6b41efe88 -r 77306bf4e1ee etc/options --- a/etc/options Thu Jun 10 11:21:57 2021 +0200 +++ b/etc/options Thu Jun 10 11:54:14 2021 +0200 @@ -6,7 +6,7 @@ -- "generate theory browser information" option document : string = "" - -- "build document in given format: pdf, dvi, false" + -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" option document_output : string = "" -- "document output directory" option document_variants : string = "document" @@ -132,7 +132,7 @@ -- "ML profiling (possible values: time, allocations)" option system_log : string = "" - -- "output for system messages (log file or \"-\" for console progress)" + -- "output for system messages (log file or \"true\" for console progress)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" @@ -305,10 +305,10 @@ section "Phabricator" -option phabricator_version_arcanist : string = "7af9846f994a8d0a1fc89af996e3ddd81f01765e" +option phabricator_version_arcanist : string = "cdae0ac68f1fed138323fa3dbb299ef3b287723c" -- "repository version for arcanist" -option phabricator_version_phabricator : string = "2afedad61c5181bb4f832cea27b9b59df19f3fd5" +option phabricator_version_phabricator : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a" -- "repository version for phabricator" diff -r 58f6b41efe88 -r 77306bf4e1ee src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Thu Jun 10 11:21:57 2021 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Thu Jun 10 11:54:14 2021 +0200 @@ -738,6 +738,9 @@ free variable whose name is already bound in the context --- for example, because a constant of that name exists --- add it to the \<^theory_text>\for\ clause. + When used in a nested target, resulting declarations are propagated + through the whole target stack. + \<^descr> \<^theory_text>\sublocale name \ expr defines defs\ interprets \expr\ into the locale \name\. A proof that the specification of \name\ implies the specification of \expr\ is required. As in the localized version of the diff -r 58f6b41efe88 -r 77306bf4e1ee src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Thu Jun 10 11:21:57 2021 +0200 +++ b/src/Doc/System/Presentation.thy Thu Jun 10 11:54:14 2021 +0200 @@ -47,9 +47,9 @@ reported by the above verbose invocation of the build process. Many Isabelle sessions (such as \<^session>\HOL-Library\ in - \<^dir>\~~/src/HOL/Library\) also provide printable documents in PDF. These are + \<^dir>\~~/src/HOL/Library\) also provide theory documents in PDF. These are prepared automatically as well if enabled like this: - @{verbatim [display] \isabelle build -o browser_info -o document=pdf -v -c HOL-Library\} + @{verbatim [display] \isabelle build -o browser_info -o document -v -c HOL-Library\} Enabling both browser info and document preparation simultaneously causes an appropriate ``document'' link to be included in the HTML index. Documents diff -r 58f6b41efe88 -r 77306bf4e1ee src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Thu Jun 10 11:21:57 2021 +0200 +++ b/src/Doc/System/Sessions.thy Thu Jun 10 11:54:14 2021 +0200 @@ -201,8 +201,9 @@ info, see also \secref{sec:info}. \<^item> @{system_option_def "document"} controls document output for a - particular session or theory; \<^verbatim>\document=pdf\ means enabled, - \<^verbatim>\document=false\ means disabled (especially for particular theories). + particular session or theory; \<^verbatim>\document=pdf\ or \<^verbatim>\document=true\ means + enabled, \<^verbatim>\document=""\ or \<^verbatim>\document=false\ means disabled (especially + for particular theories). \<^item> @{system_option_def "document_output"} specifies an alternative directory for generated output of the document preparation system; the @@ -278,7 +279,8 @@ \<^item> @{system_option_def system_log} specifies an optional log file for low-level messages produced by \<^ML>\Output.system_message\ in - Isabelle/ML; ``\<^verbatim>\-\'' refers to console progress of the build job. + Isabelle/ML; the value ``\<^verbatim>\true\'' refers to console progress of the build + job. \<^item> @{system_option_def "system_heaps"} determines the directories for session heap images: \<^path>\$ISABELLE_HEAPS\ is the user directory and @@ -410,11 +412,12 @@ The build process depends on additional options (\secref{sec:system-options}) that are passed to the prover eventually. The settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide - additional defaults, e.g.\ \<^verbatim>\ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\. - Moreover, the environment of system build options may be augmented on the - command line via \<^verbatim>\-o\~\name\\<^verbatim>\=\\value\ or \<^verbatim>\-o\~\name\, which abbreviates - \<^verbatim>\-o\~\name\\<^verbatim>\=true\ for Boolean options. Multiple occurrences of \<^verbatim>\-o\ on - the command-line are applied in the given order. + additional defaults, e.g.\ \<^verbatim>\ISABELLE_BUILD_OPTIONS="document=pdf + threads=4"\. Moreover, the environment of system build options may be + augmented on the command line via \<^verbatim>\-o\~\name\\<^verbatim>\=\\value\ or \<^verbatim>\-o\~\name\, + which abbreviates \<^verbatim>\-o\~\name\\<^verbatim>\=true\ for Boolean or string options. + Multiple occurrences of \<^verbatim>\-o\ on the command-line are applied in the given + order. \<^medskip> Option \<^verbatim>\-P\ enables PDF/HTML presentation in the given directory, where @@ -496,7 +499,7 @@ \<^smallskip> Build all sessions with HTML browser info and PDF document preparation: - @{verbatim [display] \isabelle build -a -o browser_info -o document=pdf\} + @{verbatim [display] \isabelle build -a -o browser_info -o document\} \<^smallskip> Build all sessions with a maximum of 8 parallel prover processes and 4 @@ -539,6 +542,7 @@ -U output Unicode symbols -m MARGIN margin for pretty printing (default: 76.0) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -v print all messages, including information etc. Print messages from the build database of the given session, without any checks against current sources: results from a failed build can be @@ -563,8 +567,8 @@ symbols. The default is for an old-fashioned ASCII terminal at 80 characters per line (76 + 4 characters to prefix warnings or errors). - \<^medskip> Option \<^verbatim>\-v\ prints all messages from the session database, including - extra information and tracing messages etc. + \<^medskip> Option \<^verbatim>\-v\ prints all messages from the session database that are + normally inlined into the source text, including information messages etc. \ subsubsection \Examples\ diff -r 58f6b41efe88 -r 77306bf4e1ee src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Jun 10 11:21:57 2021 +0200 +++ b/src/HOL/Finite_Set.thy Thu Jun 10 11:54:14 2021 +0200 @@ -710,21 +710,23 @@ subsection \A basic fold functional for finite sets\ -text \The intended behaviour is - \fold f z {x\<^sub>1, \, x\<^sub>n} = f x\<^sub>1 (\ (f x\<^sub>n z)\)\ - if \f\ is ``left-commutative'': +text \ + The intended behaviour is \fold f z {x\<^sub>1, \, x\<^sub>n} = f x\<^sub>1 (\ (f x\<^sub>n z)\)\ + if \f\ is ``left-commutative''. + The commutativity requirement is relativised to the carrier set \S\: \ -locale comp_fun_commute = +locale comp_fun_commute_on = + fixes S :: "'a set" fixes f :: "'a \ 'b \ 'b" - assumes comp_fun_commute: "f y \ f x = f x \ f y" + assumes comp_fun_commute_on: "x \ S \ y \ S \ f y \ f x = f x \ f y" begin -lemma fun_left_comm: "f y (f x z) = f x (f y z)" - using comp_fun_commute by (simp add: fun_eq_iff) +lemma fun_left_comm: "x \ S \ y \ S \ f y (f x z) = f x (f y z)" + using comp_fun_commute_on by (simp add: fun_eq_iff) -lemma commute_left_comp: "f y \ (f x \ g) = f x \ (f y \ g)" - by (simp add: o_assoc comp_fun_commute) +lemma commute_left_comp: "x \ S \ y \ S \ f y \ (f x \ g) = f x \ (f y \ g)" + by (simp add: o_assoc comp_fun_commute_on) end @@ -776,7 +778,7 @@ by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that) text \ - A tempting alternative for the definiens is + A tempting alternative for the definition is \<^term>\if finite A then THE y. fold_graph f z A y else e\. It allows the removal of finiteness assumptions from the theorems \fold_comm\, \fold_reindex\ and \fold_distrib\. @@ -789,7 +791,7 @@ subsubsection \From \<^const>\fold_graph\ to \<^term>\fold\\ -context comp_fun_commute +context comp_fun_commute_on begin lemma fold_graph_finite: @@ -798,7 +800,10 @@ using assms by induct simp_all lemma fold_graph_insertE_aux: - "fold_graph f z A y \ a \ A \ \y'. y = f a y' \ fold_graph f z (A - {a}) y'" + assumes "A \ S" + assumes "fold_graph f z A y" "a \ A" + shows "\y'. y = f a y' \ fold_graph f z (A - {a}) y'" + using assms(2-,1) proof (induct set: fold_graph) case emptyI then show ?case by simp @@ -812,8 +817,9 @@ case False then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'" using insertI by auto - have "f x y = f a (f x y')" - unfolding y by (rule fun_left_comm) + from insertI have "x \ S" "a \ S" by auto + then have "f x y = f a (f x y')" + unfolding y by (intro fun_left_comm; simp) moreover have "fold_graph f z (insert x A - {a}) (f x y')" using y' and \x \ a\ and \x \ A\ by (simp add: insert_Diff_if fold_graph.insertI) @@ -823,35 +829,41 @@ qed lemma fold_graph_insertE: + assumes "insert x A \ S" assumes "fold_graph f z (insert x A) v" and "x \ A" obtains y where "v = f x y" and "fold_graph f z A y" - using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1]) + using assms by (auto dest: fold_graph_insertE_aux[OF \insert x A \ S\ _ insertI1]) -lemma fold_graph_determ: "fold_graph f z A x \ fold_graph f z A y \ y = x" +lemma fold_graph_determ: + assumes "A \ S" + assumes "fold_graph f z A x" "fold_graph f z A y" + shows "y = x" + using assms(2-,1) proof (induct arbitrary: y set: fold_graph) case emptyI then show ?case by fast next case (insertI x A y v) - from \fold_graph f z (insert x A) v\ and \x \ A\ + from \insert x A \ S\ and \fold_graph f z (insert x A) v\ and \x \ A\ obtain y' where "v = f x y'" and "fold_graph f z A y'" by (rule fold_graph_insertE) - from \fold_graph f z A y'\ have "y' = y" - by (rule insertI) + from \fold_graph f z A y'\ insertI have "y' = y" + by simp with \v = f x y'\ show "v = f x y" by simp qed -lemma fold_equality: "fold_graph f z A y \ fold f z A = y" +lemma fold_equality: "A \ S \ fold_graph f z A y \ fold f z A = y" by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite) lemma fold_graph_fold: + assumes "A \ S" assumes "finite A" shows "fold_graph f z A (fold f z A)" proof - - from assms have "\x. fold_graph f z A x" + from \finite A\ have "\x. fold_graph f z A x" by (rule finite_imp_fold_graph) - moreover note fold_graph_determ + moreover note fold_graph_determ[OF \A \ S\] ultimately have "\!x. fold_graph f z A x" by (rule ex_ex1I) then have "fold_graph f z A (The (fold_graph f z A))" @@ -871,12 +883,13 @@ text \The various recursion equations for \<^const>\fold\:\ lemma fold_insert [simp]: + assumes "insert x A \ S" assumes "finite A" and "x \ A" shows "fold f z (insert x A) = f x (fold f z A)" -proof (rule fold_equality) +proof (rule fold_equality[OF \insert x A \ S\]) fix z - from \finite A\ have "fold_graph f z A (fold f z A)" - by (rule fold_graph_fold) + from \insert x A \ S\ \finite A\ have "fold_graph f z A (fold f z A)" + by (blast intro: fold_graph_fold) with \x \ A\ have "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI) then show "fold_graph f z (insert x A) (f x (fold f z A))" @@ -886,20 +899,33 @@ declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del] \ \No more proofs involve these.\ -lemma fold_fun_left_comm: "finite A \ f x (fold f z A) = fold f (f x z) A" +lemma fold_fun_left_comm: + assumes "insert x A \ S" "finite A" + shows "f x (fold f z A) = fold f (f x z) A" + using assms(2,1) proof (induct rule: finite_induct) case empty then show ?case by simp next - case insert - then show ?case - by (simp add: fun_left_comm [of x]) + case (insert y F) + then have "fold f (f x z) (insert y F) = f y (fold f (f x z) F)" + by simp + also have "\ = f x (f y (fold f z F))" + using insert by (simp add: fun_left_comm[where ?y=x]) + also have "\ = f x (fold f z (insert y F))" + proof - + from insert have "insert y F \ S" by simp + from fold_insert[OF this] insert show ?thesis by simp + qed + finally show ?case .. qed -lemma fold_insert2: "finite A \ x \ A \ fold f z (insert x A) = fold f (f x z) A" +lemma fold_insert2: + "insert x A \ S \ finite A \ x \ A \ fold f z (insert x A) = fold f (f x z) A" by (simp add: fold_fun_left_comm) lemma fold_rec: + assumes "A \ S" assumes "finite A" and "x \ A" shows "fold f z A = f x (fold f z (A - {x}))" proof - @@ -908,11 +934,12 @@ then have "fold f z A = fold f z (insert x (A - {x}))" by simp also have "\ = f x (fold f z (A - {x}))" - by (rule fold_insert) (simp add: \finite A\)+ + by (rule fold_insert) (use assms in \auto\) finally show ?thesis . qed lemma fold_insert_remove: + assumes "insert x A \ S" assumes "finite A" shows "fold f z (insert x A) = f x (fold f z (A - {x}))" proof - @@ -921,20 +948,77 @@ moreover have "x \ insert x A" by auto ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))" - by (rule fold_rec) + using \insert x A \ S\ by (blast intro: fold_rec) then show ?thesis by simp qed lemma fold_set_union_disj: + assumes "A \ S" "B \ S" assumes "finite A" "finite B" "A \ B = {}" shows "Finite_Set.fold f z (A \ B) = Finite_Set.fold f (Finite_Set.fold f z A) B" - using assms(2,1,3) by induct simp_all + using \finite B\ assms(1,2,3,5) +proof induct + case (insert x F) + have "fold f z (A \ insert x F) = f x (fold f (fold f z A) F)" + using insert by auto + also have "\ = fold f (fold f z A) (insert x F)" + using insert by (blast intro: fold_insert[symmetric]) + finally show ?case . +qed simp + end text \Other properties of \<^const>\fold\:\ +lemma fold_graph_image: + assumes "inj_on g A" + shows "fold_graph f z (g ` A) = fold_graph (f \ g) z A" +proof + fix w + show "fold_graph f z (g ` A) w = fold_graph (f o g) z A w" + proof + assume "fold_graph f z (g ` A) w" + then show "fold_graph (f \ g) z A w" + using assms + proof (induct "g ` A" w arbitrary: A) + case emptyI + then show ?case by (auto intro: fold_graph.emptyI) + next + case (insertI x A r B) + from \inj_on g B\ \x \ A\ \insert x A = image g B\ obtain x' A' + where "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'" + by (rule inj_img_insertE) + from insertI.prems have "fold_graph (f \ g) z A' r" + by (auto intro: insertI.hyps) + with \x' \ A'\ have "fold_graph (f \ g) z (insert x' A') ((f \ g) x' r)" + by (rule fold_graph.insertI) + then show ?case + by simp + qed + next + assume "fold_graph (f \ g) z A w" + then show "fold_graph f z (g ` A) w" + using assms + proof induct + case emptyI + then show ?case + by (auto intro: fold_graph.emptyI) + next + case (insertI x A r) + from \x \ A\ insertI.prems have "g x \ g ` A" + by auto + moreover from insertI have "fold_graph f z (g ` A) r" + by simp + ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)" + by (rule fold_graph.insertI) + then show ?case + by simp + qed + qed +qed + lemma fold_image: assumes "inj_on g A" shows "fold f z (g ` A) = fold (f \ g) z A" @@ -944,70 +1028,26 @@ by (auto dest: finite_imageD simp add: fold_def) next case True - have "fold_graph f z (g ` A) = fold_graph (f \ g) z A" - proof - fix w - show "fold_graph f z (g ` A) w \ fold_graph (f \ g) z A w" (is "?P \ ?Q") - proof - assume ?P - then show ?Q - using assms - proof (induct "g ` A" w arbitrary: A) - case emptyI - then show ?case by (auto intro: fold_graph.emptyI) - next - case (insertI x A r B) - from \inj_on g B\ \x \ A\ \insert x A = image g B\ obtain x' A' - where "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'" - by (rule inj_img_insertE) - from insertI.prems have "fold_graph (f \ g) z A' r" - by (auto intro: insertI.hyps) - with \x' \ A'\ have "fold_graph (f \ g) z (insert x' A') ((f \ g) x' r)" - by (rule fold_graph.insertI) - then show ?case - by simp - qed - next - assume ?Q - then show ?P - using assms - proof induct - case emptyI - then show ?case - by (auto intro: fold_graph.emptyI) - next - case (insertI x A r) - from \x \ A\ insertI.prems have "g x \ g ` A" - by auto - moreover from insertI have "fold_graph f z (g ` A) r" - by simp - ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)" - by (rule fold_graph.insertI) - then show ?case - by simp - qed - qed - qed - with True assms show ?thesis - by (auto simp add: fold_def) + then show ?thesis + by (auto simp add: fold_def fold_graph_image[OF assms]) qed lemma fold_cong: - assumes "comp_fun_commute f" "comp_fun_commute g" - and "finite A" + assumes "comp_fun_commute_on S f" "comp_fun_commute_on S g" + and "A \ S" "finite A" and cong: "\x. x \ A \ f x = g x" and "s = t" and "A = B" shows "fold f s A = fold g t B" proof - have "fold f s A = fold g s A" - using \finite A\ cong + using \finite A\ \A \ S\ cong proof (induct A) case empty then show ?case by simp next case insert - interpret f: comp_fun_commute f by (fact \comp_fun_commute f\) - interpret g: comp_fun_commute g by (fact \comp_fun_commute g\) + interpret f: comp_fun_commute_on S f by (fact \comp_fun_commute_on S f\