Quelle Wellfounded.thy Sprache: Isabelle

(*  Title:      HOL/Wellfounded.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Konrad Slind
    Author:     Alexander Krauss
    Author:     Andrei Popescu, TU Muenchen
    Author:     Martin Desharnais, MPI-INF Saarbruecken
*)

section \<open>Well-founded Recursion\<close>

theory Wellfounded
  imports Transitive_Closure
begin

subsection \<open>Basic Definitions\<close>

definition wf_on :: "'a set \ 'a rel \ bool" where
  "wf_on A r \ (\P. (\x \ A. (\y \ A. (y, x) \ r \ P y) \ P x) \ (\x \ A. P x))"

abbreviation wf :: "('a \ 'a) set \ bool" where
  "wf \ wf_on UNIV"

definition wfp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "wfp_on A R \ (\P. (\x \ A. (\y \ A. R y x \ P y) \ P x) \ (\x \ A. P x))"

abbreviation wfP :: "('a \ 'a \ bool) \ bool" where
  "wfP \ wfp_on UNIV"

alias wfp = wfP

text \<open>We keep old name \<^const>\<open>wfP\<close> for backward compatibility, but offer new name \<^const>\<open>wfp\<close> to be
consistent with similar predicates, e.g., \<^const>\<open>asymp\<close>, \<^const>\<open>transp\<close>, \<^const>\<open>totalp\<close>.\<close>

subsection \<open>Equivalence of Definitions\<close>

lemma wfp_on_wf_on_eq[pred_set_conv]: "wfp_on A (\x y. (x, y) \ r) \ wf_on A r"
  by (simp add: wfp_on_def wf_on_def)

lemma wf_def: "wf r \ (\P. (\x. (\y. (y, x) \ r \ P y) \ P x) \ (\x. P x))"
  unfolding wf_on_def by simp

lemma wfp_def: "wfp r \ wf {(x, y). r x y}"
  unfolding wf_def wfp_on_def by simp

lemma wfp_wf_eq: "wfp (\x y. (x, y) \ r) = wf r"
  using wfp_on_wf_on_eq .

subsection \<open>Induction Principles\<close>

lemma wf_on_induct[consumes 1, case_names in_set less, induct set: wf_on]:
  assumes "wf_on A r" and "x \ A" and "\x. x \ A \ (\y. y \ A \ (y, x) \ r \ P y) \ P x"
  shows "P x"
  using assms(2,3) by (auto intro: \<open>wf_on A r\<close>[unfolded wf_on_def, rule_format])

lemma wfp_on_induct[consumes 1, case_names in_set less, induct pred: wfp_on]:
  assumes "wfp_on A r" and "x \ A" and "\x. x \ A \ (\y. y \ A \ r y x \ P y) \ P x"
  shows "P x"
  using assms by (fact wf_on_induct[to_pred])

lemma wf_induct:
  assumes "wf r"
    and "\x. \y. (y, x) \ r \ P y \ P x"
  shows "P a"
  using assms by (auto intro: wf_on_induct[of UNIV])

lemmas wfp_induct = wf_induct [to_pred]

lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]

lemmas wfp_induct_rule = wf_induct_rule [to_pred, induct set: wfp]

lemma wf_on_iff_wf: "wf_on A r \ wf {(x, y) \ r. x \ A \ y \ A}"
proof (rule iffI)
  assume wf: "wf_on A r"
  show "wf {(x, y) \ r. x \ A \ y \ A}"
    unfolding wf_def
  proof (intro allI impI ballI)
    fix P x
    assume IH: "\x. (\y. (y, x) \ {(x, y). (x, y) \ r \ x \ A \ y \ A} \ P y) \ P x"
    show "P x"
    proof (cases "x \ A")
      case True
      show ?thesis
        using wf
      proof (induction x rule: wf_on_induct)
        case in_set
        thus ?case
          using True .
      next
        case (less x)
        thus ?case
          by (auto intro: IH[rule_format])
      qed
    next
      case False
      then show ?thesis
        by (auto intro: IH[rule_format])
    qed
  qed
next
  assume wf: "wf {(x, y). (x, y) \ r \ x \ A \ y \ A}"
  show "wf_on A r"
    unfolding wf_on_def
  proof (intro allI impI ballI)
    fix P x
    assume IH: "\x\A. (\y\A. (y, x) \ r \ P y) \ P x" and "x \ A"
    show "P x"
      using wf \<open>x \<in> A\<close>
    proof (induction x rule: wf_on_induct)
      case in_set
      show ?case
        by simp
    next
      case (less y)
      hence "\z. (z, y) \ r \ z \ A \ P z"
        by simp
      thus ?case
        using IH[rule_format, OF \<open>y \<in> A\<close>] by simp
    qed
  qed
qed

subsection \<open>Introduction Rules\<close>

lemma wfUNIVI: "(\P x. (\x. (\y. (y, x) \ r \ P y) \ P x) \ P x) \ wf r"
  unfolding wf_def by blast

lemmas wfpUNIVI = wfUNIVI [to_pred]

text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>.
  If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close>
lemma wfI:
  assumes "r \ A \ B"
    and "\x P. \\x. (\y. (y, x) \ r \ P y) \ P x; x \ A; x \ B\ \ P x"
  shows "wf r"
  using assms unfolding wf_def by blast

subsection \<open>Ordering Properties\<close>

lemma wf_not_sym: "wf r \ (a, x) \ r \ (x, a) \ r"
  by (induct a arbitrary: x set: wf) blast

lemma wf_asym:
  assumes "wf r" "(a, x) \ r"
  obtains "(x, a) \ r"
  by (drule wf_not_sym[OF assms])

lemma wf_imp_asym: "wf r \ asym r"
  by (auto intro: asymI elim: wf_asym)

lemma wfp_imp_asymp: "wfp r \ asymp r"
  by (rule wf_imp_asym[to_pred])

lemma wf_not_refl [simp]: "wf r \ (a, a) \ r"
  by (blast elim: wf_asym)

lemma wf_irrefl:
  assumes "wf r"
  obtains "(a, a) \ r"
  by (drule wf_not_refl[OF assms])

lemma wf_imp_irrefl:
  assumes "wf r" shows "irrefl r"
  using wf_irrefl [OF assms] by (auto simp add: irrefl_def)

lemma wfp_imp_irreflp: "wfp r \ irreflp r"
  by (rule wf_imp_irrefl[to_pred])

lemma wf_wellorderI:
  assumes wf: "wf {(x::'a::ord, y). x < y}"
    and lin: "OFCLASS('a::ord, linorder_class)"
  shows "OFCLASS('a::ord, wellorder_class)"
  apply (rule wellorder_class.intro [OF lin])
  apply (simp add: wellorder_class.intro class.wellorder_axioms.intro wf_induct_rule [OF wf])
  done

lemma (in wellorder) wf: "wf {(x, y). x < y}"
  unfolding wf_def by (blast intro: less_induct)

lemma (in wellorder) wfp_on_less[simp]: "wfp_on A (<)"
  unfolding wfp_on_def
proof (intro allI impI ballI)
  fix P x
  assume hyps: "\x\A. (\y\A. y < x \ P y) \ P x"
  show "x \ A \ P x"
  proof (induction x rule: less_induct)
    case (less x)
    show ?case
    proof (rule hyps[rule_format])
      show "x \ A"
        using \<open>x \<in> A\<close> .
    next
      show "\y. y \ A \ y < x \ P y"
        using less.IH .
    qed
  qed
qed

subsection \<open>Basic Results\<close>

