# HG changeset patch
# User paulson
# Date 1665677996 -3600
# Node ID 2317e9a192390b003faa707403c7c6d053e3377b
# Parent  71bf371a97844d3cd85fd6793faeb80645b70dee# Parent  61640505795152a7652e776be5fdc76f4745ef88
merged

diff -r 616405057951 -r 2317e9a19239 NEWS
--- a/NEWS	Thu Oct 13 17:19:50 2022 +0100
+++ b/NEWS	Thu Oct 13 17:19:56 2022 +0100
@@ -9,19 +9,23 @@
 
 *** HOL ***
 
+* Theory "HOL.Fun":
+  - Renamed lemma inj_on_strict_subset to image_strict_mono.
+    Minor INCOMPATIBILITY.
+
 * Theory "HOL.Relation":
   - Strengthened lemma total_on_singleton. Minor INCOMPATIBILITY.
   - Added lemmas.
       antisym_if_asymp
-      antisymp_ge[simp]
-      antisymp_greater[simp]
       antisymp_if_asymp
-      antisymp_le[simp]
-      antisymp_less[simp]
       irreflD
       irreflpD
-      reflp_ge[simp]
-      reflp_le[simp]
+      order.antisymp_ge[simp]
+      order.antisymp_le[simp]
+      preorder.antisymp_greater[simp]
+      preorder.antisymp_less[simp]
+      preorder.reflp_ge[simp]
+      preorder.reflp_le[simp]
       totalp_on_singleton[simp]
 
 * Theory "HOL.Wellfounded":
@@ -33,7 +37,7 @@
 * Theory "HOL-Library.FSet":
   - Added lemmas.
       fimage_strict_mono
-      inj_on_strict_fsubset
+      wfP_pfsubset
 
 
 New in Isabelle2022 (October 2022)
diff -r 616405057951 -r 2317e9a19239 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Thu Oct 13 17:19:50 2022 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Thu Oct 13 17:19:56 2022 +0100
@@ -708,7 +708,7 @@
   moreover have "inj_on f23 ?A2"
   using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
   ultimately
-  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset)
+  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: image_strict_mono)
   moreover
   {have "embed r1 r3 (f23 \<circ> f12)"
    using 1 EMB23 0 by (auto simp add: comp_embed)
diff -r 616405057951 -r 2317e9a19239 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 13 17:19:50 2022 +0100
+++ b/src/HOL/Fun.thy	Thu Oct 13 17:19:56 2022 +0100
@@ -178,7 +178,7 @@
 lemma inj_on_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A \<longleftrightarrow> inj_on g A"
   by (auto simp: inj_on_def)
 
-lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
+lemma image_strict_mono: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
   unfolding inj_on_def by blast
 
 lemma inj_compose: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
diff -r 616405057951 -r 2317e9a19239 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Oct 13 17:19:50 2022 +0100
+++ b/src/HOL/Library/FSet.thy	Thu Oct 13 17:19:56 2022 +0100
@@ -559,7 +559,7 @@
 lemma fimage_strict_mono:
   assumes "inj_on f (fset B)" and "A |\<subset>| B"
   shows "f |`| A |\<subset>| f |`| B"
-  \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.inj_on_strict_subset}.\<close>
+  \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.image_strict_mono}.\<close>
 proof (rule pfsubsetI)
   from \<open>A |\<subset>| B\<close> have "A |\<subseteq>| B"
     by (rule pfsubset_imp_fsubset)