feat(*) bump versions; use the_inverse in set-extension

AFP_VERSION

@@ -1 +1 @@
-86f66c826d6c25ab9d4cb6b58524385c8cd41ab2
+f6fe62e20895b6efbdf1c17e7a17cb5e5aeae355

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

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

ISABELLE_VERSION

@@ -1 +1 @@
-5f053991315c
+5e5dcebd1ed8

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"

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