text \<open>Point-free characterization of well-foundedness\<close>

lemma wf_onE_pf:
  assumes wf: "wf_on A r" and "B \ A" and "B \ r `` B"
  shows "B = {}"
proof -
  have "x \ B" if "x \ A" for x
    using wf
  proof (induction x rule: wf_on_induct)
    case in_set
    show ?case
      using that .
  next
    case (less x)
    have "x \ r `` B"
      using less.IH \<open>B \<subseteq> A\<close> by blast
    thus ?case
      using \<open>B \<subseteq> r `` B\<close> by blast
  qed
  with \<open>B \<subseteq> A\<close> show ?thesis
    by blast
qed

lemma wfE_pf: "wf R \ A \ R `` A \ A = {}"
  using wf_onE_pf[of UNIV, simplified] .

lemma wf_onI_pf:
  assumes "\B. B \ A \ B \ R `` B \ B = {}"
  shows "wf_on A R"
  unfolding wf_on_def
proof (intro allI impI ballI)
  fix P :: "'a \ bool" and x :: 'a
  let ?B = "{x \ A. \ P x}"
  assume "\x\A. (\y\A. (y, x) \ R \ P y) \ P x"
  hence "?B \ R `` ?B" by blast
  hence "{x \ A. \ P x} = {}"
    using assms(1)[of ?B] by simp
  moreover assume "x \ A"
  ultimately show "P x"
    by simp
qed

lemma wfI_pf: "(\A. A \ R `` A \ A = {}) \ wf R"
  using wf_onI_pf[of UNIV, simplified] .

subsubsection \<open>Minimal-element characterization of well-foundedness\<close>

lemma wf_on_iff_ex_minimal: "wf_on A R \ (\B \ A. B \ {} \ (\z \ B. \y. (y, z) \ R \ y \ B))"
proof (intro iffI allI impI)
  fix B
  assume "wf_on A R" and "B \ A" and "B \ {}"
  show "\z \ B. \y. (y, z) \ R \ y \ B"
  using wf_onE_pf[OF \<open>wf_on A R\<close> \<open>B \<subseteq> A\<close>] \<open>B \<noteq> {}\<close> by blast
next
  assume ex_min: "\B\A. B \ {} \ (\z\B. \y. (y, z) \ R \ y \ B)"
  show "wf_on A R "
  proof (rule wf_onI_pf)
    fix B
    assume "B \ A" and "B \ R `` B"
    have False if "B \ {}"
      using ex_min[rule_format, OF \<open>B \<subseteq> A\<close> \<open>B \<noteq> {}\<close>]
      using \<open>B \<subseteq> R `` B\<close> by blast
    thus "B = {}"
      by blast
  qed
qed

lemma wf_iff_ex_minimal: "wf R \ (\B. B \ {} \ (\z \ B. \y. (y, z) \ R \ y \ B))"
  using wf_on_iff_ex_minimal[of UNIV, simplified] .

lemma wfp_on_iff_ex_minimal: "wfp_on A R \ (\B \ A. B \ {} \ (\z \ B. \y. R y z \ y \ B))"
  using wf_on_iff_ex_minimal[of A, to_pred] by simp

lemma wfp_iff_ex_minimal: "wfp R \ (\B. B \ {} \ (\z \ B. \y. R y z \ y \ B))"
  using wfp_on_iff_ex_minimal[of UNIV, simplified] .

lemma wfE_min:
  assumes wf: "wf R" and Q: "x \ Q"
  obtains z where "z \ Q" "\y. (y, z) \ R \ y \ Q"
  using Q wfE_pf[OF wf, of Q] by blast

lemma wfE_min':
  "wf R \ Q \ {} \ (\z. z \ Q \ (\y. (y, z) \ R \ y \ Q) \ thesis) \ thesis"
  using wfE_min[of R _ Q] by blast

lemma wfI_min:
  assumes a: "\x Q. x \ Q \ \z\Q. \y. (y, z) \ R \ y \ Q"
  shows "wf R"
proof (rule wfI_pf)
  fix A
  assume b: "A \ R `` A"
  have False if "x \ A" for x
    using a[OF that] b by blast
  then show "A = {}" by blast
qed

lemma wf_eq_minimal: "wf r \ (\Q x. x \ Q \ (\z\Q. \y. (y, z) \ r \ y \ Q))"
  unfolding wf_iff_ex_minimal by blast

lemmas wfp_eq_minimal = wf_eq_minimal [to_pred]

subsubsection \<open>Finite characterization of well-foundedness\<close>

lemma strict_partial_order_wfp_on_finite_set:
  assumes "transp_on \ R" and "asymp_on \ R" and "finite \"
  shows "wfp_on \ R"
  unfolding Wellfounded.wfp_on_iff_ex_minimal
proof (intro allI impI)
  fix \<W>
  assume "\ \ \" and "\ \ {}"

  have "finite \"
    using finite_subset[OF \<open>\<W> \<subseteq> \<X>\<close> \<open>finite \<X>\<close>] .

  moreover have "asymp_on \ R"
    using asymp_on_subset[OF \<open>asymp_on \<X> R\<close> \<open>\<W> \<subseteq> \<X>\<close>] .

  moreover have "transp_on \ R"
    using transp_on_subset[OF \<open>transp_on \<X> R\<close> \<open>\<W> \<subseteq> \<X>\<close>] .

  ultimately have "\m\\. \x\\. x \ m \ \ R x m"
    using \<open>\<W> \<noteq> {}\<close> Finite_Set.bex_min_element[of \<W> R] by iprover

  thus "\z\\. \y. R y z \ y \ \"
    using asymp_onD[OF \<open>asymp_on \<W> R\<close>] by fast
qed

subsubsection \<open>Antimonotonicity\<close>

lemma wfp_on_mono_stronger:
  fixes
    A :: "'a set" and B :: "'b set" and
    f :: "'a \ 'b" and
    R :: "'b \ 'b \ bool" and Q :: "'a \ 'a \ bool"
  assumes
    wf: "wfp_on B R" and
    sub: "f ` A \ B" and
    mono: "\x y. x \ A \ y \ A \ Q x y \ R (f x) (f y)"
  shows "wfp_on A Q"
  unfolding wfp_on_iff_ex_minimal
proof (intro allI impI)
  fix A' :: "'a set"
  assume "A' \ A" and "A' \ {}"
  have "f ` A' \ B"
    using \<open>A' \<subseteq> A\<close> sub by blast
  moreover have "f ` A' \ {}"
    using \<open>A' \<noteq> {}\<close> by blast
  ultimately have "\z\f ` A'. \y. R y z \ y \ f ` A'"
    using wf wfp_on_iff_ex_minimal by blast
  hence "\z\A'. \y. R (f y) (f z) \ y \ A'"
    by blast
  thus "\z\A'. \y. Q y z \ y \ A'"
    using \<open>A' \<subseteq> A\<close> mono by blast
qed

lemma wf_on_mono_stronger:
  assumes
    "wf_on B r" and
    "f ` A \ B" and
    "(\x y. x \ A \ y \ A \ (x, y) \ q \ (f x, f y) \ r)"
  shows "wf_on A q"
  using assms wfp_on_mono_stronger[to_set, of B r f A q] by blast

lemma wf_on_mono_strong:
  assumes "wf_on B r" and "A \ B" and "(\x y. x \ A \ y \ A \ (x, y) \ q \ (x, y) \ r)"
  shows "wf_on A q"
  using assms wf_on_mono_stronger[of B r "\x. x" A q] by blast

