feat(HOTG) fix sorry

HOTG/Binary_Relations/HOTG_Binary_Relations_Extend.thy

@@ -110,7 +110,7 @@ lemma glue_bin_union_eq_glue_bin_union_glue [simp]: "glue (\<R> \<union> \<R>')
 
 lemma mono_glue: "((\<subseteq>) \<Rightarrow> (\<subseteq>)) glue" by auto
 
-lemma is_bin_rel_glue_if_is_bin_rel_if_mem:
+lemma is_bin_rel_glue_if_is_bin_rel_if_mem [intro]:
   assumes "\<And>R. R \<in> \<R> \<Longrightarrow> is_bin_rel R"
   shows "is_bin_rel (glue \<R>)"
   using assms by (intro is_bin_relI) auto

HOTG/Functions/HOTG_Clean_Functions.thy

@@ -104,19 +104,19 @@ lemma set_crel_dep_mono_wrt_predI':
   supply is_bin_rel_if_set_dep_bin_rel[uhint]
   using assms by (urule crel_dep_mono_wrt_predI')
 
+lemma set_crel_dep_mono_wrt_pred_if_mem_of_dom_le_if_set_rel_dep_mono_wrt_pred:
+  assumes "((x : A) \<rightarrow> B x) R"
+  and [uhint]: "is_bin_rel R"
+  and "mem_of (dom R) \<le> A"
+  shows "((x : A) \<rightarrow>\<^sub>c B x) R"
+  by (urule crel_dep_mono_wrt_predI) (urule assms)+
+
 lemma set_crel_mono_wrt_predI [intro]:
   assumes "(A \<rightarrow>\<^sub>c B) (rel R)"
   and "is_bin_rel R"
   shows "(A \<rightarrow>\<^sub>c B) R"
   using assms by (urule set_crel_dep_mono_wrt_predI)
 
-lemma set_crel_mono_wrt_predI':
-  assumes "left_total_on A R"
-  and "right_unique_on A R"
-  and "(A {\<times>} B) R"
-  shows "(A \<rightarrow>\<^sub>c B) (R :: set)"
-  using assms by (urule set_crel_dep_mono_wrt_predI')
-
 lemma set_crel_mono_wrt_predE:
   assumes "(A \<rightarrow>\<^sub>c B) R"
   obtains "(A \<rightarrow>\<^sub>c B) (rel R)" "is_bin_rel R"
@@ -135,6 +135,20 @@ lemma set_crel_mono_wrt_pred_eq_crel_mono_wrt_pred_uhint [uhint]:
   shows "(A \<rightarrow>\<^sub>c B) R \<equiv> (A' \<rightarrow>\<^sub>c B') R'"
   by (urule set_crel_dep_mono_wrt_pred_eq_crel_dep_mono_wrt_pred_uhint) (use assms in auto)
 
+lemma set_crel_mono_wrt_predI':
+  assumes "left_total_on A R"
+  and "right_unique_on A R"
+  and "(A {\<times>} B) R"
+  shows "(A \<rightarrow>\<^sub>c B) (R :: set)"
+  using assms by (urule set_crel_dep_mono_wrt_predI')
+
+lemma set_crel_mono_wrt_pred_if_mem_of_dom_le_if_set_rel_mono_wrt_pred:
+  assumes "(A \<rightarrow> B) R"
+  and "is_bin_rel R"
+  and "mem_of (dom R) \<le> A"
+  shows "(A \<rightarrow>\<^sub>c B) R"
+  using assms by (urule set_crel_dep_mono_wrt_pred_if_mem_of_dom_le_if_set_rel_dep_mono_wrt_pred)
+
 lemma eq_collect_mk_pair_eval_dom_if_set_crel_dep_mono_wrt_pred:
   assumes "((x : A) \<rightarrow>\<^sub>c B x) R"
   shows "R = {\<langle>x, R`x\<rangle> | x \<in> dom R}"
@@ -350,99 +364,4 @@ lemma set_set_crel_dep_mono_wrt_set_covariant_codom:
   by (urule subsetI, urule set_crel_dep_mono_wrt_pred_covariant_codom)
   (use assms in blast)+
 
-(* lemma eq_if_mem_if_mem_agree_if_mem_dep_functions:
-  assumes mem_dep_functions: "\<And>f. f \<in> F \<Longrightarrow> \<exists>B. f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and "agree A F"
-  and "f \<in> F"
-  and "g \<in> F"
-  shows "f = g"
-  using assms
-proof -
-  have "\<And>f. f \<in> F \<Longrightarrow> \<exists>B. f \<subseteq> \<Sum>x \<in> A. (B x)" by (blast dest: mem_dep_functions)
-  with assms show ?thesis by (intro eq_if_subset_dep_pairs_if_agree_set)
-qed
-
-lemma subset_if_agree_set_if_mem_dep_functions:
-  assumes "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and "f \<in> F"
-  and "agree A F"
-  and "g \<in> F"
-  shows "f \<subseteq> g"
-  using assms
-  by (elim mem_dep_functionsE subset_if_agree_set_if_subset_dep_pairs) auto
-
-lemma agree_set_if_eval_eq_if_mem_dep_functions:
-  assumes mem_dep_functions: "\<And>f. f \<in> F \<Longrightarrow> \<exists>B. f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and "\<And>f g x. f \<in> F \<Longrightarrow> g \<in> F \<Longrightarrow> x \<in> A \<Longrightarrow> R`x = g`x"
-  shows "agree A F"
-proof (subst agree_set_set_iff_agree_set, rule agree_setI)
-  fix x y f g presume hyps: "f \<in> F" "g \<in> F" "x \<in> A" and "\<langle>x, y\<rangle> \<in> R"
-  then have "y = R`x" using mem_dep_functions by auto
-  also have "... = g`x" by (fact assms(2)[OF hyps])
-  finally have y_eq: "y = g`x" .
-  from mem_dep_functions[OF \<open>g \<in> F\<close>] obtain B where "g \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)" by blast
-  with y_eq pair_mem_iff_eval_eq_if_mem_dom_dep_function \<open>x \<in> A\<close> show "\<langle>x, y\<rangle> \<in> g" by blast
-qed simp_all
-
-lemma eq_if_agree_if_mem_dep_functions:
-  assumes "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)" "g \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and "agree A {f, g}"
-  shows "f = g"
-  using assms
-  by (intro eq_if_mem_if_mem_agree_if_mem_dep_functions[of "{f, g}"]) auto
-
-lemma dep_functions_eval_eqI:
-  assumes "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and "g \<in> (x \<in> A') \<rightarrow>\<^sub>cs (B' x)"
-  and "f \<subseteq> g"
-  and "x \<in> A \<inter> A'"
-  shows "R`x = g`x"
-  using assms by (auto dest: right_unique_onD)
-
-lemma dep_functions_eq_if_subset:
-  assumes f_mem: "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and g_mem: "g \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B' x)"
-  and "f \<subseteq> g"
-  shows "f = g"
-proof (rule eqI)
-  fix p assume "p \<in> g"
-  with g_mem obtain x y where [simp]: "p = \<langle>x, y\<rangle>" "g`x = y" "x \<in> A" by auto
-  with assms have [simp]: "R`x = g`x" by (intro dep_functions_eval_eqI) auto
-  show "p \<in> f" using f_mem by (auto iff: pair_mem_iff_eval_eq_if_mem_dom_dep_function)
-qed (use assms in auto)
-
-lemma ex_dom_mem_dep_functions_iff:
-  "(\<exists>A. f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)) \<longleftrightarrow> f \<in> (x \<in> dom R) \<rightarrow>\<^sub>cs (B x)"
-  by auto
-
-lemma mem_dep_functions_empty_dom_iff_eq_empty [iff]:
-  "(f \<in> (x \<in> {}) \<rightarrow>\<^sub>cs (B x)) \<longleftrightarrow> f = {}"
-  by auto
-
-lemma empty_mem_dep_functions: "{} \<in> (x \<in> {}) \<rightarrow>\<^sub>cs (B x)" by simp
-
-lemma eq_singleton_if_mem_functions_singleton [simp]:
-  "f \<in> {a} \<rightarrow>\<^sub>cs {b} \<Longrightarrow> f = {\<langle>a, b\<rangle>}"
-  by force
-
-lemma singleton_mem_functionsI [intro]: "y \<in> B \<Longrightarrow> {\<langle>x, y\<rangle>} \<in> {x} \<rightarrow>\<^sub>cs B"
-  by fastforce
-
-lemma mem_dep_functions_collectI:
-  assumes "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-  and "\<And>x. x \<in> A \<Longrightarrow> P x (R`x)"
-  shows "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs {y \<in> B x | P x y}"
-  by (rule mem_dep_functions_covariant_codom) (use assms in auto)
-
-lemma mem_dep_functions_collectE:
-  assumes "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs {y \<in> B x | P x y}"
-  obtains "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)" and "\<And>x. x \<in> A \<Longrightarrow> P x (R`x)"
-proof
-  from assms show "f \<in> (x \<in> A) \<rightarrow>\<^sub>cs (B x)"
-    by (rule mem_dep_functions_covariant_codom_subset) auto
-  fix x assume "x \<in> A"
-  with assms show "P x (R`x)"
-    by (auto dest: pair_eval_mem_if_mem_if_mem_dep_functions)
-qed *)
-
 end

HOTG/Functions/HOTG_Functions_Extend.thy

@@ -64,52 +64,51 @@ proof -
   from assms show ?thesis by (urule crel_dep_mono_wrt_eq_sup_extend_if_rel_dep_mono_wrt_predI)
 qed
 
+lemma set_crel_dep_mono_wrt_pred_sup_bin_union_if_eval_eq_if_set_crel_dep_mono_wrt_pred:
+  assumes dep_funs: "((x : A) \<rightarrow>\<^sub>c B x) R" "((x : A') \<rightarrow>\<^sub>c B x) R'"
+  and "\<And>x. A x \<Longrightarrow> A' x \<Longrightarrow> R`x = R'`x"
+  shows "((x : A \<squnion> A') \<rightarrow>\<^sub>c B x) (R \<union> R')"
+proof -
+  from dep_funs have [simp]: "is_bin_rel R" "is_bin_rel R'" "is_bin_rel (R \<union> R')" by auto
+  from assms show ?thesis by (urule crel_dep_mono_wrt_pred_sup_if_eval_eq_if_crel_dep_mono_wrt_pred)
+qed
+
+end
+
 context
   fixes \<R> :: "set" and A :: "set \<Rightarrow> set" and D
   defines "D \<equiv> \<Union>R \<in> \<R>. A R"
 begin
 
-lemma rel_dep_mono_wrt_pred_glue_if_right_unique_if_rel_dep_mono_wrt_pred:
+text \<open>TODO: this should be provable from
+@{thm rel_dep_mono_wrt_pred_glue_if_right_unique_if_rel_dep_mono_wrt_pred} - but maybe requires
+Hilbert-Choice?  \<close>
+
+lemma set_rel_dep_mono_wrt_set_glue_if_right_unique_if_set_rel_dep_mono_wrt_set:
   assumes funs: "\<And>R. R \<in> \<R> \<Longrightarrow> ((x : A R) \<rightarrow> B x) R"
   and runique: "right_unique_on D (glue \<R>)"
   shows "((x : D) \<rightarrow> B x) (glue \<R>)"
-  (*TODO*)
-  sorry
-(* unfolding
-set_rel_dep_mono_wrt_set_eq_set_rel_dep_mono_wrt_pred
-set_rel_dep_mono_wrt_pred_iff_rel_dep_mono_wrt_pred
-rel_glue_eq_glue_has_inverse_on_rel *)
-(* proof -
-  (* have bla: "mem_of (\<Union>R \<in> \<R>. A R) = in_codom_on (has_inverse_on \<R> rel) *)
-    (* (\<lambda>R. mem_of (A (THE R'. rel R' = R)))" sorry *)
+proof (urule (rr) rel_dep_mono_wrt_predI dep_mono_wrt_predI left_total_onI)
+  note D_def[simp]
+  fix x assume "x \<in> D"
+  with funs obtain R where hyps: "R \<in> \<R>" "x \<in> A R" "((x : A R) \<rightarrow> B x) R" by auto
+  then have "R`x \<in> B x" by auto
+  moreover have "(glue \<R>)`x = R`x"
+  proof (rule glue_set_eval_eqI)
+    from hyps show "mem_of (A R) x" "R \<in> \<R>" by auto
+    then have "A R \<subseteq> D" by fastforce
+    with runique show "right_unique_on (mem_of (A R)) (glue \<R>)" by (blast dest: right_unique_onD)
+  qed (use hyps in \<open>auto elim: rel_dep_mono_wrt_pred_relE\<close>)
+  ultimately show "rel (glue \<R>)`x \<in> B x" by simp
+qed (use assms in \<open>(fastforce simp: D_def mem_of_eq)+\<close>)
 
-  show ?thesis
-    unfolding rel_glue_eq_glue_has_inverse_on_rel[simp] D_def[simp]
-      mem_of_idx_union_eq_in_codom_on_has_inverse_on_if_mem_of_eq_app_rel[of dom in_dom, simp]
-      (* thm rel_dep_mono_wrt_pred_glue_if_right_unique_if_rel_dep_mono_wrt_pred[where ?A=A] *)
-set_rel_dep_mono_wrt_set_eq_set_rel_dep_mono_wrt_pred
-set_rel_dep_mono_wrt_pred_iff_rel_dep_mono_wrt_pred
-rel_glue_eq_glue_has_inverse_on_rel
-bla
-    apply (rule rel_dep_mono_wrt_pred_glue_if_right_unique_if_rel_dep_mono_wrt_pred)
-    apply (use assms in auto)
-qed *)
-
-(* lemma crel_dep_mono_wrt_pred_glue_if_right_unique_if_crel_dep_mono_wrt_pred:
-  assumes "\<And>R. \<R> R \<Longrightarrow> ((x : A R) \<rightarrow>\<^sub>c B x) R"
+lemma crel_dep_mono_wrt_pred_glue_if_right_unique_if_crel_dep_mono_wrt_pred:
+  assumes "\<And>R. R \<in> \<R> \<Longrightarrow> ((x : A R) \<rightarrow>\<^sub>c B x) R"
   and "right_unique_on D (glue \<R>)"
   shows "((x : D) \<rightarrow>\<^sub>c B x) (glue \<R>)"
-  using assms by (intro crel_dep_mono_wrt_predI rel_dep_mono_wrt_pred_glue_if_right_unique_if_rel_dep_mono_wrt_pred) fastforce+ *)
-end
-
-lemma set_crel_dep_mono_wrt_pred_sup_bin_union_if_eval_eq_if_set_crel_dep_mono_wrt_pred:
-  assumes dep_funs: "((x : A) \<rightarrow>\<^sub>c B x) R" "((x : A') \<rightarrow>\<^sub>c B x) R'"
-  and "\<And>x. A x \<Longrightarrow> A' x \<Longrightarrow> R`x = R'`x"
-  shows "((x : A \<squnion> A') \<rightarrow>\<^sub>c B x) (R \<union> R')"
-proof -
-  from dep_funs have [simp]: "is_bin_rel R" "is_bin_rel R'" "is_bin_rel (R \<union> R')" by auto
-  from assms show ?thesis by (urule crel_dep_mono_wrt_pred_sup_if_eval_eq_if_crel_dep_mono_wrt_pred)
-qed
+  by (urule set_crel_dep_mono_wrt_pred_if_mem_of_dom_le_if_set_rel_dep_mono_wrt_pred,
+  urule set_rel_dep_mono_wrt_set_glue_if_right_unique_if_set_rel_dep_mono_wrt_set)
+  (use assms in \<open>auto simp: D_def mem_of_eq, fastforce\<close>)
 
 end