From b2e090503965a3e1794882b6e084fcc9555594e1 Mon Sep 17 00:00:00 2001
From: Kevin Kappelmann <accounts@kappelmann.me>
Date: Wed, 19 Jun 2024 08:46:47 +0200
Subject: [PATCH] feat(*) bump versions; use the_inverse in set-extension

---
 AFP_VERSION                                   |  2 +-
 .../HOTG_Binary_Relation_Properties.thy       |  1 +
 .../HOTG_Binary_Relations_Wellfounded.thy     | 24 +++++++++++++++++++
 ISABELLE_VERSION                              |  2 +-
 .../Set_Extensions/Set_Extensions_Base.thy    |  8 ++-----
 .../Properties/TFunctions_Inverse.thy         | 12 ++++++++++
 6 files changed, 41 insertions(+), 8 deletions(-)
 create mode 100644 HOTG/Binary_Relations/Properties/HOTG_Binary_Relations_Wellfounded.thy

diff --git a/AFP_VERSION b/AFP_VERSION
index 9e63128..2f5399c 100644
--- a/AFP_VERSION
+++ b/AFP_VERSION
@@ -1 +1 @@
-86f66c826d6c25ab9d4cb6b58524385c8cd41ab2
+f6fe62e20895b6efbdf1c17e7a17cb5e5aeae355
diff --git a/HOTG/Binary_Relations/Properties/HOTG_Binary_Relation_Properties.thy b/HOTG/Binary_Relations/Properties/HOTG_Binary_Relation_Properties.thy
index 5bed958..2e4806f 100644
--- a/HOTG/Binary_Relations/Properties/HOTG_Binary_Relation_Properties.thy
+++ b/HOTG/Binary_Relations/Properties/HOTG_Binary_Relation_Properties.thy
@@ -12,6 +12,7 @@ theory HOTG_Binary_Relation_Properties
     HOTG_Binary_Relations_Surjective
     HOTG_Binary_Relations_Symmetric
     HOTG_Binary_Relations_Transitive
+    HOTG_Binary_Relations_Wellfounded
 begin
 
 end
\ No newline at end of file
diff --git a/HOTG/Binary_Relations/Properties/HOTG_Binary_Relations_Wellfounded.thy b/HOTG/Binary_Relations/Properties/HOTG_Binary_Relations_Wellfounded.thy
new file mode 100644
index 0000000..eba660d
--- /dev/null
+++ b/HOTG/Binary_Relations/Properties/HOTG_Binary_Relations_Wellfounded.thy
@@ -0,0 +1,24 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+subsection \<open>Well-Founded\<close>
+theory HOTG_Binary_Relations_Wellfounded
+  imports
+    HOTG_Binary_Relations_Base
+    Transport.Binary_Relations_Wellfounded
+begin
+
+overloading
+  wellfounded_set \<equiv> "wellfounded :: set \<Rightarrow> bool"
+begin
+  definition "wellfounded_set (R :: set) \<equiv> wellfounded (rel R)"
+end
+
+lemma wellfounded_set_iff_wellfounded_rel [iff]:
+  "wellfounded R \<longleftrightarrow> wellfounded (rel R)"
+  unfolding wellfounded_set_def by simp
+
+lemma set_wellfounded_pred_iff_wellfounded_pred_uhint [uhint]:
+  assumes "R \<equiv> rel S"
+  shows "wellfounded S \<equiv> wellfounded R"
+  using assms by simp
+
+end
diff --git a/ISABELLE_VERSION b/ISABELLE_VERSION
index 653415a..d42fdf7 100644
--- a/ISABELLE_VERSION
+++ b/ISABELLE_VERSION
@@ -1 +1 @@
-5f053991315c
+5e5dcebd1ed8
diff --git a/Isabelle_Set/Set_Extensions/Set_Extensions_Base.thy b/Isabelle_Set/Set_Extensions/Set_Extensions_Base.thy
index 130a7c1..9c548ba 100644
--- a/Isabelle_Set/Set_Extensions/Set_Extensions_Base.thy
+++ b/Isabelle_Set/Set_Extensions/Set_Extensions_Base.thy
@@ -59,17 +59,13 @@ lemma Core_subset_Abs: "Core \<subseteq> Abs"
   unfolding Abs_def by auto
 
 definition "l x \<equiv> if has_inverse_on Core embed x
-  then (THE c : Core. embed c = x)
+  then (the_inverse_on Core embed) x
   else \<langle>Core, x\<rangle>"
 
 lemma left_embed_eq_if_mem_Core [simp]:
   assumes "c \<in> Core"
   shows "l (embed c) = c"
-proof -
-  from assms embed_injective have "(THE c' : Core. embed c' = embed c) = c"
-    by (urule bthe_eqI where chained = insert) (auto dest: injective_onD)
-  with assms show ?thesis unfolding l_def by auto
-qed
+  unfolding l_def using assms embed_injective by auto
 
 corollary left_embed_mem_Core_if_mem_Core [intro]:
   assumes "c \<in> Core"
diff --git a/Soft_Types/Functions/Properties/TFunctions_Inverse.thy b/Soft_Types/Functions/Properties/TFunctions_Inverse.thy
index fb79d08..88da79c 100644
--- a/Soft_Types/Functions/Properties/TFunctions_Inverse.thy
+++ b/Soft_Types/Functions/Properties/TFunctions_Inverse.thy
@@ -6,6 +6,18 @@ theory TFunctions_Inverse
     Transport.Functions_Inverse
 begin
 
+definition "the_inverse_on_type T \<equiv> the_inverse_on (of_type T)"
+adhoc_overloading the_inverse_on the_inverse_on_type
+
+lemma the_inverse_on_type_eq_the_inverse_on_pred [simp]:
+  "the_inverse_on T = the_inverse_on (of_type T)"
+  unfolding the_inverse_on_type_def by simp
+
+lemma the_inverse_on_type_eq_the_inverse_on_pred_uhint [uhint]:
+  assumes "P \<equiv> of_type T"
+  shows "the_inverse_on (T :: 'a type) \<equiv> the_inverse_on P"
+  using assms by simp
+
 overloading
   inverse_on_type \<equiv> "inverse_on :: 'a type \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
 begin