lemma wfp_on_mono_strong:
  "wfp_on B R \ A \ B \ (\x y. x \ A \ y \ A \ Q x y \ R x y) \ wfp_on A Q"
  using wf_on_mono_strong[of B _ A, to_pred] .

lemma wf_on_mono: "A \ B \ q \ r \ wf_on B r \ wf_on A q"
  using wf_on_mono_strong[of B r A q] by auto

lemma wfp_on_mono: "A \ B \ Q \ R \ wfp_on B R \ wfp_on A Q"
  using wfp_on_mono_strong[of B R A Q] by auto

lemma wf_on_subset: "wf_on B r \ A \ B \ wf_on A r"
  using wf_on_mono_strong .

lemma wfp_on_subset: "wfp_on B R \ A \ B \ wfp_on A R"
  using wfp_on_mono_strong .

subsubsection \<open>Equivalence between \<^const>\<open>wfp_on\<close> and \<^const>\<open>wfp\<close>\<close>

lemma wfp_on_iff_wfp: "wfp_on A R \ wfp (\x y. R x y \ x \ A \ y \ A)"
  (is "?LHS \ ?RHS")
proof (rule iffI)
  assume ?LHS
  then show ?RHS
    unfolding wfp_on_iff_ex_minimal
    by force
next
  assume ?RHS
  thus ?LHS
  proof (rule wfp_on_mono_strong)
    show "A \ UNIV"
      using subset_UNIV .
  next
    show "\x y. x \ A \ y \ A \ R x y \ R x y \ x \ A \ y \ A"
      by iprover
  qed
qed

subsubsection \<open>Well-foundedness of transitive closure\<close>

lemma bex_rtrancl_min_element_if_wf_on:
  assumes wf: "wf_on A r" and x_in: "x \ A"
  shows "\y \ A. (y, x) \ r\<^sup>* \ \(\z \ A. (z, y) \ r)"
  using wf
proof (induction x rule: wf_on_induct)
  case in_set
  thus ?case
    using x_in .
next
  case (less z)
  show ?case
  proof (cases "\y \ A. (y, z) \ r")
    case True
    then obtain y where "y \ A" and "(y, z) \ r"
      by blast
    then obtain x where "x \ A" and "(x, y) \ r\<^sup>*" and "\ (\w\A. (w, x) \ r)"
      using less.IH by blast
    show ?thesis
    proof (intro bexI conjI)
      show "(x, z) \ r\<^sup>*"
        using rtrancl.rtrancl_into_rtrancl[of x y r z]
        using \<open>(x, y) \<in> r\<^sup>*\<close> \<open>(y, z) \<in> r\<close> by blast
    next
      show "\ (\z\A. (z, x) \ r)"
        using \<open>\<not> (\<exists>w\<in>A. (w, x) \<in> r)\<close> .
    next
      show "x \ A"
        using \<open>x \<in> A\<close> .
    qed
  next
    case False
    show ?thesis
    proof (intro bexI conjI)
      show "(z, z) \ r\<^sup>*"
        using rtrancl.rtrancl_refl .
    next
      show "\ (\w\A. (w, z) \ r)"
        using False .
    next
      show "z \ A"
        using less.hyps .
    qed
  qed
qed

lemma bex_rtransclp_min_element_if_wfp_on: "wfp_on A R \ x \ A \ \y\A. R\<^sup>*\<^sup>* y x \ \ (\z\A. R z y)"
  by (rule bex_rtrancl_min_element_if_wf_on[to_pred])

lemma ex_terminating_rtranclp_strong:
  assumes wf: "wfp_on {x'. R\<^sup>*\<^sup>* x x'} R\\"
  shows "\y. R\<^sup>*\<^sup>* x y \ (\z. R y z)"
proof -
  have x_in: "x \ {x'. R\<^sup>*\<^sup>* x x'}"
    by simp

  show ?thesis
    using bex_rtransclp_min_element_if_wfp_on[OF wf x_in]
    using rtranclp.rtrancl_into_rtrancl[of R x] by blast
qed

lemma ex_terminating_rtranclp:
  assumes wf: "wfp R\\"
  shows "\y. R\<^sup>*\<^sup>* x y \ (\z. R y z)"
  using ex_terminating_rtranclp_strong[OF wfp_on_subset[OF wf subset_UNIV]] .

lemma wf_trancl:
  assumes "wf r"
  shows "wf (r\<^sup>+)"
