From 992809675b259c033029dd92372b6e758084bade Mon Sep 17 00:00:00 2001 From: Kevin Kappelmann Date: Fri, 17 May 2024 17:40:28 +0200 Subject: [PATCH] feat(HOTG) fix sorry --- .../HOTG_Binary_Relations_Extend.thy | 2 +- HOTG/Functions/HOTG_Clean_Functions.thy | 123 +++--------------- HOTG/Functions/HOTG_Functions_Extend.thy | 69 +++++----- 3 files changed, 56 insertions(+), 138 deletions(-) diff --git a/HOTG/Binary_Relations/HOTG_Binary_Relations_Extend.thy b/HOTG/Binary_Relations/HOTG_Binary_Relations_Extend.thy index 7f3a800..7512e77 100644 --- a/HOTG/Binary_Relations/HOTG_Binary_Relations_Extend.thy +++ b/HOTG/Binary_Relations/HOTG_Binary_Relations_Extend.thy @@ -110,7 +110,7 @@ lemma glue_bin_union_eq_glue_bin_union_glue [simp]: "glue (\ \ \') lemma mono_glue: "((\) \ (\)) 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 "\R. R \ \ \ is_bin_rel R" shows "is_bin_rel (glue \)" using assms by (intro is_bin_relI) auto diff --git a/HOTG/Functions/HOTG_Clean_Functions.thy b/HOTG/Functions/HOTG_Clean_Functions.thy index b0bce35..7af46ec 100644 --- a/HOTG/Functions/HOTG_Clean_Functions.thy +++ b/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) \ B x) R" + and [uhint]: "is_bin_rel R" + and "mem_of (dom R) \ A" + shows "((x : A) \\<^sub>c B x) R" + by (urule crel_dep_mono_wrt_predI) (urule assms)+ + lemma set_crel_mono_wrt_predI [intro]: assumes "(A \\<^sub>c B) (rel R)" and "is_bin_rel R" shows "(A \\<^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 {\} B) R" - shows "(A \\<^sub>c B) (R :: set)" - using assms by (urule set_crel_dep_mono_wrt_predI') - lemma set_crel_mono_wrt_predE: assumes "(A \\<^sub>c B) R" obtains "(A \\<^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 \\<^sub>c B) R \ (A' \\<^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 {\} B) R" + shows "(A \\<^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 \ B) R" + and "is_bin_rel R" + and "mem_of (dom R) \ A" + shows "(A \\<^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) \\<^sub>c B x) R" shows "R = {\x, R`x\ | x \ 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: "\f. f \ F \ \B. f \ (x \ A) \\<^sub>cs (B x)" - and "agree A F" - and "f \ F" - and "g \ F" - shows "f = g" - using assms -proof - - have "\f. f \ F \ \B. f \ \x \ 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 \ (x \ A) \\<^sub>cs (B x)" - and "f \ F" - and "agree A F" - and "g \ F" - shows "f \ 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: "\f. f \ F \ \B. f \ (x \ A) \\<^sub>cs (B x)" - and "\f g x. f \ F \ g \ F \ x \ A \ 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 \ F" "g \ F" "x \ A" and "\x, y\ \ 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 \g \ F\] obtain B where "g \ (x \ A) \\<^sub>cs (B x)" by blast - with y_eq pair_mem_iff_eval_eq_if_mem_dom_dep_function \x \ A\ show "\x, y\ \ g" by blast -qed simp_all - -lemma eq_if_agree_if_mem_dep_functions: - assumes "f \ (x \ A) \\<^sub>cs (B x)" "g \ (x \ A) \\<^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 \ (x \ A) \\<^sub>cs (B x)" - and "g \ (x \ A') \\<^sub>cs (B' x)" - and "f \ g" - and "x \ A \ A'" - shows "R`x = g`x" - using assms by (auto dest: right_unique_onD) - -lemma dep_functions_eq_if_subset: - assumes f_mem: "f \ (x \ A) \\<^sub>cs (B x)" - and g_mem: "g \ (x \ A) \\<^sub>cs (B' x)" - and "f \ g" - shows "f = g" -proof (rule eqI) - fix p assume "p \ g" - with g_mem obtain x y where [simp]: "p = \x, y\" "g`x = y" "x \ A" by auto - with assms have [simp]: "R`x = g`x" by (intro dep_functions_eval_eqI) auto - show "p \ 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: - "(\A. f \ (x \ A) \\<^sub>cs (B x)) \ f \ (x \ dom R) \\<^sub>cs (B x)" - by auto - -lemma mem_dep_functions_empty_dom_iff_eq_empty [iff]: - "(f \ (x \ {}) \\<^sub>cs (B x)) \ f = {}" - by auto - -lemma empty_mem_dep_functions: "{} \ (x \ {}) \\<^sub>cs (B x)" by simp - -lemma eq_singleton_if_mem_functions_singleton [simp]: - "f \ {a} \\<^sub>cs {b} \ f = {\a, b\}" - by force - -lemma singleton_mem_functionsI [intro]: "y \ B \ {\x, y\} \ {x} \\<^sub>cs B" - by fastforce - -lemma mem_dep_functions_collectI: - assumes "f \ (x \ A) \\<^sub>cs (B x)" - and "\x. x \ A \ P x (R`x)" - shows "f \ (x \ A) \\<^sub>cs {y \ B x | P x y}" - by (rule mem_dep_functions_covariant_codom) (use assms in auto) - -lemma mem_dep_functions_collectE: - assumes "f \ (x \ A) \\<^sub>cs {y \ B x | P x y}" - obtains "f \ (x \ A) \\<^sub>cs (B x)" and "\x. x \ A \ P x (R`x)" -proof - from assms show "f \ (x \ A) \\<^sub>cs (B x)" - by (rule mem_dep_functions_covariant_codom_subset) auto - fix x assume "x \ A" - with assms show "P x (R`x)" - by (auto dest: pair_eval_mem_if_mem_if_mem_dep_functions) -qed *) - end diff --git a/HOTG/Functions/HOTG_Functions_Extend.thy b/HOTG/Functions/HOTG_Functions_Extend.thy index 371c075..85d031f 100644 --- a/HOTG/Functions/HOTG_Functions_Extend.thy +++ b/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) \\<^sub>c B x) R" "((x : A') \\<^sub>c B x) R'" + and "\x. A x \ A' x \ R`x = R'`x" + shows "((x : A \ A') \\<^sub>c B x) (R \ R')" +proof - + from dep_funs have [simp]: "is_bin_rel R" "is_bin_rel R'" "is_bin_rel (R \ 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 \ :: "set" and A :: "set \ set" and D defines "D \ \R \ \. A R" begin -lemma rel_dep_mono_wrt_pred_glue_if_right_unique_if_rel_dep_mono_wrt_pred: +text \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? \ + +lemma set_rel_dep_mono_wrt_set_glue_if_right_unique_if_set_rel_dep_mono_wrt_set: assumes funs: "\R. R \ \ \ ((x : A R) \ B x) R" and runique: "right_unique_on D (glue \)" shows "((x : D) \ B x) (glue \)" - (*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 (\R \ \. A R) = in_codom_on (has_inverse_on \ rel) *) - (* (\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 \ D" + with funs obtain R where hyps: "R \ \" "x \ A R" "((x : A R) \ B x) R" by auto + then have "R`x \ B x" by auto + moreover have "(glue \)`x = R`x" + proof (rule glue_set_eval_eqI) + from hyps show "mem_of (A R) x" "R \ \" by auto + then have "A R \ D" by fastforce + with runique show "right_unique_on (mem_of (A R)) (glue \)" by (blast dest: right_unique_onD) + qed (use hyps in \auto elim: rel_dep_mono_wrt_pred_relE\) + ultimately show "rel (glue \)`x \ B x" by simp +qed (use assms in \(fastforce simp: D_def mem_of_eq)+\) - 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 "\R. \ R \ ((x : A R) \\<^sub>c B x) R" +lemma crel_dep_mono_wrt_pred_glue_if_right_unique_if_crel_dep_mono_wrt_pred: + assumes "\R. R \ \ \ ((x : A R) \\<^sub>c B x) R" and "right_unique_on D (glue \)" shows "((x : D) \\<^sub>c B x) (glue \)" - 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) \\<^sub>c B x) R" "((x : A') \\<^sub>c B x) R'" - and "\x. A x \ A' x \ R`x = R'`x" - shows "((x : A \ A') \\<^sub>c B x) (R \ R')" -proof - - from dep_funs have [simp]: "is_bin_rel R" "is_bin_rel R'" "is_bin_rel (R \ 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 \auto simp: D_def mem_of_eq, fastforce\) end