# HG changeset patch # User wenzelm # Date 1711484207 -3600 # Node ID 6d01661a055bd30f6601efcacf46d06a9f04c89c # Parent ce9b649ee2dde3497229200061f2e4990cfa2018# Parent 11a1f4d7af5151d66bd27e3eda809150abf2eb48 merged; diff -r ce9b649ee2dd -r 6d01661a055b NEWS --- a/NEWS Tue Mar 26 21:09:46 2024 +0100 +++ b/NEWS Tue Mar 26 21:16:47 2024 +0100 @@ -111,7 +111,7 @@ Lemmas wf_def and wfP_def are explicitly provided for backward compatibility but their usage is discouraged. Minor INCOMPATIBILITY. - Added wfp as alias for wfP for greater consistency with other predicates - such as asymp, transp, or totalp. + such as asymp, transp, or totalp. - Added lemmas. wellorder.wfp_on_less[simp] wfP_iff_ex_minimal @@ -120,13 +120,17 @@ wf_onI_pf wf_on_antimono wf_on_antimono_strong + wf_on_if_convertible_to_wf_on wf_on_iff_ex_minimal + wf_on_iff_wf wf_on_induct wf_on_subset wfp_on_antimono wfp_on_antimono_strong + wfp_on_if_convertible_to_wfp_on wfp_on_iff_ex_minimal wfp_on_induct + wfp_on_inv_imagep wfp_on_subset wfp_on_wf_on_eq diff -r ce9b649ee2dd -r 6d01661a055b src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Tue Mar 26 21:09:46 2024 +0100 +++ b/src/HOL/Wellfounded.thy Tue Mar 26 21:16:47 2024 +0100 @@ -49,12 +49,12 @@ subsection \Induction Principles\ -lemma wf_on_induct[consumes 2, case_names less, induct set: wf_on]: +lemma wf_on_induct[consumes 1, case_names in_set less, induct set: wf_on]: assumes "wf_on A r" and "x \ A" and "\x. x \ A \ (\y. y \ A \ (y, x) \ r \ P y) \ P x" shows "P x" using assms(2,3) by (auto intro: \wf_on A r\[unfolded wf_on_def, rule_format]) -lemma wfp_on_induct[consumes 2, case_names less, induct pred: wfp_on]: +lemma wfp_on_induct[consumes 1, case_names in_set less, induct pred: wfp_on]: assumes "wfp_on A r" and "x \ A" and "\x. x \ A \ (\y. y \ A \ r y x \ P y) \ P x" shows "P x" using assms by (fact wf_on_induct[to_pred]) @@ -71,6 +71,57 @@ lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] +lemma wf_on_iff_wf: "wf_on A r \ wf {(x, y) \ r. x \ A \ y \ A}" +proof (rule iffI) + assume wf: "wf_on A r" + show "wf {(x, y) \ r. x \ A \ y \ A}" + unfolding wf_def + proof (intro allI impI ballI) + fix P x + assume IH: "\x. (\y. (y, x) \ {(x, y). (x, y) \ r \ x \ A \ y \ A} \ P y) \ P x" + show "P x" + proof (cases "x \ A") + case True + show ?thesis + using wf + proof (induction x rule: wf_on_induct) + case in_set + thus ?case + using True . + next + case (less x) + thus ?case + by (auto intro: IH[rule_format]) + qed + next + case False + then show ?thesis + by (auto intro: IH[rule_format]) + qed + qed +next + assume wf: "wf {(x, y). (x, y) \ r \ x \ A \ y \ A}" + show "wf_on A r" + unfolding wf_on_def + proof (intro allI impI ballI) + fix P x + assume IH: "\x\A. (\y\A. (y, x) \ r \ P y) \ P x" and "x \ A" + show "P x" + using wf \x \ A\ + proof (induction x rule: wf_on_induct) + case in_set + show ?case + by simp + next + case (less y) + hence "\z. (z, y) \ r \ z \ A \ P z" + by simp + thus ?case + using IH[rule_format, OF \y \ A\] by simp + qed + qed +qed + subsection \Introduction Rules\ @@ -162,8 +213,12 @@ shows "B = {}" proof - have "x \ B" if "x \ A" for x - using wf that + using wf proof (induction x rule: wf_on_induct) + case in_set + show ?case + using that . + next case (less x) have "x \ r `` B" using less.IH \B \ A\ by blast @@ -906,20 +961,52 @@ by (clarsimp simp: inv_image_def wf_eq_minimal) qed +lemma wfp_on_inv_imagep: + assumes wf: "wfp_on (f ` A) R" + shows "wfp_on A (inv_imagep R f)" + unfolding wfp_on_iff_ex_minimal +proof (intro allI impI) + fix B assume "B \ A" and "B \ {}" + hence "\z\f ` B. \y. R y z \ y \ f ` B" + using wf[unfolded wfp_on_iff_ex_minimal, rule_format, of "f ` B"] by blast + thus "\z\B. \y. inv_imagep R f y z \ y \ B" + unfolding inv_imagep_def + by auto +qed + subsubsection \Conversion to a known well-founded relation\ +lemma wfp_on_if_convertible_to_wfp_on: + assumes + wf: "wfp_on (f ` A) Q" and + convertible: "(\x y. x \ A \ y \ A \ R x y \ Q (f x) (f y))" + shows "wfp_on A R" + unfolding wfp_on_iff_ex_minimal +proof (intro allI impI) + fix B assume "B \ A" and "B \ {}" + moreover from wf have "wfp_on A (inv_imagep Q f)" + by (rule wfp_on_inv_imagep) + ultimately obtain y where "y \ B" and "\z. Q (f z) (f y) \ z \ B" + unfolding wfp_on_iff_ex_minimal in_inv_imagep + by blast + thus "\z \ B. \y. R y z \ y \ B" + using \B \ A\ convertible by blast +qed + +lemma wf_on_if_convertible_to_wf_on: "wf_on (f ` A) Q \ (\x y. x \ A \ y \ A \ (x, y) \ R \ (f x, f y) \ Q) \ wf_on A R" + using wfp_on_if_convertible_to_wfp_on[to_set] . + lemma wf_if_convertible_to_wf: fixes r :: "'a rel" and s :: "'b rel" and f :: "'a \ 'b" assumes "wf s" and convertible: "\x y. (x, y) \ r \ (f x, f y) \ s" shows "wf r" -proof (rule wfI_min[of r]) - fix x :: 'a and Q :: "'a set" - assume "x \ Q" - then obtain y where "y \ Q" and "\z. (f z, f y) \ s \ z \ Q" - by (auto elim: wfE_min[OF wf_inv_image[of s f, OF \wf s\], unfolded in_inv_image]) - thus "\z \ Q. \y. (y, z) \ r \ y \ Q" - by (auto intro: convertible) +proof (rule wf_on_if_convertible_to_wf_on) + show "wf_on (range f) s" + using wf_on_subset[OF \wf s\ subset_UNIV] . +next + show "\x y. (x, y) \ r \ (f x, f y) \ s" + using convertible . qed lemma wfP_if_convertible_to_wfP: "wfP S \ (\x y. R x y \ S (f x) (f y)) \ wfP R" diff -r ce9b649ee2dd -r 6d01661a055b src/Pure/General/html.scala --- a/src/Pure/General/html.scala Tue Mar 26 21:09:46 2024 +0100 +++ b/src/Pure/General/html.scala Tue Mar 26 21:16:47 2024 +0100 @@ -239,6 +239,8 @@ body foreach { case XML.Elem(markup, Nil) => XML.output_elem(s, markup, end = true) + case XML.Elem(Markup(RAW, _), List(XML.Text(raw))) => + s ++= raw case XML.Elem(markup, ts) => if (structural && structural_elements(markup.name)) s += '\n' XML.output_elem(s, markup) @@ -261,7 +263,10 @@ /* input */ + val RAW = "raw" + def input(text: String): String = Jsoup_Entities.unescape(text) + def input_raw(text: String): XML.Elem = XML.elem(RAW, List(XML.Text(input(text)))) def parse_document(html: String): Jsoup_Document = Jsoup.parse(html) def get_document(url: String): Jsoup_Document = Jsoup.connect(url).get()