proof -
  have "P x" if induct_step: "\x. (\y. (y, x) \ r\<^sup>+ \ P y) \ P x" for P x
  proof (rule induct_step)
    show "P y" if "(y, x) \ r\<^sup>+" for y
      using \<open>wf r\<close> and that
    proof (induct x arbitrary: y)
      case (less x)
      note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close>
      from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y"
      proof cases
        case base
        show "P y"
        proof (rule induct_step)
          fix y'
          assume "(y', y) \ r\<^sup>+"
          with \<open>(y, x) \<in> r\<close> show "P y'"
            by (rule hyp [of y y'])
        qed
      next
        case step
        then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+"
          by simp
        then show "P y" by (rule hyp [of x' y])
      qed
    qed
  qed
  then show ?thesis unfolding wf_def by blast
qed

lemmas wfp_tranclp = wf_trancl [to_pred]

lemma wf_converse_trancl: "wf (r\) \ wf ((r\<^sup>+)\)"
  apply (subst trancl_converse [symmetric])
  apply (erule wf_trancl)
  done

text \<open>Well-foundedness of subsets\<close>

lemma wf_subset: "wf r \ p \ r \ wf p"
  using wf_on_mono[OF subset_UNIV, unfolded le_bool_def] ..

lemmas wfp_subset = wf_subset [to_pred]

text \<open>Well-foundedness of the empty relation\<close>

lemma wf_on_bot[iff]: "wf_on A \"
  by (simp add: wf_on_def)

lemma wfp_on_bot[iff]: "wfp_on A \"
  using wf_on_bot[to_pred] .

lemma wfp_empty [iff]: "wfp (\x y. False)"
  using wfp_on_bot by (simp add: bot_fun_def)

lemma wf_Int1: "wf r \ wf (r \ r')"
  by (erule wf_subset) (rule Int_lower1)

lemma wf_Int2: "wf r \ wf (r' \ r)"
  by (erule wf_subset) (rule Int_lower2)

text \<open>Exponentiation.\<close>
lemma wf_exp:
  assumes "wf (R ^^ n)"
  shows "wf R"
proof (rule wfI_pf)
  fix A assume "A \ R `` A"
  then have "A \ (R ^^ n) `` A"
    by (induct n) force+
  with \<open>wf (R ^^ n)\<close> show "A = {}"
    by (rule wfE_pf)
qed

text \<open>Well-foundedness of \<open>insert\<close>.\<close>
lemma wf_insert [iff]: "wf (insert (y,x) r) \ wf r \ (x,y) \ r\<^sup>*" (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    by (blast elim: wf_trancl [THEN wf_irrefl]
        intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD])
next
  assume R: ?rhs
  then have R': "Q \ {} \ (\z\Q. \y. (y, z) \ r \ y \ Q)" for Q
    by (auto simp: wf_eq_minimal)
  show ?lhs
    unfolding wf_eq_minimal
  proof clarify
    fix Q :: "'a set" and q
    assume "q \ Q"
    then obtain a where "a \ Q" and a: "\y. (y, a) \ r \ y \ Q"
      using R by (auto simp: wf_eq_minimal)
    show "\z\Q. \y'. (y', z) \ insert (y, x) r \ y' \ Q"
    proof (cases "a=x")
      case True
      show ?thesis
      proof (cases "y \ Q")
        case True
        then obtain z where "z \ Q" "(z, y) \ r\<^sup>*"
                            "\z'. (z', z) \ r \ z' \ Q \ (z', y) \ r\<^sup>*"
          using R' [of "{z \ Q. (z,y) \ r\<^sup>*}"] by auto
        then have "\y'. (y', z) \ insert (y, x) r \ y' \ Q"
          using R by(blast intro: rtrancl_trans)+
        then show ?thesis
          by (rule bexI) fact
      next
        case False
        then show ?thesis
          using a \<open>a \<in> Q\<close> by blast
      qed
    next
      case False
      with a \<open>a \<in> Q\<close> show ?thesis
        by blast
    qed
  qed
qed

subsubsection \<open>Well-foundedness of image\<close>

lemma wf_map_prod_image_Dom_Ran:
  fixes r:: "('a \ 'a) set"
    and f:: "'a \ 'b"
  assumes wf_r: "wf r"
    and inj: "\ a a'. a \ Domain r \ a' \ Range r \ f a = f a' \ a = a'"
  shows "wf (map_prod f f ` r)"
proof (unfold wf_eq_minimal, clarify)
  fix B :: "'b set" and b::"'b"
  assume "b \ B"
  define A where "A = f -` B \ Domain r"
  show "\z\B. \y. (y, z) \ map_prod f f ` r \ y \ B"
  proof (cases "A = {}")
    case False
    then obtain a0 where "a0 \ A" and "\a. (a, a0) \ r \ a \ A"
      using wfE_min[OF wf_r] by auto
    thus ?thesis
      using inj unfolding A_def
      by (intro bexI[of _ "f a0"]) auto
  qed (use \<open>b \<in> B\<close> in  \<open>unfold A_def, auto\<close>)
qed

lemma wf_map_prod_image: "wf r \ inj f \ wf (map_prod f f ` r)"
by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD)

lemma wfp_on_image: "wfp_on (f ` A) R \ wfp_on A (\a b. R (f a) (f b))"
proof (rule iffI)
  assume hyp: "wfp_on (f ` A) R"
  show "wfp_on A (\a b. R (f a) (f b))"
    unfolding wfp_on_iff_ex_minimal
  proof (intro allI impI)
    fix B
    assume "B \ A" and "B \ {}"
    hence "f ` B \ f ` A" and "f ` B \ {}"
      unfolding atomize_conj image_is_empty
      using image_mono by iprover
    hence "\z\f ` B. \y. R y z \ y \ f ` B"
      using hyp[unfolded wfp_on_iff_ex_minimal, rule_format] by iprover
    then obtain fz where "fz \ f ` B" and fz_max: "\y. R y fz \ y \ f ` B" ..

    obtain z where "z \ B" and "fz = f z"
      using \<open>fz \<in> f ` B\<close> unfolding image_iff ..

    show "\z\B. \y. R (f y) (f z) \ y \ B"
    proof (intro bexI allI impI)
      show "z \ B"
        using \<open>z \<in> B\<close> .
    next
      fix y assume "R (f y) (f z)"
      hence "f y \ f ` B"
        using fz_max \<open>fz = f z\<close> by iprover
      thus "y \ B"
        by (rule contrapos_nn) (rule imageI)
    qed
  qed
next
  assume hyp: "wfp_on A (\a b. R (f a) (f b))"
  show "wfp_on (f ` A) R"
    unfolding wfp_on_iff_ex_minimal
  proof (intro allI impI)
    fix fA
    assume "fA \ f ` A" and "fA \ {}"
    then obtain A' where "A' \<subseteq> A" and "A' \<noteq> {}" and "fA = f ` A'"
      by (auto simp only: subset_image_iff)

    obtain z where "z \ A'" and z_max: "\y. R (f y) (f z) \ y \ A'"
      using hyp[unfolded wfp_on_iff_ex_minimal, rule_format, OF \<open>A' \<subseteq> A\<close> \<open>A' \<noteq> {}\<close>] by blast

    show "\z\fA. \y. R y z \ y \ fA"
    proof (intro bexI allI impI)
      show "f z \ fA"
        unfolding \<open>fA = f ` A'\<close>
        using imageI[OF \<open>z \<in> A'\<close>] .
    next
      show "\y. R y (f z) \ y \ fA"
        unfolding \<open>fA = f ` A'\<close>
        using z_max by auto
    qed
  qed
qed

subsection \<open>Well-Foundedness Results for Unions\<close>

lemma wf_union_compatible:
  assumes "wf R" "wf S"
  assumes "R O S \ R"
  shows "wf (R \ S)"
proof (rule wfI_min)
  fix x :: 'a and Q
  let ?Q' = "{x \ Q. \y. (y, x) \ R \ y \ Q}"
  assume "x \ Q"
  obtain a where "a \ ?Q'"
    by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast
  with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'"
    by (erule wfE_min)
  have "y \ Q" if "(y, z) \ S" for y
  proof
    from that have "y \ ?Q'" by (rule zmin)
    assume "y \ Q"
    with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
    from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
    with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
    with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast
    with \<open>w \<in> Q\<close> show False by contradiction
  qed
  with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
qed

text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close>

lemma wf_UN:
  assumes r: "\i. i \ I \ wf (r i)"
    and disj: "\i j. \i \ I; j \ I; r i \ r j\ \ Domain (r i) \ Range (r j) = {}"
  shows "wf (\i\I. r i)"
  unfolding wf_eq_minimal
proof clarify
  fix A and a :: "'b"
  assume "a \ A"
  show "\z\A. \y. (y, z) \ \(r ` I) \ y \ A"
  proof (cases "\i\I. \a\A. \b\A. (b, a) \ r i")
    case True
    then obtain i b c where ibc: "i \ I" "b \ A" "c \ A" "(c,b) \ r i"
      by blast
    have ri: "\Q. Q \ {} \ \z\Q. \y. (y, z) \ r i \ y \ Q"
      using r [OF \<open>i \<in> I\<close>] unfolding wf_eq_minimal by auto
    show ?thesis
      using ri [of "{a. a \ A \ (\b\A. (b, a) \ r i) }"] ibc disj
      by blast
  next
    case False
    with \<open>a \<in> A\<close> show ?thesis
      by blast
  qed
qed

lemma wfp_SUP:
  "\i. wfp (r i) \ \i j. r i \ r j \ inf (Domainp (r i)) (Rangep (r j)) = bot \
    wfp (\<Squnion>(range r))"
  by (rule wf_UN[to_pred]) simp_all

lemma wf_Union:
  assumes "\r\R. wf r"
    and "\r\R. \s\R. r \ s \ Domain r \ Range s = {}"
  shows "wf (\R)"
  using assms wf_UN[of R "\i. i"] by simp

text \<open>
  Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction.
  \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>.
    Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>.
    By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the
    subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot
    have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well.
  \<^enum> There is no such step.
    Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min
    element of \<open>A\<close> as well.
\<close>
lemma wf_Un: "wf r \ wf s \ Domain r \ Range s = {} \ wf (r \ s)"
  using wf_union_compatible[of s r]
  by (auto simp: Un_ac)

lemma wf_union_merge: "wf (R \ S) = wf (R O R \ S O R \ S)"
  (is "wf ?A = wf ?B")
proof
  assume "wf ?A"
  with wf_trancl have wfT: "wf (?A\<^sup>+)" .
  moreover have "?B \ ?A\<^sup>+"
    by (subst trancl_unfold, subst trancl_unfold) blast
  ultimately show "wf ?B" by (rule wf_subset)
next
  assume "wf ?B"
  show "wf ?A"
  proof (rule wfI_min)
    fix Q :: "'a set" and x
    assume "x \ Q"
    with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
      by (erule wfE_min)
    then have 1: "\y. (y, z) \ R O R \ y \ Q"
      and 2: "\y. (y, z) \ S O R \ y \ Q"
      and 3: "\y. (y, z) \ S \ y \ Q"
      by auto
    show "\z\Q. \y. (y, z) \ ?A \ y \ Q"
    proof (cases "\y. (y, z) \ R \ y \ Q")
      case True
      with \<open>z \<in> Q\<close> 3 show ?thesis by blast
    next
      case False
      then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
      have "\y. (y, z') \ ?A \ y \ Q"
      proof (intro allI impI)
        fix y assume "(y, z') \ ?A"
        then show "y \ Q"
        proof
          assume "(y, z') \ R"
          then have "(y, z) \ R O R" using \(z', z) \ R\ ..
          with 1 show "y \ Q" .
        next
          assume "(y, z') \ S"
          then have "(y, z) \ S O R" using \(z', z) \ R\ ..
          with 2 show "y \ Q" .
        qed
      qed
      with \<open>z' \<in> Q\<close> show ?thesis ..
    qed
  qed
qed

lemma wf_comp_self: "wf R \ wf (R O R)" \ \special case\
  by (rule wf_union_merge [where S = "{}", simplified])

subsection \<open>Well-Foundedness of Composition\<close>

text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>

lemma qc_wf_relto_iff:
  assumes "R O S \ (R \ S)\<^sup>* O R" \ \R quasi-commutes over S\
  shows "wf (S\<^sup>* O R O S\<^sup>*) \ wf R"
    (is "wf ?S \ _")
proof
  show "wf R" if "wf ?S"
  proof -
    have "R \ ?S" by auto
    with wf_subset [of ?S] that show "wf R"
      by auto
  qed
next
  show "wf ?S" if "wf R"
  proof (rule wfI_pf)
    fix A
    assume A: "A \ ?S `` A"
    let ?X = "(R \ S)\<^sup>* `` A"
    have *: "R O (R \ S)\<^sup>* \ (R \ S)\<^sup>* O R"
    proof -
      have "(x, z) \ (R \ S)\<^sup>* O R" if "(y, z) \ (R \ S)\<^sup>*" and "(x, y) \ R" for x y z
        using that
      proof (induct y z)
        case rtrancl_refl
        then show ?case by auto
      next
        case (rtrancl_into_rtrancl a b c)
        then have "(x, c) \ ((R \ S)\<^sup>* O (R \ S)\<^sup>*) O R"
          using assms by blast
        then show ?case by simp
      qed
      then show ?thesis by auto
    qed
    then have "R O S\<^sup>* \ (R \ S)\<^sup>* O R"
      using rtrancl_Un_subset by blast
    then have "?S \ (R \ S)\<^sup>* O (R \ S)\<^sup>* O R"
      by (simp add: relcomp_mono rtrancl_mono)
    also have "\ = (R \ S)\<^sup>* O R"
      by (simp add: O_assoc[symmetric])
    finally have "?S O (R \ S)\<^sup>* \ (R \ S)\<^sup>* O R O (R \ S)\<^sup>*"
      by (simp add: O_assoc[symmetric] relcomp_mono)
    also have "\ \ (R \ S)\<^sup>* O (R \ S)\<^sup>* O R"
      using * by (simp add: relcomp_mono)
    finally have "?S O (R \ S)\<^sup>* \ (R \ S)\<^sup>* O R"
      by (simp add: O_assoc[symmetric])
    then have "(?S O (R \ S)\<^sup>*) `` A \ ((R \ S)\<^sup>* O R) `` A"
      by (simp add: Image_mono)
    moreover have "?X \ (?S O (R \ S)\<^sup>*) `` A"
      using A by (auto simp: relcomp_Image)
    ultimately have "?X \ R `` ?X"
      by (auto simp: relcomp_Image)
    then have "?X = {}"
      using \<open>wf R\<close> by (simp add: wfE_pf)
    moreover have "A \ ?X" by auto
    ultimately show "A = {}" by simp
  qed
qed

corollary wf_relcomp_compatible:
  assumes "wf R" and "R O S \ S O R"
  shows "wf (S O R)"
proof -
  have "R O S \ (R \ S)\<^sup>* O R"
    using assms by blast
  then have "wf (S\<^sup>* O R O S\<^sup>*)"
    by (simp add: assms qc_wf_relto_iff)
  then show ?thesis
    by (rule Wellfounded.wf_subset) blast
qed

subsection \<open>Acyclic relations\<close>

lemma wf_acyclic: "wf r \ acyclic r"
  by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl])

lemmas wfp_acyclicP = wf_acyclic [to_pred]

subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>

lemma finite_acyclic_wf:
  assumes "finite r" "acyclic r" shows "wf r"
  using assms
proof (induction r rule: finite_induct)
  case (insert x r)
  then show ?case
    by (cases x) simp
qed simp

lemma finite_acyclic_wf_converse: "finite r \ acyclic r \ wf (r\)"
  apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
  apply (erule acyclic_converse [THEN iffD2])
  done

text \<open>
  Observe that the converse of an irreflexive, transitive,
  and finite relation is again well-founded. Thus, we may
  employ it for well-founded induction.
\<close>
lemma wf_converse:
  assumes "irrefl r" and "trans r" and "finite r"
  shows "wf (r\)"
proof -
  have "acyclic r"
    using \<open>irrefl r\<close> and \<open>trans r\<close>
    by (simp add: irrefl_def acyclic_irrefl)
  with \<open>finite r\<close> show ?thesis
    by (rule finite_acyclic_wf_converse)
qed

lemma wf_iff_acyclic_if_finite: "finite r \ wf r = acyclic r"
  by (blast intro: finite_acyclic_wf wf_acyclic)

subsection \<open>\<^typ>\<open>nat\<close> is well-founded\<close>

lemma less_nat_rel: "(<) = (\m n. n = Suc m)\<^sup>+\<^sup>+"
proof (rule ext, rule ext, rule iffI)
  fix n m :: nat
  show "(\m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n"
    using that
  proof (induct n)
    case 0
    then show ?case by auto
  next
    case (Suc n)
    then show ?case
      by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
  qed
  show "m < n" if "(\m n. n = Suc m)\<^sup>+\<^sup>+ m n"
    using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less)
qed

definition pred_nat :: "(nat \ nat) set"
  where "pred_nat = {(m, n). n = Suc m}"

definition less_than :: "(nat \ nat) set"
  where "less_than = pred_nat\<^sup>+"

lemma less_eq: "(m, n) \ pred_nat\<^sup>+ \ m < n"
  unfolding less_nat_rel pred_nat_def trancl_def by simp

lemma pred_nat_trancl_eq_le: "(m, n) \ pred_nat\<^sup>* \ m \ n"
  unfolding less_eq rtrancl_eq_or_trancl by auto

lemma wf_pred_nat: "wf pred_nat"
  unfolding wf_def
proof clarify
  fix P x
  assume "\x'. (\y. (y, x') \ pred_nat \ P y) \ P x'"
  then show "P x"
    unfolding pred_nat_def by (induction x) blast+
qed

lemma wf_less_than [iff]: "wf less_than"
  by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])

