--- 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)
--- 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)
--- 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)"
--- 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)