diff --git a/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy b/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy --- a/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy +++ b/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy @@ -1,962 +1,962 @@ (* * Title: Decreasing Diagrams II * Author: Bertram Felgenhauer (2015) * Maintainer: Bertram Felgenhauer * License: LGPL *) section \Decreasing Diagrams\ theory Decreasing_Diagrams_II imports Decreasing_Diagrams_II_Aux "HOL-Cardinals.Wellorder_Extension" "Abstract-Rewriting.Abstract_Rewriting" begin subsection \Greek accents\ datatype accent = Acute | Grave | Macron lemma UNIV_accent: "UNIV = { Acute, Grave, Macron }" using accent.nchotomy by blast lemma finite_accent: "finite (UNIV :: accent set)" by (simp add: UNIV_accent) type_synonym 'a letter = "accent \ 'a" definition letter_less :: "('a \ 'a) set \ ('a letter \ 'a letter) set" where [simp]: "letter_less R = {(a,b). (snd a, snd b) \ R}" lemma mono_letter_less: "mono letter_less" by (auto simp add: mono_def) subsection \Comparing Greek strings\ type_synonym 'a greek = "'a letter list" definition adj_msog :: "'a greek \ 'a greek \ ('a letter \ 'a greek) \ ('a letter \ 'a greek)" where "adj_msog xs zs l \ case l of (y,ys) \ (y, case fst y of Acute \ ys @ zs | Grave \ xs @ ys | Macron \ ys)" definition ms_of_greek :: "'a greek \ ('a letter \ 'a greek) multiset" where "ms_of_greek as = mset (map (\(xs, y, zs) \ adj_msog xs zs (y, [])) (list_splits as))" lemma adj_msog_adj_msog[simp]: "adj_msog xs zs (adj_msog xs' zs' y) = adj_msog (xs @ xs') (zs' @ zs) y" by (auto simp: adj_msog_def split: accent.splits prod.splits) lemma compose_adj_msog[simp]: "adj_msog xs zs \ adj_msog xs' zs' = adj_msog (xs @ xs') (zs' @ zs)" by (simp add: comp_def) lemma adj_msog_single: "adj_msog xs zs (x,[]) = (x, (case fst x of Grave \ xs | Acute \ zs | Macron \ []))" by (simp add: adj_msog_def split: accent.splits) lemma ms_of_greek_elem: assumes "(x,xs) \ set_mset (ms_of_greek ys)" shows "x \ set ys" using assms by (auto dest: elem_list_splits_elem simp: adj_msog_def ms_of_greek_def) lemma ms_of_greek_shorter: assumes "(x, t) \# ms_of_greek s" shows "length s > length t" using assms[unfolded ms_of_greek_def in_multiset_in_set] by (auto simp: elem_list_splits_length adj_msog_def split: accent.splits) lemma msog_append: "ms_of_greek (xs @ ys) = image_mset (adj_msog [] ys) (ms_of_greek xs) + image_mset (adj_msog xs []) (ms_of_greek ys)" by (auto simp: ms_of_greek_def list_splits_append multiset.map_comp comp_def prod.case_distrib) definition nest :: "('a \ 'a) set \ ('a greek \ 'a greek) set \ ('a greek \ 'a greek) set" where [simp]: "nest r s = {(a,b). (ms_of_greek a, ms_of_greek b) \ mult (letter_less r <*lex*> s)}" lemma mono_nest: "mono (nest r)" unfolding mono_def proof (intro allI impI subsetI) fix R S x assume 1: "R \ S" and 2: "x \ nest r R" from 1 have "mult (letter_less r <*lex*> R) \ mult (letter_less r <*lex*> S)" using mono_mult mono_lex2[of "letter_less r"] unfolding mono_def by blast with 2 show "x \ nest r S" by auto qed lemma nest_mono[mono_set]: "x \ y \ (a,b) \ nest r x \ (a,b) \ nest r y" using mono_nest[unfolded mono_def, rule_format, of x y r] by blast definition greek_less :: "('a \ 'a) set \ ('a greek \ 'a greek) set" where "greek_less r = lfp (nest r)" lemma greek_less_unfold: "greek_less r = nest r (greek_less r)" using mono_nest[of r] lfp_unfold[of "nest r"] by (simp add: greek_less_def) subsection \Preservation of strict partial orders\ lemma strict_order_letter_less: assumes "strict_order r" shows "strict_order (letter_less r)" using assms unfolding irrefl_def trans_def letter_less_def by fast lemma strict_order_nest: assumes r: "strict_order r" and R: "strict_order R" shows "strict_order (nest r R)" proof - have "strict_order (mult (letter_less r <*lex*> R))" using strict_order_letter_less[of r] irrefl_lex_prod[of "letter_less r" R] trans_lex_prod[of "letter_less r" R] strict_order_mult[of "letter_less r <*lex*> R"] assms by fast from this show "strict_order (nest r R)" unfolding nest_def trans_def irrefl_def by fast qed lemma strict_order_greek_less: assumes "strict_order r" shows "strict_order (greek_less r)" by (simp add: greek_less_def strict_order_lfp[OF mono_nest strict_order_nest[OF assms]]) lemma trans_letter_less: assumes "trans r" shows "trans (letter_less r)" using assms unfolding trans_def letter_less_def by fast lemma trans_order_nest: "trans (nest r R)" using trans_mult unfolding nest_def trans_def by fast lemma trans_greek_less[simp]: "trans (greek_less r)" by (subst greek_less_unfold) (rule trans_order_nest) lemma mono_greek_less: "mono greek_less" unfolding greek_less_def mono_def proof (intro allI impI lfp_mono) fix r s :: "('a \ 'a) set" and R :: "('a greek \ 'a greek) set" assume "r \ s" then have "letter_less r <*lex*> R \ letter_less s <*lex*> R" using mono_letter_less mono_lex1 unfolding mono_def by metis then show "nest r R \ nest s R" using mono_mult unfolding nest_def mono_def by blast qed subsection \Involution\ definition inv_letter :: "'a letter \ 'a letter" where "inv_letter l \ case l of (a, x) \ (case a of Grave \ Acute | Acute \ Grave | Macron \ Macron, x)" lemma inv_letter_pair[simp]: "inv_letter (a, x) = (case a of Grave \ Acute | Acute \ Grave | Macron \ Macron, x)" by (simp add: inv_letter_def) lemma snd_inv_letter[simp]: "snd (inv_letter x) = snd x" by (simp add: inv_letter_def split: prod.splits) lemma inv_letter_invol[simp]: "inv_letter (inv_letter x) = x" by (simp add: inv_letter_def split: prod.splits accent.splits) lemma inv_letter_mono[simp]: assumes "(x, y) \ letter_less r" shows "(inv_letter x, inv_letter y) \ letter_less r" using assms by simp definition inv_greek :: "'a greek \ 'a greek" where "inv_greek s = rev (map inv_letter s)" lemma inv_greek_invol[simp]: "inv_greek (inv_greek s) = s" by (simp add: inv_greek_def rev_map comp_def) lemma inv_greek_append: "inv_greek (s @ t) = inv_greek t @ inv_greek s" by (simp add: inv_greek_def) definition inv_msog :: "('a letter \ 'a greek) multiset \ ('a letter \ 'a greek) multiset" where "inv_msog M = image_mset (\(x, t). (inv_letter x, inv_greek t)) M" lemma inv_msog_invol[simp]: "inv_msog (inv_msog M) = M" by (simp add: inv_msog_def multiset.map_comp comp_def prod.case_distrib) lemma ms_of_greek_inv_greek: "ms_of_greek (inv_greek M) = inv_msog (ms_of_greek M)" unfolding inv_msog_def inv_greek_def ms_of_greek_def list_splits_rev list_splits_map mset_map multiset.map_comp mset_rev inv_letter_def adj_msog_def by (rule cong[OF cong[OF refl[of "image_mset"]] refl]) (auto split: accent.splits) lemma inv_greek_mono: assumes "trans r" and "(s, t) \ greek_less r" shows "(inv_greek s, inv_greek t) \ greek_less r" using assms(2) proof (induct "length s + length t" arbitrary: s t rule: less_induct) note * = trans_lex_prod[OF trans_letter_less[OF \trans r\] trans_greek_less[of r]] case (less s t) have "(inv_msog (ms_of_greek s), inv_msog (ms_of_greek t)) \ mult (letter_less r <*lex*> greek_less r)" unfolding inv_msog_def proof (induct rule: mult_of_image_mset[OF * *]) case (1 x y) thus ?case by (auto intro: less(1) split: prod.splits dest!: ms_of_greek_shorter) next case 2 thus ?case using less(2) by (subst(asm) greek_less_unfold) simp qed thus ?case by (subst greek_less_unfold) (auto simp: ms_of_greek_inv_greek) qed subsection \Monotonicity of @{term "greek_less r"}\ lemma greek_less_rempty[simp]: "(a,[]) \ greek_less r \ False" by (subst greek_less_unfold) (auto simp: ms_of_greek_def) lemma greek_less_nonempty: assumes "b \ []" shows "(a,b) \ greek_less r \ (a,b) \ nest r (greek_less r)" by (subst greek_less_unfold) simp lemma greek_less_lempty[simp]: "([],b) \ greek_less r \ b \ []" proof assume "([],b) \ greek_less r" then show "b \ []" using greek_less_rempty by fast next assume "b \ []" then show "([],b) \ greek_less r" unfolding greek_less_nonempty[OF \b \ []\] by (simp add: ms_of_greek_def) qed lemma greek_less_singleton: "(a, b) \ letter_less r \ ([a], [b]) \ greek_less r" by (subst greek_less_unfold) (auto split: accent.splits simp: adj_msog_def ms_of_greek_def) lemma ms_of_greek_cons: "ms_of_greek (x # s) = {# adj_msog [] s (x,[]) #} + image_mset (adj_msog [x] []) (ms_of_greek s)" using msog_append[of "[x]" s] by (auto simp add: adj_msog_def ms_of_greek_def accent.splits) lemma greek_less_cons_mono: assumes "trans r" shows "(s, t) \ greek_less r \ (x # s, x # t) \ greek_less r" proof (induct "length s + length t" arbitrary: s t rule: less_induct) note * = trans_lex_prod[OF trans_letter_less[OF \trans r\] trans_greek_less[of r]] case (less s t) { fix M have "(M + image_mset (adj_msog [x] []) (ms_of_greek s), M + image_mset (adj_msog [x] []) (ms_of_greek t)) \ mult (letter_less r <*lex*> greek_less r)" proof (rule mult_on_union, induct rule: mult_of_image_mset[OF * *]) case (1 x y) thus ?case unfolding adj_msog_def by (auto intro: less(1) split: prod.splits accent.splits dest!: ms_of_greek_shorter) next case 2 thus ?case using less(2) by (subst(asm) greek_less_unfold) simp qed } moreover { fix N have "({# adj_msog [] s (x,[]) #} + N,{# adj_msog [] t (x,[]) #} + N) \ (mult (letter_less r <*lex*> greek_less r))\<^sup>=" by (auto simp: adj_msog_def less split: accent.splits) } ultimately show ?case using transD[OF trans_mult] by (subst greek_less_unfold) (fastforce simp: ms_of_greek_cons) qed lemma greek_less_app_mono2: assumes "trans r" and "(s, t) \ greek_less r" shows "(p @ s, p @ t) \ greek_less r" using assms by (induct p) (auto simp add: greek_less_cons_mono) lemma greek_less_app_mono1: assumes "trans r" and "(s, t) \ greek_less r" shows "(s @ p, t @ p) \ greek_less r" using inv_greek_mono[of r "inv_greek p @ inv_greek s" "inv_greek p @ inv_greek t"] by (simp add: assms inv_greek_append inv_greek_mono greek_less_app_mono2) subsection \Well-founded-ness of @{term "greek_less r"}\ lemma greek_embed: assumes "trans r" shows "list_emb (\a b. (a, b): reflcl (letter_less r)) a b \ (a, b) \ reflcl (greek_less r)" proof (induct rule: list_emb.induct) case (list_emb_Cons a b y) thus ?case using trans_greek_less[unfolded trans_def] \trans r\ greek_less_app_mono1[of r "[]" "[y]" a] greek_less_app_mono2[of r a b "[y]"] by auto next case (list_emb_Cons2 x y a b) thus ?case using trans_greek_less[unfolded trans_def] \trans r\ greek_less_singleton[of x y r] greek_less_app_mono1[of r "[x]" "[y]" a] greek_less_app_mono2[of r a b "[y]"] by auto qed simp lemma wqo_letter_less: assumes t: "trans r" and w: "wqo_on (\a b. (a, b) \ r\<^sup>=) UNIV" shows "wqo_on (\a b. (a, b) \ (letter_less r)\<^sup>=) UNIV" -proof (rule wqo_on_hom[of _ id _ "prod_le (=) (\a b. (a, b) \ r\<^sup>=)", unfolded image_id id_apply]) +proof (rule wqo_on_hom[of id _ _ "prod_le (=) (\a b. (a, b) \ r\<^sup>=)", unfolded image_id id_apply]) show "wqo_on (prod_le ((=) :: accent \ accent \ bool) (\a b. (a, b) \ r\<^sup>=)) UNIV" by (rule dickson[OF finite_eq_wqo_on[OF finite_accent] w, unfolded UNIV_Times_UNIV]) qed (insert t, auto simp: transp_on_def trans_def prod_le_def) lemma wf_greek_less: assumes "wf r" and "trans r" shows "wf (greek_less r)" proof - obtain q where "r \ q" and "well_order q" by (metis total_well_order_extension \wf r\) define q' where "q' = q - Id" from \well_order q\ have "reflcl q' = q" by (auto simp add: well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def q'_def) from \well_order q\ have "trans q'" and "irrefl q'" unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def antisym_def trans_def irrefl_def q'_def by blast+ from \r \ q\ \wf r\ have "r \ q'" by (auto simp add: q'_def) have "wqo_on (\a b. (a,b) \ (greek_less q')\<^sup>=) UNIV" - proof (intro wqo_on_hom[of "(\a b. (a, b) \ (greek_less q')\<^sup>=)" "id" UNIV + proof (intro wqo_on_hom[of id UNIV "(\a b. (a, b) \ (greek_less q')\<^sup>=)" "list_emb (\a b. (a, b) \ (letter_less q')\<^sup>=)", unfolded surj_id]) - show "transp_on (\a b. (a, b) \ (greek_less q')\<^sup>=) UNIV" + show "transp (\a b. (a, b) \ (greek_less q')\<^sup>=)" using trans_greek_less[of q'] unfolding trans_def transp_on_def by blast next show "\x\UNIV. \y\UNIV. list_emb (\a b. (a, b) \ (letter_less q')\<^sup>=) x y \ (id x, id y) \ (greek_less q')\<^sup>=" using greek_embed[OF \trans q'\] by auto next show "wqo_on (list_emb (\a b. (a, b) \ (letter_less q')\<^sup>=)) UNIV" using higman[OF wqo_letter_less[OF \trans q'\]] \well_order q\ \reflcl q' = q\ by (auto simp: well_order_implies_wqo) qed with wqo_on_imp_wfp_on[OF this] strict_order_strict[OF strict_order_greek_less] \irrefl q'\ \trans q'\ have "wfp_on (\a b. (a, b) \ greek_less q') UNIV" by force then show ?thesis using mono_greek_less \r \ q'\ wf_subset unfolding wf_iff_wfp_on[symmetric] mono_def by metis qed subsection \Basic Comparisons\ lemma pairwise_imp_mult: assumes "N \ {#}" and "\x \ set_mset M. \y \ set_mset N. (x, y) \ r" shows "(M, N) \ mult r" using assms one_step_implies_mult[of _ _ _ "{#}"] by auto lemma singleton_greek_less: assumes as: "snd ` set as \ under r b" shows "(as, [(a,b)]) \ greek_less r" proof - { fix e assume "e \ set_mset (ms_of_greek as)" with as ms_of_greek_elem[of _ _ as] have "(e, ((a,b),[])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover have "ms_of_greek [(a,b)] = {# ((a,b),[]) #}" by (auto simp: ms_of_greek_def adj_msog_def split: accent.splits) ultimately show ?thesis by (subst greek_less_unfold) (auto intro!: pairwise_imp_mult) qed lemma peak_greek_less: assumes as: "snd ` set as \ under r a" and b': "b' \ {[(Grave,b)],[]}" and cs: "snd ` set cs \ under r a \ under r b" and a': "a' \ {[(Acute,a)],[]}" and bs: "snd ` set bs \ under r b" shows "(as @ b' @ cs @ a' @ bs, [(Acute,a),(Grave,b)]) \ greek_less r" proof - let ?A = "(Acute,a)" and ?B = "(Grave,b)" have "(ms_of_greek (as @ b' @ cs @ a' @ bs), ms_of_greek [?A,?B]) \ mult (letter_less r <*lex*> greek_less r)" proof (intro pairwise_imp_mult) (* we distinguish 5 cases depending on where in xs an element e originates *) { fix e assume "e \ set_mset (ms_of_greek as)" with as ms_of_greek_elem[of _ _ as] have "(adj_msog [] (b' @ cs @ a' @ bs) e, (?A,[?B])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover { fix e assume "e \ set_mset (ms_of_greek b')" with b' singleton_greek_less[OF as] ms_of_greek_elem[of _ _ b'] have "(adj_msog as (cs @ a' @ bs) e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def) } moreover { fix e assume "e \ set_mset (ms_of_greek cs)" with cs ms_of_greek_elem[of _ _ cs] have "(adj_msog (as @ b') (a' @ bs) e, (?A,[?B])) \ letter_less r <*lex*> greek_less r \ (adj_msog (as @ b') (a' @ bs) e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover { fix e assume "e \ set_mset (ms_of_greek a')" with a' singleton_greek_less[OF bs] ms_of_greek_elem[of _ _ a'] have "(adj_msog (as @ b' @ cs) bs e, (?A,[?B])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def) } moreover { fix e assume "e \ set_mset (ms_of_greek bs)" with bs ms_of_greek_elem[of _ _ bs] have "(adj_msog (as @ b' @ cs @ a') [] e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover have "ms_of_greek [?A,?B] = {# (?B,[?A]), (?A,[?B]) #}" by (simp add: adj_msog_def ms_of_greek_def) ultimately show "\x\set_mset (ms_of_greek (as @ b' @ cs @ a' @ bs)). \y\set_mset (ms_of_greek [?A,?B]). (x, y) \ letter_less r <*lex*> greek_less r" by (auto simp: msog_append) blast qed (auto simp: ms_of_greek_def) then show ?thesis by (subst greek_less_unfold) auto qed lemma rcliff_greek_less1: assumes "trans r" (* unused assumption kept for symmetry with lcliff_greek_less1 *) and as: "snd ` set as \ under r a \ under r b" and b': "b' \ {[(Grave,b)],[]}" and cs: "snd ` set cs \ under r b" and a': "a' = [(Macron,a)]" and bs: "snd ` set bs \ under r b" shows "(as @ b' @ cs @ a' @ bs, [(Macron,a),(Grave,b)]) \ greek_less r" proof - let ?A = "(Macron,a)" and ?B = "(Grave,b)" have *: "ms_of_greek [?A,?B] = {#(?B,[?A]), (?A,[])#}" "ms_of_greek [?A] = {#(?A,[])#}" by (simp_all add: ms_of_greek_def adj_msog_def) then have **: "ms_of_greek [(Macron, a), (Grave, b)] - {#((Macron, a), [])#} \ {#}" by (auto) (* we distinguish 5 cases depending on where in xs an element e originates *) { fix e assume "e \ set_mset (ms_of_greek as)" with as ms_of_greek_elem[of _ _ as] have "(adj_msog [] (b' @ cs @ a' @ bs) e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (force simp: adj_msog_def under_def) } moreover { fix e assume "e \ set_mset (ms_of_greek b')" with b' singleton_greek_less as ms_of_greek_elem[of _ _ b'] have "(adj_msog as (cs @ a' @ bs) e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def) } moreover { fix e assume "e \ set_mset (ms_of_greek cs)" with cs ms_of_greek_elem[of _ _ cs] have "(adj_msog (as @ b') (a' @ bs) e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover { fix e assume "e \ set_mset (ms_of_greek bs)" with bs ms_of_greek_elem[of _ _ bs] have "(adj_msog (as @ b' @ cs @ a') [] e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover have "ms_of_greek [?A,?B] = {# (?B,[?A]), (?A,[]) #}" by (simp add: adj_msog_def ms_of_greek_def) ultimately have "\x\set_mset (ms_of_greek (as @ b' @ cs @ a' @ bs) - {#(?A,[])#}). \y\set_mset (ms_of_greek [?A,?B] - {#(?A,[])#}). (x, y) \ letter_less r <*lex*> greek_less r" unfolding msog_append by (auto simp: a' msog_append ac_simps * adj_msog_single) from one_step_implies_mult[OF ** this,of "{#(?A,[])#}"] have "(ms_of_greek (as @ b' @ cs @ a' @ bs), ms_of_greek [?A,?B]) \ mult (letter_less r <*lex*> greek_less r)" unfolding a' msog_append by (auto simp: a' ac_simps * adj_msog_single) then show ?thesis by (subst greek_less_unfold) auto qed lemma rcliff_greek_less2: assumes "trans r" (* unused assumption kept for symmetry with lcliff_greek_less2 *) and as: "snd ` set as \ under r a" and b': "b' \ {[(Grave,b)],[]}" and cs: "snd ` set cs \ under r a \ under r b" shows "(as @ b' @ cs, [(Macron,a),(Grave,b)]) \ greek_less r" proof - let ?A = "(Macron,a)" and ?B = "(Grave,b)" have "(ms_of_greek (as @ b' @ cs), ms_of_greek [?A,?B]) \ mult (letter_less r <*lex*> greek_less r)" proof (intro pairwise_imp_mult) (* we distinguish 3 cases depending on where in xs an element e originates *) { fix e assume "e \ set_mset (ms_of_greek as)" with as ms_of_greek_elem[of _ _ as] have "(adj_msog [] (b' @ cs) e, (?A,[])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover { fix e assume "e \ set_mset (ms_of_greek b')" with b' singleton_greek_less[OF as] ms_of_greek_elem[of _ _ b'] have "(adj_msog as (cs) e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def ms_of_greek_def) } moreover { fix e assume "e \ set_mset (ms_of_greek cs)" with cs ms_of_greek_elem[of _ _ cs] have "(adj_msog (as @ b') [] e, (?A,[])) \ letter_less r <*lex*> greek_less r \ (adj_msog (as @ b') [] e, (?B,[?A])) \ letter_less r <*lex*> greek_less r" by (cases e) (fastforce simp: adj_msog_def under_def) } moreover have *: "ms_of_greek [?A,?B] = {# (?B,[?A]), (?A,[]) #}" by (simp add: adj_msog_def ms_of_greek_def) ultimately show "\x\set_mset (ms_of_greek (as @ b' @ cs)). \y\set_mset (ms_of_greek [?A,?B]). (x, y) \ letter_less r <*lex*> greek_less r" by (auto simp: msog_append adj_msog_single ac_simps *) blast qed (auto simp: ms_of_greek_def) then show ?thesis by (subst greek_less_unfold) auto qed lemma snd_inv_greek [simp]: "snd ` set (inv_greek as) = snd ` set as" by (force simp: inv_greek_def) lemma lcliff_greek_less1: assumes "trans r" and as: "snd ` set as \ under r a" and b': "b' = [(Macron,b)]" and cs: "snd ` set cs \ under r a" and a': "a' \ {[(Acute,a)],[]}" and bs: "snd ` set bs \ under r a \ under r b" shows "(as @ b' @ cs @ a' @ bs, [(Acute,a),(Macron,b)]) \ greek_less r" proof - have *: "inv_greek [(Acute,a),(Macron,b)] = [(Macron,b),(Grave,a)]" by (simp add: inv_greek_def) have "(inv_greek (inv_greek (as @ b' @ cs @ a' @ bs)), inv_greek (inv_greek ([(Acute,a),(Macron,b)]))) \ greek_less r" apply (rule inv_greek_mono[OF \trans r\]) apply (unfold inv_greek_append append_assoc *) apply (insert assms) apply (rule rcliff_greek_less1, auto simp: inv_greek_def) done then show ?thesis by simp qed lemma lcliff_greek_less2: assumes "trans r" and cs: "snd ` set cs \ under r a \ under r b" and a': "a' \ {[(Acute,a)],[]}" and bs: "snd ` set bs \ under r b" shows "(cs @ a' @ bs, [(Acute,a),(Macron,b)]) \ greek_less r" proof - have *: "inv_greek [(Acute,a),(Macron,b)] = [(Macron,b),(Grave,a)]" by (simp add: inv_greek_def) have "(inv_greek (inv_greek (cs @ a' @ bs)), inv_greek (inv_greek ([(Acute,a),(Macron,b)]))) \ greek_less r" apply (rule inv_greek_mono[OF \trans r\]) apply (unfold inv_greek_append append_assoc *) apply (insert assms) apply (rule rcliff_greek_less2, auto simp: inv_greek_def) done then show ?thesis by simp qed subsection \Labeled abstract rewriting\ context fixes L R E :: "'b \ 'a rel" begin definition lstep :: "'b letter \ 'a rel" where [simp]: "lstep x = (case x of (a, i) \ (case a of Acute \ (L i)\ | Grave \ R i | Macron \ E i))" fun lconv :: "'b greek \ 'a rel" where "lconv [] = Id" | "lconv (x # xs) = lstep x O lconv xs" lemma lconv_append[simp]: "lconv (xs @ ys) = lconv xs O lconv ys" by (induct xs) auto lemma conversion_join_or_peak_or_cliff: obtains (join) as bs cs where "set as \ {Grave}" and "set bs \ {Macron}" and "set cs \ {Acute}" and "ds = as @ bs @ cs" | (peak) as bs where "ds = as @ ([Acute] @ [Grave]) @ bs" | (lcliff) as bs where "ds = as @ ([Acute] @ [Macron]) @ bs" | (rcliff) as bs where "ds = as @ ([Macron] @ [Grave]) @ bs" proof (induct ds arbitrary: thesis) case (Cons d ds thesis) note IH = this show ?case proof (rule IH(1)) fix as bs assume "ds = as @ ([Acute] @ [Grave]) @ bs" then show ?case using IH(3)[of "d # as" bs] by simp next fix as bs assume "ds = as @ ([Acute] @ [Macron]) @ bs" then show ?case using IH(4)[of "d # as" bs] by simp next fix as bs assume "ds = as @ ([Macron] @ [Grave]) @ bs" then show ?case using IH(5)[of "d # as" bs] by simp next fix as bs cs assume *: "set as \ {Grave}" "set bs \ {Macron}" "set cs \ {Acute}" "ds = as @ bs @ cs" show ?case proof (cases d) case Grave thus ?thesis using * IH(2)[of "d # as" bs cs] by simp next case Macron show ?thesis proof (cases as) case Nil thus ?thesis using * Macron IH(2)[of as "d # bs" cs] by simp next case (Cons a as) thus ?thesis using * Macron IH(5)[of "[]" "as @ bs @ cs"] by simp qed next case Acute show ?thesis proof (cases as) case Nil note as = this show ?thesis proof (cases bs) case Nil thus ?thesis using * as Acute IH(2)[of "[]" "[]" "d # cs"] by simp next case (Cons b bs) thus ?thesis using * as Acute IH(4)[of "[]" "bs @ cs"] by simp qed next case (Cons a as) thus ?thesis using * Acute IH(3)[of "[]" "as @ bs @ cs"] by simp qed qed qed qed auto lemma map_eq_append_split: assumes "map f xs = ys1 @ ys2" obtains xs1 xs2 where "ys1 = map f xs1" "ys2 = map f xs2" "xs = xs1 @ xs2" proof (insert assms, induct ys1 arbitrary: xs thesis) case (Cons y ys) note IH = this show ?case proof (cases xs) case (Cons x xs') show ?thesis proof (rule IH(1)) fix xs1 xs2 assume "ys = map f xs1" "ys2 = map f xs2" "xs' = xs1 @ xs2" thus ?thesis using Cons IH(2)[of "x # xs1" xs2] IH(3) by simp next show "map f xs' = ys @ ys2" using Cons IH(3) by simp qed qed (insert Cons, simp) qed auto lemmas map_eq_append_splits = map_eq_append_split map_eq_append_split[OF sym] abbreviation "conversion' M \ ((\i \ M. R i) \ (\i \ M. E i) \ (\i \ M. L i)\)\<^sup>*" abbreviation "valley' M \ (\i \ M. R i)\<^sup>* O (\i \ M. E i)\<^sup>* O ((\i \ M. L i)\)\<^sup>*" lemma conversion_to_lconv: assumes "(u, v) \ conversion' M" obtains xs where "snd ` set xs \ M" and "(u, v) \ lconv xs" using assms proof (induct arbitrary: thesis rule: converse_rtrancl_induct) case base show ?case using base[of "[]"] by simp next case (step u' x) from step(1) obtain p where "snd p \ M" and "(u', x) \ lstep p" by (force split: accent.splits) moreover obtain xs where "snd ` set xs \ M" "(x, v) \ lconv xs" by (rule step(3)) ultimately show ?case using step(4)[of "p # xs"] by auto qed definition lpeak :: "'b rel \ 'b \ 'b \ 'b greek \ bool" where "lpeak r a b xs \ (\as b' cs a' bs. snd ` set as \ under r a \ b' \ {[(Grave,b)],[]} \ snd ` set cs \ under r a \ under r b \ a' \ {[(Acute,a)],[]} \ snd ` set bs \ under r b \ xs = as @ b' @ cs @ a' @ bs)" definition lcliff :: "'b rel \ 'b \ 'b \ 'b greek \ bool" where "lcliff r a b xs \ (\as b' cs a' bs. snd ` set as \ under r a \ b' = [(Macron,b)] \ snd ` set cs \ under r a \ a' \ {[(Acute,a)],[]} \ snd ` set bs \ under r a \ under r b \ xs = as @ b' @ cs @ a' @ bs) \ (\cs a' bs. snd ` set cs \ under r a \ under r b \ a' \ {[(Acute,a)],[]} \ snd ` set bs \ under r b \ xs = cs @ a' @ bs)" definition rcliff :: "'b rel \ 'b \ 'b \ 'b greek \ bool" where "rcliff r a b xs \ (\as b' cs a' bs. snd ` set as \ under r a \ under r b \ b' \ {[(Grave,b)],[]} \ snd ` set cs \ under r b \ a' = [(Macron,a)] \ snd ` set bs \ under r b \ xs = as @ b' @ cs @ a' @ bs) \ (\as b' cs. snd ` set as \ under r a \ b' \ {[(Grave,b)],[]} \ snd ` set cs \ under r a \ under r b \ xs = as @ b' @ cs)" lemma dd_commute_modulo_conv[case_names wf trans peak lcliff rcliff]: assumes "wf r" and "trans r" and pk: "\a b s t u. (s, t) \ L a \ (s, u) \ R b \ \xs. lpeak r a b xs \ (t, u) \ lconv xs" and lc: "\a b s t u. (s, t) \ L a \ (s, u) \ E b \ \xs. lcliff r a b xs \ (t, u) \ lconv xs" and rc: "\a b s t u. (s, t) \ (E a)\ \ (s, u) \ R b \ \xs. rcliff r a b xs \ (t, u) \ lconv xs" shows "conversion' UNIV \ valley' UNIV" proof (intro subrelI) fix u v assume "(u,v) \ conversion' UNIV" then obtain xs where "(u, v) \ lconv xs" by (auto intro: conversion_to_lconv[of u v]) then show "(u, v) \ valley' UNIV" proof (induct xs rule: wf_induct[of "greek_less r"]) case 1 thus ?case using wf_greek_less[OF \wf r\ \trans r\] . next case (2 xs) show ?case proof (rule conversion_join_or_peak_or_cliff[of "map fst xs"]) fix as bs cs assume *: "set as \ {Grave}" "set bs \ {Macron}" "set cs \ {Acute}" "map fst xs = as @ bs @ cs" then show "(u, v) \ valley' UNIV" proof (elim map_eq_append_splits) fix as' bs' cs' bcs' assume as: "set as \ {Grave}" "as = map fst as'" and bs: "set bs \ {Macron}" "bs = map fst bs'" and cs: "set cs \ {Acute}" "cs = map fst cs'" and xs: "xs = as' @ bcs'" "bcs' = bs' @ cs'" from as(1)[unfolded as(2)] have as': "\x y. (x,y) \ lconv as' \ (x,y) \ (\a. R a)\<^sup>*" proof (induct as') case (Cons x' xs) have "\x y z i. (x,y) \ R i \ (y,z) \ (\a. R a)\<^sup>* \ (x,z) \ (\a. R a)\<^sup>*" by (rule rtrancl_trans) auto with Cons show ?case by auto qed simp from bs(1)[unfolded bs(2)] have bs': "\x y. (x,y) \ lconv bs' \ (x,y) \ (\a. E a)\<^sup>*" proof (induct bs') case (Cons x' xs) have "\x y z i. (x,y) \ E i \ (y,z) \ (\a. E a)\<^sup>* \ (x,z) \ (\a. E a)\<^sup>*" by (rule rtrancl_trans) auto with Cons show ?case by auto qed simp from cs(1)[unfolded cs(2)] have cs': "\x y. (x,y) \ lconv cs' \ (x,y) \ ((\a. L a)\)\<^sup>*" proof (induct cs') case (Cons x' xs) have "\x y z i. (x,y) \ (L i)\ \ (y,z) \ ((\a. L a)\)\<^sup>* \ (x,z) \ ((\a. L a)\)\<^sup>*" by (rule rtrancl_trans) auto with Cons show ?case by auto qed simp from 2(2) as' bs' cs' show "(u, v) \ valley' UNIV" unfolding xs lconv_append by auto (meson relcomp.simps) qed next fix as bs assume *: "map fst xs = as @ ([Acute] @ [Grave]) @ bs" { fix p a b q t' s' u' assume xs: "xs = p @ [(Acute,a),(Grave,b)] @ q" and p: "(u,t') \ lconv p" and a: "(s',t') \ L a" and b: "(s',u') \ R b" and q: "(u',v) \ lconv q" obtain js where lp: "lpeak r a b js" and js: "(t',u') \ lconv js" using pk[OF a b] by auto from lp have "(js, [(Acute,a),(Grave,b)]) \ greek_less r" unfolding lpeak_def using peak_greek_less[of _ r a _ b] by fastforce then have "(p @ js @ q, xs) \ greek_less r" unfolding xs by (intro greek_less_app_mono1 greek_less_app_mono2 \trans r\) auto moreover have "(u, v) \ lconv (p @ js @ q)" using p q js by auto ultimately have "(u, v) \ valley' UNIV" using 2(1) by blast } with * show "(u, v) \ valley' UNIV" using 2(2) by (auto elim!: map_eq_append_splits relcompEpair simp del: append.simps) simp next fix as bs assume *: "map fst xs = as @ ([Acute] @ [Macron]) @ bs" { fix p a b q t' s' u' assume xs: "xs = p @ [(Acute,a),(Macron,b)] @ q" and p: "(u,t') \ lconv p" and a: "(s',t') \ L a" and b: "(s',u') \ E b" and q: "(u',v) \ lconv q" obtain js where lp: "lcliff r a b js" and js: "(t',u') \ lconv js" using lc[OF a b] by auto from lp have "(js, [(Acute,a),(Macron,b)]) \ greek_less r" unfolding lcliff_def using lcliff_greek_less1[OF \trans r\, of _ a _ b] lcliff_greek_less2[OF \trans r\, of _ a b] by fastforce then have "(p @ js @ q, xs) \ greek_less r" unfolding xs by (intro greek_less_app_mono1 greek_less_app_mono2 \trans r\) auto moreover have "(u, v) \ lconv (p @ js @ q)" using p q js by auto ultimately have "(u, v) \ valley' UNIV" using 2(1) by blast } with * show "(u, v) \ valley' UNIV" using 2(2) by (auto elim!: map_eq_append_splits relcompEpair simp del: append.simps) simp next fix as bs assume *: "map fst xs = as @ ([Macron] @ [Grave]) @ bs" { fix p a b q t' s' u' assume xs: "xs = p @ [(Macron,a),(Grave,b)] @ q" and p: "(u,t') \ lconv p" and a: "(s',t') \ (E a)\" and b: "(s',u') \ R b" and q: "(u',v) \ lconv q" obtain js where lp: "rcliff r a b js" and js: "(t',u') \ lconv js" using rc[OF a b] by auto from lp have "(js, [(Macron,a),(Grave,b)]) \ greek_less r" unfolding rcliff_def using rcliff_greek_less1[OF \trans r\, of _ a b] rcliff_greek_less2[OF \trans r\, of _ a _ b] by fastforce then have "(p @ js @ q, xs) \ greek_less r" unfolding xs by (intro greek_less_app_mono1 greek_less_app_mono2 \trans r\) auto moreover have "(u, v) \ lconv (p @ js @ q)" using p q js by auto ultimately have "(u, v) \ valley' UNIV" using 2(1) by blast } with * show "(u, v) \ valley' UNIV" using 2(2) by (auto elim!: map_eq_append_splits relcompEpair simp del: append.simps) simp qed qed qed section \Results\ subsection \Church-Rosser modulo\ text \Decreasing diagrams for Church-Rosser modulo, commutation version.\ lemma dd_commute_modulo[case_names wf trans peak lcliff rcliff]: assumes "wf r" and "trans r" and pk: "\a b s t u. (s, t) \ L a \ (s, u) \ R b \ (t, u) \ conversion' (under r a) O (R b)\<^sup>= O conversion' (under r a \ under r b) O ((L a)\)\<^sup>= O conversion' (under r b)" and lc: "\a b s t u. (s, t) \ L a \ (s, u) \ E b \ (t, u) \ conversion' (under r a) O E b O conversion' (under r a) O ((L a)\)\<^sup>= O conversion' (under r a \ under r b) \ (t, u) \ conversion' (under r a \ under r b) O ((L a )\)\<^sup>= O conversion' (under r b)" and rc: "\a b s t u. (s, t) \ (E a)\ \ (s, u) \ R b \ (t, u) \ conversion' (under r a \ under r b) O (R b)\<^sup>= O conversion' (under r b) O E a O conversion' (under r b) \ (t, u) \ conversion' (under r a) O (R b)\<^sup>= O conversion' (under r a \ under r b)" shows "conversion' UNIV \ valley' UNIV" proof (cases rule: dd_commute_modulo_conv[of r]) case (peak a b s t u) { fix w x y z assume "(t, w) \ conversion' (under r a)" from conversion_to_lconv[OF this] obtain as where "snd ` set as \ under r a" "(t, w) \ lconv as" by auto moreover assume "(w, x) \ (R b)\<^sup>=" then obtain b' where "b' \ {[(Grave,b)],[]}" "(w, x) \ lconv b'" by fastforce moreover assume "(x, y) \ conversion' (under r a \ under r b)" from conversion_to_lconv[OF this] obtain cs where "snd ` set cs \ under r a \ under r b" "(x, y) \ lconv cs" by auto moreover assume "(y, z) \ ((L a)\)\<^sup>=" then obtain a' where "a' \ {[(Acute,a)],[]}" "(y, z) \ lconv a'" by fastforce moreover assume "(z, u) \ conversion' (under r b)" from conversion_to_lconv[OF this] obtain bs where "snd ` set bs \ under r b" "(z, u) \ lconv bs" by auto ultimately have "\xs. lpeak r a b xs \ (t, u) \ lconv xs" by (intro exI[of _ "as @ b' @ cs @ a' @ bs"], unfold lconv_append lpeak_def) blast } then show ?case using pk[OF peak] by blast next case (lcliff a b s t u) { fix w x y z assume "(t, w) \ conversion' (under r a)" from conversion_to_lconv[OF this] obtain as where "snd ` set as \ under r a" "(t, w) \ lconv as" by auto moreover assume "(w, x) \ E b" then obtain b' where "b' = [(Macron,b)]" "(w, x) \ lconv b'" by fastforce moreover assume "(x, y) \ conversion' (under r a)" from conversion_to_lconv[OF this] obtain cs where "snd ` set cs \ under r a" "(x, y) \ lconv cs" by auto moreover assume "(y, z) \ ((L a)\)\<^sup>=" then obtain a' where "a' \ {[(Acute,a)],[]}" "(y, z) \ lconv a'" by fastforce moreover assume "(z, u) \ conversion' (under r a \ under r b)" from conversion_to_lconv[OF this] obtain bs where "snd ` set bs \ under r a \ under r b" "(z, u) \ lconv bs" by auto ultimately have "\xs. lcliff r a b xs \ (t, u) \ lconv xs" by (intro exI[of _ "as @ b' @ cs @ a' @ bs"], unfold lconv_append lcliff_def) blast } moreover { fix w x assume "(t, w) \ conversion' (under r a \ under r b)" from conversion_to_lconv[OF this] obtain cs where "snd ` set cs \ under r a \ under r b" "(t, w) \ lconv cs" by auto moreover assume "(w, x) \ ((L a)\)\<^sup>=" then obtain a' where "a' \ {[(Acute,a)],[]}" "(w, x) \ lconv a'" by fastforce moreover assume "(x, u) \ conversion' (under r b)" from conversion_to_lconv[OF this] obtain bs where "snd ` set bs \ under r b" "(x, u) \ lconv bs" by auto ultimately have "\xs. lcliff r a b xs \ (t, u) \ lconv xs" by (intro exI[of _ "cs @ a' @ bs"], unfold lconv_append lcliff_def) blast } ultimately show ?case using lc[OF lcliff] by blast next case (rcliff a b s t u) { fix w x y z assume "(t, w) \ conversion' (under r a \ under r b)" from conversion_to_lconv[OF this] obtain as where "snd ` set as \ under r a \ under r b" "(t, w) \ lconv as" by auto moreover assume "(w, x) \ (R b)\<^sup>=" then obtain b' where "b' \ {[(Grave,b)],[]}" "(w, x) \ lconv b'" by fastforce moreover assume "(x, y) \ conversion' (under r b)" from conversion_to_lconv[OF this] obtain cs where "snd ` set cs \ under r b" "(x, y) \ lconv cs" by auto moreover assume "(y, z) \ E a" then obtain a' where "a' = [(Macron,a)]" "(y, z) \ lconv a'" by fastforce moreover assume "(z, u) \ conversion' (under r b)" from conversion_to_lconv[OF this] obtain bs where "snd ` set bs \ under r b" "(z, u) \ lconv bs" by auto ultimately have "\xs. rcliff r a b xs \ (t, u) \ lconv xs" by (intro exI[of _ "as @ b' @ cs @ a' @ bs"], unfold lconv_append rcliff_def) blast } moreover { fix w x assume "(t, w) \ conversion' (under r a)" from conversion_to_lconv[OF this] obtain as where "snd ` set as \ under r a" "(t, w) \ lconv as" by auto moreover assume "(w, x) \ (R b)\<^sup>=" then obtain b' where "b' \ {[(Grave,b)],[]}" "(w, x) \ lconv b'" by fastforce moreover assume "(x, u) \ conversion' (under r a \ under r b)" from conversion_to_lconv[OF this] obtain cs where "snd ` set cs \ under r a \ under r b" "(x, u) \ lconv cs" by auto ultimately have "\xs. rcliff r a b xs \ (t, u) \ lconv xs" by (intro exI[of _ "as @ b' @ cs"], unfold lconv_append rcliff_def) blast } ultimately show ?case using rc[OF rcliff] by blast qed fact+ end (* context *) text \Decreasing diagrams for Church-Rosser modulo.\ lemma dd_cr_modulo[case_names wf trans symE peak cliff]: assumes "wf r" and "trans r" and E: "\i. sym (E i)" and pk: "\a b s t u. (s, t) \ L a \ (s, u) \ L b \ (t, u) \ conversion' L L E (under r a) O (L b)\<^sup>= O conversion' L L E (under r a \ under r b) O ((L a)\)\<^sup>= O conversion' L L E (under r b)" and cl: "\a b s t u. (s, t) \ L a \ (s, u) \ E b \ (t, u) \ conversion' L L E (under r a) O E b O conversion' L L E (under r a) O ((L a)\)\<^sup>= O conversion' L L E (under r a \ under r b) \ (t, u) \ conversion' L L E (under r a \ under r b) O ((L a )\)\<^sup>= O conversion' L L E (under r b)" shows "conversion' L L E UNIV \ valley' L L E UNIV" proof (induct rule: dd_commute_modulo[of r]) note E' = E[unfolded sym_conv_converse_eq] case (rcliff a b s t u) show ?case using cl[OF rcliff(2) rcliff(1)[unfolded E'], unfolded converse_iff[of t u,symmetric]] by (auto simp only: E' converse_inward) (auto simp only: ac_simps) qed fact+ subsection \Commutation and confluence\ abbreviation "conversion'' L R M \ ((\i \ M. R i) \ (\i \ M. L i)\)\<^sup>*" abbreviation "valley'' L R M \ (\i \ M. R i)\<^sup>* O ((\i \ M. L i)\)\<^sup>*" text \Decreasing diagrams for commutation.\ lemma dd_commute[case_names wf trans peak]: assumes "wf r" and "trans r" and pk: "\a b s t u. (s, t) \ L a \ (s, u) \ R b \ (t, u) \ conversion'' L R (under r a) O (R b)\<^sup>= O conversion'' L R (under r a \ under r b) O ((L a)\)\<^sup>= O conversion'' L R (under r b)" shows "commute (\i. L i) (\i. R i)" proof - have "((\i. L i)\)\<^sup>* O (\i. R i)\<^sup>* \ conversion'' L R UNIV" by regexp also have "\ \ valley'' L R UNIV" using dd_commute_modulo[OF assms(1,2), of L R "\_. {}"] pk by auto finally show ?thesis by (simp only: commute_def) qed text \Decreasing diagrams for confluence.\ lemmas dd_cr[case_names wf trans peak] = dd_commute[of _ L L for L, unfolded CR_iff_self_commute[symmetric]] subsection \Extended decreasing diagrams\ context fixes r q :: "'b rel" assumes "wf r" and "trans r" and "trans q" and "refl q" and compat: "r O q \ r" begin private abbreviation (input) down :: "('b \ 'a rel) \ ('b \ 'a rel)" where "down L \ \i. \j \ under q i. L j" private lemma Union_down: "(\i. down L i) = (\i. L i)" using \refl q\ by (auto simp: refl_on_def under_def) text \Extended decreasing diagrams for commutation.\ lemma edd_commute[case_names wf transr transq reflq compat peak]: assumes pk: "\a b s t u. (s, t) \ L a \ (s, u) \ R b \ (t, u) \ conversion'' L R (under r a) O (down R b)\<^sup>= O conversion'' L R (under r a \ under r b) O ((down L a)\)\<^sup>= O conversion'' L R (under r b)" shows "commute (\i. L i) (\i. R i)" unfolding Union_down[of L, symmetric] Union_down[of R, symmetric] proof (induct rule: dd_commute[of r "down L" "down R"]) case (peak a b s t u) then obtain a' b' where a': "(a', a) \ q" "(s, t) \ L a'" and b': "(b', b) \ q" "(s, u) \ R b'" by (auto simp: under_def) have "\a' a. (a',a) \ q \ under r a' \ under r a" using compat by (auto simp: under_def) then have aux1: "\a' a L. (a',a) \ q \ (\i \ under r a'. L i) \ (\i \ under r a. L i)" by auto have aux2: "\a' a L. (a',a) \ q \ down L a' \ down L a" using \trans q\ by (auto simp: under_def trans_def) have aux3: "\a L. (\i \ under r a. L i) \ (\i \ under r a. down L i)" using \refl q\ by (auto simp: under_def refl_on_def) from aux1[OF a'(1), of L] aux1[OF a'(1), of R] aux2[OF a'(1), of L] aux1[OF b'(1), of L] aux1[OF b'(1), of R] aux2[OF b'(1), of R] aux3[of L] aux3[of R] show ?case by (intro subsetD[OF _ pk[OF \(s, t) \ L a'\ \(s, u) \ R b'\]], unfold UN_Un) (intro relcomp_mono rtrancl_mono Un_mono iffD2[OF converse_mono]; fast) qed fact+ text \Extended decreasing diagrams for confluence.\ lemmas edd_cr[case_names wf transr transq reflq compat peak] = edd_commute[of L L for L, unfolded CR_iff_self_commute[symmetric]] end (* context *) end (* Decreasing_Diagrams_II *) diff --git a/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy b/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy --- a/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy +++ b/thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy @@ -1,261 +1,261 @@ (* Title: Decreasing Diagrams II Author: Bertram Felgenhauer (2015) Maintainer: Bertram Felgenhauer License: LGPL or BSD License clarification: This file is also licensed under the BSD license to facilitate reuse and moving snippets from here to more suitable places. *) section \Preliminaries\ theory Decreasing_Diagrams_II_Aux imports Well_Quasi_Orders.Multiset_Extension Well_Quasi_Orders.Well_Quasi_Orders begin subsection \Trivialities\ (* move to Relation.thy? *) abbreviation "strict_order R \ irrefl R \ trans R" (* move to Relation.thy? *) lemma strict_order_strict: "strict_order q \ strict (\a b. (a, b) \ q\<^sup>=) = (\a b. (a, b) \ q)" unfolding trans_def irrefl_def by fast (* move to Wellfounded.thy? *) lemma mono_lex1: "mono (\r. lex_prod r s)" by (auto simp add: mono_def) (* move to Wellfounded.thy? *) lemma mono_lex2: "mono (lex_prod r)" by (auto simp add: mono_def) lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp converse_converse converse_Id subsection \Complete lattices and least fixed points\ context complete_lattice begin subsubsection \A chain-based induction principle\ abbreviation set_chain :: "'a set \ bool" where "set_chain C \ \x \ C. \y \ C. x \ y \ y \ x" lemma lfp_chain_induct: assumes mono: "mono f" and step: "\x. P x \ P (f x)" and chain: "\C. set_chain C \ \ x \ C. P x \ P (Sup C)" shows "P (lfp f)" unfolding lfp_eq_fixp[OF mono] proof (rule fixp_induct) show "monotone (\) (\) f" using mono unfolding order_class.mono_def monotone_def . next show "P (Sup {})" using chain[of "{}"] by simp next show "ccpo.admissible Sup (\) P" by (auto simp add: chain ccpo.admissible_def Complete_Partial_Order.chain_def) qed fact subsubsection \Preservation of transitivity, asymmetry, irreflexivity by suprema\ lemma trans_Sup_of_chain: assumes "set_chain C" and trans: "\R. R \ C \ trans R" shows "trans (Sup C)" proof (intro transI) fix x y z assume "(x,y) \ Sup C" and "(y,z) \ Sup C" from \(x,y) \ Sup C\ obtain R where "R \ C" and "(x,y) \ R" by blast from \(y,z) \ Sup C\ obtain S where "S \ C" and "(y,z) \ S" by blast from \R \ C\ and \S \ C\ and \set_chain C\ have "R \ S = R \ R \ S = S" by blast with \R \ C\ and \S \ C\ have "R \ S \ C" by fastforce with \(x,y) \ R\ and \(y,z) \ S\ and trans[of "R \ S"] have "(x,z) \ R \ S" unfolding trans_def by blast with \R \ S \ C\ show "(x,z) \ \C" by blast qed lemma asym_Sup_of_chain: assumes "set_chain C" and asym: "\ R. R \ C \ asym R" shows "asym (Sup C)" proof (intro asymI notI) fix a b assume "(a,b) \ Sup C" then obtain "R" where "R \ C" and "(a,b) \ R" by blast assume "(b,a) \ Sup C" then obtain "S" where "S \ C" and "(b,a) \ S" by blast from \R \ C\ and \S \ C\ and \set_chain C\ have "R \ S = R \ R \ S = S" by blast with \R \ C\ and \S \ C\ have "R \ S \ C" by fastforce with \(a,b) \ R\ and \(b,a) \ S\ and asym[THEN asymD] show "False" by blast qed lemma strict_order_lfp: assumes "mono f" and "\R. strict_order R \ strict_order (f R)" shows "strict_order (lfp f)" proof (intro lfp_chain_induct[of f strict_order]) fix C :: "('b \ 'b) set set" assume "set_chain C" and "\R \ C. strict_order R" from this show "strict_order (Sup C)" using asym_on_iff_irrefl_on_if_trans[of _ UNIV] by (metis asym_Sup_of_chain trans_Sup_of_chain) qed fact+ lemma trans_lfp: assumes "mono f" and "\R. trans R \ trans (f R)" shows "trans (lfp f)" by (metis lfp_chain_induct[of f trans] assms trans_Sup_of_chain) end (* complete_lattice *) subsection \Multiset extension\ lemma mulex_iff_mult: "mulex r M N \ (M,N) \ mult {(M,N) . r M N}" by (auto simp add: mulex_on_def restrict_to_def mult_def mulex1_def tranclp_unfold) lemma multI: assumes "trans r" "M = I + K" "N = I + J" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k,j) \ r" shows "(M,N) \ mult r" using assms one_step_implies_mult by blast lemma multE: assumes "trans r" and "(M,N) \ mult r" obtains I J K where "M = I + K" "N = I + J" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k,j) \ r" using mult_implies_one_step[OF assms] by blast lemma mult_on_union: "(M,N) \ mult r \ (K + M, K + N) \ mult r" using mulex_on_union[of "\x y. (x,y) \ r" UNIV] by (auto simp: mulex_iff_mult) lemma mult_on_union': "(M,N) \ mult r \ (M + K, N + K) \ mult r" using mulex_on_union'[of "\x y. (x,y) \ r" UNIV] by (auto simp: mulex_iff_mult) lemma mult_on_add_mset: "(M,N) \ mult r \ (add_mset k M, add_mset k N) \ mult r" unfolding add_mset_add_single[of k M] add_mset_add_single[of k N] by (rule mult_on_union') lemma mult_empty[simp]: "(M,{#}) \ mult R" by (metis mult_def not_less_empty trancl.cases) lemma mult_singleton[simp]: "(x, y) \ r \ (add_mset x M, add_mset y M) \ mult r" unfolding add_mset_add_single[of x M] add_mset_add_single[of y M] apply (rule mult_on_union) using mult1_singleton[of x y r] by (auto simp add: mult_def mult_on_union) lemma empty_mult[simp]: "({#},N) \ mult R \ N \ {#}" using empty_mulex_on[of N UNIV "\M N. (M,N) \ R"] by (auto simp add: mulex_iff_mult) lemma trans_mult: "trans (mult R)" unfolding mult_def by simp lemma strict_order_mult: assumes "irrefl R" and "trans R" shows "irrefl (mult R)" and "trans (mult R)" proof - show "irrefl (mult R)" unfolding irrefl_def proof (intro allI notI, elim multE[OF \trans R\]) fix M I J K assume "M = I + J" "M = I + K" "J \ {#}" and *: "\k \ set_mset K. \j \ set_mset J. (k, j) \ R" from \M = I + J\ and \M = I + K\ have "J = K" by simp have "finite (set_mset J)" by simp then have "set_mset J = {}" using * unfolding \J = K\ by (induct rule: finite_induct) (simp, metis assms insert_absorb insert_iff insert_not_empty irrefl_def transD) then show "False" using \J \ {#}\ by simp qed qed (simp add: trans_mult) lemma mult_of_image_mset: assumes "trans R" and "trans R'" and "\x y. x \ set_mset N \ y \ set_mset M \ (x,y) \ R \ (f x, f y) \ R'" and "(N, M) \ mult R" shows "(image_mset f N, image_mset f M) \ mult R'" proof (insert assms(4), elim multE[OF assms(1)]) fix I J K assume "N = I + K" "M = I + J" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k, j) \ R" thus "(image_mset f N, image_mset f M) \ mult R'" using assms(2,3) by (intro multI) (auto, blast) qed subsection \Incrementality of @{term mult1} and @{term mult}\ lemma mono_mult1: "mono mult1" unfolding mono_def mult1_def by blast lemma mono_mult: "mono mult" unfolding mono_def mult_def proof (intro allI impI subsetI) fix R S :: "'a rel" and x assume "R \ S" and "x \ (mult1 R)\<^sup>+" then show "x \ (mult1 S)\<^sup>+" using mono_mult1[unfolded mono_def] trancl_mono[of x "mult1 R" "mult1 S"] by auto qed subsection \Well-orders and well-quasi-orders\ lemma wf_iff_wfp_on: "wf p \ wfp_on (\a b. (a, b) \ p) UNIV" unfolding wfp_on_iff_inductive_on wf_def inductive_on_def by force lemma well_order_implies_wqo: assumes "well_order r" shows "wqo_on (\a b. (a, b) \ r) UNIV" proof (intro wqo_onI almost_full_onI) - show "transp_on (\a b. (a, b) \ r) UNIV" using assms + show "transp (\a b. (a, b) \ r)" using assms by (auto simp only: well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def - trans_def transp_on_def) + trans_def transp_def) next fix f :: "nat \ 'a" show "good (\a b. (a, b) \ r) f" using assms unfolding well_order_on_def wf_iff_wfp_on wfp_on_def not_ex not_all de_Morgan_conj proof (elim conjE allE exE) fix x assume "linear_order r" and "f x \ UNIV \ (f (Suc x), f x) \ r - Id" then have "(f x, f (Suc x)) \ r" using \linear_order r\ by (force simp: linear_order_on_def Relation.total_on_def partial_order_on_def preorder_on_def refl_on_def) then show "good (\a b. (a, b) \ r) f" by (auto simp: good_def) qed qed subsection \Splitting lists into prefix, element, and suffix\ fun list_splits :: "'a list \ ('a list \ 'a \ 'a list) list" where "list_splits [] = []" | "list_splits (x # xs) = ([], x, xs) # map (\(xs, x', xs'). (x # xs, x', xs')) (list_splits xs)" lemma list_splits_empty[simp]: "list_splits xs = [] \ xs = []" by (cases xs) simp_all lemma elem_list_splits_append: assumes "(ys, y, zs) \ set (list_splits xs)" shows "ys @ [y] @ zs = xs" using assms by (induct xs arbitrary: ys) auto lemma elem_list_splits_length: assumes "(ys, y, zs) \ set (list_splits xs)" shows "length ys < length xs" and "length zs < length xs" using elem_list_splits_append[OF assms] by auto lemma elem_list_splits_elem: assumes "(xs, y, ys) \ set (list_splits zs)" shows "y \ set zs" using elem_list_splits_append[OF assms] by force lemma list_splits_append: "list_splits (xs @ ys) = map (\(xs', x', ys'). (xs', x', ys' @ ys)) (list_splits xs) @ map (\(xs', x', ys'). (xs @ xs', x', ys')) (list_splits ys)" by (induct xs) auto lemma list_splits_rev: "list_splits (rev xs) = map (\(xs, x, ys). (rev ys, x, rev xs)) (rev (list_splits xs))" by (induct xs) (auto simp add: list_splits_append comp_def prod.case_distrib rev_map) lemma list_splits_map: "list_splits (map f xs) = map (\(xs, x, ys). (map f xs, f x, map f ys)) (list_splits xs)" by (induct xs) auto end (* Decreasing_Diagrams_II_Aux *) diff --git a/thys/Groebner_Macaulay/Monomial_Module.thy b/thys/Groebner_Macaulay/Monomial_Module.thy --- a/thys/Groebner_Macaulay/Monomial_Module.thy +++ b/thys/Groebner_Macaulay/Monomial_Module.thy @@ -1,553 +1,553 @@ section \Monomial Modules\ theory Monomial_Module imports Groebner_Bases.Reduced_GB begin text \Properties of modules generated by sets of monomials, and (reduced) Gr\"obner bases thereof.\ subsection \Sets of Monomials\ definition is_monomial_set :: "('a \\<^sub>0 'b::zero) set \ bool" where "is_monomial_set A \ (\p\A. is_monomial p)" lemma is_monomial_setI: "(\p. p \ A \ is_monomial p) \ is_monomial_set A" by (simp add: is_monomial_set_def) lemma is_monomial_setD: "is_monomial_set A \ p \ A \ is_monomial p" by (simp add: is_monomial_set_def) lemma is_monomial_set_subset: "is_monomial_set B \ A \ B \ is_monomial_set A" by (auto simp: is_monomial_set_def) lemma is_monomial_set_Un: "is_monomial_set (A \ B) \ (is_monomial_set A \ is_monomial_set B)" by (auto simp: is_monomial_set_def) subsection \Modules\ context term_powerprod begin lemma monomial_pmdl: assumes "is_monomial_set B" and "p \ pmdl B" shows "monomial (lookup p v) v \ pmdl B" using assms(2) proof (induct p rule: pmdl_induct) case base: module_0 show ?case by (simp add: pmdl.span_zero) next case step: (module_plus p b c t) have eq: "monomial (lookup (p + monom_mult c t b) v) v = monomial (lookup p v) v + monomial (lookup (monom_mult c t b) v) v" by (simp only: single_add lookup_add) from assms(1) step.hyps(3) have "is_monomial b" by (rule is_monomial_setD) then obtain d u where b: "b = monomial d u" by (rule is_monomial_monomial) have "monomial (lookup (monom_mult c t b) v) v \ pmdl B" proof (simp add: b monom_mult_monomial lookup_single when_def pmdl.span_zero, intro impI) assume "t \ u = v" hence "monomial (c * d) v = monom_mult c t b" by (simp add: b monom_mult_monomial) also from step.hyps(3) have "\ \ pmdl B" by (rule monom_mult_in_pmdl) finally show "monomial (c * d) v \ pmdl B" . qed with step.hyps(2) show ?case unfolding eq by (rule pmdl.span_add) qed lemma monomial_pmdl_field: assumes "is_monomial_set B" and "p \ pmdl B" and "v \ keys (p::_ \\<^sub>0 'b::field)" shows "monomial c v \ pmdl B" proof - from assms(1, 2) have "monomial (lookup p v) v \ pmdl B" by (rule monomial_pmdl) hence "monom_mult (c / lookup p v) 0 (monomial (lookup p v) v) \ pmdl B" by (rule pmdl_closed_monom_mult) with assms(3) show ?thesis by (simp add: monom_mult_monomial splus_zero in_keys_iff) qed end (* term_powerprod *) context ordered_term begin lemma keys_monomial_pmdl: assumes "is_monomial_set F" and "p \ pmdl F" and "t \ keys p" obtains f where "f \ F" and "f \ 0" and "lt f adds\<^sub>t t" using assms(2) assms(3) proof (induct arbitrary: thesis rule: pmdl_induct) case module_0 from this(2) show ?case by simp next case step: (module_plus p f0 c s) from assms(1) step(3) have "is_monomial f0" unfolding is_monomial_set_def .. hence "keys f0 = {lt f0}" and "f0 \ 0" by (rule keys_monomial, rule monomial_not_0) from Poly_Mapping.keys_add step(6) have "t \ keys p \ keys (monom_mult c s f0)" .. thus ?case proof assume "t \ keys p" from step(2)[OF _ this] obtain f where "f \ F" and "f \ 0" and "lt f adds\<^sub>t t" by blast thus ?thesis by (rule step(5)) next assume "t \ keys (monom_mult c s f0)" with keys_monom_mult_subset have "t \ (\) s ` keys f0" .. hence "t = s \ lt f0" by (simp add: \keys f0 = {lt f0}\) hence "lt f0 adds\<^sub>t t" by (simp add: term_simps) with \f0 \ F\ \f0 \ 0\ show ?thesis by (rule step(5)) qed qed lemma image_lt_monomial_lt: "lt ` monomial (1::'b::zero_neq_one) ` lt ` F = lt ` F" by (auto simp: lt_monomial intro!: image_eqI) subsection \Reduction\ lemma red_setE2: assumes "red B p q" obtains b where "b \ B" and "b \ 0" and "red {b} p q" proof - from assms obtain b t where "b \ B" and "red_single p q b t" by (rule red_setE) from this(2) have "b \ 0" by (simp add: red_single_def) have "red {b} p q" by (rule red_setI, simp, fact) show ?thesis by (rule, fact+) qed lemma red_monomial_keys: assumes "is_monomial r" and "red {r} p q" shows "card (keys p) = Suc (card (keys q))" proof - from assms(2) obtain s where rs: "red_single p q r s" unfolding red_singleton .. hence cp0: "lookup p (s \ lt r) \ 0" and q_def0: "q = p - monom_mult (lookup p (s \ lt r) / lc r) s r" unfolding red_single_def by simp_all from assms(1) obtain c t where "c \ 0" and r_def: "r = monomial c t" by (rule is_monomial_monomial) have ltr: "lt r = t" unfolding r_def by (rule lt_monomial, fact) have lcr: "lc r = c" unfolding r_def by (rule lc_monomial) define u where "u = s \ t" from q_def0 have "q = p - monom_mult (lookup p u / c) s r" unfolding u_def ltr lcr . also have "... = p - monomial ((lookup p u / c) * c) u" unfolding u_def r_def monom_mult_monomial .. finally have q_def: "q = p - monomial (lookup p u) u" using \c \ 0\ by simp from cp0 have "lookup p u \ 0" unfolding u_def ltr . hence "u \ keys p" by (simp add: in_keys_iff) have "keys q = keys p - {u}" unfolding q_def proof (rule, rule) fix x assume "x \ keys (p - monomial (lookup p u) u)" hence "lookup (p - monomial (lookup p u) u) x \ 0" by (simp add: in_keys_iff) hence a: "lookup p x - lookup (monomial (lookup p u) u) x \ 0" unfolding lookup_minus . hence "x \ u" unfolding lookup_single by auto with a have "lookup p x \ 0" unfolding lookup_single by auto show "x \ keys p - {u}" proof from \lookup p x \ 0\ show "x \ keys p" by (simp add: in_keys_iff) next from \x \ u\ show "x \ {u}" by simp qed next show "keys p - {u} \ keys (p - monomial (lookup p u) u)" proof fix x assume "x \ keys p - {u}" hence "x \ keys p" and "x \ u" by auto from \x \ keys p\ have "lookup p x \ 0" by (simp add: in_keys_iff) with \x \ u\ have "lookup (p - monomial (lookup p u) u) x \ 0" by (simp add: lookup_minus lookup_single) thus "x \ keys (p - monomial (lookup p u) u)" by (simp add: in_keys_iff) qed qed have "Suc (card (keys q)) = card (keys p)" unfolding \keys q = keys p - {u}\ by (rule card_Suc_Diff1, rule finite_keys, fact) thus ?thesis by simp qed lemma red_monomial_monomial_setD: assumes "is_monomial p" and "is_monomial_set B" and "red B p q" shows "q = 0" proof - from assms(3) obtain b where "b \ B" and "b \ 0" and *: "red {b} p q" by (rule red_setE2) from assms(2) this(1) have "is_monomial b" by (rule is_monomial_setD) hence "card (keys p) = Suc (card (keys q))" using * by (rule red_monomial_keys) with assms(1) show ?thesis by (simp add: is_monomial_def) qed corollary is_red_monomial_monomial_setD: assumes "is_monomial p" and "is_monomial_set B" and "is_red B p" shows "red B p 0" proof - from assms(3) obtain q where "red B p q" by (rule is_redE) moreover from assms(1, 2) this have "q = 0" by (rule red_monomial_monomial_setD) ultimately show ?thesis by simp qed corollary is_red_monomial_monomial_set_in_pmdl: "is_monomial p \ is_monomial_set B \ is_red B p \ p \ pmdl B" by (intro red_rtranclp_0_in_pmdl r_into_rtranclp is_red_monomial_monomial_setD) corollary red_rtrancl_monomial_monomial_set_cases: assumes "is_monomial p" and "is_monomial_set B" and "(red B)\<^sup>*\<^sup>* p q" obtains "q = p" | "q = 0" using assms(3) proof (induct q arbitrary: thesis rule: rtranclp_induct) case base from refl show ?case by (rule base) next case (step y z) show ?case proof (rule step.hyps) assume "y = p" with step.hyps(2) have "red B p z" by simp with assms(1, 2) have "z = 0" by (rule red_monomial_monomial_setD) thus ?thesis by (rule step.prems) next assume "y = 0" from step.hyps(2) have "is_red B 0" unfolding \y = 0\ by (rule is_redI) with irred_0 show ?thesis .. qed qed lemma is_red_monomial_lt: assumes "0 \ B" shows "is_red (monomial (1::'b::field) ` lt ` B) = is_red B" proof fix p let ?B = "monomial (1::'b) ` lt ` B" show "is_red ?B p \ is_red B p" proof assume "is_red ?B p" then obtain f v where "f \ ?B" and "v \ keys p" and adds: "lt f adds\<^sub>t v" by (rule is_red_addsE) from this(1) have "lt f \ lt ` ?B" by (rule imageI) also have "\ = lt ` B" by (fact image_lt_monomial_lt) finally obtain b where "b \ B" and eq: "lt f = lt b" .. note this(1) moreover from this assms have "b \ 0" by blast moreover note \v \ keys p\ moreover from adds have "lt b adds\<^sub>t v" by (simp only: eq) ultimately show "is_red B p" by (rule is_red_addsI) next assume "is_red B p" then obtain b v where "b \ B" and "v \ keys p" and adds: "lt b adds\<^sub>t v" by (rule is_red_addsE) from this(1) have "lt b \ lt ` B" by (rule imageI) also from image_lt_monomial_lt have "\ = lt ` ?B" by (rule sym) finally obtain f where "f \ ?B" and eq: "lt b = lt f" .. note this(1) moreover from this have "f \ 0" by (auto simp: monomial_0_iff) moreover note \v \ keys p\ moreover from adds have "lt f adds\<^sub>t v" by (simp only: eq) ultimately show "is_red ?B p" by (rule is_red_addsI) qed qed end (* ordered_term *) subsection \Gr\"obner Bases\ context gd_term begin lemma monomial_set_is_GB: assumes "is_monomial_set G" shows "is_Groebner_basis G" unfolding GB_alt_1 proof fix f assume "f \ pmdl G" thus "(red G)\<^sup>*\<^sup>* f 0" proof (induct f rule: poly_mapping_plus_induct) case 1 show ?case .. next case (2 f c t) let ?f = "monomial c t + f" from 2(1) have "t \ keys (monomial c t)" by simp from this 2(2) have "t \ keys ?f" by (rule in_keys_plusI1) with assms \?f \ pmdl G\ obtain g where "g \ G" and "g \ 0" and "lt g adds\<^sub>t t" by (rule keys_monomial_pmdl) from this(1) have "red G ?f f" proof (rule red_setI) from \lt g adds\<^sub>t t\ have "component_of_term (lt g) = component_of_term t" and "lp g adds pp_of_term t" by (simp_all add: adds_term_def) from this have eq: "(pp_of_term t - lp g) \ lt g = t" by (simp add: adds_minus splus_def term_of_pair_pair) moreover from 2(2) have "lookup ?f t = c" by (simp add: lookup_add in_keys_iff) ultimately show "red_single (monomial c t + f) f g (pp_of_term t - lp g)" proof (simp add: red_single_def \g \ 0\ \t \ keys ?f\ 2(1)) from \g \ 0\ have "lc g \ 0" by (rule lc_not_0) hence "monomial c t = monom_mult (c / lc g) (pp_of_term t - lp g) (monomial (lc g) (lt g))" by (simp add: monom_mult_monomial eq) moreover from assms \g \ G\ have "is_monomial g" unfolding is_monomial_set_def .. ultimately show "monomial c t = monom_mult (c / lc g) (pp_of_term t - lp g) g" by (simp only: monomial_eq_itself) qed qed have "f \ pmdl G" by (rule pmdl_closed_red, fact subset_refl, fact+) hence "(red G)\<^sup>*\<^sup>* f 0" by (rule 2(3)) with \red G ?f f\ show ?case by simp qed qed context fixes d assumes dgrad: "dickson_grading (d::'a \ nat)" begin context fixes F m assumes fin_comps: "finite (component_of_term ` Keys F)" and F_sub: "F \ dgrad_p_set d m" and F_monom: "is_monomial_set (F::(_ \\<^sub>0 'b::field) set)" begin text \The proof of the following lemma could be simplified, analogous to homogeneous ideals.\ lemma reduced_GB_subset_monic_dgrad_p_set: "reduced_GB F \ monic ` F" proof - from subset_refl obtain F' where "F' \ F - {0}" and "lt ` (F - {0}) = lt ` F'" and "inj_on lt F'" by (rule subset_imageE_inj) define G where "G = {f \ F'. \f'\F'. lt f' adds\<^sub>t lt f \ f' = f}" have "G \ F'" by (simp add: G_def) hence "G \ F - {0}" using \F' \ F - {0}\ by (rule subset_trans) also have "\ \ F" by blast finally have "G \ F" . have 1: thesis if "f \ F" and "f \ 0" and "\g. g \ G \ lt g adds\<^sub>t lt f \ thesis" for thesis f proof - let ?K = "component_of_term ` Keys F" let ?A = "{t. pp_of_term t \ dgrad_set d m \ component_of_term t \ ?K}" let ?Q = "{f' \ F'. lt f' adds\<^sub>t lt f}" from dgrad fin_comps have "almost_full_on (adds\<^sub>t) ?A" by (rule Dickson_term) - moreover have "transp_on (adds\<^sub>t) ?A" by (auto intro: transp_onI dest: adds_term_trans) + moreover have "transp_on ?A (adds\<^sub>t)" by (auto intro: transp_onI dest: adds_term_trans) ultimately have "wfp_on (strict (adds\<^sub>t)) ?A" by (rule af_trans_imp_wf) moreover have "lt f \ lt ` ?Q" proof - from that(1, 2) have "f \ F - {0}" by simp hence "lt f \ lt ` (F - {0})" by (rule imageI) also have "\ = lt ` F'" by fact finally have "lt f \ lt ` F'" . with adds_term_refl show ?thesis by fastforce qed moreover have "lt ` ?Q \ ?A" proof fix s assume "s \ lt ` ?Q" then obtain q where "q \ ?Q" and s: "s = lt q" .. from this(1) have "q \ F'" by simp hence "q \ F - {0}" using \F' \ F - {0}\ .. hence "q \ F" and "q \ 0" by simp_all from this(1) F_sub have "q \ dgrad_p_set d m" .. from \q \ 0\ have "lt q \ keys q" by (rule lt_in_keys) hence "pp_of_term (lt q) \ pp_of_term ` keys q" by (rule imageI) also from \q \ dgrad_p_set d m\ have "\ \ dgrad_set d m" by (simp add: dgrad_p_set_def) finally have 1: "pp_of_term s \ dgrad_set d m" by (simp only: s) from \lt q \ keys q\ \q \ F\ have "lt q \ Keys F" by (rule in_KeysI) hence "component_of_term s \ ?K" unfolding s by (rule imageI) with 1 show "s \ ?A" by simp qed ultimately obtain t where "t \ lt ` ?Q" and t_min: "\s. strict (adds\<^sub>t) s t \ s \ lt ` ?Q" by (rule wfp_onE_min) blast from this(1) obtain g where "g \ ?Q" and t: "t = lt g" .. from this(1) have "g \ F'" and adds: "lt g adds\<^sub>t lt f" by simp_all show ?thesis proof (rule that) { fix f' assume "f' \ F'" assume "lt f' adds\<^sub>t lt g" hence "lt f' adds\<^sub>t lt f" using adds by (rule adds_term_trans) with \f' \ F'\ have "f' \ ?Q" by simp hence "lt f' \ lt ` ?Q" by (rule imageI) with t_min have "\ strict (adds\<^sub>t) (lt f') (lt g)" unfolding t by blast with \lt f' adds\<^sub>t lt g\ have "lt g adds\<^sub>t lt f'" by blast with \lt f' adds\<^sub>t lt g\ have "lt f' = lt g" by (rule adds_term_antisym) with \inj_on lt F'\ have "f' = g" using \f' \ F'\ \g \ F'\ by (rule inj_onD) } with \g \ F'\ show "g \ G" by (simp add: G_def) qed fact qed have 2: "is_red G q" if "q \ pmdl F" and "q \ 0" for q proof - from that(2) have "keys q \ {}" by simp then obtain t where "t \ keys q" by blast with F_monom that(1) obtain f where "f \ F" and "f \ 0" and *: "lt f adds\<^sub>t t" by (rule keys_monomial_pmdl) from this(1, 2) obtain g where "g \ G" and "lt g adds\<^sub>t lt f" by (rule 1) from this(2) have **: "lt g adds\<^sub>t t" using * by (rule adds_term_trans) from \g \ G\ \G \ F - {0}\ have "g \ F - {0}" .. hence "g \ 0" by simp with \g \ G\ show ?thesis using \t \ keys q\ ** by (rule is_red_addsI) qed from \G \ F - {0}\ have "G \ F" by blast hence "pmdl G \ pmdl F" by (rule pmdl.span_mono) note dgrad fin_comps F_sub moreover have "is_reduced_GB (monic ` G)" unfolding is_reduced_GB_def GB_image_monic proof (intro conjI image_monic_is_auto_reduced image_monic_is_monic_set) from dgrad show "is_Groebner_basis G" proof (rule isGB_I_is_red) from \G \ F\ F_sub show "G \ dgrad_p_set d m" by (rule subset_trans) next fix f assume "f \ pmdl G" hence "f \ pmdl F" using \pmdl G \ pmdl F\ .. moreover assume "f \ 0" ultimately show "is_red G f" by (rule 2) qed next show "is_auto_reduced G" unfolding is_auto_reduced_def proof (intro ballI notI) fix g assume "g \ G" hence "g \ F" using \G \ F\ .. with F_monom have "is_monomial g" by (rule is_monomial_setD) hence keys_g: "keys g = {lt g}" by (rule keys_monomial) assume "is_red (G - {g}) g" then obtain g' t where "g' \ G - {g}" and "t \ keys g" and adds: "lt g' adds\<^sub>t t" by (rule is_red_addsE) from this(1) have "g' \ F'" and "g' \ g" by (simp_all add: G_def) from \t \ keys g\ have "t = lt g" by (simp add: keys_g) with \g \ G\ \g' \ F'\ adds have "g' = g" by (simp add: G_def) with \g' \ g\ show False .. qed next show "0 \ monic ` G" proof assume "0 \ monic ` G" then obtain g where "0 = monic g" and "g \ G" .. moreover from this(2) \G \ F - {0}\ have "g \ 0" by blast ultimately show False by (simp add: monic_0_iff) qed qed moreover have "pmdl (monic ` G) = pmdl F" unfolding pmdl_image_monic proof show "pmdl F \ pmdl G" proof (rule pmdl.span_subset_spanI, rule) fix f assume "f \ F" hence "f \ pmdl F" by (rule pmdl.span_base) note dgrad moreover from \G \ F\ F_sub have "G \ dgrad_p_set d m" by (rule subset_trans) moreover note \pmdl G \ pmdl F\ 2 \f \ pmdl F\ moreover from \f \ F\ F_sub have "f \ dgrad_p_set d m" .. ultimately have "(red G)\<^sup>*\<^sup>* f 0" by (rule is_red_implies_0_red_dgrad_p_set) thus "f \ pmdl G" by (rule red_rtranclp_0_in_pmdl) qed qed fact ultimately have "reduced_GB F = monic ` G" by (rule reduced_GB_unique_dgrad_p_set) also from \G \ F\ have "\ \ monic ` F" by (rule image_mono) finally show ?thesis . qed corollary reduced_GB_is_monomial_set_dgrad_p_set: "is_monomial_set (reduced_GB F)" proof (rule is_monomial_setI) fix g assume "g \ reduced_GB F" also have "\ \ monic ` F" by (fact reduced_GB_subset_monic_dgrad_p_set) finally obtain f where "f \ F" and g: "g = monic f" .. from F_monom this(1) have "is_monomial f" by (rule is_monomial_setD) hence "card (keys f) = 1" by (simp only: is_monomial_def) hence "f \ 0" by auto hence "lc f \ 0" by (rule lc_not_0) hence "1 / lc f \ 0" by simp hence "keys g = (\) 0 ` keys f" by (simp add: keys_monom_mult monic_def g) also from refl have "\ = (\x. x) ` keys f" by (rule image_cong) (simp only: splus_zero) finally show "is_monomial g" using \card (keys f) = 1\ by (simp only: is_monomial_def image_ident) qed end lemma is_red_reduced_GB_monomial_dgrad_set: assumes "finite (component_of_term ` S)" and "pp_of_term ` S \ dgrad_set d m" shows "is_red (reduced_GB (monomial 1 ` S)) = is_red (monomial (1::'b::field) ` S)" proof fix p let ?F = "monomial (1::'b) ` S" from assms(1) have 1: "finite (component_of_term ` Keys ?F)" by (simp add: Keys_def) moreover from assms(2) have 2: "?F \ dgrad_p_set d m" by (auto simp: dgrad_p_set_def) moreover have "is_monomial_set ?F" by (auto intro!: is_monomial_setI monomial_is_monomial) ultimately have "reduced_GB ?F \ monic ` ?F" by (rule reduced_GB_subset_monic_dgrad_p_set) also have "\ = ?F" by (auto simp: monic_def intro!: image_eqI) finally have 3: "reduced_GB ?F \ ?F" . show "is_red (reduced_GB ?F) p \ is_red ?F p" proof assume "is_red (reduced_GB ?F) p" thus "is_red ?F p" using 3 by (rule is_red_subset) next assume "is_red ?F p" then obtain f v where "f \ ?F" and "v \ keys p" and "f \ 0" and adds1: "lt f adds\<^sub>t v" by (rule is_red_addsE) from this(1) have "f \ pmdl ?F" by (rule pmdl.span_base) from dgrad 1 2 have "is_Groebner_basis (reduced_GB ?F)" by (rule reduced_GB_is_GB_dgrad_p_set) moreover from \f \ pmdl ?F\ dgrad 1 2 have "f \ pmdl (reduced_GB ?F)" by (simp only: reduced_GB_pmdl_dgrad_p_set) ultimately obtain g where "g \ reduced_GB ?F" and "g \ 0" and "lt g adds\<^sub>t lt f" using \f \ 0\ by (rule GB_adds_lt) from this(3) adds1 have "lt g adds\<^sub>t v" by (rule adds_term_trans) with \g \ reduced_GB ?F\ \g \ 0\ \v \ keys p\ show "is_red (reduced_GB ?F) p" by (rule is_red_addsI) qed qed corollary is_red_reduced_GB_monomial_lt_GB_dgrad_p_set: assumes "finite (component_of_term ` Keys G)" and "G \ dgrad_p_set d m" and "0 \ G" shows "is_red (reduced_GB (monomial (1::'b::field) ` lt ` G)) = is_red G" proof - let ?S = "lt ` G" let ?G = "monomial (1::'b) ` ?S" from assms(3) have "?S \ Keys G" by (auto intro: lt_in_keys in_KeysI) hence "component_of_term ` ?S \ component_of_term ` Keys G" and *: "pp_of_term ` ?S \ pp_of_term ` Keys G" by (rule image_mono)+ from this(1) have "finite (component_of_term ` ?S)" using assms(1) by (rule finite_subset) moreover from * have "pp_of_term ` ?S \ dgrad_set d m" proof (rule subset_trans) from assms(2) show "pp_of_term ` Keys G \ dgrad_set d m" by (auto simp: dgrad_p_set_def Keys_def) qed ultimately have "is_red (reduced_GB ?G) = is_red ?G" by (rule is_red_reduced_GB_monomial_dgrad_set) also from assms(3) have "\ = is_red G" by (rule is_red_monomial_lt) finally show ?thesis . qed lemma reduced_GB_monomial_lt_reduced_GB_dgrad_p_set: assumes "finite (component_of_term ` Keys F)" and "F \ dgrad_p_set d m" shows "reduced_GB (monomial 1 ` lt ` reduced_GB F) = monomial (1::'b::field) ` lt ` reduced_GB F" proof (rule reduced_GB_unique) let ?G = "reduced_GB F" let ?F = "monomial (1::'b) ` lt ` ?G" from dgrad assms have "0 \ ?G" and ar: "is_auto_reduced ?G" and "finite ?G" by (rule reduced_GB_nonzero_dgrad_p_set, rule reduced_GB_is_auto_reduced_dgrad_p_set, rule finite_reduced_GB_dgrad_p_set) from this(3) show "finite ?F" by (intro finite_imageI) show "is_reduced_GB ?F" unfolding is_reduced_GB_def proof (intro conjI monomial_set_is_GB) show "is_monomial_set ?F" by (auto intro!: is_monomial_setI monomial_is_monomial) next show "is_monic_set ?F" by (simp add: is_monic_set_def) next show "0 \ ?F" by (auto simp: monomial_0_iff) next show "is_auto_reduced ?F" unfolding is_auto_reduced_def proof (intro ballI notI) fix f assume "f \ ?F" then obtain g where "g \ ?G" and f: "f = monomial 1 (lt g)" by blast assume "is_red (?F - {f}) f" then obtain f' v where "f' \ ?F - {f}" and "v \ keys f" and "f' \ 0" and adds1: "lt f' adds\<^sub>t v" by (rule is_red_addsE) from this(1) have "f' \ ?F" and "f' \ f" by simp_all from this(1) obtain g' where "g' \ ?G" and f': "f' = monomial 1 (lt g')" by blast from \v \ keys f\ have v: "v = lt g" by (simp add: f) from ar \g \ ?G\ have "\ is_red (?G - {g}) g" by (rule is_auto_reducedD) moreover have "is_red (?G - {g}) g" proof (rule is_red_addsI) from \g' \ ?G\ \f' \ f\ show "g' \ ?G - {g}" by (auto simp: f f') next from \g' \ ?G\ \0 \ ?G\ show "g' \ 0" by blast next from \g \ ?G\ \0 \ ?G\ have "g \ 0" by blast thus "lt g \ keys g" by (rule lt_in_keys) next from adds1 show adds2: "lt g' adds\<^sub>t lt g" by (simp add: v f' lt_monomial) qed ultimately show False .. qed qed qed (fact refl) end end (* gd_term *) end (* theory *) diff --git a/thys/Open_Induction/Open_Induction.thy b/thys/Open_Induction/Open_Induction.thy --- a/thys/Open_Induction/Open_Induction.thy +++ b/thys/Open_Induction/Open_Induction.thy @@ -1,181 +1,181 @@ (* Title: Open Induction Author: Mizuhito Ogawa Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Open Induction\ theory Open_Induction imports Restricted_Predicates begin subsection \(Greatest) Lower Bounds and Chains\ text \ A set \B\ has the \emph{lower bound} \x\ iff \x\ is less than or equal to every element of \B\. \ definition "lb P B x \ (\y\B. P\<^sup>=\<^sup>= x y)" lemma lbI [Pure.intro]: "(\y. y \ B \ P\<^sup>=\<^sup>= x y) \ lb P B x" by (auto simp: lb_def) text \ A set \B\ has the \emph{greatest lower bound} \x\ iff \x\ is a lower bound of \B\ \emph{and} less than or equal to every other lower bound of \B\. \ definition "glb P B x \ lb P B x \ (\y. lb P B y \ P\<^sup>=\<^sup>= y x)" lemma glbI [Pure.intro]: "lb P B x \ (\y. lb P B y \ P\<^sup>=\<^sup>= y x) \ glb P B x" by (auto simp: glb_def) text \Antisymmetric relations have unique glbs.\ lemma glb_unique: "antisymp_on A P \ x \ A \ y \ A \ glb P B x \ glb P B y \ x = y" by (auto simp: glb_def antisymp_on_def) context pred_on begin lemma chain_glb: - assumes "transp_on (\) A" + assumes "transp_on A (\)" shows "chain C \ glb (\) C x \ x \ A \ y \ A \ y \ x \ chain ({y} \ C)" using assms [unfolded transp_on_def] unfolding chain_def glb_def lb_def by (cases "C = {}") blast+ subsection \Open Properties\ definition "open Q \ (\C. chain C \ C \ {} \ (\x\A. glb (\) C x \ Q x) \ (\y\C. Q y))" lemma openI [Pure.intro]: "(\C. chain C \ C \ {} \ \x\A. glb (\) C x \ Q x \ \y\C. Q y) \ open Q" by (auto simp: open_def) lemma open_glb: "\chain C; C \ {}; open Q; \x\C. \ Q x; x \ A; glb (\) C x\ \ \ Q x" by (auto simp: open_def) subsection \Downward Completeness\ text \ A relation \\\ is \emph{downward-complete} iff every non-empty \\\-chain has a greatest lower bound. \ definition "downward_complete \ (\C. chain C \ C \ {} \ (\x\A. glb (\) C x))" lemma downward_completeI [Pure.intro]: assumes "\C. chain C \ C \ {} \ \x\A. glb (\) C x" shows "downward_complete" using assms by (auto simp: downward_complete_def) end abbreviation "open_on P Q A \ pred_on.open A P Q" abbreviation "dc_on P A \ pred_on.downward_complete A P" lemmas open_on_def = pred_on.open_def and dc_on_def = pred_on.downward_complete_def lemma dc_onI [Pure.intro]: assumes "\C. chain_on P C A \ C \ {} \ \x\A. glb P C x" shows "dc_on P A" using assms by (auto simp: dc_on_def) lemma open_onI [Pure.intro]: "(\C. chain_on P C A \ C \ {} \ \x\A. glb P C x \ Q x \ \y\C. Q y) \ open_on P Q A" by (auto simp: open_on_def) lemma chain_on_reflclp: "chain_on P\<^sup>=\<^sup>= A C \ chain_on P A C" by (auto simp: pred_on.chain_def) lemma lb_reflclp: "lb P\<^sup>=\<^sup>= B x \ lb P B x" by (auto simp: lb_def) lemma glb_reflclp: "glb P\<^sup>=\<^sup>= B x \ glb P B x" by (auto simp: glb_def lb_reflclp) lemma dc_on_reflclp: "dc_on P\<^sup>=\<^sup>= A \ dc_on P A" by (auto simp: dc_on_def chain_on_reflclp glb_reflclp) subsection \The Open Induction Principle\ lemma open_induct_on [consumes 4, case_names less]: assumes qo: "qo_on P A" and "dc_on P A" and "open_on P Q A" and "x \ A" and ind: "\x. \x \ A; \y. \y \ A; strict P y x\ \ Q y\ \ Q x" shows "Q x" proof (rule ccontr) assume "\ Q x" let ?B = "{x\A. \ Q x}" have "?B \ A" by blast interpret B: pred_on ?B P . from B.Hausdorff obtain M where chain: "B.chain M" and max: "\C. B.chain C \ M \ C \ M = C" by (auto simp: B.maxchain_def) then have "M \ ?B" by (auto simp: B.chain_def) show False proof (cases "M = {}") assume "M = {}" moreover have "B.chain {x}" using \x \ A\ and \\ Q x\ by (simp add: B.chain_def) ultimately show False using max by blast next interpret A: pred_on A P . assume "M \ {}" have "A.chain M" using chain by (auto simp: A.chain_def B.chain_def) moreover with \dc_on P A\ and \M \ {}\ obtain m where "m \ A" and "glb P M m" by (auto simp: A.downward_complete_def) ultimately have "\ Q m" and "m \ ?B" using A.open_glb [OF _ \M \ {}\ \open_on P Q A\ _ _ \glb P M m\] and \M \ ?B\ by auto from ind [OF \m \ A\] and \\ Q m\ obtain y where "y \ A" and "strict P y m" and "\ Q y" by blast then have "P y m" and "y \ ?B" by simp+ - from transp_on_subset [OF \?B \ A\ qo_on_imp_transp_on [OF qo]] - have "transp_on P ?B" . + from transp_on_subset [OF qo_on_imp_transp_on [OF qo] \?B \ A\] + have "transp_on ?B P" . from B.chain_glb [OF this chain \glb P M m\ \m \ ?B\ \y \ ?B\ \P y m\] have "B.chain ({y} \ M)" . then show False using \glb P M m\ and \strict P y m\ by (cases "y \ M") (auto dest: max simp: glb_def lb_def) qed qed subsection \Open Induction on Universal Domains\ text \Open induction on quasi-orders (i.e., @{class preorder}).\ lemma (in preorder) dc_open_induct [consumes 2, case_names less]: assumes "dc_on (\) UNIV" and "open_on (\) Q UNIV" and "\x. (\y. y < x \ Q y) \ Q x" shows "Q x" proof - have "qo_on (\) UNIV" by (auto simp: qo_on_def transp_on_def reflp_on_def dest: order_trans) from open_induct_on [OF this assms(1,2)] show "Q x" using assms(3) unfolding less_le_not_le by blast qed subsection \Type Class of Downward Complete Orders\ class dcorder = preorder + assumes dc_on_UNIV: "dc_on (\) UNIV" begin text \Open induction on downward-complete orders.\ lemmas open_induct [consumes 1, case_names less] = dc_open_induct [OF dc_on_UNIV] end end diff --git a/thys/Open_Induction/Restricted_Predicates.thy b/thys/Open_Induction/Restricted_Predicates.thy --- a/thys/Open_Induction/Restricted_Predicates.thy +++ b/thys/Open_Induction/Restricted_Predicates.thy @@ -1,634 +1,611 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Binary Predicates Restricted to Elements of a Given Set\ theory Restricted_Predicates imports Main begin text \ A subset \C\ of \A\ is a \emph{chain} on \A\ (w.r.t.\ \P\) iff for all pairs of elements of \C\, one is less than or equal to the other one. \ abbreviation "chain_on P C A \ pred_on.chain A P C" lemmas chain_on_def = pred_on.chain_def lemma chain_on_subset: "A \ B \ chain_on P C A \ chain_on P C B" by (force simp: chain_on_def) lemma chain_on_imp_subset: "chain_on P C A \ C \ A" by (simp add: chain_on_def) lemma subchain_on: assumes "C \ D" and "chain_on P D A" shows "chain_on P C A" using assms by (auto simp: chain_on_def) definition restrict_to :: "('a \ 'a \ bool) \ 'a set \ ('a \ 'a \ bool)" where "restrict_to P A = (\x y. x \ A \ y \ A \ P x y)" -definition transp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "transp_on P A \ (\x\A. \y\A. \z\A. P x y \ P y z \ P x z)" - abbreviation "strict P \ \x y. P x y \ \ (P y x)" abbreviation "incomparable P \ \x y. \ P x y \ \ P y x" abbreviation "antichain_on P f A \ \(i::nat) j. f i \ A \ (i < j \ incomparable P (f i) (f j))" lemma strict_reflclp_conv [simp]: "strict (P\<^sup>=\<^sup>=) = strict P" by auto -lemma transp_onI [Pure.intro]: - "(\x y z. \x \ A; y \ A; z \ A; P x y; P y z\ \ P x z) \ transp_on P A" - unfolding transp_on_def by blast - lemma reflp_on_reflclp_simp [simp]: assumes "reflp_on A P" and "a \ A" and "b \ A" shows "P\<^sup>=\<^sup>= a b = P a b" using assms by (auto simp: reflp_on_def) lemmas reflp_on_converse_simp = reflp_on_conversp - -lemma transp_on_converse: - "transp_on P A \ transp_on P\\ A" - unfolding transp_on_def by blast - -lemma transp_on_converse_simp [simp]: - "transp_on P\\ A \ transp_on P A" - unfolding transp_on_def by blast - -lemma transp_on_reflclp: - "transp_on P A \ transp_on P\<^sup>=\<^sup>= A" - unfolding transp_on_def by blast +lemmas irreflp_on_converse_simp = irreflp_on_converse +lemmas transp_on_converse_simp = transp_on_conversep lemma transp_on_strict: - "transp_on P A \ transp_on (strict P) A" + "transp_on A P \ transp_on A (strict P)" unfolding transp_on_def by blast -lemma transp_on_subset: - "A \ B \ transp_on P B \ transp_on P A" - by (auto simp: transp_on_def) - definition wfp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "wfp_on P A \ \ (\f. \i. f i \ A \ P (f (Suc i)) (f i))" definition inductive_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "inductive_on P A \ (\Q. (\y\A. (\x\A. P x y \ Q x) \ Q y) \ (\x\A. Q x))" lemma inductive_onI [Pure.intro]: assumes "\Q x. \x \ A; (\y. \y \ A; \x. \x \ A; P x y\ \ Q x\ \ Q y)\ \ Q x" shows "inductive_on P A" using assms unfolding inductive_on_def by metis text \ If @{term P} is well-founded on @{term A} then every non-empty subset @{term Q} of @{term A} has a minimal element @{term z} w.r.t. @{term P}, i.e., all elements that are @{term P}-smaller than @{term z} are not in @{term Q}. \ lemma wfp_on_imp_minimal: assumes "wfp_on P A" shows "\Q x. x \ Q \ Q \ A \ (\z\Q. \y. P y z \ y \ Q)" proof (rule ccontr) assume "\ ?thesis" then obtain Q x where *: "x \ Q" "Q \ A" and "\z. \y. z \ Q \ P y z \ y \ Q" by metis from choice [OF this(3)] obtain f where **: "\x\Q. P (f x) x \ f x \ Q" by blast let ?S = "\i. (f ^^ i) x" have ***: "\i. ?S i \ Q" proof fix i show "?S i \ Q" by (induct i) (auto simp: * **) qed then have "\i. ?S i \ A" using * by blast moreover have "\i. P (?S (Suc i)) (?S i)" proof fix i show "P (?S (Suc i)) (?S i)" by (induct i) (auto simp: * ** ***) qed ultimately have "\i. ?S i \ A \ P (?S (Suc i)) (?S i)" by blast with assms(1) show False unfolding wfp_on_def by fast qed lemma minimal_imp_inductive_on: assumes "\Q x. x \ Q \ Q \ A \ (\z\Q. \y. P y z \ y \ Q)" shows "inductive_on P A" proof (rule ccontr) assume "\ ?thesis" then obtain Q x where *: "\y\A. (\x\A. P x y \ Q x) \ Q y" and **: "x \ A" "\ Q x" by (auto simp: inductive_on_def) let ?Q = "{x\A. \ Q x}" from ** have "x \ ?Q" by auto moreover have "?Q \ A" by auto ultimately obtain z where "z \ ?Q" and min: "\y. P y z \ y \ ?Q" using assms [THEN spec [of _ ?Q], THEN spec [of _ x]] by blast from \z \ ?Q\ have "z \ A" and "\ Q z" by auto with * obtain y where "y \ A" and "P y z" and "\ Q y" by auto then have "y \ ?Q" by auto with \P y z\ and min show False by auto qed lemmas wfp_on_imp_inductive_on = wfp_on_imp_minimal [THEN minimal_imp_inductive_on] lemma inductive_on_induct [consumes 2, case_names less, induct pred: inductive_on]: assumes "inductive_on P A" and "x \ A" and "\y. \ y \ A; \x. \ x \ A; P x y \ \ Q x \ \ Q y" shows "Q x" using assms unfolding inductive_on_def by metis lemma inductive_on_imp_wfp_on: assumes "inductive_on P A" shows "wfp_on P A" proof - let ?Q = "\x. \ (\f. f 0 = x \ (\i. f i \ A \ P (f (Suc i)) (f i)))" { fix x assume "x \ A" with assms have "?Q x" proof (induct rule: inductive_on_induct) fix y assume "y \ A" and IH: "\x. x \ A \ P x y \ ?Q x" show "?Q y" proof (rule ccontr) assume "\ ?Q y" then obtain f where *: "f 0 = y" "\i. f i \ A \ P (f (Suc i)) (f i)" by auto then have "P (f (Suc 0)) (f 0)" and "f (Suc 0) \ A" by auto with IH and * have "?Q (f (Suc 0))" by auto with * show False by auto qed qed } then show ?thesis unfolding wfp_on_def by blast qed definition qo_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "qo_on P A \ reflp_on A P \ transp_on P A" + "qo_on P A \ reflp_on A P \ transp_on A P" definition po_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "po_on P A \ (irreflp_on A P \ transp_on P A)" + "po_on P A \ (irreflp_on A P \ transp_on A P)" lemma po_onI [Pure.intro]: - "\irreflp_on A P; transp_on P A\ \ po_on P A" + "\irreflp_on A P; transp_on A P\ \ po_on P A" by (auto simp: po_on_def) -lemmas irreflp_on_converse_simp = irreflp_on_converse - lemma po_on_converse_simp [simp]: "po_on P\\ A \ po_on P A" by (simp add: po_on_def) lemma po_on_imp_qo_on: "po_on P A \ qo_on (P\<^sup>=\<^sup>=) A" unfolding po_on_def qo_on_def by (metis reflp_on_reflclp transp_on_reflclp) lemma po_on_imp_irreflp_on: "po_on P A \ irreflp_on A P" by (auto simp: po_on_def) lemma po_on_imp_transp_on: - "po_on P A \ transp_on P A" + "po_on P A \ transp_on A P" by (auto simp: po_on_def) lemma po_on_subset: assumes "A \ B" and "po_on P B" shows "po_on P A" using transp_on_subset and irreflp_on_subset and assms unfolding po_on_def by blast lemma transp_on_irreflp_on_imp_antisymp_on: - assumes "transp_on P A" and "irreflp_on A P" + assumes "transp_on A P" and "irreflp_on A P" shows "antisymp_on A (P\<^sup>=\<^sup>=)" proof (rule antisymp_onI) fix a b assume "a \ A" and "b \ A" and "P\<^sup>=\<^sup>= a b" and "P\<^sup>=\<^sup>= b a" show "a = b" proof (rule ccontr) assume "a \ b" with \P\<^sup>=\<^sup>= a b\ and \P\<^sup>=\<^sup>= b a\ have "P a b" and "P b a" by auto - with \transp_on P A\ and \a \ A\ and \b \ A\ have "P a a" unfolding transp_on_def by blast + with \transp_on A P\ and \a \ A\ and \b \ A\ have "P a a" unfolding transp_on_def by blast with \irreflp_on A P\ and \a \ A\ show False unfolding irreflp_on_def by blast qed qed lemma po_on_imp_antisymp_on: assumes "po_on P A" shows "antisymp_on A P" -using transp_on_irreflp_on_imp_antisymp_on [of P A] and assms by (auto simp: po_on_def) +using transp_on_irreflp_on_imp_antisymp_on [of A P] and assms by (auto simp: po_on_def) lemma strict_reflclp [simp]: assumes "x \ A" and "y \ A" - and "transp_on P A" and "irreflp_on A P" + and "transp_on A P" and "irreflp_on A P" shows "strict (P\<^sup>=\<^sup>=) x y = P x y" using assms unfolding transp_on_def irreflp_on_def by blast lemma qo_on_imp_reflp_on: "qo_on P A \ reflp_on A P" by (auto simp: qo_on_def) lemma qo_on_imp_transp_on: - "qo_on P A \ transp_on P A" + "qo_on P A \ transp_on A P" by (auto simp: qo_on_def) lemma qo_on_subset: "A \ B \ qo_on P B \ qo_on P A" unfolding qo_on_def using reflp_on_subset and transp_on_subset by blast text \ Quasi-orders are instances of the @{class preorder} class. \ lemma qo_on_UNIV_conv: "qo_on P UNIV \ class.preorder P (strict P)" (is "?lhs = ?rhs") proof assume "?lhs" then show "?rhs" unfolding qo_on_def class.preorder_def using qo_on_imp_reflp_on [of P UNIV] and qo_on_imp_transp_on [of P UNIV] by (auto simp: reflp_on_def) (unfold transp_on_def, blast) next assume "?rhs" then show "?lhs" unfolding class.preorder_def by (auto simp: qo_on_def reflp_on_def transp_on_def) qed lemma wfp_on_iff_inductive_on: "wfp_on P A \ inductive_on P A" by (blast intro: inductive_on_imp_wfp_on wfp_on_imp_inductive_on) lemma wfp_on_iff_minimal: "wfp_on P A \ (\Q x. x \ Q \ Q \ A \ (\z\Q. \y. P y z \ y \ Q))" using wfp_on_imp_minimal [of P A] and minimal_imp_inductive_on [of A P] and inductive_on_imp_wfp_on [of P A] by blast text \ Every non-empty well-founded set @{term A} has a minimal element, i.e., an element that is not greater than any other element. \ lemma wfp_on_imp_has_min_elt: assumes "wfp_on P A" and "A \ {}" shows "\x\A. \y\A. \ P y x" using assms unfolding wfp_on_iff_minimal by force lemma wfp_on_induct [consumes 2, case_names less, induct pred: wfp_on]: assumes "wfp_on P A" and "x \ A" and "\y. \ y \ A; \x. \ x \ A; P x y \ \ Q x \ \ Q y" shows "Q x" using assms and inductive_on_induct [of P A x] unfolding wfp_on_iff_inductive_on by blast lemma wfp_on_UNIV [simp]: "wfp_on P UNIV \ wfP P" unfolding wfp_on_iff_inductive_on inductive_on_def wfP_def wf_def by force subsection \Measures on Sets (Instead of Full Types)\ definition inv_image_betw :: "('b \ 'b \ bool) \ ('a \ 'b) \ 'a set \ 'b set \ ('a \ 'a \ bool)" where "inv_image_betw P f A B = (\x y. x \ A \ y \ A \ f x \ B \ f y \ B \ P (f x) (f y))" definition measure_on :: "('a \ nat) \ 'a set \ 'a \ 'a \ bool" where "measure_on f A = inv_image_betw (<) f A UNIV" lemma in_inv_image_betw [simp]: "inv_image_betw P f A B x y \ x \ A \ y \ A \ f x \ B \ f y \ B \ P (f x) (f y)" by (auto simp: inv_image_betw_def) lemma in_measure_on [simp, code_unfold]: "measure_on f A x y \ x \ A \ y \ A \ f x < f y" by (simp add: measure_on_def) lemma wfp_on_inv_image_betw [simp, intro!]: assumes "wfp_on P B" shows "wfp_on (inv_image_betw P f A B) A" (is "wfp_on ?P A") proof (rule ccontr) assume "\ ?thesis" then obtain g where "\i. g i \ A \ ?P (g (Suc i)) (g i)" by (auto simp: wfp_on_def) with assms show False by (auto simp: wfp_on_def) qed lemma wfp_less: "wfp_on (<) (UNIV :: nat set)" using wf_less by (auto simp: wfP_def) lemma wfp_on_measure_on [iff]: "wfp_on (measure_on f A) A" unfolding measure_on_def by (rule wfp_less [THEN wfp_on_inv_image_betw]) lemma wfp_on_mono: "A \ B \ (\x y. x \ A \ y \ A \ P x y \ Q x y) \ wfp_on Q B \ wfp_on P A" unfolding wfp_on_def by (metis subsetD) lemma wfp_on_subset: "A \ B \ wfp_on P B \ wfp_on P A" using wfp_on_mono by blast lemma restrict_to_iff [iff]: "restrict_to P A x y \ x \ A \ y \ A \ P x y" by (simp add: restrict_to_def) lemma wfp_on_restrict_to [simp]: "wfp_on (restrict_to P A) A = wfp_on P A" by (auto simp: wfp_on_def) lemma irreflp_on_strict [simp, intro]: "irreflp_on A (strict P)" by (auto simp: irreflp_on_def) lemma transp_on_map': - assumes "transp_on Q B" + assumes "transp_on B Q" and "g ` A \ B" and "h ` A \ B" and "\x. x \ A \ Q\<^sup>=\<^sup>= (h x) (g x)" - shows "transp_on (\x y. Q (g x) (h y)) A" + shows "transp_on A (\x y. Q (g x) (h y))" using assms unfolding transp_on_def by auto (metis imageI subsetD) lemma transp_on_map: - assumes "transp_on Q B" + assumes "transp_on B Q" and "h ` A \ B" - shows "transp_on (\x y. Q (h x) (h y)) A" - using transp_on_map' [of Q B h A h, simplified, OF assms] by blast + shows "transp_on A (\x y. Q (h x) (h y))" + using transp_on_map' [of B Q h A h, simplified, OF assms] by blast lemma irreflp_on_map: assumes "irreflp_on B Q" and "h ` A \ B" shows "irreflp_on A (\x y. Q (h x) (h y))" using assms unfolding irreflp_on_def by auto lemma po_on_map: assumes "po_on Q B" and "h ` A \ B" shows "po_on (\x y. Q (h x) (h y)) A" using assms and transp_on_map and irreflp_on_map unfolding po_on_def by auto lemma chain_transp_on_less: - assumes "\i. f i \ A \ P (f i) (f (Suc i))" and "transp_on P A" and "i < j" + assumes "\i. f i \ A \ P (f i) (f (Suc i))" and "transp_on A P" and "i < j" shows "P (f i) (f j)" using \i < j\ proof (induct j) case 0 then show ?case by simp next case (Suc j) show ?case proof (cases "i = j") case True with Suc show ?thesis using assms(1) by simp next case False with Suc have "P (f i) (f j)" by force moreover from assms have "P (f j) (f (Suc j))" by auto ultimately show ?thesis using assms(1, 2) unfolding transp_on_def by blast qed qed lemma wfp_on_imp_irreflp_on: assumes "wfp_on P A" shows "irreflp_on A P" proof (rule irreflp_onI) fix x assume "x \ A" show "\ P x x" proof let ?f = "\_. x" assume "P x x" then have "\i. P (?f (Suc i)) (?f i)" by blast with \x \ A\ have "\ wfp_on P A" by (auto simp: wfp_on_def) with assms show False by contradiction qed qed inductive accessible_on :: "('a \ 'a \ bool) \ 'a set \ 'a \ bool" for P and A where accessible_onI [Pure.intro]: "\x \ A; \y. \y \ A; P y x\ \ accessible_on P A y\ \ accessible_on P A x" lemma accessible_on_imp_mem: assumes "accessible_on P A a" shows "a \ A" using assms by (induct) auto lemma accessible_on_induct [consumes 1, induct pred: accessible_on]: assumes *: "accessible_on P A a" and IH: "\x. \accessible_on P A x; \y. \y \ A; P y x\ \ Q y\ \ Q x" shows "Q a" by (rule * [THEN accessible_on.induct]) (auto intro: IH accessible_onI) lemma accessible_on_downward: "accessible_on P A b \ a \ A \ P a b \ accessible_on P A a" by (cases rule: accessible_on.cases) fast lemma accessible_on_restrict_to_downwards: assumes "(restrict_to P A)\<^sup>+\<^sup>+ a b" and "accessible_on P A b" shows "accessible_on P A a" using assms by (induct) (auto dest: accessible_on_imp_mem accessible_on_downward) lemma accessible_on_imp_inductive_on: assumes "\x\A. accessible_on P A x" shows "inductive_on P A" proof fix Q x assume "x \ A" and *: "\y. \y \ A; \x. \x \ A; P x y\ \ Q x\ \ Q y" with assms have "accessible_on P A x" by auto then show "Q x" proof (induct) case (1 z) then have "z \ A" by (blast dest: accessible_on_imp_mem) show ?case by (rule *) fact+ qed qed lemmas accessible_on_imp_wfp_on = accessible_on_imp_inductive_on [THEN inductive_on_imp_wfp_on] lemma wfp_on_tranclp_imp_wfp_on: assumes "wfp_on (P\<^sup>+\<^sup>+) A" shows "wfp_on P A" by (rule ccontr) (insert assms, auto simp: wfp_on_def) lemma inductive_on_imp_accessible_on: assumes "inductive_on P A" shows "\x\A. accessible_on P A x" proof fix x assume "x \ A" with assms show "accessible_on P A x" by (induct) (auto intro: accessible_onI) qed lemma inductive_on_accessible_on_conv: "inductive_on P A \ (\x\A. accessible_on P A x)" using inductive_on_imp_accessible_on and accessible_on_imp_inductive_on by blast lemmas wfp_on_imp_accessible_on = wfp_on_imp_inductive_on [THEN inductive_on_imp_accessible_on] lemma wfp_on_accessible_on_iff: "wfp_on P A \ (\x\A. accessible_on P A x)" by (blast dest: wfp_on_imp_accessible_on accessible_on_imp_wfp_on) lemma accessible_on_tranclp: assumes "accessible_on P A x" shows "accessible_on ((restrict_to P A)\<^sup>+\<^sup>+) A x" (is "accessible_on ?P A x") using assms proof (induct) case (1 x) then have "x \ A" by (blast dest: accessible_on_imp_mem) then show ?case proof (rule accessible_onI) fix y assume "y \ A" assume "?P y x" then show "accessible_on ?P A y" proof (cases) assume "restrict_to P A y x" with 1 and \y \ A\ show ?thesis by blast next fix z assume "?P y z" and "restrict_to P A z x" with 1 have "accessible_on ?P A z" by (auto simp: restrict_to_def) from accessible_on_downward [OF this \y \ A\ \?P y z\] show ?thesis . qed qed qed lemma wfp_on_restrict_to_tranclp: assumes "wfp_on P A" shows "wfp_on ((restrict_to P A)\<^sup>+\<^sup>+) A" using wfp_on_imp_accessible_on [OF assms] and accessible_on_tranclp [of P A] and accessible_on_imp_wfp_on [of A "(restrict_to P A)\<^sup>+\<^sup>+"] by blast lemma wfp_on_restrict_to_tranclp': assumes "wfp_on (restrict_to P A)\<^sup>+\<^sup>+ A" shows "wfp_on P A" by (rule ccontr) (insert assms, auto simp: wfp_on_def) lemma wfp_on_restrict_to_tranclp_wfp_on_conv: "wfp_on (restrict_to P A)\<^sup>+\<^sup>+ A \ wfp_on P A" using wfp_on_restrict_to_tranclp [of P A] and wfp_on_restrict_to_tranclp' [of P A] by blast lemma tranclp_idemp [simp]: "(P\<^sup>+\<^sup>+)\<^sup>+\<^sup>+ = P\<^sup>+\<^sup>+" (is "?l = ?r") proof (intro ext) fix x y show "?l x y = ?r x y" proof assume "?l x y" then show "?r x y" by (induct) auto next assume "?r x y" then show "?l x y" by (induct) auto qed qed (*TODO: move the following 3 lemmas to Transitive_Closure?*) lemma stepfun_imp_tranclp: assumes "f 0 = x" and "f (Suc n) = z" and "\i\n. P (f i) (f (Suc i))" shows "P\<^sup>+\<^sup>+ x z" using assms by (induct n arbitrary: x z) (auto intro: tranclp.trancl_into_trancl) lemma tranclp_imp_stepfun: assumes "P\<^sup>+\<^sup>+ x z" shows "\f n. f 0 = x \ f (Suc n) = z \ (\i\n. P (f i) (f (Suc i)))" (is "\f n. ?P x z f n") using assms proof (induct rule: tranclp_induct) case (base y) let ?f = "(\_. y)(0 := x)" have "?f 0 = x" and "?f (Suc 0) = y" by auto moreover have "\i\0. P (?f i) (?f (Suc i))" using base by auto ultimately show ?case by blast next case (step y z) then obtain f n where IH: "?P x y f n" by blast then have *: "\i\n. P (f i) (f (Suc i))" and [simp]: "f 0 = x" "f (Suc n) = y" by auto let ?n = "Suc n" let ?f = "f(Suc ?n := z)" have "?f 0 = x" and "?f (Suc ?n) = z" by auto moreover have "\i\?n. P (?f i) (?f (Suc i))" using \P y z\ and * by auto ultimately show ?case by blast qed lemma tranclp_stepfun_conv: "P\<^sup>+\<^sup>+ x y \ (\f n. f 0 = x \ f (Suc n) = y \ (\i\n. P (f i) (f (Suc i))))" using tranclp_imp_stepfun and stepfun_imp_tranclp by metis subsection \Facts About Predecessor Sets\ lemma qo_on_predecessor_subset_conv': assumes "qo_on P A" and "B \ A" and "C \ A" shows "{x\A. \y\B. P x y} \ {x\A. \y\C. P x y} \ (\x\B. \y\C. P x y)" using assms by (auto simp: subset_eq qo_on_def reflp_on_def, unfold transp_on_def) metis+ lemma qo_on_predecessor_subset_conv: "\qo_on P A; x \ A; y \ A\ \ {z\A. P z x} \ {z\A. P z y} \ P x y" using qo_on_predecessor_subset_conv' [of P A "{x}" "{y}"] by simp lemma po_on_predecessors_eq_conv: assumes "po_on P A" and "x \ A" and "y \ A" shows "{z\A. P\<^sup>=\<^sup>= z x} = {z\A. P\<^sup>=\<^sup>= z y} \ x = y" using assms(2-) and reflp_on_reflclp [of A P] and po_on_imp_antisymp_on [OF \po_on P A\] unfolding antisymp_on_def reflp_on_def by blast lemma restrict_to_rtranclp: - assumes "transp_on P A" + assumes "transp_on A P" and "x \ A" and "y \ A" shows "(restrict_to P A)\<^sup>*\<^sup>* x y \ P\<^sup>=\<^sup>= x y" proof - { assume "(restrict_to P A)\<^sup>*\<^sup>* x y" then have "P\<^sup>=\<^sup>= x y" using assms by (induct) (auto, unfold transp_on_def, blast) } with assms show ?thesis by auto qed lemma reflp_on_restrict_to_rtranclp: - assumes "reflp_on A P" and "transp_on P A" + assumes "reflp_on A P" and "transp_on A P" and "x \ A" and "y \ A" shows "(restrict_to P A)\<^sup>*\<^sup>* x y \ P x y" unfolding restrict_to_rtranclp [OF assms(2-)] unfolding reflp_on_reflclp_simp [OF assms(1, 3-)] .. end diff --git a/thys/Saturation_Framework/Given_Clause_Architectures.thy b/thys/Saturation_Framework/Given_Clause_Architectures.thy --- a/thys/Saturation_Framework/Given_Clause_Architectures.thy +++ b/thys/Saturation_Framework/Given_Clause_Architectures.thy @@ -1,1177 +1,1179 @@ (* Title: Given Clause Prover Architectures * Author: Sophie Tourret , 2019-2020 *) section \Given Clause Prover Architectures\ text \This section covers all the results presented in the section 4 of the report. This is where abstract architectures of provers are defined and proven dynamically refutationally complete.\ theory Given_Clause_Architectures imports Lambda_Free_RPOs.Lambda_Free_Util Labeled_Lifting_to_Non_Ground_Calculi begin subsection \Basis of the Given Clause Prover Architectures\ locale given_clause_basis = std?: labeled_lifting_intersection Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q Red_F_q \_F_q \_I_q "{\\<^sub>F\<^sub>L :: ('f \ 'l) inference. Infer (map fst (prems_of \\<^sub>F\<^sub>L)) (fst (concl_of \\<^sub>F\<^sub>L)) \ Inf_F}" for Bot_F :: "'f set" and Inf_F :: "'f inference set" and Bot_G :: "'g set" and Q :: "'q set" and entails_q :: "'q \ 'g set \ 'g set \ bool" and Inf_G_q :: \'q \ 'g inference set\ and Red_I_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" and \_F_q :: "'q \ 'f \ 'g set" and \_I_q :: "'q \ 'f inference \ 'g inference set option" + fixes Equiv_F :: "'f \ 'f \ bool" (infix "\" 50) and Prec_F :: "'f \ 'f \ bool" (infix "\\" 50) and Prec_L :: "'l \ 'l \ bool" (infix "\L" 50) and active :: "'l" assumes equiv_equiv_F: "equivp (\)" and wf_prec_F: "minimal_element (\\) UNIV" and wf_prec_L: "minimal_element (\L) UNIV" and compat_equiv_prec: "C1 \ D1 \ C2 \ D2 \ C1 \\ C2 \ D1 \\ D2" and equiv_F_grounding: "q \ Q \ C1 \ C2 \ \_F_q q C1 \ \_F_q q C2" and prec_F_grounding: "q \ Q \ C2 \\ C1 \ \_F_q q C1 \ \_F_q q C2" and active_minimal: "l2 \ active \ active \L l2" and at_least_two_labels: "\l2. active \L l2" and static_ref_comp: "statically_complete_calculus Bot_F Inf_F (\\\) no_labels.Red_I_\ no_labels.Red_F_\_empty" begin abbreviation Inf_FL :: "('f \ 'l) inference set" where "Inf_FL \ {\\<^sub>F\<^sub>L. Infer (map fst (prems_of \\<^sub>F\<^sub>L)) (fst (concl_of \\<^sub>F\<^sub>L)) \ Inf_F}" abbreviation Prec_eq_F :: "'f \ 'f \ bool" (infix "\\" 50) where "C \\ D \ C \ D \ C \\ D" definition Prec_FL :: "('f \ 'l) \ ('f \ 'l) \ bool" (infix "\" 50) where "Cl1 \ Cl2 \ fst Cl1 \\ fst Cl2 \ (fst Cl1 \ fst Cl2 \ snd Cl1 \L snd Cl2)" lemma irrefl_prec_F: "\ C \\ C" by (simp add: minimal_element.po[OF wf_prec_F, unfolded po_on_def irreflp_on_def]) lemma trans_prec_F: "C1 \\ C2 \ C2 \\ C3 \ C1 \\ C3" by (auto intro: minimal_element.po[OF wf_prec_F, unfolded po_on_def transp_on_def, THEN conjunct2, simplified, rule_format]) lemma wf_prec_FL: "minimal_element (\) UNIV" proof show "po_on (\) UNIV" unfolding po_on_def proof - show "irreflp_on UNIV (\)" unfolding irreflp_on_def Prec_FL_def + show "irreflp (\)" unfolding irreflp_on_def Prec_FL_def proof fix Cl assume a_in: "Cl \ (UNIV::('f \ 'l) set)" have "\ (fst Cl \\ fst Cl)" using wf_prec_F minimal_element.min_elt_ex by force moreover have "\ (snd Cl \L snd Cl)" using wf_prec_L minimal_element.min_elt_ex by force ultimately show "\ (fst Cl \\ fst Cl \ fst Cl \ fst Cl \ snd Cl \L snd Cl)" by blast qed next - show "transp_on (\) UNIV" unfolding transp_on_def Prec_FL_def - proof (simp, intro allI impI) - fix C1 l1 C2 l2 C3 l3 - assume trans_hyp: "(C1 \\ C2 \ C1 \ C2 \ l1 \L l2) \ (C2 \\ C3 \ C2 \ C3 \ l2 \L l3)" - have "C1 \\ C2 \ C2 \ C3 \ C1 \\ C3" + show "transp (\)" unfolding Prec_FL_def + proof (rule transpI) + fix Cl1 Cl2 Cl3 + assume trans_hyps: + "(fst Cl1 \\ fst Cl2 \ fst Cl1 \ fst Cl2 \ snd Cl1 \L snd Cl2)" + "(fst Cl2 \\ fst Cl3 \ fst Cl2 \ fst Cl3 \ snd Cl2 \L snd Cl3)" + have "fst Cl1 \\ fst Cl2 \ fst Cl2 \ fst Cl3 \ fst Cl1 \\ fst Cl3" using compat_equiv_prec by (metis equiv_equiv_F equivp_def) - moreover have "C1 \ C2 \ C2 \\ C3 \ C1 \\ C3" + moreover have "fst Cl1 \ fst Cl2 \ fst Cl2 \\ fst Cl3 \ fst Cl1 \\ fst Cl3" using compat_equiv_prec by (metis equiv_equiv_F equivp_def) - moreover have "l1 \L l2 \ l2 \L l3 \ l1 \L l3" - using wf_prec_L unfolding minimal_element_def po_on_def transp_on_def by (meson UNIV_I) - moreover have "C1 \ C2 \ C2 \ C3 \ C1 \ C3" + moreover have "snd Cl1 \L snd Cl2 \ snd Cl2 \L snd Cl3 \ snd Cl1 \L snd Cl3" + using wf_prec_L unfolding minimal_element_def po_on_def transp_def by (meson UNIV_I) + moreover have "fst Cl1 \ fst Cl2 \ fst Cl2 \ fst Cl3 \ fst Cl1 \ fst Cl3" using equiv_equiv_F by (meson equivp_transp) - ultimately show "C1 \\ C3 \ C1 \ C3 \ l1 \L l3" using trans_hyp - using trans_prec_F by blast + ultimately show "fst Cl1 \\ fst Cl3 \ fst Cl1 \ fst Cl3 \ snd Cl1 \L snd Cl3" + using trans_hyps trans_prec_F by blast qed qed next show "wfp_on (\) UNIV" unfolding wfp_on_def proof assume contra: "\f. \i. f i \ UNIV \ f (Suc i) \ f i" then obtain f where f_suc: "\i. f (Suc i) \ f i" by blast define R :: "(('f \ 'l) \ ('f \ 'l)) set" where "R = {(Cl1, Cl2). fst Cl1 \\ fst Cl2}" define S :: "(('f \ 'l) \ ('f \ 'l)) set" where "S = {(Cl1, Cl2). fst Cl1 \ fst Cl2 \ snd Cl1 \L snd Cl2}" obtain k where f_chain: "\i. (f (Suc (i + k)), f (i + k)) \ S" proof (atomize_elim, rule wf_infinite_down_chain_compatible[of R f S]) show "wf R" unfolding R_def using wf_app[OF wf_prec_F[unfolded minimal_element_def, THEN conjunct2, unfolded wfp_on_UNIV wfP_def]] by force next show "\i. (f (Suc i), f i) \ R \ S" using f_suc unfolding R_def S_def Prec_FL_def by blast next show "R O S \ R" unfolding R_def S_def using compat_equiv_prec equiv_equiv_F equivp_reflp by fastforce qed define g where "\i. g i = f (i + k)" have g_chain: "\i. (g (Suc i), g i) \ S" unfolding g_def using f_chain by simp have wf_s: "wf S" unfolding S_def by (rule wf_subset[OF wf_app[OF wf_prec_L[unfolded minimal_element_def, THEN conjunct2, unfolded wfp_on_UNIV wfP_def], of snd]]) fast show False using g_chain[unfolded S_def] wf_s[unfolded S_def, folded wfP_def wfp_on_UNIV, unfolded wfp_on_def] by auto qed qed definition active_subset :: "('f \ 'l) set \ ('f \ 'l) set" where "active_subset M = {CL \ M. snd CL = active}" definition passive_subset :: "('f \ 'l) set \ ('f \ 'l) set" where "passive_subset M = {CL \ M. snd CL \ active}" lemma active_subset_insert[simp]: "active_subset (insert Cl N) = (if snd Cl = active then {Cl} else {}) \ active_subset N" unfolding active_subset_def by auto lemma active_subset_union[simp]: "active_subset (M \ N) = active_subset M \ active_subset N" unfolding active_subset_def by auto lemma passive_subset_insert[simp]: "passive_subset (insert Cl N) = (if snd Cl \ active then {Cl} else {}) \ passive_subset N" unfolding passive_subset_def by auto lemma passive_subset_union[simp]: "passive_subset (M \ N) = passive_subset M \ passive_subset N" unfolding passive_subset_def by auto sublocale std?: statically_complete_calculus Bot_FL Inf_FL "(\\\L)" Red_I Red_F using labeled_static_ref[OF static_ref_comp] . lemma labeled_tiebreaker_lifting: assumes q_in: "q \ Q" shows "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_I_L_q q) (\g. Prec_FL)" proof - have "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_I_L_q q) (\g Cl Cl'. False)" using ord_fam_lifted_q[OF q_in] . then have "standard_lifting Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q) Bot_FL (\_F_L_q q) (\_I_L_q q)" using lifted_q[OF q_in] by blast then show "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_I_L_q q) (\g. Prec_FL)" using wf_prec_FL by (simp add: tiebreaker_lifting.intro tiebreaker_lifting_axioms.intro) qed sublocale lifting_intersection Inf_FL Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q Bot_FL \_F_L_q \_I_L_q "\g. Prec_FL" using labeled_tiebreaker_lifting unfolding lifting_intersection_def by (simp add: lifting_intersection_axioms.intro no_labels.ground.consequence_relation_family_axioms no_labels.ground.inference_system_family_axioms) notation derive (infix "\L" 50) lemma std_Red_I_eq: "std.Red_I = Red_I_\" unfolding Red_I_\_q_def Red_I_\_L_q_def by simp lemma std_Red_F_eq: "std.Red_F = Red_F_\_empty" unfolding Red_F_\_empty_q_def Red_F_\_empty_L_q_def by simp sublocale statically_complete_calculus Bot_FL Inf_FL "(\\\L)" Red_I Red_F by unfold_locales (use statically_complete std_Red_I_eq in auto) (* lem:redundant-labeled-inferences *) lemma labeled_red_inf_eq_red_inf: assumes i_in: "\ \ Inf_FL" shows "\ \ Red_I N \ to_F \ \ no_labels.Red_I_\ (fst ` N)" proof assume i_in2: "\ \ Red_I N" then have "X \ Red_I_\_q ` Q \ \ \ X N" for X unfolding Red_I_def by blast obtain X0 where "X0 \ Red_I_\_q ` Q" using Q_nonempty by blast then obtain q0 where x0_is: "X0 N = Red_I_\_q q0 N" by blast then obtain Y0 where y0_is: "Y0 (fst ` N) = to_F ` (X0 N)" by auto have "Y0 (fst ` N) = no_labels.Red_I_\_q q0 (fst ` N)" unfolding y0_is proof show "to_F ` X0 N \ no_labels.Red_I_\_q q0 (fst ` N)" proof fix \0 assume i0_in: "\0 \ to_F ` X0 N" then have i0_in2: "\0 \ to_F ` Red_I_\_q q0 N" using x0_is by argo then obtain \0_FL where i0_FL_in: "\0_FL \ Inf_FL" and i0_to_i0_FL: "\0 = to_F \0_FL" and subs1: "((\_I_L_q q0 \0_FL) \ None \ the (\_I_L_q q0 \0_FL) \ Red_I_q q0 (\_Fset_q q0 N)) \ ((\_I_L_q q0 \0_FL = None) \ \_F_L_q q0 (concl_of \0_FL) \ \_Fset_q q0 N \ Red_F_q q0 (\_Fset_q q0 N))" unfolding Red_I_\_q_def by blast have concl_swap: "fst (concl_of \0_FL) = concl_of \0" unfolding concl_of_def i0_to_i0_FL to_F_def by simp have i0_in3: "\0 \ Inf_F" using i0_to_i0_FL Inf_FL_to_Inf_F[OF i0_FL_in] unfolding to_F_def by blast { assume not_none: "\_I_q q0 \0 \ None" and "the (\_I_q q0 \0) \ {}" then obtain \1 where i1_in: "\1 \ the (\_I_q q0 \0)" by blast have "the (\_I_q q0 \0) \ Red_I_q q0 (no_labels.\_Fset_q q0 (fst ` N))" using subs1 i0_to_i0_FL not_none by auto } moreover { assume is_none: "\_I_q q0 \0 = None" then have "\_F_q q0 (concl_of \0) \ no_labels.\_Fset_q q0 (fst ` N) \ Red_F_q q0 (no_labels.\_Fset_q q0 (fst ` N))" using subs1 i0_to_i0_FL concl_swap by simp } ultimately show "\0 \ no_labels.Red_I_\_q q0 (fst ` N)" unfolding no_labels.Red_I_\_q_def using i0_in3 by auto qed next show "no_labels.Red_I_\_q q0 (fst ` N) \ to_F ` X0 N" proof fix \0 assume i0_in: "\0 \ no_labels.Red_I_\_q q0 (fst ` N)" then have i0_in2: "\0 \ Inf_F" unfolding no_labels.Red_I_\_q_def by blast obtain \0_FL where i0_FL_in: "\0_FL \ Inf_FL" and i0_to_i0_FL: "\0 = to_F \0_FL" using Inf_F_to_Inf_FL[OF i0_in2] unfolding to_F_def by (smt (verit) Ex_list_of_length fst_conv inference.exhaust_sel inference.sel(1) inference.sel(2) map_fst_zip) have concl_swap: "fst (concl_of \0_FL) = concl_of \0" unfolding concl_of_def i0_to_i0_FL to_F_def by simp have subs1: "((\_I_L_q q0 \0_FL) \ None \ the (\_I_L_q q0 \0_FL) \ Red_I_q q0 (\_Fset_q q0 N)) \ ((\_I_L_q q0 \0_FL = None) \ \_F_L_q q0 (concl_of \0_FL) \ (\_Fset_q q0 N \ Red_F_q q0 (\_Fset_q q0 N)))" using i0_in i0_to_i0_FL concl_swap unfolding no_labels.Red_I_\_q_def by simp then have "\0_FL \ Red_I_\_q q0 N" using i0_FL_in unfolding Red_I_\_q_def by simp then show "\0 \ to_F ` X0 N" using x0_is i0_to_i0_FL i0_in2 by blast qed qed then have "Y \ no_labels.Red_I_\_q ` Q \ to_F \ \ Y (fst ` N)" for Y using i_in2 no_labels.Red_I_def std_Red_I_eq red_inf_impl by force then show "to_F \ \ no_labels.Red_I_\ (fst ` N)" unfolding Red_I_def no_labels.Red_I_\_def by blast next assume to_F_in: "to_F \ \ no_labels.Red_I_\ (fst ` N)" have imp_to_F: "X \ no_labels.Red_I_\_q ` Q \ to_F \ \ X (fst ` N)" for X using to_F_in unfolding no_labels.Red_I_\_def by blast then have to_F_in2: "to_F \ \ no_labels.Red_I_\_q q (fst ` N)" if "q \ Q" for q using that by auto have "Red_I_\_q q N = {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q (fst ` N)}" for q proof show "Red_I_\_q q N \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q (fst ` N)}" proof fix q0 \1 assume i1_in: "\1 \ Red_I_\_q q0 N" have i1_in2: "\1 \ Inf_FL" using i1_in unfolding Red_I_\_q_def by blast then have to_F_i1_in: "to_F \1 \ Inf_F" using Inf_FL_to_Inf_F unfolding to_F_def by blast have concl_swap: "fst (concl_of \1) = concl_of (to_F \1)" unfolding concl_of_def to_F_def by simp then have i1_to_F_in: "to_F \1 \ no_labels.Red_I_\_q q0 (fst ` N)" using i1_in to_F_i1_in unfolding Red_I_\_q_def no_labels.Red_I_\_q_def by force show "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q0 (fst ` N)}" using i1_in2 i1_to_F_in by blast qed next show "{\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q (fst ` N)} \ Red_I_\_q q N" proof fix q0 \1 assume i1_in: "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q0 (fst ` N)}" then have i1_in2: "\1 \ Inf_FL" by blast then have to_F_i1_in: "to_F \1 \ Inf_F" using Inf_FL_to_Inf_F unfolding to_F_def by blast have concl_swap: "fst (concl_of \1) = concl_of (to_F \1)" unfolding concl_of_def to_F_def by simp then have "((\_I_L_q q0 \1) \ None \ the (\_I_L_q q0 \1) \ Red_I_q q0 (\_Fset_q q0 N)) \ (\_I_L_q q0 \1 = None \ \_F_L_q q0 (concl_of \1) \ \_Fset_q q0 N \ Red_F_q q0 (\_Fset_q q0 N))" using i1_in unfolding no_labels.Red_I_\_q_def by auto then show "\1 \ Red_I_\_q q0 N" using i1_in2 unfolding Red_I_\_q_def by blast qed qed then have "\ \ Red_I_\_q q N" if "q \ Q" for q using that to_F_in2 i_in unfolding Red_I_\_q_def no_labels.Red_I_\_q_def by auto then show "\ \ Red_I_\ N" unfolding Red_I_\_def by blast qed (* lem:redundant-labeled-formulas *) lemma red_labeled_clauses: assumes \C \ no_labels.Red_F_\_empty (fst ` N) \ (\C' \ fst ` N. C' \\ C) \ (\(C', L') \ N. L' \L L \ C' \\ C)\ shows \(C, L) \ Red_F N\ proof - note assms moreover have i: \C \ no_labels.Red_F_\_empty (fst ` N) \ (C, L) \ Red_F N\ proof - assume "C \ no_labels.Red_F_\_empty (fst ` N)" then have "C \ no_labels.Red_F_\_empty_q q (fst ` N)" if "q \ Q" for q unfolding no_labels.Red_F_\_empty_def using that by fast then have g_in_red: "\_F_q q C \ Red_F_q q (no_labels.\_Fset_q q (fst ` N))" if "q \ Q" for q unfolding no_labels.Red_F_\_empty_q_def using that by blast have "\_F_L_q q (C, L) \ Red_F_q q (\_Fset_q q N)" if "q \ Q" for q using that g_in_red by simp then show ?thesis unfolding Red_F_def Red_F_\_q_def by blast qed moreover have ii: \\C' \ fst ` N. C' \\ C \ (C, L) \ Red_F N\ proof - assume "\C' \ fst ` N. C' \\ C" then obtain C' where c'_in: "C' \ fst ` N" and c_prec_c': "C' \\ C" by blast obtain L' where c'_l'_in: "(C', L') \ N" using c'_in by auto have c'_l'_prec: "(C', L') \ (C, L)" using c_prec_c' unfolding Prec_FL_def by simp have c_in_c'_g: "\_F_q q C \ \_F_q q C'" if "q \ Q" for q using prec_F_grounding[OF that c_prec_c'] by presburger then have "\_F_L_q q (C, L) \ \_F_L_q q (C', L')" if "q \ Q" for q using that by auto then have "(C, L) \ Red_F_\_q q N" if "q \ Q" for q unfolding Red_F_\_q_def using that c'_l'_in c'_l'_prec by blast then show ?thesis unfolding Red_F_def by blast qed moreover have iii: \\(C', L') \ N. L' \L L \ C' \\ C \ (C, L) \ Red_F N\ proof - assume "\(C', L') \ N. L' \L L \ C' \\ C" then obtain C' L' where c'_l'_in: "(C', L') \ N" and l'_sub_l: "L' \L L" and c'_sub_c: "C' \\ C" by fast have "(C, L) \ Red_F N" if "C' \\ C" using that c'_l'_in ii by fastforce moreover { assume equiv_c_c': "C \ C'" then have equiv_c'_c: "C' \ C" using equiv_equiv_F by (simp add: equivp_symp) then have c'_l'_prec: "(C', L') \ (C, L)" using l'_sub_l unfolding Prec_FL_def by simp have "\_F_q q C = \_F_q q C'" if "q \ Q" for q using that equiv_F_grounding equiv_c_c' equiv_c'_c by (simp add: set_eq_subset) then have "\_F_L_q q (C, L) = \_F_L_q q (C', L')" if "q \ Q" for q using that by auto then have "(C, L) \ Red_F_\_q q N" if "q \ Q" for q unfolding Red_F_\_q_def using that c'_l'_in c'_l'_prec by blast then have ?thesis unfolding Red_F_def by blast } ultimately show ?thesis using c'_sub_c equiv_equiv_F equivp_symp by fastforce qed ultimately show ?thesis by blast qed end subsection \Given Clause Procedure\ locale given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q Red_F_q \_F_q \_I_q Equiv_F Prec_F Prec_L active for Bot_F :: "'f set" and Inf_F :: "'f inference set" and Bot_G :: "'g set" and Q :: "'q set" and entails_q :: "'q \ 'g set \ 'g set \ bool" and Inf_G_q :: \'q \ 'g inference set\ and Red_I_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" and \_F_q :: "'q \ 'f \ 'g set" and \_I_q :: "'q \ 'f inference \ 'g inference set option" and Equiv_F :: "'f \ 'f \ bool" (infix "\" 50) and Prec_F :: "'f \ 'f \ bool" (infix "\\" 50) and Prec_L :: "'l \ 'l \ bool" (infix "\L" 50) and active :: 'l + assumes inf_have_prems: "\F \ Inf_F \ prems_of \F \ []" begin lemma labeled_inf_have_prems: "\ \ Inf_FL \ prems_of \ \ []" using inf_have_prems by fastforce inductive step :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\GC" 50) where process: "N1 = N \ M \ N2 = N \ M' \ M \ Red_F (N \ M') \ active_subset M' = {} \ N1 \GC N2" | infer: "N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Inf_between (fst ` active_subset N) {C} \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)) \ N1 \GC N2" lemma one_step_equiv: "N1 \GC N2 \ N1 \L N2" proof (cases N1 N2 rule: step.cases) show "N1 \GC N2 \ N1 \GC N2" by blast next fix N M M' assume gc_step: "N1 \GC N2" and n1_is: "N1 = N \ M" and n2_is: "N2 = N \ M'" and m_red: "M \ Red_F (N \ M')" and active_empty: "active_subset M' = {}" have "N1 - N2 \ Red_F N2" using n1_is n2_is m_red by auto then show "N1 \L N2" unfolding derive.simps by blast next fix N C L M assume gc_step: "N1 \GC N2" and n1_is: "N1 = N \ {(C, L)}" and not_active: "L \ active" and n2_is: "N2 = N \ {(C, active)} \ M" and active_empty: "active_subset M = {}" have "(C, active) \ N2" using n2_is by auto moreover have "C \\ C" using equiv_equiv_F by (metis equivp_def) moreover have "active \L L" using active_minimal[OF not_active] . ultimately have "{(C, L)} \ Red_F N2" using red_labeled_clauses by blast moreover have "N1 - N2 = {} \ N1 - N2 = {(C, L)}" using n1_is n2_is by blast ultimately have "N1 - N2 \ Red_F N2" using std_Red_F_eq by blast then show "N1 \L N2" unfolding derive.simps by blast qed (* lem:gc-derivations-are-red-derivations *) lemma gc_to_red: "chain (\GC) Ns \ chain (\L) Ns" using one_step_equiv Lazy_List_Chain.chain_mono by blast lemma (in-) all_ex_finite_set: "(\(j::nat)\{0..(n::nat). P j n) \ (\n1 n2. \j\{0.. P j n2 \ n1 = n2) \ finite {n. \j \ {0.. nat \ bool" assume allj_exn: "\j\{0..n. P j n" and uniq_n: "\n1 n2. \j\{0.. P j n2 \ n1 = n2" have "{n. \j \ {0..((\j. {n. P j n}) ` {0..j\{0.. finite {n. \j \ {0..j. {n. P j n}"] by simp have "\j\{0..!n. P j n" using allj_exn uniq_n by blast then have "\j\{0..j \ {0..GC) Ns" and init_state: "active_subset (lhd Ns) = {}" and final_state: "passive_subset (Liminf_llist Ns) = {}" shows "fair Ns" unfolding fair_def proof fix \ assume i_in: "\ \ Inf_from (Liminf_llist Ns)" note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have i_in_inf_fl: "\ \ Inf_FL" using i_in unfolding Inf_from_def by blast have "Liminf_llist Ns = active_subset (Liminf_llist Ns)" using final_state unfolding passive_subset_def active_subset_def by blast then have i_in2: "\ \ Inf_from (active_subset (Liminf_llist Ns))" using i_in by simp define m where "m = length (prems_of \)" then have m_def_F: "m = length (prems_of (to_F \))" unfolding to_F_def by simp have i_in_F: "to_F \ \ Inf_F" using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast then have m_pos: "m > 0" using m_def_F using inf_have_prems by blast have exist_nj: "\j \ {0..nj. enat (Suc nj) < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns nj) \ (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k)))" proof clarify fix j assume j_in: "j \ {0.. ! j" using i_in2 unfolding m_def Inf_from_def active_subset_def by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv) then have "(C, active) \ Liminf_llist Ns" using j_in i_in unfolding m_def Inf_from_def by force then obtain nj where nj_is: "enat nj < llength Ns" and c_in2: "(C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns})" unfolding Liminf_llist_def using init_state by blast then have c_in3: "\k. k \ nj \ enat k < llength Ns \ (C, active) \ lnth Ns k" by blast have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def lhd_is by force obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns \ (C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))" by blast then have in_allk: "\k. k \ nj_min \ enat k < llength Ns \ (C, active) \ (lnth Ns k)" using c_in3 nj_is c_in2 by (metis (mono_tags, lifting) INT_E LeastI_ex mem_Collect_eq) have njm_smaller_D: "enat nj_min < llength Ns" using nj_min_is by (smt LeastI_ex \\thesis. (\nj. \enat nj < llength Ns; (C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns})\ \ thesis) \ thesis\) have "nj_min > 0" using nj_is c_in2 nj_pos nj_min_is lhd_is by (metis (mono_tags, lifting) Collect_empty_eq \(C, active) \ Liminf_llist Ns\ \Liminf_llist Ns = active_subset (Liminf_llist Ns)\ \\k\nj_min. enat k < llength Ns \ (C, active) \ lnth Ns k\ active_subset_def init_state linorder_not_less mem_Collect_eq zero_enat_def chain_length_pos[OF deriv]) then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto then have njm_prec_njm: "njm_prec < nj_min" by blast then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp have njm_prec_smaller_d: "njm_prec < llength Ns" by (rule less_trans[OF njm_prec_njm_enat njm_smaller_D]) have njm_prec_all_suc: "\k>njm_prec. enat k < llength Ns \ (C, active) \ lnth Ns k" using nj_prec_is in_allk by simp have notin_njm_prec: "(C, active) \ lnth Ns njm_prec" proof (rule ccontr) assume "\ (C, active) \ lnth Ns njm_prec" then have absurd_hyp: "(C, active) \ lnth Ns njm_prec" by simp have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is by (smt LeastI_ex Suc_leD \\thesis. (\nj. \enat nj < llength Ns; (C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns})\ \ thesis) \ thesis\ enat_ord_simps(1) le_eq_less_or_eq le_less_trans) have "(C, active) \ \ (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns})" proof - { fix k assume k_in: "njm_prec \ k \ enat k < llength Ns" have "k = njm_prec \ (C, active) \ lnth Ns k" using absurd_hyp by simp moreover have "njm_prec < k \ (C, active) \ lnth Ns k" using nj_prec_is in_allk k_in by simp ultimately have "(C, active) \ lnth Ns k" using k_in by fastforce } then show "(C, active) \ \ (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns})" by blast qed then have "enat njm_prec < llength Ns \ (C, active) \ \ (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns})" using prec_smaller by blast then show False using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast qed then have notin_active_subs_njm_prec: "(C, active) \ active_subset (lnth Ns njm_prec)" unfolding active_subset_def by blast then show "\nj. enat (Suc nj) < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns nj) \ (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k))" using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting) active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv) qed define nj_set where "nj_set = {nj. (\j\{0.. prems_of \ ! j \ active_subset (lnth Ns nj) \ (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k)))}" then have nj_not_empty: "nj_set \ {}" proof - have zero_in: "0 \ {0.. ! 0 \ active_subset (lnth Ns n0)" and "\k>n0. enat k < llength Ns \ prems_of \ ! 0 \ active_subset (lnth Ns k)" using exist_nj by fast then have "n0 \ nj_set" unfolding nj_set_def using zero_in by blast then show "nj_set \ {}" by auto qed have nj_finite: "finite nj_set" using all_ex_finite_set[OF exist_nj] by (metis (no_types, lifting) Suc_ile_eq dual_order.strict_implies_order linorder_neqE_nat nj_set_def) (* the n below in the n-1 from the pen-and-paper proof *) have "\n \ nj_set. \nj \ nj_set. nj \ n" using nj_not_empty nj_finite using Max_ge Max_in by blast then obtain n where n_in: "n \ nj_set" and n_bigger: "\nj \ nj_set. nj \ n" by blast then obtain j0 where j0_in: "j0 \ {0.. ! j0 \ active_subset (lnth Ns n)" and j0_allin: "(\k. k > n \ enat k < llength Ns \ prems_of \ ! j0 \ active_subset (lnth Ns k))" unfolding nj_set_def by blast obtain C0 where C0_is: "prems_of \ ! j0 = (C0, active)" using j0_in using i_in2 unfolding m_def Inf_from_def active_subset_def by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv) then have C0_prems_i: "(C0, active) \ set (prems_of \)" using in_set_conv_nth j0_in m_def by force have C0_in: "(C0, active) \ (lnth Ns (Suc n))" using C0_is j0_allin suc_n_length by (simp add: active_subset_def) have C0_notin: "(C0, active) \ (lnth Ns n)" using C0_is j0_notin unfolding active_subset_def by simp have step_n: "lnth Ns n \GC lnth Ns (Suc n)" using deriv chain_lnth_rel n_in unfolding nj_set_def by blast have "\N C L M. (lnth Ns n = N \ {(C, L)} \ lnth Ns (Suc n) = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Inf_between (fst ` active_subset N) {C} \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)))" proof - have proc_or_infer: "(\N1 N M N2 M'. lnth Ns n = N1 \ lnth Ns (Suc n) = N2 \ N1 = N \ M \ N2 = N \ M' \ M \ Red_F (N \ M') \ active_subset M' = {}) \ (\N1 N C L N2 M. lnth Ns n = N1 \ lnth Ns (Suc n) = N2 \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Inf_between (fst ` active_subset N) {C} \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)))" using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n by blast show ?thesis using C0_in C0_notin proc_or_infer j0_in C0_is by (smt Un_iff active_subset_def mem_Collect_eq snd_conv sup_bot.right_neutral) qed then obtain N M L where inf_from_subs: "no_labels.Inf_between (fst ` active_subset N) {C0} \ no_labels.Red_I (fst ` (N \ {(C0, active)} \ M))" and nth_d_is: "lnth Ns n = N \ {(C0, L)}" and suc_nth_d_is: "lnth Ns (Suc n) = N \ {(C0, active)} \ M" and l_not_active: "L \ active" using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce have "j \ {0.. prems_of \ ! j \ prems_of \ ! j0 \ prems_of \ ! j \ (active_subset N)" for j proof - fix j assume j_in: "j \ {0.. ! j \ prems_of \ ! j0" obtain nj where nj_len: "enat (Suc nj) < llength Ns" and nj_prems: "prems_of \ ! j \ active_subset (lnth Ns nj)" and nj_greater: "(\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k))" using exist_nj j_in by blast then have "nj \ nj_set" unfolding nj_set_def using j_in by blast moreover have "nj \ n" proof (rule ccontr) assume "\ nj \ n" then have "prems_of \ ! j = (C0, active)" using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n by (smt Un_iff nth_d_is suc_nth_d_is l_not_active active_subset_def insertCI insertE lessI mem_Collect_eq nj_greater nj_prems snd_conv suc_n_length) then show False using j_not_j0 C0_is by simp qed ultimately have "nj < n" using n_bigger by force then have "prems_of \ ! j \ (active_subset (lnth Ns n))" using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order unfolding nj_set_def by blast then show "prems_of \ ! j \ (active_subset N)" using nth_d_is l_not_active unfolding active_subset_def by force qed then have "set (prems_of \) \ active_subset N \ {(C0, active)}" using C0_prems_i C0_is m_def by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI) moreover have "\ (set (prems_of \) \ active_subset N - {(C0, active)})" using C0_prems_i by blast ultimately have "\ \ Inf_between (active_subset N) {(C0, active)}" using i_in_inf_fl unfolding Inf_between_def Inf_from_def by blast then have "to_F \ \ no_labels.Inf_between (fst ` active_subset N) {C0}" unfolding to_F_def Inf_between_def Inf_from_def no_labels.Inf_between_def no_labels.Inf_from_def using Inf_FL_to_Inf_F by force then have "to_F \ \ no_labels.Red_I (fst ` (lnth Ns (Suc n)))" using suc_nth_d_is inf_from_subs by fastforce then have "\q \ Q. (\_I_q q (to_F \) \ None \ the (\_I_q q (to_F \)) \ Red_I_q q (\ (\_F_q q ` fst ` lnth Ns (Suc n)))) \ (\_I_q q (to_F \) = None \ \_F_q q (concl_of (to_F \)) \ \ (\_F_q q ` fst ` lnth Ns (Suc n)) \ Red_F_q q (\ (\_F_q q ` fst ` lnth Ns (Suc n))))" unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\_q_def by blast then have "\ \ Red_I_\ (lnth Ns (Suc n))" using i_in_inf_fl unfolding Red_I_\_def Red_I_\_q_def by (simp add: to_F_def) then show "\ \ Sup_llist (lmap Red_I_\ Ns)" unfolding Sup_llist_def using suc_n_length by auto qed theorem gc_complete_Liminf: assumes deriv: "chain (\GC) Ns" and init_state: "active_subset (lhd Ns) = {}" and final_state: "passive_subset (Liminf_llist Ns) = {}" and b_in: "B \ Bot_F" and bot_entailed: "no_labels.entails_\ (fst ` lhd Ns) {B}" shows "\BL \ Bot_FL. BL \ Liminf_llist Ns" proof - note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have labeled_b_in: "(B, active) \ Bot_FL" using b_in by simp have labeled_bot_entailed: "entails_\_L (lhd Ns) {(B, active)}" using labeled_entailment_lifting bot_entailed lhd_is by fastforce have fair: "fair Ns" using gc_fair[OF deriv init_state final_state] . then show ?thesis using dynamically_complete_Liminf[OF labeled_b_in gc_to_red[OF deriv] fair labeled_bot_entailed] by blast qed (* thm:gc-completeness *) theorem gc_complete: assumes deriv: "chain (\GC) Ns" and init_state: "active_subset (lhd Ns) = {}" and final_state: "passive_subset (Liminf_llist Ns) = {}" and b_in: "B \ Bot_F" and bot_entailed: "no_labels.entails_\ (fst ` lhd Ns) {B}" shows "\i. enat i < llength Ns \ (\BL \ Bot_FL. BL \ lnth Ns i)" proof - note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have "\BL\Bot_FL. BL \ Liminf_llist Ns" using assms by (rule gc_complete_Liminf) then show ?thesis unfolding Liminf_llist_def by auto qed end subsection \Lazy Given Clause Procedure\ locale lazy_given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q Red_F_q \_F_q \_I_q Equiv_F Prec_F Prec_L active for Bot_F :: "'f set" and Inf_F :: "'f inference set" and Bot_G :: "'g set" and Q :: "'q set" and entails_q :: "'q \ 'g set \ 'g set \ bool" and Inf_G_q :: \'q \ 'g inference set\ and Red_I_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" and \_F_q :: "'q \ 'f \ 'g set" and \_I_q :: "'q \ 'f inference \ 'g inference set option" and Equiv_F :: "'f \ 'f \ bool" (infix "\" 50) and Prec_F :: "'f \ 'f \ bool" (infix "\\" 50) and Prec_L :: "'l \ 'l \ bool" (infix "\L" 50) and active :: 'l begin inductive step :: "'f inference set \ ('f \ 'l) set \ 'f inference set \ ('f \ 'l) set \ bool" (infix "\LGC" 50) where process: "N1 = N \ M \ N2 = N \ M' \ M \ Red_F (N \ M') \ active_subset M' = {} \ (T, N1) \LGC (T, N2)" | schedule_infer: "T2 = T1 \ T' \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ L \ active \ T' = no_labels.Inf_between (fst ` active_subset N) {C} \ (T1, N1) \LGC (T2, N2)" | compute_infer: "T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I (fst ` (N1 \ M)) \ (T1, N1) \LGC (T2, N2)" | delete_orphan_infers: "T1 = T2 \ T' \ T' \ no_labels.Inf_from (fst ` active_subset N) = {} \ (T1, N) \LGC (T2, N)" lemma premise_free_inf_always_from: "\ \ Inf_F \ prems_of \ = [] \ \ \ no_labels.Inf_from N" unfolding no_labels.Inf_from_def by simp lemma one_step_equiv: "(T1, N1) \LGC (T2, N2) \ N1 \L N2" proof (cases "(T1, N1)" "(T2, N2)" rule: step.cases) show "(T1, N1) \LGC (T2, N2) \ (T1, N1) \LGC (T2, N2)" by blast next fix N M M' assume n1_is: "N1 = N \ M" and n2_is: "N2 = N \ M'" and m_red: "M \ Red_F (N \ M')" have "N1 - N2 \ Red_F N2" using n1_is n2_is m_red by auto then show "N1 \L N2" unfolding derive.simps by blast next fix N C L M assume n1_is: "N1 = N \ {(C, L)}" and not_active: "L \ active" and n2_is: "N2 = N \ {(C, active)}" have "(C, active) \ N2" using n2_is by auto moreover have "C \\ C" by (metis equivp_def equiv_equiv_F) moreover have "active \L L" using active_minimal[OF not_active] . ultimately have "{(C, L)} \ Red_F N2" using red_labeled_clauses by blast then have "N1 - N2 \ Red_F N2" using std_Red_F_eq using n1_is n2_is by blast then show "N1 \L N2" unfolding derive.simps by blast next fix M assume n2_is: "N2 = N1 \ M" have "N1 - N2 \ Red_F N2" using n2_is by blast then show "N1 \L N2" unfolding derive.simps by blast next assume n2_is: "N2 = N1" have "N1 - N2 \ Red_F N2" using n2_is by blast then show "N1 \L N2" unfolding derive.simps by blast qed (* lem:lgc-derivations-are-red-derivations *) lemma lgc_to_red: "chain (\LGC) Ns \ chain (\L) (lmap snd Ns)" using one_step_equiv Lazy_List_Chain.chain_mono by (smt chain_lmap prod.collapse) (* lem:fair-lgc-derivations *) lemma lgc_fair: assumes deriv: "chain (\LGC) Ns" and init_state: "active_subset (snd (lhd Ns)) = {}" and final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and no_prems_init: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd Ns)" and final_schedule: "Liminf_llist (lmap fst Ns) = {}" shows "fair (lmap snd Ns)" unfolding fair_def proof fix \ assume i_in: "\ \ Inf_from (Liminf_llist (lmap snd Ns))" note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have i_in_inf_fl: "\ \ Inf_FL" using i_in unfolding Inf_from_def by blast have "Liminf_llist (lmap snd Ns) = active_subset (Liminf_llist (lmap snd Ns))" using final_state unfolding passive_subset_def active_subset_def by blast then have i_in2: "\ \ Inf_from (active_subset (Liminf_llist (lmap snd Ns)))" using i_in by simp define m where "m = length (prems_of \)" then have m_def_F: "m = length (prems_of (to_F \))" unfolding to_F_def by simp have i_in_F: "to_F \ \ Inf_F" using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast have exist_nj: "\j \ {0..nj. enat (Suc nj) < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns nj)) \ (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k))))" proof clarify fix j assume j_in: "j \ {0.. ! j" using i_in2 unfolding m_def Inf_from_def active_subset_def by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv) then have "(C, active) \ Liminf_llist (lmap snd Ns)" using j_in i_in unfolding m_def Inf_from_def by force then obtain nj where nj_is: "enat nj < llength Ns" and c_in2: "(C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))" unfolding Liminf_llist_def using init_state by fastforce then have c_in3: "\k. k \ nj \ enat k < llength Ns \ (C, active) \ snd (lnth Ns k)" by blast have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def lhd_is by fastforce obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns \ (C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns})))" by blast then have in_allk: "\k. k \ nj_min \ enat k < llength Ns \ (C, active) \ snd (lnth Ns k)" using c_in3 nj_is c_in2 INT_E LeastI_ex [of "\n. enat n < llength Ns \ (C, active) \ \ (snd ` lnth Ns ` {na. n \ na \ enat na < llength Ns})"] by blast have njm_smaller_D: "enat nj_min < llength Ns" using nj_min_is by (smt LeastI_ex \\thesis. (\nj. \enat nj < llength Ns; (C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))\ \ thesis) \ thesis\) have "nj_min > 0" using nj_is c_in2 nj_pos nj_min_is lhd_is by (metis (mono_tags, lifting) active_subset_def emptyE in_allk init_state mem_Collect_eq not_less snd_conv zero_enat_def chain_length_pos[OF deriv]) then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto then have njm_prec_njm: "njm_prec < nj_min" by blast then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp have njm_prec_smaller_d: "njm_prec < llength Ns" by (rule less_trans[OF njm_prec_njm_enat njm_smaller_D]) have njm_prec_all_suc: "\k>njm_prec. enat k < llength Ns \ (C, active) \ snd (lnth Ns k)" using nj_prec_is in_allk by simp have notin_njm_prec: "(C, active) \ snd (lnth Ns njm_prec)" proof (rule ccontr) assume "\ (C, active) \ snd (lnth Ns njm_prec)" then have absurd_hyp: "(C, active) \ snd (lnth Ns njm_prec)" by simp have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is by (smt LeastI_ex Suc_leD \\thesis. (\nj. \enat nj < llength Ns; (C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))\ \ thesis) \ thesis\ enat_ord_simps(1) le_eq_less_or_eq le_less_trans) have "(C, active) \ \ (snd ` (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns}))" proof - { fix k assume k_in: "njm_prec \ k \ enat k < llength Ns" have "k = njm_prec \ (C, active) \ snd (lnth Ns k)" using absurd_hyp by simp moreover have "njm_prec < k \ (C, active) \ snd (lnth Ns k)" using nj_prec_is in_allk k_in by simp ultimately have "(C, active) \ snd (lnth Ns k)" using k_in by fastforce } then show "(C, active) \ \ (snd ` (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns}))" by blast qed then have "enat njm_prec < llength Ns \ (C, active) \ \ (snd ` (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns}))" using prec_smaller by blast then show False using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast qed then have notin_active_subs_njm_prec: "(C, active) \ active_subset (snd (lnth Ns njm_prec))" unfolding active_subset_def by blast then show "\nj. enat (Suc nj) < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns nj)) \ (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting) active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv) qed define nj_set where "nj_set = {nj. (\j\{0.. prems_of \ ! j \ active_subset (snd (lnth Ns nj)) \ (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k))))}" { assume m_null: "m = 0" then have "enat 0 < llength Ns \ to_F \ \ fst (lhd Ns)" using no_prems_init i_in_F m_def_F zero_enat_def chain_length_pos[OF deriv] by auto then have "\n. enat n < llength Ns \ to_F \ \ fst (lnth Ns n)" unfolding lhd_is by blast } moreover { assume m_pos: "m > 0" have nj_not_empty: "nj_set \ {}" proof - have zero_in: "0 \ {0.. ! 0 \ active_subset (snd (lnth Ns n0))" and "\k>n0. enat k < llength Ns \ prems_of \ ! 0 \ active_subset (snd (lnth Ns k))" using exist_nj by fast then have "n0 \ nj_set" unfolding nj_set_def using zero_in by blast then show "nj_set \ {}" by auto qed have nj_finite: "finite nj_set" using all_ex_finite_set[OF exist_nj] by (metis (no_types, lifting) Suc_ile_eq dual_order.strict_implies_order linorder_neqE_nat nj_set_def) have "\n \ nj_set. \nj \ nj_set. nj \ n" using nj_not_empty nj_finite using Max_ge Max_in by blast then obtain n where n_in: "n \ nj_set" and n_bigger: "\nj \ nj_set. nj \ n" by blast then obtain j0 where j0_in: "j0 \ {0.. ! j0 \ active_subset (snd (lnth Ns n))" and j0_allin: "(\k. k > n \ enat k < llength Ns \ prems_of \ ! j0 \ active_subset (snd (lnth Ns k)))" unfolding nj_set_def by blast obtain C0 where C0_is: "prems_of \ ! j0 = (C0, active)" using j0_in i_in2 unfolding m_def Inf_from_def active_subset_def by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv) then have C0_prems_i: "(C0, active) \ set (prems_of \)" using in_set_conv_nth j0_in m_def by force have C0_in: "(C0, active) \ (snd (lnth Ns (Suc n)))" using C0_is j0_allin suc_n_length by (simp add: active_subset_def) have C0_notin: "(C0, active) \ (snd (lnth Ns n))" using C0_is j0_notin unfolding active_subset_def by simp have step_n: "lnth Ns n \LGC lnth Ns (Suc n)" using deriv chain_lnth_rel n_in unfolding nj_set_def by blast have is_scheduled: "\T2 T1 T' N1 N C L N2. lnth Ns n = (T1, N1) \ lnth Ns (Suc n) = (T2, N2) \ T2 = T1 \ T' \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ L \ active \ T' = no_labels.Inf_between (fst ` active_subset N) {C}" using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n C0_in C0_notin unfolding active_subset_def by fastforce then obtain T2 T1 T' N1 N L N2 where nth_d_is: "lnth Ns n = (T1, N1)" and suc_nth_d_is: "lnth Ns (Suc n) = (T2, N2)" and t2_is: "T2 = T1 \ T'" and n1_is: "N1 = N \ {(C0, L)}" "N2 = N \ {(C0, active)}" and l_not_active: "L \ active" and tp_is: "T' = no_labels.Inf_between (fst ` active_subset N) {C0}" using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce have "j \ {0.. prems_of \ ! j \ prems_of \ ! j0 \ prems_of \ ! j \ (active_subset N)" for j proof - fix j assume j_in: "j \ {0.. ! j \ prems_of \ ! j0" obtain nj where nj_len: "enat (Suc nj) < llength Ns" and nj_prems: "prems_of \ ! j \ active_subset (snd (lnth Ns nj))" and nj_greater: "(\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using exist_nj j_in by blast then have "nj \ nj_set" unfolding nj_set_def using j_in by blast moreover have "nj \ n" proof (rule ccontr) assume "\ nj \ n" then have "prems_of \ ! j = (C0, active)" using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n active_subset_def is_scheduled nj_greater nj_prems suc_n_length by auto then show False using j_not_j0 C0_is by simp qed ultimately have "nj < n" using n_bigger by force then have "prems_of \ ! j \ (active_subset (snd (lnth Ns n)))" using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order unfolding nj_set_def by blast then show "prems_of \ ! j \ (active_subset N)" using nth_d_is l_not_active n1_is unfolding active_subset_def by force qed then have prems_i_active: "set (prems_of \) \ active_subset N \ {(C0, active)}" using C0_prems_i C0_is m_def by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI) moreover have "\ (set (prems_of \) \ active_subset N - {(C0, active)})" using C0_prems_i by blast ultimately have "\ \ Inf_between (active_subset N) {(C0, active)}" using i_in_inf_fl prems_i_active unfolding Inf_between_def Inf_from_def by blast then have "to_F \ \ no_labels.Inf_between (fst ` active_subset N) {C0}" unfolding to_F_def Inf_between_def Inf_from_def no_labels.Inf_between_def no_labels.Inf_from_def using Inf_FL_to_Inf_F by force then have i_in_t2: "to_F \ \ T2" using tp_is t2_is by simp have "j \ {0.. (\k. k > n \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" for j proof (cases "j = j0") case True assume "j = j0" then show "(\k. k > n \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using j0_allin by simp next case False assume j_in: "j \ {0.. j0" obtain nj where nj_len: "enat (Suc nj) < llength Ns" and nj_prems: "prems_of \ ! j \ active_subset (snd (lnth Ns nj))" and nj_greater: "(\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using exist_nj j_in by blast then have "nj \ nj_set" unfolding nj_set_def using j_in by blast then show "(\k. k > n \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using nj_greater n_bigger by auto qed then have allj_allk: "(\c\ set (prems_of \). (\k. k > n \ enat k < llength Ns \ c \ active_subset (snd (lnth Ns k))))" using m_def by (metis atLeast0LessThan in_set_conv_nth lessThan_iff) have "\c\ set (prems_of \). snd c = active" using prems_i_active unfolding active_subset_def by auto then have ex_n_i_in: "\n. enat (Suc n) < llength Ns \ to_F \ \ fst (lnth Ns (Suc n)) \ (\c\ set (prems_of \). snd c = active) \ (\c\ set (prems_of \). (\k. k > n \ enat k < llength Ns \ c \ active_subset (snd (lnth Ns k))))" using allj_allk i_in_t2 suc_nth_d_is fstI n_in nj_set_def by auto then have "\n. enat n < llength Ns \ to_F \ \ fst (lnth Ns n) \ (\c\ set (prems_of \). snd c = active) \ (\c\ set (prems_of \). (\k. k \ n \ enat k < llength Ns \ c \ active_subset (snd (lnth Ns k))))" by auto } ultimately obtain n T2 N2 where i_in_suc_n: "to_F \ \ fst (lnth Ns n)" and all_prems_active_after: "m > 0 \ (\c\ set (prems_of \). (\k. k \ n \ enat k < llength Ns \ c \ active_subset (snd (lnth Ns k))))" and suc_n_length: "enat n < llength Ns" and suc_nth_d_is: "lnth Ns n = (T2, N2)" by (metis less_antisym old.prod.exhaust zero_less_Suc) then have i_in_t2: "to_F \ \ T2" by simp have "\p\n. enat (Suc p) < llength Ns \ to_F \ \ (fst (lnth Ns p)) \ to_F \ \ (fst (lnth Ns (Suc p)))" proof (rule ccontr) assume contra: "\ (\p\n. enat (Suc p) < llength Ns \ to_F \ \ (fst (lnth Ns p)) \ to_F \ \ (fst (lnth Ns (Suc p))))" then have i_in_suc: "p0 \ n \ enat (Suc p0) < llength Ns \ to_F \ \ (fst (lnth Ns p0)) \ to_F \ \ (fst (lnth Ns (Suc p0)))" for p0 by blast have "p0 \ n \ enat p0 < llength Ns \ to_F \ \ (fst (lnth Ns p0))" for p0 proof (induction rule: nat_induct_at_least) case base then show ?case using i_in_t2 suc_nth_d_is by simp next case (Suc p0) assume p_bigger_n: "n \ p0" and induct_hyp: "enat p0 < llength Ns \ to_F \ \ fst (lnth Ns p0)" and sucsuc_smaller_d: "enat (Suc p0) < llength Ns" have suc_p_bigger_n: "n \ p0" using p_bigger_n by simp have suc_smaller_d: "enat p0 < llength Ns" using sucsuc_smaller_d Suc_ile_eq dual_order.strict_implies_order by blast then have "to_F \ \ fst (lnth Ns p0)" using induct_hyp by blast then show ?case using i_in_suc[OF suc_p_bigger_n sucsuc_smaller_d] by blast qed then have i_in_all_bigger_n: "\j. j \ n \ enat j < llength Ns \ to_F \ \ (fst (lnth Ns j))" by presburger have "llength (lmap fst Ns) = llength Ns" by force then have "to_F \ \ \ (lnth (lmap fst Ns) ` {j. n \ j \ enat j < llength (lmap fst Ns)})" using i_in_all_bigger_n using Suc_le_D by auto then have "to_F \ \ Liminf_llist (lmap fst Ns)" unfolding Liminf_llist_def using suc_n_length by auto then show False using final_schedule by fast qed then obtain p where p_greater_n: "p \ n" and p_smaller_d: "enat (Suc p) < llength Ns" and i_in_p: "to_F \ \ (fst (lnth Ns p))" and i_notin_suc_p: "to_F \ \ (fst (lnth Ns (Suc p)))" by blast have p_neq_n: "Suc p \ n" using i_notin_suc_p i_in_suc_n by blast have step_p: "lnth Ns p \LGC lnth Ns (Suc p)" using deriv p_smaller_d chain_lnth_rel by blast then have "\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M))" proof - have ci_or_do: "(\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M))) \ (\T1 T2 T' N. lnth Ns p = (T1, N) \ lnth Ns (Suc p) = (T2, N) \ T1 = T2 \ T' \ T' \ no_labels.Inf_from (fst ` active_subset N) = {})" using step.simps[of "lnth Ns p" "lnth Ns (Suc p)"] step_p i_in_p i_notin_suc_p by fastforce then have p_greater_n_strict: "n < Suc p" using suc_nth_d_is p_greater_n i_in_t2 i_notin_suc_p le_eq_less_or_eq by force have "m > 0 \ j \ {0.. prems_of (to_F \) ! j \ fst ` active_subset (snd (lnth Ns p))" for j proof - fix j assume m_pos: "m > 0" and j_in: "j \ {0.. ! j \ (active_subset (snd (lnth Ns p)))" using all_prems_active_after[OF m_pos] p_smaller_d m_def p_greater_n p_neq_n by (meson Suc_ile_eq atLeastLessThan_iff dual_order.strict_implies_order nth_mem p_greater_n_strict) then have "fst (prems_of \ ! j) \ fst ` active_subset (snd (lnth Ns p))" by blast then show "prems_of (to_F \) ! j \ fst ` active_subset (snd (lnth Ns p))" unfolding to_F_def using j_in m_def by simp qed then have prems_i_active_p: "m > 0 \ to_F \ \ no_labels.Inf_from (fst ` active_subset (snd (lnth Ns p)))" using i_in_F unfolding no_labels.Inf_from_def by (smt atLeast0LessThan in_set_conv_nth lessThan_iff m_def_F mem_Collect_eq subsetI) have "m = 0 \ (\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M)))" using ci_or_do premise_free_inf_always_from[of "to_F \" "fst ` active_subset _", OF i_in_F] m_def i_in_p i_notin_suc_p m_def_F by auto then show "(\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M)))" using ci_or_do i_in_p i_notin_suc_p prems_i_active_p unfolding active_subset_def by force qed then obtain T1p T2p N1p N2p Mp where "lnth Ns p = (T1p, N1p)" and suc_p_is: "lnth Ns (Suc p) = (T2p, N2p)" and "T1p = T2p \ {to_F \}" and "T2p \ {to_F \} = {}" and n2p_is: "N2p = N1p \ Mp"and "active_subset Mp = {}" and i_in_red_inf: "to_F \ \ no_labels.Red_I_\ (fst ` (N1p \ Mp))" using i_in_p i_notin_suc_p by fastforce have "to_F \ \ no_labels.Red_I (fst ` (snd (lnth Ns (Suc p))))" using i_in_red_inf suc_p_is n2p_is by fastforce then have "\q \ Q. (\_I_q q (to_F \) \ None \ the (\_I_q q (to_F \)) \ Red_I_q q (\ (\_F_q q ` fst ` snd (lnth Ns (Suc p))))) \ (\_I_q q (to_F \) = None \ \_F_q q (concl_of (to_F \)) \ \ (\_F_q q ` fst ` snd (lnth Ns (Suc p))) \ Red_F_q q (\ (\_F_q q ` fst ` snd (lnth Ns (Suc p)))))" unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\_q_def by blast then have "\ \ Red_I_\ (snd (lnth Ns (Suc p)))" using i_in_inf_fl unfolding Red_I_\_def Red_I_\_q_def by (simp add: to_F_def) then show "\ \ Sup_llist (lmap Red_I_\ (lmap snd Ns))" unfolding Sup_llist_def using suc_n_length p_smaller_d by auto qed theorem lgc_complete_Liminf: assumes deriv: "chain (\LGC) Ns" and init_state: "active_subset (snd (lhd Ns)) = {}" and final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and no_prems_init: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd Ns)" and final_schedule: "Liminf_llist (lmap fst Ns) = {}" and b_in: "B \ Bot_F" and bot_entailed: "no_labels.entails_\ (fst ` snd (lhd Ns)) {B}" shows "\BL \ Bot_FL. BL \ Liminf_llist (lmap snd Ns)" proof - have labeled_b_in: "(B, active) \ Bot_FL" using b_in by simp have simp_snd_lmap: "lhd (lmap snd Ns) = snd (lhd Ns)" by (rule llist.map_sel(1)[OF chain_not_lnull[OF deriv]]) have labeled_bot_entailed: "entails_\_L (snd (lhd Ns)) {(B, active)}" using labeled_entailment_lifting bot_entailed by fastforce have "fair (lmap snd Ns)" using lgc_fair[OF deriv init_state final_state no_prems_init final_schedule] . then show ?thesis using dynamically_complete_Liminf labeled_b_in lgc_to_red[OF deriv] labeled_bot_entailed simp_snd_lmap std_Red_I_eq by presburger qed (* thm:lgc-completeness *) theorem lgc_complete: assumes deriv: "chain (\LGC) Ns" and init_state: "active_subset (snd (lhd Ns)) = {}" and final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and no_prems_init: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd Ns)" and final_schedule: "Liminf_llist (lmap fst Ns) = {}" and b_in: "B \ Bot_F" and bot_entailed: "no_labels.entails_\ (fst ` snd (lhd Ns)) {B}" shows "\i. enat i < llength Ns \ (\BL \ Bot_FL. BL \ snd (lnth Ns i))" proof - have "\BL\Bot_FL. BL \ Liminf_llist (lmap snd Ns)" using assms by (rule lgc_complete_Liminf) then show ?thesis unfolding Liminf_llist_def by auto qed end end diff --git a/thys/Well_Quasi_Orders/Almost_Full.thy b/thys/Well_Quasi_Orders/Almost_Full.thy --- a/thys/Well_Quasi_Orders/Almost_Full.thy +++ b/thys/Well_Quasi_Orders/Almost_Full.thy @@ -1,551 +1,550 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \The Almost-Full Property\ theory Almost_Full imports "HOL-Library.Sublist" "HOL-Library.Ramsey" "Regular-Sets.Regexp_Method" "Abstract-Rewriting.Seq" Least_Enum Infinite_Sequences Open_Induction.Restricted_Predicates begin (*TODO: move*) lemma le_Suc_eq': "x \ Suc y \ x = 0 \ (\x'. x = Suc x' \ x' \ y)" by (cases x) auto lemma ex_leq_Suc: "(\i\Suc j. P i) \ P 0 \ (\i\j. P (Suc i))" by (auto simp: le_Suc_eq') lemma ex_less_Suc: "(\i P 0 \ (\iBasic Definitions and Facts\ text \ An infinite sequence is \emph{good} whenever there are indices @{term "i < j"} such that @{term "P (f i) (f j)"}. \ definition good :: "('a \ 'a \ bool) \ (nat \ 'a) \ bool" where "good P f \ (\i j. i < j \ P (f i) (f j))" text \A sequence that is not good is called \emph{bad}.\ abbreviation "bad P f \ \ good P f" lemma goodI: "\i < j; P (f i) (f j)\ \ good P f" by (auto simp: good_def) lemma goodE [elim]: "good P f \ (\i j. \i < j; P (f i) (f j)\ \ Q) \ Q" by (auto simp: good_def) lemma badE [elim]: "bad P f \ ((\i j. i < j \ \ P (f i) (f j)) \ Q) \ Q" by (auto simp: good_def) definition almost_full_on :: "('a \ 'a \ bool) \ 'a set \ bool" where "almost_full_on P A \ (\f \ SEQ A. good P f)" lemma almost_full_onI [Pure.intro]: "(\f. \i. f i \ A \ good P f) \ almost_full_on P A" unfolding almost_full_on_def by blast lemma almost_full_onD: fixes f :: "nat \ 'a" and A :: "'a set" assumes "almost_full_on P A" and "\i. f i \ A" obtains i j where "i < j" and "P (f i) (f j)" using assms unfolding almost_full_on_def by blast subsection \An equivalent inductive definition\ inductive af for A where now: "(\x y. x \ A \ y \ A \ P x y) \ af A P" | later: "(\x. x \ A \ af A (\y z. P y z \ P x y)) \ af A P" lemma af_imp_almost_full_on: assumes "af A P" shows "almost_full_on P A" proof fix f :: "nat \ 'a" assume "\i. f i \ A" with assms obtain i and j where "i < j" and "P (f i) (f j)" proof (induct arbitrary: f thesis) case (later P) define g where [simp]: "g i = f (Suc i)" for i have "f 0 \ A" and "\i. g i \ A" using later by auto then obtain i and j where "i < j" and "P (g i) (g j) \ P (f 0) (g i)" using later by blast then consider "P (g i) (g j)" | "P (f 0) (g i)" by blast then show ?case using \i < j\ by (cases) (auto intro: later) qed blast then show "good P f" by (auto simp: good_def) qed lemma af_mono: assumes "af A P" and "\x y. x \ A \ y \ A \ P x y \ Q x y" shows "af A Q" using assms proof (induct arbitrary: Q) case (now P) then have "\x y. x \ A \ y \ A \ Q x y" by blast then show ?case by (rule af.now) next case (later P) show ?case proof (intro af.later [of A Q]) fix x assume "x \ A" then show "af A (\y z. Q y z \ Q x y)" using later(3) by (intro later(2) [of x]) auto qed qed lemma accessible_on_imp_af: assumes "accessible_on P A x" shows "af A (\u v. \ P v u \ \ P u x)" using assms proof (induct) case (1 x) then have "af A (\u v. (\ P v u \ \ P u x) \ \ P u y \ \ P y x)" if "y \ A" for y using that by (cases "P y x") (auto intro: af.now af_mono) then show ?case by (rule af.later) qed lemma wfp_on_imp_af: assumes "wfp_on P A" shows "af A (\x y. \ P y x)" using assms by (auto simp: wfp_on_accessible_on_iff intro: accessible_on_imp_af af.later) lemma af_leq: "af UNIV ((\) :: nat \ nat \ bool)" using wf_less [folded wfP_def wfp_on_UNIV, THEN wfp_on_imp_af] by (simp add: not_less) definition "NOTAF A P = (SOME x. x \ A \ \ af A (\y z. P y z \ P x y))" lemma not_af: "\ af A P \ (\x y. x \ A \ y \ A \ \ P x y) \ (\x\A. \ af A (\y z. P y z \ P x y))" unfolding af.simps [of A P] by blast fun F where "F A P 0 = NOTAF A P" | "F A P (Suc i) = (let x = NOTAF A P in F A (\y z. P y z \ P x y) i)" lemma almost_full_on_imp_af: assumes af: "almost_full_on P A" shows "af A P" proof (rule ccontr) assume "\ af A P" then have *: "F A P n \ A \ \ af A (\y z. P y z \ (\i\n. P (F A P i) y) \ (\j\n. \i. i < j \ P (F A P i) (F A P j)))" for n proof (induct n arbitrary: P) case 0 from \\ af A P\ have "\x. x \ A \ \ af A (\y z. P y z \ P x y)" by (auto intro: af.intros) then have "NOTAF A P \ A \ \ af A (\y z. P y z \ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex) with 0 show ?case by simp next case (Suc n) from \\ af A P\ have "\x. x \ A \ \ af A (\y z. P y z \ P x y)" by (auto intro: af.intros) then have "NOTAF A P \ A \ \ af A (\y z. P y z \ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex) from Suc(1) [OF this [THEN conjunct2]] show ?case by (fastforce simp: ex_leq_Suc ex_less_Suc elim!: back_subst [where P = "\x. \ af A x"]) qed then have "F A P \ SEQ A" by auto from af [unfolded almost_full_on_def, THEN bspec, OF this] and not_af [OF * [THEN conjunct2]] show False unfolding good_def by blast qed hide_const NOTAF F lemma almost_full_on_UNIV: "almost_full_on (\_ _. True) UNIV" by (auto simp: almost_full_on_def good_def) lemma almost_full_on_imp_reflp_on: assumes "almost_full_on P A" shows "reflp_on A P" using assms by (auto simp: almost_full_on_def reflp_on_def) lemma almost_full_on_subset: "A \ B \ almost_full_on P B \ almost_full_on P A" by (auto simp: almost_full_on_def) lemma almost_full_on_mono: assumes "A \ B" and "\x y. Q x y \ P x y" and "almost_full_on Q B" shows "almost_full_on P A" using assms by (metis almost_full_on_def almost_full_on_subset good_def) text \ Every sequence over elements of an almost-full set has a homogeneous subsequence. \ lemma almost_full_on_imp_homogeneous_subseq: assumes "almost_full_on P A" and "\i::nat. f i \ A" shows "\\::nat \ nat. \i j. i < j \ \ i < \ j \ P (f (\ i)) (f (\ j))" proof - define X where "X = {{i, j} | i j::nat. i < j \ P (f i) (f j)}" define Y where "Y = - X" define h where "h = (\Z. if Z \ X then 0 else Suc 0)" have [iff]: "\x y. h {x, y} = 0 \ {x, y} \ X" by (auto simp: h_def) have [iff]: "\x y. h {x, y} = Suc 0 \ {x, y} \ Y" by (auto simp: h_def Y_def) have "\x\UNIV. \y\UNIV. x \ y \ h {x, y} < 2" by (simp add: h_def) from Ramsey2 [OF infinite_UNIV_nat this] obtain I c where "infinite I" and "c < 2" and *: "\x\I. \y\I. x \ y \ h {x, y} = c" by blast then interpret infinitely_many1 "\i. i \ I" by (unfold_locales) (simp add: infinite_nat_iff_unbounded) have "c = 0 \ c = 1" using \c < 2\ by arith then show ?thesis proof assume [simp]: "c = 0" have "\i j. i < j \ P (f (enum i)) (f (enum j))" proof (intro allI impI) fix i j :: nat assume "i < j" from * and enum_P and enum_less [OF \i < j\] have "{enum i, enum j} \ X" by auto with enum_less [OF \i < j\] show "P (f (enum i)) (f (enum j))" by (auto simp: X_def doubleton_eq_iff) qed then show ?thesis using enum_less by blast next assume [simp]: "c = 1" have "\i j. i < j \ \ P (f (enum i)) (f (enum j))" proof (intro allI impI) fix i j :: nat assume "i < j" from * and enum_P and enum_less [OF \i < j\] have "{enum i, enum j} \ Y" by auto with enum_less [OF \i < j\] show "\ P (f (enum i)) (f (enum j))" by (auto simp: Y_def X_def doubleton_eq_iff) qed then have "\ good P (f \ enum)" by auto moreover have "\i. f (enum i) \ A" using assms by auto ultimately show ?thesis using \almost_full_on P A\ by (simp add: almost_full_on_def) qed qed text \ Almost full relations do not admit infinite antichains. \ lemma almost_full_on_imp_no_antichain_on: assumes "almost_full_on P A" shows "\ antichain_on P f A" proof assume *: "antichain_on P f A" then have "\i. f i \ A" by simp with assms have "good P f" by (auto simp: almost_full_on_def) then obtain i j where "i < j" and "P (f i) (f j)" unfolding good_def by auto moreover with * have "incomparable P (f i) (f j)" by auto ultimately show False by blast qed text \ If the image of a function is almost-full then also its preimage is almost-full. \ lemma almost_full_on_map: assumes "almost_full_on Q B" and "h ` A \ B" shows "almost_full_on (\x y. Q (h x) (h y)) A" (is "almost_full_on ?P A") proof fix f assume "\i::nat. f i \ A" then have "\i. h (f i) \ B" using \h ` A \ B\ by auto with \almost_full_on Q B\ [unfolded almost_full_on_def, THEN bspec, of "h \ f"] show "good ?P f" unfolding good_def comp_def by blast qed text \ The homomorphic image of an almost-full set is almost-full. \ lemma almost_full_on_hom: fixes h :: "'a \ 'b" assumes hom: "\x y. \x \ A; y \ A; P x y\ \ Q (h x) (h y)" and af: "almost_full_on P A" shows "almost_full_on Q (h ` A)" proof fix f :: "nat \ 'b" assume "\i. f i \ h ` A" then have "\i. \x. x \ A \ f i = h x" by (auto simp: image_def) from choice [OF this] obtain g where *: "\i. g i \ A \ f i = h (g i)" by blast show "good Q f" proof (rule ccontr) assume bad: "bad Q f" { fix i j :: nat assume "i < j" from bad have "\ Q (f i) (f j)" using \i < j\ by (auto simp: good_def) with hom have "\ P (g i) (g j)" using * by auto } then have "bad P g" by (auto simp: good_def) with af and * show False by (auto simp: good_def almost_full_on_def) qed qed text \ The monomorphic preimage of an almost-full set is almost-full. \ lemma almost_full_on_mon: assumes mon: "\x y. \x \ A; y \ A\ \ P x y = Q (h x) (h y)" "bij_betw h A B" and af: "almost_full_on Q B" shows "almost_full_on P A" proof fix f :: "nat \ 'a" assume *: "\i. f i \ A" then have **: "\i. (h \ f) i \ B" using mon by (auto simp: bij_betw_def) show "good P f" proof (rule ccontr) assume bad: "bad P f" { fix i j :: nat assume "i < j" from bad have "\ P (f i) (f j)" using \i < j\ by (auto simp: good_def) with mon have "\ Q (h (f i)) (h (f j))" using * by (auto simp: bij_betw_def inj_on_def) } then have "bad Q (h \ f)" by (auto simp: good_def) with af and ** show False by (auto simp: good_def almost_full_on_def) qed qed text \ Every total and well-founded relation is almost-full. \ lemma total_on_and_wfp_on_imp_almost_full_on: assumes "totalp_on A P" and "wfp_on P A" shows "almost_full_on P\<^sup>=\<^sup>= A" proof (rule ccontr) assume "\ almost_full_on P\<^sup>=\<^sup>= A" then obtain f :: "nat \ 'a" where *: "\i. f i \ A" and "\i j. i < j \ \ P\<^sup>=\<^sup>= (f i) (f j)" unfolding almost_full_on_def by (auto dest: badE) with \totalp_on A P\ have "\i j. i < j \ P (f j) (f i)" unfolding totalp_on_def by blast then have "\i. P (f (Suc i)) (f i)" by auto with \wfp_on P A\ and * show False unfolding wfp_on_def by blast qed lemma Nil_imp_good_list_emb [simp]: assumes "f i = []" shows "good (list_emb P) f" proof (rule ccontr) assume "bad (list_emb P) f" moreover have "(list_emb P) (f i) (f (Suc i))" unfolding assms by auto ultimately show False unfolding good_def by auto qed lemma ne_lists: assumes "xs \ []" and "xs \ lists A" shows "hd xs \ A" and "tl xs \ lists A" using assms by (case_tac [!] xs) simp_all lemma list_emb_eq_length_induct [consumes 2, case_names Nil Cons]: assumes "length xs = length ys" and "list_emb P xs ys" and "Q [] []" and "\x y xs ys. \P x y; list_emb P xs ys; Q xs ys\ \ Q (x#xs) (y#ys)" shows "Q xs ys" using assms(2, 1, 3-) by (induct) (auto dest: list_emb_length) lemma list_emb_eq_length_P: assumes "length xs = length ys" and "list_emb P xs ys" shows "\iSpecial Case: Finite Sets\ text \ Every reflexive relation on a finite set is almost-full. \ lemma finite_almost_full_on: assumes finite: "finite A" and refl: "reflp_on A P" shows "almost_full_on P A" proof fix f :: "nat \ 'a" assume *: "\i. f i \ A" let ?I = "UNIV::nat set" have "f ` ?I \ A" using * by auto with finite and finite_subset have 1: "finite (f ` ?I)" by blast have "infinite ?I" by auto from pigeonhole_infinite [OF this 1] obtain k where "infinite {j. f j = f k}" by auto then obtain l where "k < l" and "f l = f k" unfolding infinite_nat_iff_unbounded by auto then have "P (f k) (f l)" using refl and * by (auto simp: reflp_on_def) with \k < l\ show "good P f" by (auto simp: good_def) qed lemma eq_almost_full_on_finite_set: assumes "finite A" shows "almost_full_on (=) A" using finite_almost_full_on [OF assms, of "(=)"] by (auto simp: reflp_on_def) subsection \Further Results\ lemma af_trans_extension_imp_wf: assumes subrel: "\x y. P x y \ Q x y" and af: "almost_full_on P A" - and trans: "transp_on Q A" + and trans: "transp_on A Q" shows "wfp_on (strict Q) A" proof (unfold wfp_on_def, rule notI) assume "\f. \i. f i \ A \ strict Q (f (Suc i)) (f i)" then obtain f where *: "\i. f i \ A \ ((strict Q)\\) (f i) (f (Suc i))" by blast - from chain_transp_on_less [OF this] - and transp_on_strict [THEN transp_on_converse, OF trans] - have "\i j. i < j \ \ Q (f i) (f j)" by blast + from chain_transp_on_less[OF this] + have "\i j. i < j \ \ Q (f i) (f j)" using trans using transp_on_conversep transp_on_strict by blast with subrel have "\i j. i < j \ \ P (f i) (f j)" by blast with af show False using * by (auto simp: almost_full_on_def good_def) qed lemma af_trans_imp_wf: assumes "almost_full_on P A" - and "transp_on P A" + and "transp_on A P" shows "wfp_on (strict P) A" using assms by (intro af_trans_extension_imp_wf) lemma wf_and_no_antichain_imp_qo_extension_wf: assumes wf: "wfp_on (strict P) A" and anti: "\ (\f. antichain_on P f A)" and subrel: "\x\A. \y\A. P x y \ Q x y" and qo: "qo_on Q A" shows "wfp_on (strict Q) A" proof (rule ccontr) - have "transp_on (strict Q) A" + have "transp_on A (strict Q)" using qo unfolding qo_on_def transp_on_def by blast - then have *: "transp_on ((strict Q)\\) A" by (rule transp_on_converse) + then have *: "transp_on A ((strict Q)\\)" by simp assume "\ wfp_on (strict Q) A" then obtain f :: "nat \ 'a" where A: "\i. f i \ A" and "\i. strict Q (f (Suc i)) (f i)" unfolding wfp_on_def by blast+ then have "\i. f i \ A \ ((strict Q)\\) (f i) (f (Suc i))" by auto from chain_transp_on_less [OF this *] have *: "\i j. i < j \ \ P (f i) (f j)" using subrel and A by blast show False proof (cases) assume "\k. \i>k. \j>i. P (f j) (f i)" then obtain k where "\i>k. \j>i. P (f j) (f i)" by auto from subchain [of k _ f, OF this] obtain g where "\i j. i < j \ g i < g j" and "\i. P (f (g (Suc i))) (f (g i))" by auto with * have "\i. strict P (f (g (Suc i))) (f (g i))" by blast with wf [unfolded wfp_on_def not_ex, THEN spec, of "\i. f (g i)"] and A show False by fast next assume "\ (\k. \i>k. \j>i. P (f j) (f i))" then have "\k. \i>k. \j>i. \ P (f j) (f i)" by auto from choice [OF this] obtain h where "\k. h k > k" and **: "\k. (\j>h k. \ P (f j) (f (h k)))" by auto define \ where [simp]: "\ = (\i. (h ^^ Suc i) 0)" have "\i. \ i < \ (Suc i)" using \\k. h k > k\ by (induct_tac i) auto then have mono: "\i j. i < j \ \ i < \ j" by (metis lift_Suc_mono_less) then have "\i j. i < j \ \ P (f (\ j)) (f (\ i))" using ** by auto with mono [THEN *] have "\i j. i < j \ incomparable P (f (\ j)) (f (\ i))" by blast moreover have "\i j. i < j \ \ incomparable P (f (\ i)) (f (\ j))" using anti [unfolded not_ex, THEN spec, of "\i. f (\ i)"] and A by blast ultimately show False by blast qed qed lemma every_qo_extension_wf_imp_af: assumes ext: "\Q. (\x\A. \y\A. P x y \ Q x y) \ qo_on Q A \ wfp_on (strict Q) A" and "qo_on P A" shows "almost_full_on P A" proof from \qo_on P A\ have refl: "reflp_on A P" - and trans: "transp_on P A" + and trans: "transp_on A P" by (auto intro: qo_on_imp_reflp_on qo_on_imp_transp_on) fix f :: "nat \ 'a" assume "\i. f i \ A" then have A: "\i. f i \ A" .. show "good P f" proof (rule ccontr) assume "\ ?thesis" then have bad: "\i j. i < j \ \ P (f i) (f j)" by (auto simp: good_def) then have *: "\i j. P (f i) (f j) \ i \ j" by (metis not_le_imp_less) define D where [simp]: "D = (\x y. \i. x = f (Suc i) \ y = f i)" define P' where "P' = restrict_to P A" define Q where [simp]: "Q = (sup P' D)\<^sup>*\<^sup>*" have **: "\i j. (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+ (f i) (f j) \ i > j" proof - fix i j assume "(D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+ (f i) (f j)" then show "i > j" apply (induct "f i" "f j" arbitrary: j) apply (insert A, auto dest!: * simp: P'_def reflp_on_restrict_to_rtranclp [OF refl trans]) apply (metis "*" dual_order.strict_trans1 less_Suc_eq_le refl reflp_on_def) by (metis le_imp_less_Suc less_trans) qed have "\x\A. \y\A. P x y \ Q x y" by (auto simp: P'_def) moreover have "qo_on Q A" by (auto simp: qo_on_def reflp_on_def transp_on_def) ultimately have "wfp_on (strict Q) A" using ext [THEN spec, of Q] by blast moreover have "\i. f i \ A \ strict Q (f (Suc i)) (f i)" proof fix i have "\ Q (f i) (f (Suc i))" proof assume "Q (f i) (f (Suc i))" then have "(sup P' D)\<^sup>*\<^sup>* (f i) (f (Suc i))" by auto moreover have "(sup P' D)\<^sup>*\<^sup>* = sup (P'\<^sup>*\<^sup>*) (P'\<^sup>*\<^sup>* OO (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+)" proof - have "\A B. (A \ B)\<^sup>* = A\<^sup>* \ A\<^sup>* O (B O A\<^sup>*)\<^sup>+" by regexp from this [to_pred] show ?thesis by blast qed ultimately have "sup (P'\<^sup>*\<^sup>*) (P'\<^sup>*\<^sup>* OO (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+) (f i) (f (Suc i))" by simp then have "(P'\<^sup>*\<^sup>* OO (D OO P'\<^sup>*\<^sup>*)\<^sup>+\<^sup>+) (f i) (f (Suc i))" by auto then have "Suc i < i" using ** apply auto by (metis (lifting, mono_tags) less_le relcompp.relcompI tranclp_into_tranclp2) then show False by auto qed with A [of i] show "f i \ A \ strict Q (f (Suc i)) (f i)" by auto qed ultimately show False unfolding wfp_on_def by blast qed qed end diff --git a/thys/Well_Quasi_Orders/Higman_OI.thy b/thys/Well_Quasi_Orders/Higman_OI.thy --- a/thys/Well_Quasi_Orders/Higman_OI.thy +++ b/thys/Well_Quasi_Orders/Higman_OI.thy @@ -1,263 +1,263 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \A Proof of Higman's Lemma via Open Induction\ theory Higman_OI imports Open_Induction.Open_Induction Minimal_Elements Almost_Full begin subsection \Some facts about the suffix relation\ lemma wfp_on_strict_suffix: "wfp_on strict_suffix A" by (rule wfp_on_mono [OF subset_refl, of _ _ "measure_on length A"]) (auto simp: strict_suffix_def suffix_def) lemma po_on_strict_suffix: "po_on strict_suffix A" by (force simp: strict_suffix_def po_on_def transp_on_def irreflp_on_def) subsection \Lexicographic Order on Infinite Sequences\ lemma antisymp_on_LEX: assumes "irreflp_on A P" and "antisymp_on A P" shows "antisymp_on (SEQ A) (LEX P)" proof (rule antisymp_onI) fix f g assume SEQ: "f \ SEQ A" "g \ SEQ A" and "LEX P f g" and "LEX P g f" then obtain i j where "P (f i) (g i)" and "P (g j) (f j)" and "\kk SEQ A" and "g \ SEQ A" and "h \ SEQ A" + assumes "transp_on A P" and "f \ SEQ A" and "g \ SEQ A" and "h \ SEQ A" and "LEX P f g" and "LEX P g h" shows "LEX P f h" using assms by (auto simp: LEX_def transp_on_def) (metis less_trans linorder_neqE_nat) lemma qo_on_LEXEQ: - "transp_on P A \ qo_on (LEXEQ P) (SEQ A)" -by (auto simp: qo_on_def reflp_on_def transp_on_def [of "LEXEQ P"] dest: LEX_trans) + "transp_on A P \ qo_on (LEXEQ P) (SEQ A)" +by (auto simp: qo_on_def reflp_on_def transp_on_def [of _ "LEXEQ P"] dest: LEX_trans) context minimal_element begin lemma glb_LEX_lexmin: assumes "chain_on (LEX P) C (SEQ A)" and "C \ {}" shows "glb (LEX P) C (lexmin C)" proof have "C \ SEQ A" using assms by (auto simp: chain_on_def) then have "lexmin C \ SEQ A" using \C \ {}\ by (intro lexmin_SEQ_mem) note * = \C \ SEQ A\ \C \ {}\ note lex = LEX_imp_less [folded irreflp_on_def, OF po [THEN po_on_imp_irreflp_on]] \ \\lexmin C\ is a lower bound\ show "lb (LEX P) C (lexmin C)" proof fix f assume "f \ C" then show "LEXEQ P (lexmin C) f" proof (cases "f = lexmin C") define i where "i = (LEAST i. f i \ lexmin C i)" case False then have neq: "\i. f i \ lexmin C i" by blast from LeastI_ex [OF this, folded i_def] and not_less_Least [where P = "\i. f i \ lexmin C i", folded i_def] have neq: "f i \ lexmin C i" and eq: "\j eq_upto C (lexmin C) i" "f i \ ith (eq_upto C (lexmin C) i) i" using \f \ C\ by force+ moreover from ** have "\ P (f i) (lexmin C i)" using lexmin_minimal [OF *, of "f i" i] and \f \ C\ and \C \ SEQ A\ by blast moreover obtain g where "g \ eq_upto C (lexmin C) (Suc i)" using eq_upto_lexmin_non_empty [OF *] by blast ultimately have "P (lexmin C i) (f i)" using neq and \C \ SEQ A\ and assms(1) and lex [of g f i] and lex [of f g i] by (auto simp: eq_upto_def chain_on_def) with eq show ?thesis by (auto simp: LEX_def) qed simp qed \ \\lexmin C\ is greater than or equal to any other lower bound\ fix f assume lb: "lb (LEX P) C f" then show "LEXEQ P f (lexmin C)" proof (cases "f = lexmin C") define i where "i = (LEAST i. f i \ lexmin C i)" case False then have neq: "\i. f i \ lexmin C i" by blast from LeastI_ex [OF this, folded i_def] and not_less_Least [where P = "\i. f i \ lexmin C i", folded i_def] have neq: "f i \ lexmin C i" and eq: "\j eq_upto C (lexmin C) (Suc i)" and "h \ C" using eq_upto_lexmin_non_empty [OF *] by (auto simp: eq_upto_def) then have [simp]: "\j. j < Suc i \ h j = lexmin C j" by auto with lb and \h \ C\ have "LEX P f h" using neq by (auto simp: lb_def) then have "P (f i) (h i)" using neq and eq and \C \ SEQ A\ and \h \ C\ by (intro lex) auto with eq show ?thesis by (auto simp: LEX_def) qed simp qed lemma dc_on_LEXEQ: "dc_on (LEXEQ P) (SEQ A)" proof fix C assume "chain_on (LEXEQ P) C (SEQ A)" and "C \ {}" then have chain: "chain_on (LEX P) C (SEQ A)" by (auto simp: chain_on_def) then have "C \ SEQ A" by (auto simp: chain_on_def) then have "lexmin C \ SEQ A" using \C \ {}\ by (intro lexmin_SEQ_mem) have "glb (LEX P) C (lexmin C)" by (rule glb_LEX_lexmin [OF chain \C \ {}\]) then have "glb (LEXEQ P) C (lexmin C)" by (auto simp: glb_def lb_def) with \lexmin C \ SEQ A\ show "\f \ SEQ A. glb (LEXEQ P) C f" by blast qed end text \ Properties that only depend on finite initial segments of a sequence (i.e., which are open with respect to the product topology). \ definition "pt_open_on Q A \ (\f\A. Q f \ (\n. (\g\A. (\i Q g)))" lemma pt_open_onD: "pt_open_on Q A \ Q f \ f \ A \ (\n. (\g\A. (\i Q g))" unfolding pt_open_on_def by blast lemma pt_open_on_good: "pt_open_on (good Q) (SEQ A)" proof (unfold pt_open_on_def, intro ballI) fix f assume f: "f \ SEQ A" show "good Q f = (\n. \g\SEQ A. (\i good Q g)" proof assume "good Q f" then obtain i and j where *: "i < j" "Q (f i) (f j)" by auto have "\g\SEQ A. (\i good Q g" proof (intro ballI impI) fix g assume "g \ SEQ A" and "\in. \g\SEQ A. (\i good Q g" .. next assume "\n. \g\SEQ A. (\i good Q g" with f show "good Q f" by blast qed qed context minimal_element begin lemma pt_open_on_imp_open_on_LEXEQ: assumes "pt_open_on Q (SEQ A)" shows "open_on (LEXEQ P) Q (SEQ A)" proof fix C assume chain: "chain_on (LEXEQ P) C (SEQ A)" and ne: "C \ {}" and "\g\SEQ A. glb (LEXEQ P) C g \ Q g" then obtain g where g: "g \ SEQ A" and "glb (LEXEQ P) C g" and Q: "Q g" by blast then have glb: "glb (LEX P) C g" by (auto simp: glb_def lb_def) from chain have "chain_on (LEX P) C (SEQ A)" and C: "C \ SEQ A" by (auto simp: chain_on_def) note * = glb_LEX_lexmin [OF this(1) ne] have "lexmin C \ SEQ A" using ne and C by (intro lexmin_SEQ_mem) from glb_unique [OF _ g this glb *] and antisymp_on_LEX [OF po_on_imp_irreflp_on [OF po] po_on_imp_antisymp_on [OF po]] have [simp]: "lexmin C = g" by auto from assms [THEN pt_open_onD, OF Q g] obtain n :: nat where **: "\h. h \ SEQ A \ (\i Q h" by blast from eq_upto_lexmin_non_empty [OF C ne, of n] obtain f where "f \ eq_upto C g n" by auto then have "f \ C" and "Q f" using ** [of f] and C by force+ then show "\f\C. Q f" by blast qed lemma open_on_good: "open_on (LEXEQ P) (good Q) (SEQ A)" by (intro pt_open_on_imp_open_on_LEXEQ pt_open_on_good) end lemma open_on_LEXEQ_imp_pt_open_on_counterexample: fixes a b :: "'a" defines "A \ {a, b}" and "P \ (\x y. False)" and "Q \ (\f. \i. f i = b)" assumes [simp]: "a \ b" shows "minimal_element P A" and "open_on (LEXEQ P) Q (SEQ A)" and "\ pt_open_on Q (SEQ A)" proof - show "minimal_element P A" by standard (auto simp: P_def po_on_def irreflp_on_def transp_on_def wfp_on_def) show "open_on (LEXEQ P) Q (SEQ A)" by (auto simp: P_def open_on_def chain_on_def SEQ_def glb_def lb_def LEX_def) show "\ pt_open_on Q (SEQ A)" proof define f :: "nat \ 'a" where "f \ (\x. b)" have "f \ SEQ A" by (auto simp: A_def f_def) moreover assume "pt_open_on Q (SEQ A)" ultimately have "Q f \ (\n. (\g\SEQ A. (\i Q g))" unfolding pt_open_on_def by blast moreover have "Q f" by (auto simp: Q_def f_def) moreover have "\g\SEQ A. (\i \ Q g" for n by (intro bexI [of _ "f(n := a)"]) (auto simp: f_def Q_def A_def) ultimately show False by blast qed qed lemma higman: assumes "almost_full_on P A" shows "almost_full_on (list_emb P) (lists A)" proof interpret minimal_element strict_suffix "lists A" by (unfold_locales) (intro po_on_strict_suffix wfp_on_strict_suffix)+ fix f presume "f \ SEQ (lists A)" with qo_on_LEXEQ [OF po_on_imp_transp_on [OF po_on_strict_suffix]] and dc_on_LEXEQ and open_on_good show "good (list_emb P) f" proof (induct rule: open_induct_on) case (less f) define h where "h i = hd (f i)" for i show ?case proof (cases "\i. f i = []") case False then have ne: "\i. f i \ []" by auto with \f \ SEQ (lists A)\ have "\i. h i \ A" by (auto simp: h_def ne_lists) from almost_full_on_imp_homogeneous_subseq [OF assms this] obtain \ :: "nat \ nat" where mono: "\i j. i < j \ \ i < \ j" and P: "\i j. i < j \ P (h (\ i)) (h (\ j))" by blast define f' where "f' i = (if i < \ 0 then f i else tl (f (\ (i - \ 0))))" for i have f': "f' \ SEQ (lists A)" using ne and \f \ SEQ (lists A)\ by (auto simp: f'_def dest: list.set_sel) have [simp]: "\i. \ 0 \ i \ h (\ (i - \ 0)) # f' i = f (\ (i - \ 0))" "\i. i < \ 0 \ f' i = f i" using ne by (auto simp: f'_def h_def) moreover have "strict_suffix (f' (\ 0)) (f (\ 0))" using ne by (auto simp: f'_def) ultimately have "LEX strict_suffix f' f" by (auto simp: LEX_def) with LEX_imp_not_LEX [OF this] have "strict (LEXEQ strict_suffix) f' f" using po_on_strict_suffix [of UNIV] unfolding po_on_def irreflp_on_def transp_on_def by blast from less(2) [OF f' this] have "good (list_emb P) f'" . then obtain i j where "i < j" and emb: "list_emb P (f' i) (f' j)" by (auto simp: good_def) consider "j < \ 0" | "\ 0 \ i" | "i < \ 0" and "\ 0 \ j" by arith then show ?thesis proof (cases) case 1 with \i < j\ and emb show ?thesis by (auto simp: good_def) next case 2 with \i < j\ and P have "P (h (\ (i - \ 0))) (h (\ (j - \ 0)))" by auto with emb have "list_emb P (h (\ (i - \ 0)) # f' i) (h (\ (j - \ 0)) # f' j)" by auto then have "list_emb P (f (\ (i - \ 0))) (f (\ (j - \ 0)))" using 2 and \i < j\ by auto moreover with 2 and \i have "\ (i - \ 0) < \ (j - \ 0)" using mono by auto ultimately show ?thesis by (auto simp: good_def) next case 3 with emb have "list_emb P (f i) (f' j)" by auto moreover have "f (\ (j - \ 0)) = h (\ (j - \ 0)) # f' j" using 3 by auto ultimately have "list_emb P (f i) (f (\ (j - \ 0)))" by auto moreover have "i < \ (j - \ 0)" using mono [of 0 "j - \ 0"] and 3 by force ultimately show ?thesis by (auto simp: good_def) qed qed auto qed qed blast end diff --git a/thys/Well_Quasi_Orders/Kruskal.thy b/thys/Well_Quasi_Orders/Kruskal.thy --- a/thys/Well_Quasi_Orders/Kruskal.thy +++ b/thys/Well_Quasi_Orders/Kruskal.thy @@ -1,187 +1,187 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Kruskal's Tree Theorem\ theory Kruskal imports Well_Quasi_Orders begin locale kruskal_tree = fixes F :: "('b \ nat) set" and mk :: "'b \ 'a list \ ('a::size)" and root :: "'a \ 'b \ nat" and args :: "'a \ 'a list" and trees :: "'a set" assumes size_arg: "t \ trees \ s \ set (args t) \ size s < size t" and root_mk: "(f, length ts) \ F \ root (mk f ts) = (f, length ts)" and args_mk: "(f, length ts) \ F \ args (mk f ts) = ts" and mk_root_args: "t \ trees \ mk (fst (root t)) (args t) = t" and trees_root: "t \ trees \ root t \ F" and trees_arity: "t \ trees \ length (args t) = snd (root t)" and trees_args: "\s. t \ trees \ s \ set (args t) \ s \ trees" begin lemma mk_inject [iff]: assumes "(f, length ss) \ F" and "(g, length ts) \ F" shows "mk f ss = mk g ts \ f = g \ ss = ts" proof - { assume "mk f ss = mk g ts" then have "root (mk f ss) = root (mk g ts)" and "args (mk f ss) = args (mk g ts)" by auto } show ?thesis using root_mk [OF assms(1)] and root_mk [OF assms(2)] and args_mk [OF assms(1)] and args_mk [OF assms(2)] by auto qed inductive emb for P where arg: "\(f, m) \ F; length ts = m; \t\set ts. t \ trees; t \ set ts; emb P s t\ \ emb P s (mk f ts)" | list_emb: "\(f, m) \ F; (g, n) \ F; length ss = m; length ts = n; \s \ set ss. s \ trees; \t \ set ts. t \ trees; P (f, m) (g, n); list_emb (emb P) ss ts\ \ emb P (mk f ss) (mk g ts)" monos list_emb_mono lemma almost_full_on_trees: assumes "almost_full_on P F" shows "almost_full_on (emb P) trees" (is "almost_full_on ?P ?A") proof (rule ccontr) interpret mbs ?A . assume "\ ?thesis" from mbs' [OF this] obtain m where bad: "m \ BAD ?P" and min: "\g. (m, g) \ gseq \ good ?P g" .. then have trees: "\i. m i \ trees" by auto define r where "r i = root (m i)" for i define a where "a i = args (m i)" for i define S where "S = \{set (a i) | i. True}" have m: "\i. m i = mk (fst (r i)) (a i)" by (simp add: r_def a_def mk_root_args [OF trees]) have lists: "\i. a i \ lists S" by (auto simp: a_def S_def) have arity: "\i. length (a i) = snd (r i)" using trees_arity [OF trees] by (auto simp: r_def a_def) then have sig: "\i. (fst (r i), length (a i)) \ F" using trees_root [OF trees] by (auto simp: a_def r_def) have a_trees: "\i. \t \ set (a i). t \ trees" by (auto simp: a_def trees_args [OF trees]) have "almost_full_on ?P S" proof (rule ccontr) assume "\ ?thesis" then obtain s :: "nat \ 'a" where S: "\i. s i \ S" and bad_s: "bad ?P s" by (auto simp: almost_full_on_def) define n where "n = (LEAST n. \k. s k \ set (a n))" have "\n. \k. s k \ set (a n)" using S by (force simp: S_def) from LeastI_ex [OF this] obtain k where sk: "s k \ set (a n)" by (auto simp: n_def) have args: "\k. \m \ n. s k \ set (a m)" using S by (auto simp: S_def) (metis Least_le n_def) define m' where "m' i = (if i < n then m i else s (k + (i - n)))" for i have m'_less: "\i. i < n \ m' i = m i" by (simp add: m'_def) have m'_geq: "\i. i \ n \ m' i = s (k + (i - n))" by (simp add: m'_def) have "bad ?P m'" proof assume "good ?P m'" then obtain i j where "i < j" and emb: "?P (m' i) (m' j)" by auto { assume "j < n" with \i < j\ and emb have "?P (m i) (m j)" by (auto simp: m'_less) with \i < j\ and bad have False by blast } moreover { assume "n \ i" with \i < j\ and emb have "?P (s (k + (i - n))) (s (k + (j - n)))" and "k + (i - n) < k + (j - n)" by (auto simp: m'_geq) with bad_s have False by auto } moreover { assume "i < n" and "n \ j" with \i < j\ and emb have *: "?P (m i) (s (k + (j - n)))" by (auto simp: m'_less m'_geq) with args obtain l where "l \ n" and **: "s (k + (j - n)) \ set (a l)" by blast from emb.arg [OF sig [of l] _ a_trees [of l] ** *] have "?P (m i) (m l)" by (simp add: m) moreover have "i < l" using \i < n\ and \n \ l\ by auto ultimately have False using bad by blast } ultimately show False using \i < j\ by arith qed moreover have "(m, m') \ gseq" proof - have "m \ SEQ ?A" using trees by auto moreover have "m' \ SEQ ?A" using trees and S and trees_args [OF trees] by (auto simp: m'_def a_def S_def) moreover have "\i < n. m i = m' i" by (auto simp: m'_less) moreover have "size (m' n) < size (m n)" using sk and size_arg [OF trees, unfolded m] by (auto simp: m m'_geq root_mk [OF sig] args_mk [OF sig]) ultimately show ?thesis by (auto simp: gseq_def) qed ultimately show False using min by blast qed from almost_full_on_lists [OF this, THEN almost_full_on_imp_homogeneous_subseq, OF lists] obtain \ :: "nat \ nat" where less: "\i j. i < j \ \ i < \ j" and lemb: "\i j. i < j \ list_emb ?P (a (\ i)) (a (\ j))" by blast have roots: "\i. r (\ i) \ F" using trees [THEN trees_root] by (auto simp: r_def) then have "r \ \ \ SEQ F" by auto with assms have "good P (r \ \)" by (auto simp: almost_full_on_def) then obtain i j where "i < j" and "P (r (\ i)) (r (\ j))" by auto with lemb [OF \i < j\] have "?P (m (\ i)) (m (\ j))" using sig and arity and a_trees by (auto simp: m intro!: emb.list_emb) with less [OF \i < j\] and bad show False by blast qed inductive_cases emb_mk2 [consumes 1, case_names arg list_emb]: "emb P s (mk g ts)" inductive_cases list_emb_Nil2_cases: "list_emb P xs []" and list_emb_Cons_cases: "list_emb P xs (y#ys)" lemma list_emb_trans_right: assumes "list_emb P xs ys" and "list_emb (\y z. P y z \ (\x. P x y \ P x z)) ys zs" shows "list_emb P xs zs" using assms(2, 1) by (induct arbitrary: xs) (auto elim!: list_emb_Nil2_cases list_emb_Cons_cases) lemma emb_trans: assumes trans: "\f g h. f \ F \ g \ F \ h \ F \ P f g \ P g h \ P f h" assumes "emb P s t" and "emb P t u" shows "emb P s u" using assms(3, 2) proof (induct arbitrary: s) case (arg f m ts v) then show ?case by (auto intro: emb.arg) next case (list_emb f m g n ss ts) note IH = this from \emb P s (mk f ss)\ show ?case proof (cases rule: emb_mk2) case arg then show ?thesis using IH by (auto elim!: list_emb_set intro: emb.arg) next case list_emb then show ?thesis using IH by (auto intro: emb.intros dest: trans list_emb_trans_right) qed qed lemma transp_on_emb: - assumes "transp_on P F" - shows "transp_on (emb P) trees" + assumes "transp_on F P" + shows "transp_on trees (emb P)" using assms and emb_trans [of P] unfolding transp_on_def by blast lemma kruskal: assumes "wqo_on P F" shows "wqo_on (emb P) trees" using almost_full_on_trees [of P] and assms by (metis transp_on_emb wqo_on_def) end end diff --git a/thys/Well_Quasi_Orders/Multiset_Extension.thy b/thys/Well_Quasi_Orders/Multiset_Extension.thy --- a/thys/Well_Quasi_Orders/Multiset_Extension.thy +++ b/thys/Well_Quasi_Orders/Multiset_Extension.thy @@ -1,623 +1,623 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Multiset Extension of Orders (as Binary Predicates)\ (*TODO: move theory (and maybe rename)*) theory Multiset_Extension imports Open_Induction.Restricted_Predicates "HOL-Library.Multiset" begin definition multisets :: "'a set \ 'a multiset set" where "multisets A = {M. set_mset M \ A}" lemma in_multisets_iff: "M \ multisets A \ set_mset M \ A" by (simp add: multisets_def) lemma empty_multisets [simp]: "{#} \ multisets F" by (simp add: in_multisets_iff) lemma multisets_union [simp]: "M \ multisets A \ N \ multisets A \ M + N \ multisets A" by (auto simp add: in_multisets_iff) definition mulex1 :: "('a \ 'a \ bool) \ 'a multiset \ 'a multiset \ bool" where "mulex1 P = (\M N. (M, N) \ mult1 {(x, y). P x y})" lemma mulex1_empty [iff]: "mulex1 P M {#} \ False" using not_less_empty [of M "{(x, y). P x y}"] by (auto simp: mulex1_def) lemma mulex1_add: "mulex1 P N (M0 + {#a#}) \ (\M. mulex1 P M M0 \ N = M + {#a#}) \ (\K. (\b. b \# K \ P b a) \ N = M0 + K)" using less_add [of N a M0 "{(x, y). P x y}"] by (auto simp: mulex1_def) lemma mulex1_self_add_right [simp]: "mulex1 P A (add_mset a A)" proof - let ?R = "{(x, y). P x y}" thm mult1_def have "A + {#a#} = A + {#a#}" by simp moreover have "A = A + {#}" by simp moreover have "\b. b \# {#} \ (b, a) \ ?R" by simp ultimately have "(A, add_mset a A) \ mult1 ?R" unfolding mult1_def by blast then show ?thesis by (simp add: mulex1_def) qed lemma empty_mult1 [simp]: "({#}, {#a#}) \ mult1 R" proof - have "{#a#} = {#} + {#a#}" by simp moreover have "{#} = {#} + {#}" by simp moreover have "\b. b \# {#} \ (b, a) \ R" by simp ultimately show ?thesis unfolding mult1_def by force qed lemma empty_mulex1 [simp]: "mulex1 P {#} {#a#}" using empty_mult1 [of a "{(x, y). P x y}"] by (simp add: mulex1_def) definition mulex_on :: "('a \ 'a \ bool) \ 'a set \ 'a multiset \ 'a multiset \ bool" where "mulex_on P A = (restrict_to (mulex1 P) (multisets A))\<^sup>+\<^sup>+" abbreviation mulex :: "('a \ 'a \ bool) \ 'a multiset \ 'a multiset \ bool" where "mulex P \ mulex_on P UNIV" lemma mulex_on_induct [consumes 1, case_names base step, induct pred: mulex_on]: assumes "mulex_on P A M N" and "\M N. \M \ multisets A; N \ multisets A; mulex1 P M N\ \ Q M N" and "\L M N. \mulex_on P A L M; Q L M; N \ multisets A; mulex1 P M N\ \ Q L N" shows "Q M N" using assms unfolding mulex_on_def by (induct) blast+ lemma mulex_on_self_add_singleton_right [simp]: assumes "a \ A" and "M \ multisets A" shows "mulex_on P A M (add_mset a M)" proof - have "mulex1 P M (M + {#a#})" by simp with assms have "restrict_to (mulex1 P) (multisets A) M (add_mset a M)" by (auto simp: multisets_def) then show ?thesis unfolding mulex_on_def by blast qed lemma singleton_multisets [iff]: "{#x#} \ multisets A \ x \ A" by (auto simp: multisets_def) lemma union_multisetsD: assumes "M + N \ multisets A" shows "M \ multisets A \ N \ multisets A" using assms by (auto simp: multisets_def) lemma mulex_on_multisetsD [dest]: assumes "mulex_on P F M N" shows "M \ multisets F" and "N \ multisets F" using assms by (induct) auto lemma union_multisets_iff [iff]: "M + N \ multisets A \ M \ multisets A \ N \ multisets A" by (auto dest: union_multisetsD) lemma add_mset_multisets_iff [iff]: "add_mset a M \ multisets A \ a \ A \ M \ multisets A" unfolding add_mset_add_single[of a M] union_multisets_iff by auto lemma mulex_on_trans: "mulex_on P A L M \ mulex_on P A M N \ mulex_on P A L N" by (auto simp: mulex_on_def) lemma transp_on_mulex_on: - "transp_on (mulex_on P A) B" + "transp_on B (mulex_on P A)" using mulex_on_trans [of P A] by (auto simp: transp_on_def) lemma mulex_on_add_right [simp]: assumes "mulex_on P A M N" and "a \ A" shows "mulex_on P A M (add_mset a N)" proof - from assms have "a \ A" and "N \ multisets A" by auto then have "mulex_on P A N (add_mset a N)" by simp with \mulex_on P A M N\ show ?thesis by (rule mulex_on_trans) qed lemma empty_mulex_on [simp]: assumes "M \ {#}" and "M \ multisets A" shows "mulex_on P A {#} M" using assms proof (induct M) case (add a M) show ?case proof (cases "M = {#}") assume "M = {#}" with add show ?thesis by (auto simp: mulex_on_def) next assume "M \ {#}" with add show ?thesis by (auto intro: mulex_on_trans) qed qed simp lemma mulex_on_self_add_right [simp]: assumes "M \ multisets A" and "K \ multisets A" and "K \ {#}" shows "mulex_on P A M (M + K)" using assms proof (induct K) case empty then show ?case by (cases "K = {#}") auto next case (add a M) show ?case proof (cases "M = {#}") assume "M = {#}" with add show ?thesis by auto next assume "M \ {#}" with add show ?thesis by (auto dest: mulex_on_add_right simp add: ac_simps) qed qed lemma mult1_singleton [iff]: "({#x#}, {#y#}) \ mult1 R \ (x, y) \ R" proof assume "(x, y) \ R" then have "{#y#} = {#} + {#y#}" and "{#x#} = {#} + {#x#}" and "\b. b \# {#x#} \ (b, y) \ R" by auto then show "({#x#}, {#y#}) \ mult1 R" unfolding mult1_def by blast next assume "({#x#}, {#y#}) \ mult1 R" then obtain M0 K a where "{#y#} = add_mset a M0" and "{#x#} = M0 + K" and "\b. b \# K \ (b, a) \ R" unfolding mult1_def by blast then show "(x, y) \ R" by (auto simp: add_eq_conv_diff) qed lemma mulex1_singleton [iff]: "mulex1 P {#x#} {#y#} \ P x y" using mult1_singleton [of x y "{(x, y). P x y}"] by (simp add: mulex1_def) lemma singleton_mulex_onI: "P x y \ x \ A \ y \ A \ mulex_on P A {#x#} {#y#}" by (auto simp: mulex_on_def) lemma reflclp_mulex_on_add_right [simp]: assumes "(mulex_on P A)\<^sup>=\<^sup>= M N" and "M \ multisets A" and "a \ A" shows "mulex_on P A M (N + {#a#})" using assms by (cases "M = N") simp_all lemma reflclp_mulex_on_add_right' [simp]: assumes "(mulex_on P A)\<^sup>=\<^sup>= M N" and "M \ multisets A" and "a \ A" shows "mulex_on P A M ({#a#} + N)" using reflclp_mulex_on_add_right [OF assms] by (simp add: ac_simps) lemma mulex_on_union_right [simp]: assumes "mulex_on P F A B" and "K \ multisets F" shows "mulex_on P F A (K + B)" using assms proof (induct K) case (add a K) then have "a \ F" and "mulex_on P F A (B + K)" by (auto simp: multisets_def ac_simps) then have "mulex_on P F A ((B + K) + {#a#})" by simp then show ?case by (simp add: ac_simps) qed simp lemma mulex_on_union_right' [simp]: assumes "mulex_on P F A B" and "K \ multisets F" shows "mulex_on P F A (B + K)" using mulex_on_union_right [OF assms] by (simp add: ac_simps) text \Adapted from @{thm all_accessible} in @{theory "HOL-Library.Multiset"}.\ lemma accessible_on_mulex1_multisets: assumes wf: "wfp_on P A" shows "\M\multisets A. accessible_on (mulex1 P) (multisets A) M" proof let ?P = "mulex1 P" let ?A = "multisets A" let ?acc = "accessible_on ?P ?A" { fix M M0 a assume M0: "?acc M0" and "a \ A" and "M0 \ ?A" and wf_hyp: "\b. \b \ A; P b a\ \ (\M. ?acc (M) \ ?acc (M + {#b#}))" and acc_hyp: "\M. M \ ?A \ ?P M M0 \ ?acc (M + {#a#})" then have "add_mset a M0 \ ?A" by (auto simp: multisets_def) then have "?acc (add_mset a M0)" proof (rule accessible_onI [of "add_mset a M0"]) fix N assume "N \ ?A" and "?P N (add_mset a M0)" then have "((\M. M \ ?A \ ?P M M0 \ N = M + {#a#}) \ (\K. (\b. b \# K \ P b a) \ N = M0 + K))" using mulex1_add [of P N M0 a] by (auto simp: multisets_def) then show "?acc (N)" proof (elim exE disjE conjE) fix M assume "M \ ?A" and "?P M M0" and N: "N = M + {#a#}" from acc_hyp have "M \ ?A \ ?P M M0 \ ?acc (M + {#a#})" .. with \M \ ?A\ and \?P M M0\ have "?acc (M + {#a#})" by blast then show "?acc (N)" by (simp only: N) next fix K assume N: "N = M0 + K" assume "\b. b \# K \ P b a" moreover from N and \N \ ?A\ have "K \ ?A" by (auto simp: multisets_def) ultimately have "?acc (M0 + K)" proof (induct K) case empty from M0 show "?acc (M0 + {#})" by simp next case (add x K) from add.prems have "x \ A" and "P x a" by (auto simp: multisets_def) with wf_hyp have "\M. ?acc M \ ?acc (M + {#x#})" by blast moreover from add have "?acc (M0 + K)" by (auto simp: multisets_def) ultimately show "?acc (M0 + (add_mset x K))" by simp qed then show "?acc N" by (simp only: N) qed qed } note tedious_reasoning = this fix M assume "M \ ?A" then show "?acc M" proof (induct M) show "?acc {#}" proof (rule accessible_onI) show "{#} \ ?A" by (auto simp: multisets_def) next fix b assume "?P b {#}" then show "?acc b" by simp qed next case (add a M) then have "?acc M" by (auto simp: multisets_def) from add have "a \ A" by (auto simp: multisets_def) with wf have "\M. ?acc M \ ?acc (add_mset a M)" proof (induct) case (less a) then have r: "\b. \b \ A; P b a\ \ (\M. ?acc M \ ?acc (M + {#b#}))" by auto show "\M. ?acc M \ ?acc (add_mset a M)" proof (intro allI impI) fix M' assume "?acc M'" moreover then have "M' \ ?A" by (blast dest: accessible_on_imp_mem) ultimately show "?acc (add_mset a M')" by (induct) (rule tedious_reasoning [OF _ \a \ A\ _ r], auto) qed qed with \?acc (M)\ show "?acc (add_mset a M)" by blast qed qed lemmas wfp_on_mulex1_multisets = accessible_on_mulex1_multisets [THEN accessible_on_imp_wfp_on] lemmas irreflp_on_mulex1 = wfp_on_mulex1_multisets [THEN wfp_on_imp_irreflp_on] lemma wfp_on_mulex_on_multisets: assumes "wfp_on P A" shows "wfp_on (mulex_on P A) (multisets A)" using wfp_on_mulex1_multisets [OF assms] by (simp only: mulex_on_def wfp_on_restrict_to_tranclp_wfp_on_conv) lemmas irreflp_on_mulex_on = wfp_on_mulex_on_multisets [THEN wfp_on_imp_irreflp_on] lemma mulex1_union: "mulex1 P M N \ mulex1 P (K + M) (K + N)" by (auto simp: mulex1_def mult1_union) lemma mulex_on_union: assumes "mulex_on P A M N" and "K \ multisets A" shows "mulex_on P A (K + M) (K + N)" using assms proof (induct) case (base M N) then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union) moreover from base have "(K + M) \ multisets A" and "(K + N) \ multisets A" by (auto simp: multisets_def) ultimately have "restrict_to (mulex1 P) (multisets A) (K + M) (K + N)" by auto then show ?case by (auto simp: mulex_on_def) next case (step L M N) then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union) moreover from step have "(K + M) \ multisets A" and "(K + N) \ multisets A" by blast+ ultimately have "(restrict_to (mulex1 P) (multisets A))\<^sup>+\<^sup>+ (K + M) (K + N)" by auto moreover have "mulex_on P A (K + L) (K + M)" using step by blast ultimately show ?case by (auto simp: mulex_on_def) qed lemma mulex_on_union': assumes "mulex_on P A M N" and "K \ multisets A" shows "mulex_on P A (M + K) (N + K)" using mulex_on_union [OF assms] by (simp add: ac_simps) lemma mulex_on_add_mset: assumes "mulex_on P A M N" and "m \ A" shows "mulex_on P A (add_mset m M) (add_mset m N)" unfolding add_mset_add_single[of m M] add_mset_add_single[of m N] apply (rule mulex_on_union') using assms by auto lemma union_mulex_on_mono: "mulex_on P F A C \ mulex_on P F B D \ mulex_on P F (A + B) (C + D)" by (metis mulex_on_multisetsD mulex_on_trans mulex_on_union mulex_on_union') lemma mulex_on_add_mset': assumes "P m n" and "m \ A" and "n \ A" and "M \ multisets A" shows "mulex_on P A (add_mset m M) (add_mset n M)" unfolding add_mset_add_single[of m M] add_mset_add_single[of n M] apply (rule mulex_on_union) using assms by (auto simp: mulex_on_def) lemma mulex_on_add_mset_mono: assumes "P m n" and "m \ A" and "n \ A" and "mulex_on P A M N" shows "mulex_on P A (add_mset m M) (add_mset n N)" unfolding add_mset_add_single[of m M] add_mset_add_single[of n N] apply (rule union_mulex_on_mono) using assms by (auto simp: mulex_on_def) lemma union_mulex_on_mono1: "A \ multisets F \ (mulex_on P F)\<^sup>=\<^sup>= A C \ mulex_on P F B D \ mulex_on P F (A + B) (C + D)" by (auto intro: union_mulex_on_mono mulex_on_union) lemma union_mulex_on_mono2: "B \ multisets F \ mulex_on P F A C \ (mulex_on P F)\<^sup>=\<^sup>= B D \ mulex_on P F (A + B) (C + D)" by (auto intro: union_mulex_on_mono mulex_on_union') lemma mult1_mono: assumes "\x y. \x \ A; y \ A; (x, y) \ R\ \ (x, y) \ S" and "M \ multisets A" and "N \ multisets A" and "(M, N) \ mult1 R" shows "(M, N) \ mult1 S" using assms unfolding mult1_def multisets_def by auto (metis (full_types) subsetD) lemma mulex1_mono: assumes "\x y. \x \ A; y \ A; P x y\ \ Q x y" and "M \ multisets A" and "N \ multisets A" and "mulex1 P M N" shows "mulex1 Q M N" using mult1_mono [of A "{(x, y). P x y}" "{(x, y). Q x y}" M N] and assms unfolding mulex1_def by blast lemma mulex_on_mono: assumes *: "\x y. \x \ A; y \ A; P x y\ \ Q x y" and "mulex_on P A M N" shows "mulex_on Q A M N" proof - let ?rel = "\P. (restrict_to (mulex1 P) (multisets A))" from \mulex_on P A M N\ have "(?rel P)\<^sup>+\<^sup>+ M N" by (simp add: mulex_on_def) then have "(?rel Q)\<^sup>+\<^sup>+ M N" proof (induct rule: tranclp.induct) case (r_into_trancl M N) then have "M \ multisets A" and "N \ multisets A" by auto from mulex1_mono [OF * this] and r_into_trancl show ?case by auto next case (trancl_into_trancl L M N) then have "M \ multisets A" and "N \ multisets A" by auto from mulex1_mono [OF * this] and trancl_into_trancl have "?rel Q M N" by auto with \(?rel Q)\<^sup>+\<^sup>+ L M\ show ?case by (rule tranclp.trancl_into_trancl) qed then show ?thesis by (simp add: mulex_on_def) qed lemma mult1_reflcl: assumes "(M, N) \ mult1 R" shows "(M, N) \ mult1 (R\<^sup>=)" using assms by (auto simp: mult1_def) lemma mulex1_reflclp: assumes "mulex1 P M N" shows "mulex1 (P\<^sup>=\<^sup>=) M N" using mulex1_mono [of UNIV P "P\<^sup>=\<^sup>=" M N, OF _ _ _ assms] by (auto simp: multisets_def) lemma mulex_on_reflclp: assumes "mulex_on P A M N" shows "mulex_on (P\<^sup>=\<^sup>=) A M N" using mulex_on_mono [OF _ assms, of "P\<^sup>=\<^sup>="] by auto lemma surj_on_multisets_mset: "\M\multisets A. \xs\lists A. M = mset xs" proof fix M assume "M \ multisets A" then show "\xs\lists A. M = mset xs" proof (induct M) case empty show ?case by simp next case (add a M) then obtain xs where "xs \ lists A" and "M = mset xs" by auto then have "add_mset a M = mset (a # xs)" by simp moreover have "a # xs \ lists A" using \xs \ lists A\ and add by auto ultimately show ?case by blast qed qed lemma image_mset_lists [simp]: "mset ` lists A = multisets A" using surj_on_multisets_mset [of A] by auto (metis mem_Collect_eq multisets_def set_mset_mset subsetI) lemma multisets_UNIV [simp]: "multisets UNIV = UNIV" by (metis image_mset_lists lists_UNIV surj_mset) lemma non_empty_multiset_induct [consumes 1, case_names singleton add]: assumes "M \ {#}" and "\x. P {#x#}" and "\x M. P M \ P (add_mset x M)" shows "P M" using assms by (induct M) auto lemma mulex_on_all_strict: assumes "X \ {#}" assumes "X \ multisets A" and "Y \ multisets A" and *: "\y. y \# Y \ (\x. x \# X \ P y x)" shows "mulex_on P A Y X" using assms proof (induction X arbitrary: Y rule: non_empty_multiset_induct) case (singleton x) then have "mulex1 P Y {#x#}" unfolding mulex1_def mult1_def by auto with singleton show ?case by (auto simp: mulex_on_def) next case (add x M) let ?Y = "{# y \# Y. \x. x \# M \ P y x #}" let ?Z = "Y - ?Y" have Y: "Y = ?Z + ?Y" by (subst multiset_eq_iff) auto from \Y \ multisets A\ have "?Y \ multisets A" by (metis multiset_partition union_multisets_iff) moreover have "\y. y \# ?Y \ (\x. x \# M \ P y x)" by auto moreover have "M \ multisets A" using add by auto ultimately have "mulex_on P A ?Y M" using add by blast moreover have "mulex_on P A ?Z {#x#}" proof - have "{#x#} = {#} + {#x#}" by simp moreover have "?Z = {#} + ?Z" by simp moreover have "\y. y \# ?Z \ P y x" using add.prems by (auto simp add: in_diff_count split: if_splits) ultimately have "mulex1 P ?Z {#x#}" unfolding mulex1_def mult1_def by blast moreover have "{#x#} \ multisets A" using add.prems by auto moreover have "?Z \ multisets A" using \Y \ multisets A\ by (metis diff_union_cancelL multiset_partition union_multisetsD) ultimately show ?thesis by (auto simp: mulex_on_def) qed ultimately have "mulex_on P A (?Y + ?Z) (M + {#x#})" by (rule union_mulex_on_mono) then show ?case using Y by (simp add: ac_simps) qed text \The following lemma shows that the textbook definition (e.g., ``Term Rewriting and All That'') is the same as the one used below.\ lemma diff_set_Ex_iff: "X \ {#} \ X \# M \ N = (M - X) + Y \ X \ {#} \ (\Z. M = Z + X \ N = Z + Y)" by (auto) (metis add_diff_cancel_left' multiset_diff_union_assoc union_commute) text \Show that @{const mulex_on} is equivalent to the textbook definition of multiset-extension for transitive base orders.\ lemma mulex_on_alt_def: - assumes trans: "transp_on P A" + assumes trans: "transp_on A P" shows "mulex_on P A M N \ M \ multisets A \ N \ multisets A \ (\X Y Z. X \ {#} \ N = Z + X \ M = Z + Y \ (\y. y \# Y \ (\x. x \# X \ P y x)))" (is "?P M N \ ?Q M N") proof assume "?P M N" then show "?Q M N" proof (induct M N) case (base M N) then obtain a M0 K where N: "N = M0 + {#a#}" and M: "M = M0 + K" and *: "\b. b \# K \ P b a" and "M \ multisets A" and "N \ multisets A" by (auto simp: mulex1_def mult1_def) moreover then have "{#a#} \ multisets A" and "K \ multisets A" by auto moreover have "{#a#} \ {#}" by auto moreover have "N = M0 + {#a#}" by fact moreover have "M = M0 + K" by fact moreover have "\y. y \# K \ (\x. x \# {#a#} \ P y x)" using * by auto ultimately show ?case by blast next case (step L M N) then obtain X Y Z where "L \ multisets A" and "M \ multisets A" and "N \ multisets A" and "X \ multisets A" and "Y \ multisets A" and M: "M = Z + X" and L: "L = Z + Y" and "X \ {#}" and Y: "\y. y \# Y \ (\x. x \# X \ P y x)" and "mulex1 P M N" by blast from \mulex1 P M N\ obtain a M0 K where N: "N = add_mset a M0" and M': "M = M0 + K" and *: "\b. b \# K \ P b a" unfolding mulex1_def mult1_def by blast have L': "L = (M - X) + Y" by (simp add: L M) have K: "\y. y \# K \ (\x. x \# {#a#} \ P y x)" using * by auto txt \The remainder of the proof is adapted from the proof of Lemma 2.5.4. of the book ``Term Rewriting and All That.''\ let ?X = "add_mset a (X - K)" let ?Y = "(K - X) + Y" have "L \ multisets A" and "N \ multisets A" by fact+ moreover have "?X \ {#} \ (\Z. N = Z + ?X \ L = Z + ?Y)" proof - have "?X \ {#}" by auto moreover have "?X \# N" using M N M' by (simp add: add.commute [of "{#a#}"]) (metis Multiset.diff_subset_eq_self add.commute add_diff_cancel_right) moreover have "L = (N - ?X) + ?Y" proof (rule multiset_eqI) fix x :: 'a let ?c = "\M. count M x" let ?ic = "\x. int (?c x)" from \?X \# N\ have *: "?c {#a#} + ?c (X - K) \ ?c N" by (auto simp add: subseteq_mset_def split: if_splits) from * have **: "?c (X - K) \ ?c M0" unfolding N by (auto split: if_splits) have "?ic (N - ?X + ?Y) = int (?c N - ?c ?X) + ?ic ?Y" by simp also have "\ = int (?c N - (?c {#a#} + ?c (X - K))) + ?ic (K - X) + ?ic Y" by simp also have "\ = ?ic N - (?ic {#a#} + ?ic (X - K)) + ?ic (K - X) + ?ic Y" using of_nat_diff [OF *] by simp also have "\ = (?ic N - ?ic {#a#}) - ?ic (X - K) + ?ic (K - X) + ?ic Y" by simp also have "\ = (?ic N - ?ic {#a#}) + (?ic (K - X) - ?ic (X - K)) + ?ic Y" by simp also have "\ = (?ic N - ?ic {#a#}) + (?ic K - ?ic X) + ?ic Y" by simp also have "\ = (?ic N - ?ic ?X) + ?ic ?Y" by (simp add: N) also have "\ = ?ic L" unfolding L' M' N using ** by (simp add: algebra_simps) finally show "?c L = ?c (N - ?X + ?Y)" by simp qed ultimately show ?thesis by (metis diff_set_Ex_iff) qed moreover have "\y. y \# ?Y \ (\x. x \# ?X \ P y x)" proof (intro allI impI) fix y assume "y \# ?Y" then have "y \# K - X \ y \# Y" by auto then show "\x. x \# ?X \ P y x" proof assume "y \# K - X" then have "y \# K" by (rule in_diffD) with K show ?thesis by auto next assume "y \# Y" with Y obtain x where "x \# X" and "P y x" by blast { assume "x \# X - K" with \P y x\ have ?thesis by auto } moreover { assume "x \# K" with * have "P x a" by auto moreover have "y \ A" using \Y \ multisets A\ and \y \# Y\ by (auto simp: multisets_def) moreover have "a \ A" using \N \ multisets A\ by (auto simp: N) moreover have "x \ A" using \M \ multisets A\ and \x \# K\ by (auto simp: M' multisets_def) ultimately have "P y a" using \P y x\ and trans unfolding transp_on_def by blast then have ?thesis by force } moreover from \x \# X\ have "x \# X - K \ x \# K" by (auto simp add: in_diff_count not_in_iff) ultimately show ?thesis by auto qed qed ultimately show ?case by blast qed next assume "?Q M N" then obtain X Y Z where "M \ multisets A" and "N \ multisets A" and "X \ {#}" and N: "N = Z + X" and M: "M = Z + Y" and *: "\y. y \# Y \ (\x. x \# X \ P y x)" by blast with mulex_on_all_strict [of X A Y] have "mulex_on P A Y X" by auto moreover from \N \ multisets A\ have "Z \ multisets A" by (auto simp: N) ultimately show "?P M N" unfolding M N by (metis mulex_on_union) qed end diff --git a/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy b/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy --- a/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy +++ b/thys/Well_Quasi_Orders/Well_Quasi_Orders.thy @@ -1,317 +1,317 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Well-Quasi-Orders\ theory Well_Quasi_Orders imports Almost_Full_Relations begin subsection \Basic Definitions\ definition wqo_on :: "('a \ 'a \ bool) \ 'a set \ bool" where - "wqo_on P A \ transp_on P A \ almost_full_on P A" + "wqo_on P A \ transp_on A P \ almost_full_on P A" lemma wqo_on_UNIV: "wqo_on (\_ _. True) UNIV" using almost_full_on_UNIV by (auto simp: wqo_on_def transp_on_def) lemma wqo_onI [Pure.intro]: - "\transp_on P A; almost_full_on P A\ \ wqo_on P A" + "\transp_on A P; almost_full_on P A\ \ wqo_on P A" unfolding wqo_on_def almost_full_on_def by blast lemma wqo_on_imp_reflp_on: "wqo_on P A \ reflp_on A P" using almost_full_on_imp_reflp_on by (auto simp: wqo_on_def) lemma wqo_on_imp_transp_on: - "wqo_on P A \ transp_on P A" + "wqo_on P A \ transp_on A P" by (auto simp: wqo_on_def) lemma wqo_on_imp_almost_full_on: "wqo_on P A \ almost_full_on P A" by (auto simp: wqo_on_def) lemma wqo_on_imp_qo_on: "wqo_on P A \ qo_on P A" by (metis qo_on_def wqo_on_imp_reflp_on wqo_on_imp_transp_on) lemma wqo_on_imp_good: "wqo_on P A \ \i. f i \ A \ good P f" by (auto simp: wqo_on_def almost_full_on_def) lemma wqo_on_subset: "A \ B \ wqo_on P B \ wqo_on P A" using almost_full_on_subset [of A B P] - and transp_on_subset [of A B P] + and transp_on_subset [of B P A] unfolding wqo_on_def by blast subsection \Equivalent Definitions\ text \ Given a quasi-order @{term P}, the following statements are equivalent: \begin{enumerate} \item @{term P} is a almost-full. \item @{term P} does neither allow decreasing chains nor antichains. \item Every quasi-order extending @{term P} is well-founded. \end{enumerate} \ lemma wqo_af_conv: assumes "qo_on P A" shows "wqo_on P A \ almost_full_on P A" using assms by (metis qo_on_def wqo_on_def) lemma wqo_wf_and_no_antichain_conv: assumes "qo_on P A" shows "wqo_on P A \ wfp_on (strict P) A \ \ (\f. antichain_on P f A)" unfolding wqo_af_conv [OF assms] using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]] and almost_full_on_imp_no_antichain_on [of P A] and wf_and_no_antichain_imp_qo_extension_wf [of P A] and every_qo_extension_wf_imp_af [OF _ assms] by blast lemma wqo_extensions_wf_conv: assumes "qo_on P A" shows "wqo_on P A \ (\Q. (\x\A. \y\A. P x y \ Q x y) \ qo_on Q A \ wfp_on (strict Q) A)" unfolding wqo_af_conv [OF assms] using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]] and almost_full_on_imp_no_antichain_on [of P A] and wf_and_no_antichain_imp_qo_extension_wf [of P A] and every_qo_extension_wf_imp_af [OF _ assms] by blast lemma wqo_on_imp_wfp_on: "wqo_on P A \ wfp_on (strict P) A" by (metis (no_types) wqo_on_imp_qo_on wqo_wf_and_no_antichain_conv) text \ The homomorphic image of a wqo set is wqo. \ lemma wqo_on_hom: - assumes "transp_on Q (h ` A)" + assumes "transp_on (h ` A) Q" and "\x\A. \y\A. P x y \ Q (h x) (h y)" and "wqo_on P A" shows "wqo_on Q (h ` A)" using assms and almost_full_on_hom [of A P Q h] unfolding wqo_on_def by blast text \ The monomorphic preimage of a wqo set is wqo. \ lemma wqo_on_mon: assumes *: "\x\A. \y\A. P x y \ Q (h x) (h y)" and bij: "bij_betw h A B" and wqo: "wqo_on Q B" shows "wqo_on P A" proof - - have "transp_on P A" - proof + have "transp_on A P" + proof (rule transp_onI) fix x y z assume [intro!]: "x \ A" "y \ A" "z \ A" and "P x y" and "P y z" with * have "Q (h x) (h y)" and "Q (h y) (h z)" by blast+ with wqo_on_imp_transp_on [OF wqo] have "Q (h x) (h z)" using bij by (auto simp: bij_betw_def transp_on_def) with * show "P x z" by blast qed with assms and almost_full_on_mon [of A P Q h] show ?thesis unfolding wqo_on_def by blast qed subsection \A Type Class for Well-Quasi-Orders\ text \ In a well-quasi-order (wqo) every infinite sequence is good. \ class wqo = preorder + assumes good: "good (\) f" lemma wqo_on_class [simp, intro]: "wqo_on (\) (UNIV :: ('a :: wqo) set)" using good by (auto simp: wqo_on_def transp_on_def almost_full_on_def dest: order_trans) lemma wqo_on_UNIV_class_wqo [intro!]: "wqo_on P UNIV \ class.wqo P (strict P)" by (unfold_locales) (auto simp: wqo_on_def almost_full_on_def, unfold transp_on_def, blast) text \ The following lemma converts between @{const wqo_on} (for the special case that the domain is the universe of a type) and the class predicate @{const class.wqo}. \ lemma wqo_on_UNIV_conv: "wqo_on P UNIV \ class.wqo P (strict P)" (is "?lhs = ?rhs") proof assume "?lhs" then show "?rhs" by auto next assume "?rhs" then show "?lhs" unfolding class.wqo_def class.preorder_def class.wqo_axioms_def by (auto simp: wqo_on_def almost_full_on_def transp_on_def) qed text \ The strict part of a wqo is well-founded. \ lemma (in wqo) "wfP (<)" proof - have "class.wqo (\) (<)" .. hence "wqo_on (\) UNIV" unfolding less_le_not_le [abs_def] wqo_on_UNIV_conv [symmetric] . from wqo_on_imp_wfp_on [OF this] show ?thesis unfolding less_le_not_le [abs_def] wfp_on_UNIV . qed lemma wqo_on_with_bot: assumes "wqo_on P A" shows "wqo_on (option_le P) A\<^sub>\" (is "wqo_on ?P ?A") proof - - { from assms have trans [unfolded transp_on_def]: "transp_on P A" + { from assms have trans [unfolded transp_on_def]: "transp_on A P" by (auto simp: wqo_on_def) - have "transp_on ?P ?A" + have "transp_on ?A ?P" by (auto simp: transp_on_def elim!: with_bot_cases, insert trans) blast } moreover { from assms and almost_full_on_with_bot have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) } ultimately show ?thesis by (auto simp: wqo_on_def) qed lemma wqo_on_option_UNIV [intro]: "wqo_on P UNIV \ wqo_on (option_le P) UNIV" using wqo_on_with_bot [of P UNIV] by simp text \ When two sets are wqo, then their disjoint sum is wqo. \ lemma wqo_on_Plus: assumes "wqo_on P A" and "wqo_on Q B" shows "wqo_on (sum_le P Q) (A <+> B)" (is "wqo_on ?P ?A") proof - - { from assms have trans [unfolded transp_on_def]: "transp_on P A" "transp_on Q B" + { from assms have trans [unfolded transp_on_def]: "transp_on A P" "transp_on B Q" by (auto simp: wqo_on_def) - have "transp_on ?P ?A" + have "transp_on ?A ?P" unfolding transp_on_def by (auto, insert trans) (blast+) } moreover { from assms and almost_full_on_Plus have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) } ultimately show ?thesis by (auto simp: wqo_on_def) qed lemma wqo_on_sum_UNIV [intro]: "wqo_on P UNIV \ wqo_on Q UNIV \ wqo_on (sum_le P Q) UNIV" using wqo_on_Plus [of P UNIV Q UNIV] by simp subsection \Dickson's Lemma\ lemma wqo_on_Sigma: fixes A1 :: "'a set" and A2 :: "'b set" assumes "wqo_on P1 A1" and "wqo_on P2 A2" shows "wqo_on (prod_le P1 P2) (A1 \ A2)" (is "wqo_on ?P ?A") proof - - { from assms have "transp_on P1 A1" and "transp_on P2 A2" by (auto simp: wqo_on_def) - hence "transp_on ?P ?A" unfolding transp_on_def prod_le_def by blast } + { from assms have "transp_on A1 P1" and "transp_on A2 P2" by (auto simp: wqo_on_def) + hence "transp_on ?A ?P" unfolding transp_on_def prod_le_def by blast } moreover { from assms and almost_full_on_Sigma [of P1 A1 P2 A2] have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) } ultimately show ?thesis by (auto simp: wqo_on_def) qed lemmas dickson = wqo_on_Sigma lemma wqo_on_prod_UNIV [intro]: "wqo_on P UNIV \ wqo_on Q UNIV \ wqo_on (prod_le P Q) UNIV" using wqo_on_Sigma [of P UNIV Q UNIV] by simp subsection \Higman's Lemma\ lemma transp_on_list_emb: - assumes "transp_on P A" - shows "transp_on (list_emb P) (lists A)" + assumes "transp_on A P" + shows "transp_on (lists A) (list_emb P)" using assms and list_emb_trans [of _ _ _ P] unfolding transp_on_def by blast lemma wqo_on_lists: assumes "wqo_on P A" shows "wqo_on (list_emb P) (lists A)" using assms and almost_full_on_lists and transp_on_list_emb by (auto simp: wqo_on_def) lemmas higman = wqo_on_lists lemma wqo_on_list_UNIV [intro]: "wqo_on P UNIV \ wqo_on (list_emb P) UNIV" using wqo_on_lists [of P UNIV] by simp text \ Every reflexive and transitive relation on a finite set is a wqo. \ lemma finite_wqo_on: - assumes "finite A" and refl: "reflp_on A P" and "transp_on P A" + assumes "finite A" and refl: "reflp_on A P" and "transp_on A P" shows "wqo_on P A" using assms and finite_almost_full_on by (auto simp: wqo_on_def) lemma finite_eq_wqo_on: assumes "finite A" shows "wqo_on (=) A" using finite_wqo_on [OF assms, of "(=)"] by (auto simp: reflp_on_def transp_on_def) lemma wqo_on_lists_over_finite_sets: "wqo_on (list_emb (=)) (UNIV::('a::finite) list set)" using wqo_on_lists [OF finite_eq_wqo_on [OF finite [of "UNIV::('a::finite) set"]]] by simp lemma wqo_on_map: fixes P and Q and h defines "P' \ \x y. P x y \ Q (h x) (h y)" assumes "wqo_on P A" and "wqo_on Q B" and subset: "h ` A \ B" shows "wqo_on P' A" proof let ?Q = "\x y. Q (h x) (h y)" - from \wqo_on P A\ have "transp_on P A" + from \wqo_on P A\ have "transp_on A P" by (rule wqo_on_imp_transp_on) - then show "transp_on P' A" + then show "transp_on A P'" using \wqo_on Q B\ and subset unfolding wqo_on_def transp_on_def P'_def by blast from \wqo_on P A\ have "almost_full_on P A" by (rule wqo_on_imp_almost_full_on) from \wqo_on Q B\ have "almost_full_on Q B" by (rule wqo_on_imp_almost_full_on) show "almost_full_on P' A" proof fix f assume *: "\i::nat. f i \ A" from almost_full_on_imp_homogeneous_subseq [OF \almost_full_on P A\ this] obtain g :: "nat \ nat" where g: "\i j. i < j \ g i < g j" and **: "\i. f (g i) \ A \ P (f (g i)) (f (g (Suc i)))" using * by auto - from chain_transp_on_less [OF ** \transp_on P A\] + from chain_transp_on_less [OF ** \transp_on A P\] have **: "\i j. i < j \ P (f (g i)) (f (g j))" . let ?g = "\i. h (f (g i))" from * and subset have B: "\i. ?g i \ B" by auto with \almost_full_on Q B\ [unfolded almost_full_on_def good_def, THEN bspec, of ?g] obtain i j :: nat where "i < j" and "Q (?g i) (?g j)" by blast with ** [OF \i < j\] have "P' (f (g i)) (f (g j))" by (auto simp: P'_def) with g [OF \i < j\] show "good P' f" by (auto simp: good_def) qed qed lemma wqo_on_UNIV_nat: "wqo_on (\) (UNIV :: nat set)" unfolding wqo_on_def transp_on_def using almost_full_on_UNIV_nat by simp end diff --git a/thys/Well_Quasi_Orders/Wqo_Multiset.thy b/thys/Well_Quasi_Orders/Wqo_Multiset.thy --- a/thys/Well_Quasi_Orders/Wqo_Multiset.thy +++ b/thys/Well_Quasi_Orders/Wqo_Multiset.thy @@ -1,60 +1,60 @@ (* Title: Well-Quasi-Orders Author: Christian Sternagel Maintainer: Christian Sternagel License: LGPL *) section \Multiset Extension Preserves Well-Quasi-Orders\ theory Wqo_Multiset imports Multiset_Extension Well_Quasi_Orders begin lemma list_emb_imp_reflclp_mulex_on: assumes "xs \ lists A" and "ys \ lists A" and "list_emb P xs ys" shows "(mulex_on P A)\<^sup>=\<^sup>= (mset xs) (mset ys)" using assms(3, 1, 2) proof (induct) case (list_emb_Nil ys) then show ?case by (cases ys) (auto intro!: empty_mulex_on simp: multisets_def) next case (list_emb_Cons xs ys y) then show ?case by (auto intro!: mulex_on_self_add_singleton_right simp: multisets_def) next case (list_emb_Cons2 x y xs ys) then show ?case by (force intro: union_mulex_on_mono mulex_on_add_mset mulex_on_add_mset' mulex_on_add_mset_mono simp: multisets_def) qed text \The (reflexive closure of the) multiset extension of an almost-full relation is almost-full.\ lemma almost_full_on_multisets: assumes "almost_full_on P A" shows "almost_full_on (mulex_on P A)\<^sup>=\<^sup>= (multisets A)" proof - let ?P = "(mulex_on P A)\<^sup>=\<^sup>=" from almost_full_on_hom [OF _ almost_full_on_lists, of A P ?P mset, OF list_emb_imp_reflclp_mulex_on, simplified] show ?thesis using assms by blast qed lemma wqo_on_multisets: assumes "wqo_on P A" shows "wqo_on (mulex_on P A)\<^sup>=\<^sup>= (multisets A)" proof - from transp_on_mulex_on [of P A "multisets A"] - show "transp_on (mulex_on P A)\<^sup>=\<^sup>= (multisets A)" + from transp_on_mulex_on [of "multisets A" P A] + show "transp_on (multisets A) (mulex_on P A)\<^sup>=\<^sup>=" unfolding transp_on_def by blast next from almost_full_on_multisets [OF assms [THEN wqo_on_imp_almost_full_on]] show "almost_full_on (mulex_on P A)\<^sup>=\<^sup>= (multisets A)" . qed end