lemma trans_less_than [iff]: "trans less_than"
  by (simp add: less_than_def)

lemma less_than_iff [iff]: "((x,y) \ less_than) = (x
  by (simp add: less_than_def less_eq)

lemma irrefl_less_than: "irrefl less_than"
  using irrefl_def by blast

lemma asym_less_than: "asym less_than"
  by (rule asymI) simp

lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
  using total_on_def by force+

lemma wf_less: "wf {(x, y::nat). x < y}"
  by (rule Wellfounded.wellorder_class.wf)

subsection \<open>Accessible Part\<close>

text \<open>
  Inductive definition of the accessible part \<open>acc r\<close> of a
  relation; see also \<^cite>\<open>"paulin-tlca"\<close>.
\<close>

inductive_set acc :: "('a \ 'a) set \ 'a set" for r :: "('a \ 'a) set"
  where accI: "(\y. (y, x) \ r \ y \ acc r) \ x \ acc r"

abbreviation termip :: "('a \ 'a \ bool) \ 'a \ bool"
  where "termip r \ accp (r\\)"

abbreviation termi :: "('a \ 'a) set \ 'a set"
  where "termi r \ acc (r\)"

lemmas accpI = accp.accI

lemma accp_eq_acc [code]: "accp r = (\x. x \ Wellfounded.acc {(x, y). r x y})"
  by (simp add: acc_def)

