# 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 \<open>Induction Principles\<close>
 
-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 \<in> A" and "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> P y) \<Longrightarrow> P x"
   shows "P x"
   using assms(2,3) by (auto intro: \<open>wf_on A r\<close>[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 \<in> A" and "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> r y x \<Longrightarrow> P y) \<Longrightarrow> 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 \<longleftrightarrow> wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}"
+proof (rule iffI)
+  assume wf: "wf_on A r"
+  show "wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}"
+    unfolding wf_def
+  proof (intro allI impI ballI)
+    fix P x
+    assume IH: "\<forall>x. (\<forall>y. (y, x) \<in> {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A} \<longrightarrow> P y) \<longrightarrow> P x"
+    show "P x"
+    proof (cases "x \<in> 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) \<in> r \<and> x \<in> A \<and> y \<in> A}"
+  show "wf_on A r"
+    unfolding wf_on_def
+  proof (intro allI impI ballI)
+    fix P x
+    assume IH: "\<forall>x\<in>A. (\<forall>y\<in>A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x" and "x \<in> A"
+    show "P x"
+      using wf \<open>x \<in> A\<close>
+    proof (induction x rule: wf_on_induct)
+      case in_set
+      show ?case
+        by simp
+    next
+      case (less y)
+      hence "\<And>z. (z, y) \<in> r \<Longrightarrow> z \<in> A \<Longrightarrow> P z"
+        by simp
+      thus ?case
+        using IH[rule_format, OF \<open>y \<in> A\<close>] by simp
+    qed
+  qed
+qed
+
 
 subsection \<open>Introduction Rules\<close>
 
@@ -162,8 +213,12 @@
   shows "B = {}"
 proof -
   have "x \<notin> B" if "x \<in> 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 \<notin> r `` B"
       using less.IH \<open>B \<subseteq> A\<close> 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 \<subseteq> A" and "B \<noteq> {}"
+  hence "\<exists>z\<in>f ` B. \<forall>y. R y z \<longrightarrow> y \<notin> f ` B"
+    using wf[unfolded wfp_on_iff_ex_minimal, rule_format, of "f ` B"] by blast
+  thus "\<exists>z\<in>B. \<forall>y. inv_imagep R f y z \<longrightarrow> y \<notin> B"
+    unfolding inv_imagep_def
+    by auto
+qed
+
 
 subsubsection \<open>Conversion to a known well-founded relation\<close>
 
+lemma wfp_on_if_convertible_to_wfp_on:
+  assumes
+    wf: "wfp_on (f ` A) Q" and
+    convertible: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q (f x) (f y))"
+  shows "wfp_on A R"
+  unfolding wfp_on_iff_ex_minimal
+proof (intro allI impI)
+  fix B assume "B \<subseteq> A" and "B \<noteq> {}"
+  moreover from wf have "wfp_on A (inv_imagep Q f)"
+    by (rule wfp_on_inv_imagep)
+  ultimately obtain y where "y \<in> B" and "\<And>z. Q (f z) (f y) \<Longrightarrow> z \<notin> B"
+    unfolding wfp_on_iff_ex_minimal in_inv_imagep
+    by blast
+  thus "\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B"
+    using \<open>B \<subseteq> A\<close> convertible by blast
+qed
+
+lemma wf_on_if_convertible_to_wf_on: "wf_on (f ` A) Q \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (f x, f y) \<in> Q) \<Longrightarrow> 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 \<Rightarrow> 'b"
   assumes "wf s" and convertible: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (f x, f y) \<in> s"
   shows "wf r"
-proof (rule wfI_min[of r])
-  fix x :: 'a and Q :: "'a set"
-  assume "x \<in> Q"
-  then obtain y where "y \<in> Q" and "\<And>z. (f z, f y) \<in> s \<Longrightarrow> z \<notin> Q"
-    by (auto elim: wfE_min[OF wf_inv_image[of s f, OF \<open>wf s\<close>], unfolded in_inv_image])
-  thus "\<exists>z \<in> Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> 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 \<open>wf s\<close> subset_UNIV] .
+next
+  show "\<And>x y. (x, y) \<in> r \<Longrightarrow> (f x, f y) \<in> s"
+    using convertible .
 qed
 
 lemma wfP_if_convertible_to_wfP: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> 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()