(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2018

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      InfiniteChains.thy
    Author:     Andreas Viktor Hess, DTU
*)

section {* Theory: Lemmas for infinite chains *}
theory InfiniteChains 
imports Main
begin

subsection {* The reachable states from a given start state, as a subset of the original relation *}
abbreviation successors where
  "successors r x \<equiv> {(x,y) | y. (x,y) \<in> r}"

inductive_set reachable for r::"('a \<times> 'a) set" and x::'a where 
  Base[simp]: "(x,a) \<in> r \<Longrightarrow> (x,a) \<in> reachable r x"
| Step[simp]: "\<lbrakk>(a,b) \<in> reachable r x; (b,c) \<in> r\<rbrakk> \<Longrightarrow> (b,c) \<in> reachable r x"

lemma successors_subset: "successors r x \<subseteq> reachable r x" by auto

lemma reachableD[dest]: "(a,b) \<in> reachable r x \<Longrightarrow> a = x \<or> (x,a) \<in> r\<^sup>+"
by (induct a b rule: reachable.induct) (meson reachable.cases trancl.simps)+

lemma reachableD'[dest]: "(a,b) \<in> reachable r x \<Longrightarrow> (x,b) \<in> r\<^sup>+"
by (induct a b rule: reachable.induct) (meson reachable.simps trancl.simps)+

lemma reachableI[intro]: "\<lbrakk>(x,a) \<in> r\<^sup>+; (a,b) \<in> r\<rbrakk> \<Longrightarrow> (a,b) \<in> reachable r x"
proof (induction arbitrary: b rule: trancl_induct)
  case (base y) thus ?case by (metis Step[OF Base[OF base.hyps] base.prems])
next
  case (step y z)
  hence "(y, z) \<in> reachable r x" by blast
  thus ?case using Step[OF _ step.prems] by metis
qed

lemma reachable_empty[simp]: "reachable {} x = {}"
proof (rule ccontr)
  assume "reachable {} x \<noteq> {}"
  then obtain y z where "(y,z) \<in> reachable {} x" by auto
  thus False by (induct rule: reachable.induct) auto
qed

lemma reachable_infinite: "infinite {(x,a) \<in> r | a} \<Longrightarrow> infinite (reachable r x)" by simp

lemma reachable_subset: "reachable r x \<subseteq> r"
proof
  fix y assume *: "y \<in> reachable r x"
  then obtain a b where y: "y = (a,b)" by (metis surj_pair)
  hence "(a,b) \<in> reachable r x" by (metis *)
  hence "(a,b) \<in> r" by (induct rule: reachable.induct) auto
  thus "y \<in> r" by (metis y)
qed

lemma reachable_finite: "finite r \<Longrightarrow> finite (reachable r x)"
using finite_subset reachable_subset by metis

lemma reachable_unfold:
  "reachable r x = {(x,a) | a. (x,a) \<in> r} \<union> {(a,b) \<in> r. (x,a) \<in> r\<^sup>+}" (is "reachable r x = ?S")
proof
  { fix x1 x2 assume "(x1,x2) \<in> reachable r x"
    hence "(x1,x2) \<in> ?S" by (induct rule: reachable.induct) auto
  }
  thus "reachable r x \<subseteq> ?S" by auto

  show "?S \<subseteq> reachable r x" by auto
qed

lemma reachableD''[dest]:
  "y \<in> reachable r x \<Longrightarrow> y \<in> {(x,a) | a. (x,a) \<in> r} \<union> {(a,b) \<in> r. (x,a) \<in> r\<^sup>+}"
by (metis reachable_unfold)

lemma reachable_unfold':
  "reachable r x = \<Union>{insert (x,a) (reachable r a) | a. (x,a) \<in> r}" (is "?A = ?B")
proof
  { fix a b assume "(a,b) \<in> ?A"
    hence "(a,b) \<in> ?B"
    proof (induction a b rule: reachable.induct)
      case (Step a b c)
      then obtain d where d: "(a,b) \<in> insert (x,d) (reachable r d)" "(x,d) \<in> r" by moura
      hence "(a = x \<and> b = d) \<or> (a,b) \<in> reachable r d" by auto
      moreover {
        assume "a = x" "b = d"
        hence ?case using reachable.Base[OF Step.hyps(2)] d(2) by auto
      }
      moreover {
        assume "(a,b) \<in> reachable r d"
        hence ?case using reachable.Step[OF _ Step.hyps(2)] d(2) by auto
      }
      ultimately show ?case by auto
    qed auto
  }
  thus "?A \<subseteq> ?B" by auto

  { fix a b assume "(a,b) \<in> ?B"
    then obtain d where d: "(a,b) \<in> insert (x,d) (reachable r d)" "(x,d) \<in> r" by moura
    hence "(a,b) \<in> ?A" by force
  }
  thus "?B \<subseteq> ?A" by auto
qed

lemma reachable_trancl[intro]: "(x,y) \<in> r\<^sup>+ \<Longrightarrow> (x,y) \<in> (reachable r x)\<^sup>+"
proof (induction rule: trancl_induct)
  case (step y z) thus ?case by (meson reachable.Step trancl.simps)