text \<open>Induction rules\<close>

theorem accp_induct:
  assumes major: "accp r a"
  assumes hyp: "\x. accp r x \ \y. r y x \ P y \ P x"
  shows "P a"
  apply (rule major [THEN accp.induct])
  apply (rule hyp)
   apply (rule accp.accI)
   apply auto
  done

lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]

theorem accp_downward: "accp r b \ r a b \ accp r a"
  by (cases rule: accp.cases)

lemma not_accp_down:
  assumes na: "\ accp R x"
  obtains z where "R z x" and "\ accp R z"
proof -
  assume a: "\z. R z x \ \ accp R z \ thesis"
  show thesis
  proof (cases "\z. R z x \ accp R z")
    case True
    then have "\z. R z x \ accp R z" by auto
    then have "accp R x" by (rule accp.accI)
    with na show thesis ..
  next
    case False then obtain z where "R z x" and "\ accp R z"
      by auto
    with a show thesis .
  qed
qed

lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \ accp r a \ accp r b"
  by (erule rtranclp_induct) (blast dest: accp_downward)+

theorem accp_downwards: "accp r a \ r\<^sup>*\<^sup>* b a \ accp r b"
  by (blast dest: accp_downwards_aux)

theorem accp_wfpI: "\x. accp r x \ wfp r"
proof (rule wfpUNIVI)
  fix P x
  assume "\x. accp r x" "\x. (\y. r y x \ P y) \ P x"
  then show "P x"
    using accp_induct[where P = P] by blast
qed

theorem accp_wfpD: "wfp r \ accp r x"
  apply (erule wfp_induct_rule)
  apply (rule accp.accI)
  apply blast
  done

theorem wfp_iff_accp: "wfp r = (\x. accp r x)"
  by (blast intro: accp_wfpI dest: accp_wfpD)

text \<open>Smaller relations have bigger accessible parts:\<close>

lemma accp_subset:
  assumes "R1 \ R2"
  shows "accp R2 \ accp R1"
proof (rule predicate1I)
  fix x
  assume "accp R2 x"
  then show "accp R1 x"
  proof (induct x)
    fix x
    assume "\y. R2 y x \ accp R1 y"
    with assms show "accp R1 x"
      by (blast intro: accp.accI)
  qed
qed

text \<open>This is a generalized induction theorem that works on
  subsets of the accessible part.\<close>

lemma accp_subset_induct:
  assumes subset: "D \ accp R"
    and dcl: "\x z. D x \ R z x \ D z"
    and "D x"
    and istep: "\x. D x \ (\z. R z x \ P z) \ P x"
  shows "P x"
proof -
  from subset and \<open>D x\<close>
  have "accp R x" ..
  then show "P x" using \<open>D x\<close>
  proof (induct x)
    fix x
    assume "D x" and "\y. R y x \ D y \ P y"
    with dcl and istep show "P x" by blast
  qed
qed

text \<open>Set versions of the above theorems\<close>

lemmas acc_induct = accp_induct [to_set]
lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
lemmas acc_downward = accp_downward [to_set]
lemmas not_acc_down = not_accp_down [to_set]
lemmas acc_downwards_aux = accp_downwards_aux [to_set]
lemmas acc_downwards = accp_downwards [to_set]
lemmas acc_wfI = accp_wfpI [to_set]
lemmas acc_wfD = accp_wfpD [to_set]
lemmas wf_iff_acc = wfp_iff_accp [to_set]
lemmas acc_subset = accp_subset [to_set]
lemmas acc_subset_induct = accp_subset_induct [to_set]

subsection \<open>Tools for building wellfounded relations\<close>

text \<open>Inverse Image\<close>

lemma wf_inv_image [simp,intro!]:
  fixes f :: "'a \ 'b"
  assumes "wf r"
  shows "wf (inv_image r f)"
proof -
  have "\x P. x \ P \ \z\P. \y. (f y, f z) \ r \ y \ P"
  proof -
    fix P and x::'a
    assume "x \ P"
    then obtain w where w: "w \ {w. \x::'a. x \ P \ f x = w}"
      by auto
    have *: "\Q u. u \ Q \ \z\Q. \y. (y, z) \ r \ y \ Q"
      using assms by (auto simp add: wf_eq_minimal)
    show "\z\P. \y. (f y, f z) \ r \ y \ P"
      using * [OF w] by auto
  qed
  then show ?thesis
    by (clarsimp simp: inv_image_def wf_eq_minimal)
qed

lemma wfp_on_inv_imagep:
  assumes wf: "wfp_on (f ` A) R"
  shows "wfp_on A (inv_imagep R f)"
  unfolding wfp_on_iff_ex_minimal
proof (intro allI impI)
  fix B assume "B \ A" and "B \ {}"
  hence "\z\f ` B. \y. R y z \ y \ f ` B"
    using wf[unfolded wfp_on_iff_ex_minimal, rule_format, of "f ` B"] by blast
  thus "\z\B. \y. inv_imagep R f y z \ y \ B"
    unfolding inv_imagep_def
    by auto
qed

subsubsection \<open>Conversion to a known well-founded relation\<close>

lemma wfp_on_if_convertible_to_wfp_on:
  assumes
    wf: "wfp_on (f ` A) Q" and
    convertible: "(\x y. x \ A \ y \ A \ R x y \ Q (f x) (f y))"
  shows "wfp_on A R"
  unfolding wfp_on_iff_ex_minimal
proof (intro allI impI)
  fix B assume "B \ A" and "B \ {}"
  moreover from wf have "wfp_on A (inv_imagep Q f)"
    by (rule wfp_on_inv_imagep)
  ultimately obtain y where "y \ B" and "\z. Q (f z) (f y) \ z \ B"
    unfolding wfp_on_iff_ex_minimal in_inv_imagep
    by blast
  thus "\z \ B. \y. R y z \ y \ B"
    using \<open>B \<subseteq> A\<close> convertible by blast
qed

lemma wf_on_if_convertible_to_wf_on: "wf_on (f ` A) Q \ (\x y. x \ A \ y \ A \ (x, y) \ R \ (f x, f y) \ Q) \ wf_on A R"
  using wfp_on_if_convertible_to_wfp_on[to_set] .

