Theory Decreasing_Diagrams_II_Aux

(* Title:      Decreasing Diagrams II  
   Author:     Bertram Felgenhauer (2015)
   Maintainer: Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at>
   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⇧=) = (λ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_on[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)⇧+"
  then show "x ∈ (mult1 S)⇧+"
  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 (λ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_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 *)