# HG changeset patch
# User desharna
# Date 1665672349 -7200
# Node ID bed09d3ddc237992e060eef9a86557389e442405
# Parent  3158975d80e279700074e3bbb285ddabadcec80c# Parent  e381884c09d4f47e5b7d28c1dd43361fe82abd1c
merged

diff -r e381884c09d4 -r bed09d3ddc23 NEWS
--- a/NEWS	Thu Oct 13 14:49:15 2022 +0200
+++ b/NEWS	Thu Oct 13 16:45:49 2022 +0200
@@ -9,6 +9,10 @@
 
 *** 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.
@@ -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 e381884c09d4 -r bed09d3ddc23 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Thu Oct 13 16:45:49 2022 +0200
@@ -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 e381884c09d4 -r bed09d3ddc23 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 13 16:45:49 2022 +0200
@@ -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 e381884c09d4 -r bed09d3ddc23 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/Library/FSet.thy	Thu Oct 13 16:45:49 2022 +0200
@@ -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)