lemma wf_if_convertible_to_wf:
  fixes r :: "'a rel" and s :: "'b rel" and f :: "'a \ 'b"
  assumes "wf s" and convertible: "\x y. (x, y) \ r \ (f x, f y) \ s"
  shows "wf r"
proof (rule wf_on_if_convertible_to_wf_on)
  show "wf_on (range f) s"
    using wf_on_subset[OF \<open>wf s\<close> subset_UNIV] .
next
  show "\x y. (x, y) \ r \ (f x, f y) \ s"
    using convertible .
qed

lemma wfp_if_convertible_to_wfp: "wfp S \ (\x y. R x y \ S (f x) (f y)) \ wfp R"
  using wf_if_convertible_to_wf[to_pred, of S R f] by simp

text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
  Sledgehammer.\<close>

lemma wfp_if_convertible_to_nat:
  fixes f :: "_ \ nat"
  shows "(\x y. R x y \ f x < f y) \ wfp R"
  by (rule wfp_if_convertible_to_wfp[of "(<) :: nat \ nat \ bool", simplified])

subsubsection \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>

definition measure :: "('a \ nat) \ ('a \ 'a) set"
  where "measure = inv_image less_than"

lemma in_measure[simp, code_unfold]: "(x, y) \ measure f \ f x < f y"
  by (simp add:measure_def)

lemma wf_measure [iff]: "wf (measure f)"
  unfolding measure_def by (rule wf_less_than [THEN wf_inv_image])

lemma wf_if_measure: "(\x. P x \ f(g x) < f x) \ wf {(y,x). P x \ y = g x}"
  for f :: "'a \ nat"
  using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq
  by (rule wf_subset) auto

subsubsection \<open>Lexicographic combinations\<close>

definition lex_prod :: "('a \'a) set \ ('b \ 'b) set \ (('a \ 'b) \ ('a \ 'b)) set"
    (infixr \<open><*lex*>\<close> 80)
    where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \ ra \ a = a' \ (b, b') \ rb}"

lemma in_lex_prod[simp]: "((a, b), (a', b')) \ r <*lex*> s \ (a, a') \ r \ a = a' \ (b, b') \ s"
  by (auto simp:lex_prod_def)

lemma wf_on_lex_prod[intro]:
  assumes wfA: "wf_on A r\<^sub>A" and wfB: "wf_on B r\<^sub>B"
  shows "wf_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)"
  unfolding wf_on_iff_ex_minimal
proof (intro allI impI)
  fix AB assume "AB \ A \ B" and "AB \ {}"
  hence "fst ` AB \ A" and "snd ` AB \ B"
    by auto

  from \<open>fst ` AB \<subseteq> A\<close> \<open>AB \<noteq> {}\<close> obtain a where
    a_in: "a \ fst ` AB" and
    a_minimal: "(\y. (y, a) \ r\<^sub>A \ y \ fst ` AB)"
    using wfA[unfolded wf_on_iff_ex_minimal, rule_format, of "fst ` AB"]
    by auto

  from \<open>snd ` AB \<subseteq> B\<close> \<open>AB \<noteq> {}\<close> a_in obtain b where
    b_in: "b \ snd ` {p \ AB. fst p = a}" and
    b_minimal: "(\y. (y, b) \ r\<^sub>B \ y \ snd ` {p \ AB. fst p = a})"
    using wfB[unfolded wf_on_iff_ex_minimal, rule_format, of "snd ` {p \ AB. fst p = a}"]
    by blast

  show "\z\AB. \y. (y, z) \ r\<^sub>A <*lex*> r\<^sub>B \ y \ AB"
  proof (rule bexI)
    show "(a, b) \ AB"
      using b_in by (simp add: image_iff)
  next
    show "\y. (y, (a, b)) \ r\<^sub>A <*lex*> r\<^sub>B \ y \ AB"
    proof (intro allI impI)
      fix p assume "(p, (a, b)) \ r\<^sub>A <*lex*> r\<^sub>B"
      hence "(fst p, a) \ r\<^sub>A \ fst p = a \ (snd p, b) \ r\<^sub>B"
        unfolding lex_prod_def by auto
      thus "p \ AB"
      proof (elim disjE conjE)
        assume "(fst p, a) \ r\<^sub>A"
        hence "fst p \ fst ` AB"
          using a_minimal by simp
        thus ?thesis
          by (rule contrapos_nn) simp
      next
        assume "fst p = a" and "(snd p, b) \ r\<^sub>B"
        hence "snd p \ snd ` {p \ AB. fst p = a}"
          using b_minimal by simp
        thus "p \ AB"
          by (rule contrapos_nn) (simp add: \<open>fst p = a\<close>)
      qed
    qed
  qed
qed

lemma wf_lex_prod [intro!]:
  assumes "wf ra" "wf rb"
  shows "wf (ra <*lex*> rb)"
  using wf_on_lex_prod[OF \<open>wf ra\<close> \<open>wf rb\<close>, unfolded UNIV_Times_UNIV] .

lemma refl_lex_prod[simp]: "refl r\<^sub>B \ refl (r\<^sub>A <*lex*> r\<^sub>B)"
  by (auto intro!: reflI dest: refl_onD)

lemma irrefl_on_lex_prod[simp]:
  "irrefl_on A r\<^sub>A \ irrefl_on B r\<^sub>B \ irrefl_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)"
  by (auto intro!: irrefl_onI dest: irrefl_onD)

lemma irrefl_lex_prod[simp]: "irrefl r\<^sub>A \ irrefl r\<^sub>B \ irrefl (r\<^sub>A <*lex*> r\<^sub>B)"
  by (rule irrefl_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])

lemma sym_on_lex_prod[simp]:
  "sym_on A r\<^sub>A \ sym_on B r\<^sub>B \ sym_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)"
  by (auto intro!: sym_onI dest: sym_onD)

lemma sym_lex_prod[simp]:
  "sym r\<^sub>A \ sym r\<^sub>B \ sym (r\<^sub>A <*lex*> r\<^sub>B)"
  by (rule sym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])

lemma asym_on_lex_prod[simp]:
  "asym_on A r\<^sub>A \ asym_on B r\<^sub>B \ asym_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)"
  by (auto intro!: asym_onI dest: asym_onD)

lemma asym_lex_prod[simp]:
  "asym r\<^sub>A \ asym r\<^sub>B \ asym (r\<^sub>A <*lex*> r\<^sub>B)"
  by (rule asym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])

lemma trans_on_lex_prod[simp]:
  assumes "trans_on A r\<^sub>A" and "trans_on B r\<^sub>B"
  shows "trans_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)"
proof (rule trans_onI)
  fix x y z
  show "x \ A \ B \ y \ A \ B \ z \ A \ B \
       (x, y) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (y, z) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (x, z) \<in> r\<^sub>A <*lex*> r\<^sub>B"
  using trans_onD[OF \<open>trans_on A r\<^sub>A\<close>, of "fst x" "fst y" "fst z"]
  using trans_onD[OF \<open>trans_on B r\<^sub>B\<close>, of "snd x" "snd y" "snd z"]
  by auto
qed

lemma trans_lex_prod [simp,intro!]: "trans r\<^sub>A \ trans r\<^sub>B \ trans (r\<^sub>A <*lex*> r\<^sub>B)"
  by (rule trans_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])

lemma total_on_lex_prod[simp]:
  "total_on A r\<^sub>A \ total_on B r\<^sub>B \ total_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)"
  by (auto simp: total_on_def)

lemma total_lex_prod[simp]: "total r\<^sub>A \ total r\<^sub>B \ total (r\<^sub>A <*lex*> r\<^sub>B)"
  by (rule total_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])