qed auto

lemma reachable_trancl': "(x,y) \<in> (reachable r x)\<^sup>+ \<Longrightarrow> (x,y) \<in> r\<^sup>+"
proof (induction rule: trancl_induct)
  case (base y) thus ?case using reachable_subset by fastforce
next
  case (step y z) thus ?case by (metis reachable.cases trancl_into_trancl) 
qed

lemma reachable_rooted: "\<forall>(a,b) \<in> reachable r x. (x,a) \<in> (reachable r x)\<^sup>+ \<or> a = x"
proof -
  { fix a b assume "(a,b) \<in> reachable r x"
    hence "(x,a) \<in> (reachable r x)\<^sup>+ \<or> a = x"
    proof (cases "a = x")
      case False
      hence "(a,b) \<in> {(c,d) \<in> r. (x,c) \<in> r\<^sup>+}"
        using \<open>(a, b) \<in> reachable r x\<close> reachable_unfold[of r x] by auto 
      hence "(x,a) \<in> r\<^sup>+" "(a,b) \<in> r" by auto
      moreover
      { fix y assume "(x,y) \<in> r\<^sup>+"
        hence "(x,y) \<in> (reachable r x)\<^sup>+" by (induct rule: trancl_induct, auto)
      }
      hence "successors (r\<^sup>+) x \<subseteq> (reachable r x)\<^sup>+" by auto
      ultimately show ?thesis by blast
    qed metis
  }
  thus ?thesis by auto
qed


subsection {* Proving the existence of infinite paths in relations as mappings from naturals to states *}
fun rel_chain_fun::"nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a" where
  "rel_chain_fun 0 x _ _ = x"
| "rel_chain_fun (Suc i) x y r = (if i = 0 then y else SOME z. (rel_chain_fun i x y r, z) \<in> r)"

lemma infinite_chain_intro:
  fixes r::"('a \<times> 'a) set"
  assumes "\<forall>(a,b) \<in> r. \<exists>c. (b,c) \<in> r" "r \<noteq> {}"
  shows "\<exists>f. \<forall>i::nat. (f i, f (Suc i)) \<in> r"
proof -
  from assms(2) obtain a b where "(a,b) \<in> r" by auto

  let ?P = "\<lambda>i. (rel_chain_fun i a b r, rel_chain_fun (Suc i) a b r) \<in> r"
  let ?Q = "\<lambda>i. \<exists>z. (rel_chain_fun i a b r, z) \<in> r"

  have base: "?P 0" using \<open>(a,b) \<in> r\<close> by auto

  { fix i assume *: "?P i"
    hence "?Q (Suc i)" using assms(1) by auto
    have "?P (Suc i)" using someI_ex[OF \<open>?Q (Suc i)\<close>] by auto
  }
  hence step: "\<And>i. ?P i \<Longrightarrow> ?P (Suc i)" by metis

  have "\<forall>i::nat. (rel_chain_fun i a b r, rel_chain_fun (Suc i) a b r) \<in> r"
    using base step nat_induct[of ?P] by simp
  thus ?thesis by fastforce
qed

lemma infinite_chain_intro':
  fixes r::"('a \<times> 'a) set"
  assumes base: "\<exists>b. (x,b) \<in> r" and step: "\<forall>b. (x,b) \<in> r\<^sup>+ \<longrightarrow> (\<exists>c. (b,c) \<in> r)" 
  shows "\<exists>f. \<forall>i::nat. (f i, f (Suc i)) \<in> r"
proof -
  let ?s = "{(a,b) \<in> r. a = x \<or> (x,a) \<in> r\<^sup>+}"

  have "?s \<noteq> {}" using base by auto

  { fix a b assume "(a,b) \<in> ?s" "a = x" hence "\<exists>c. (b,c) \<in> ?s" using step by auto }
  moreover
  { fix a b assume "(a,b) \<in> ?s" "a \<noteq> x"
    hence "(x,a) \<in> r\<^sup>+" by auto
    hence "(x,b) \<in> r\<^sup>+" using \<open>(a,b) \<in> ?s\<close> by auto
    hence "\<exists>c. (b,c) \<in> r" using step by auto
    hence "\<exists>c. (b,c) \<in> ?s" using \<open>(x,b) \<in> r\<^sup>+\<close> by auto
  }
  ultimately have "\<forall>(a,b) \<in> ?s. \<exists>c. (b,c) \<in> ?s" by blast
  hence "\<exists>f. \<forall>i. (f i, f (Suc i)) \<in> ?s" using infinite_chain_intro[of ?s] \<open>?s \<noteq> {}\<close> by blast
  thus ?thesis by auto
qed

lemma infinite_chain_mono:
  assumes "S \<subseteq> T" "\<exists>f. \<forall>i::nat. (f i, f (Suc i)) \<in> S"
  shows "\<exists>f. \<forall>i::nat. (f i, f (Suc i)) \<in> T"
using assms by auto


end