text \<open>lexicographic combinations with measure functions\<close>

definition mlex_prod :: "('a \ nat) \ ('a \ 'a) set \ ('a \ 'a) set" (infixr \<*mlex*>\ 80)
  where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\x. (f x, x))"

lemma
  wf_mlex: "wf R \ wf (f <*mlex*> R)" and
  mlex_less: "f x < f y \ (x, y) \ f <*mlex*> R" and
  mlex_leq: "f x \ f y \ (x, y) \ R \ (x, y) \ f <*mlex*> R" and
  mlex_iff: "(x, y) \ f <*mlex*> R \ f x < f y \ f x = f y \ (x, y) \ R"
  by (auto simp: mlex_prod_def)

text \<open>Proper subset relation on finite sets.\<close>
definition finite_psubset :: "('a set \ 'a set) set"
  where "finite_psubset = {(A, B). A \ B \ finite B}"

lemma wf_finite_psubset[simp]: "wf finite_psubset"
  apply (unfold finite_psubset_def)
  apply (rule wf_measure [THEN wf_subset])
  apply (simp add: measure_def inv_image_def less_than_def less_eq)
  apply (fast elim!: psubset_card_mono)
  done

lemma trans_finite_psubset: "trans finite_psubset"
  by (auto simp: finite_psubset_def less_le trans_def)

lemma in_finite_psubset[simp]: "(A, B) \ finite_psubset \ A \ B \ finite B"
  unfolding finite_psubset_def by auto

text \<open>max- and min-extension of order to finite sets\<close>

inductive_set max_ext :: "('a \ 'a) set \ ('a set \ 'a set) set"
  for R :: "('a \ 'a) set"
  where max_extI[intro]:
    "finite X \ finite Y \ Y \ {} \ (\x. x \ X \ \y\Y. (x, y) \ R) \ (X, Y) \ max_ext R"

lemma max_ext_wf:
  assumes wf: "wf r"
  shows "wf (max_ext r)"
proof (rule acc_wfI, intro allI)
  show "M \ acc (max_ext r)" (is "_ \ ?W") for M
  proof (induct M rule: infinite_finite_induct)
    case empty
    show ?case
      by (rule accI) (auto elim: max_ext.cases)
  next
    case (insert a M)
    from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
    proof (induct arbitrary: M)
      fix M a
      assume "M \ ?W"
      assume [intro]: "finite M"
      assume hyp: "\b M. (b, a) \ r \ M \ ?W \ finite M \ insert b M \ ?W"
      have add_less: "M \ ?W \ (\y. y \ N \ (y, a) \ r) \ N \ M \ ?W"
        if "finite N" "finite M" for N M :: "'a set"
        using that by (induct N arbitrary: M) (auto simp: hyp)
      show "insert a M \ ?W"
      proof (rule accI)
        fix N
        assume Nless: "(N, insert a M) \ max_ext r"
        then have *: "\x. x \ N \ (x, a) \ r \ (\y \ M. (x, y) \ r)"
          by (auto elim!: max_ext.cases)

        let ?N1 = "{n \ N. (n, a) \ r}"
        let ?N2 = "{n \ N. (n, a) \ r}"
        have N: "?N1 \ ?N2 = N" by (rule set_eqI) auto
        from Nless have "finite N" by (auto elim: max_ext.cases)
        then have finites: "finite ?N1" "finite ?N2" by auto

        have "?N2 \ ?W"
        proof (cases "M = {}")
          case [simp]: True
          have Mw: "{} \ ?W" by (rule accI) (auto elim: max_ext.cases)
          from * have "?N2 = {}" by auto
          with Mw show "?N2 \ ?W" by (simp only:)
        next
          case False
          from * finites have N2: "(?N2, M) \ max_ext r"
            using max_extI[OF _ _ \<open>M \<noteq> {}\<close>, where ?X = ?N2] by auto
          with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
        qed
        with finites have "?N1 \ ?N2 \ ?W"
          by (rule add_less) simp
        then show "N \ ?W" by (simp only: N)
      qed
    qed
  next
    case infinite
    show ?case
      by (rule accI) (auto elim: max_ext.cases simp: infinite)
  qed
qed

lemma max_ext_additive: "(A, B) \ max_ext R \ (C, D) \ max_ext R \ (A \ C, B \ D) \ max_ext R"
  by (force elim!: max_ext.cases)

definition min_ext :: "('a \ 'a) set \ ('a set \ 'a set) set"
  where "min_ext r = {(X, Y) | X Y. X \ {} \ (\y \ Y. (\x \ X. (x, y) \ r))}"

lemma min_ext_wf:
  assumes "wf r"
  shows "wf (min_ext r)"
proof (rule wfI_min)
  show "\m \ Q. (\n. (n, m) \ min_ext r \ n \ Q)" if nonempty: "x \ Q"
    for Q :: "'a set set" and x
  proof (cases "Q = {{}}")
    case True
    then show ?thesis by (simp add: min_ext_def)
  next
    case False
    with nonempty obtain e x where "x \ Q" "e \ x" by force
    then have eU: "e \ \Q" by auto
    with \<open>wf r\<close>
    obtain z where z: "z \ \Q" "\y. (y, z) \ r \ y \ \Q"
      by (erule wfE_min)
    from z obtain m where "m \ Q" "z \ m" by auto
    from \<open>m \<in> Q\<close> show ?thesis
    proof (intro rev_bexI allI impI)
      fix n
      assume smaller: "(n, m) \ min_ext r"
      with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r"
        by (auto simp: min_ext_def)
      with z(2) show "n \ Q" by auto
    qed
  qed
qed

subsubsection \<open>Bounded increase must terminate\<close>

lemma wf_bounded_measure:
  fixes ub :: "'a \ nat"
    and f :: "'a \ nat"
  assumes "\a b. (b, a) \ r \ ub b \ ub a \ ub a \ f b \ f b > f a"
  shows "wf r"
  by (rule wf_subset[OF wf_measure[of "\a. ub a - f a"]]) (auto dest: assms)

lemma wf_bounded_set:
  fixes ub :: "'a \ 'b set"
    and f :: "'a \ 'b set"
  assumes "\a b. (b,a) \ r \ finite (ub a) \ ub b \ ub a \ ub a \ f b \ f b \ f a"
  shows "wf r"
  apply (rule wf_bounded_measure[of r "\a. card (ub a)" "\a. card (f a)"])
  apply (drule assms)
  apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
  done

lemma finite_subset_wf:
  assumes "finite A"
  shows "wf {(X, Y). X \ Y \ Y \ A}"
  by (rule wf_subset[OF wf_finite_psubset[unfolded finite_psubset_def]])
    (auto intro: finite_subset[OF _ assms])

hide_const (open) acc accp

subsection \<open>Code Generation Setup\<close>

text \<open>Code equations with \<^const>\<open>wf\<close> or \<^const>\<open>wfp\<close> on the left-hand side are not supported by the
code generation module because of the \<^const>\<open>UNIV\<close> hidden behind the abbreviations. To sidestep this
problem, we provide the following wrapper definitions and use @{attribute code_abbrev} to register
the definitions with the pre- and post-processors of the code generator.\<close>

definition wf_code :: "('a \ 'a) set \ bool" where
  [code_abbrev]: "wf_code r \ wf r"

definition wfp_code :: "('a \ 'a \ bool) \ bool" where
  [code_abbrev]: "wfp_code R \ wfp R"

end

quality100%

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.