Theory RelUtils

theory RelUtils
  imports Main "HOL.Transitive_Closure"
begin

― ‹NOTE added definition.›
definition reflexive where 
  "reflexive R  x. R x x"

― ‹NOTE translation of 'TC' in relationScript.sml:69.›
― ‹TODO can we replace this with something from 'HOL.Transitive\_Closure'?›
definition TC where
  "TC R a b  (P. (x y. R x y  P x y)  (x y z. P x y  P y z  P x z)  P a b)"

― ‹NOTE adapts transitive closure definitions of Isabelle and HOL4.›
lemma TC_equiv_tranclp: "TC R a b  (R++ a b)"
proof -
  {
    have "TC R a b  (R++ a b)"
      unfolding TC_def 
      using tranclp.r_into_trancl tranclp_trans
      by metis
  }
  moreover 
  {
    have "(R++ a b)  TC R a b" proof(induction rule: tranclp.induct)
      case (r_into_trancl a b)
      then show ?case by(subst TC_def; auto)
    next
      case (trancl_into_trancl a b c)
      then show ?case unfolding TC_def by blast
    qed 
  }
  ultimately show ?thesis
    by fast
qed

lemma TC_IMP_NOT_TC_CONJ_1:
  fixes R P  and  x y
  assumes "¬(R++ x y)"
  shows "¬((λx y. R x y  P x y)++ x y)"
proof -
  from assms(1) have 1: "¬TC R x y"
    using TC_equiv_tranclp
    by fast
  {
    assume P: "¬TC R x y"
    then obtain P where a: "(x y. R x y  P x y)  (x y z. P x y  P y z  P x z)  ¬P x y" 
      unfolding TC_def
      by blast
    {
      assume P_1: "(x y. R x y  P x y)" "(x y z. P x y  P y z  P x z)"
      then have "(x y. R x y  P x y  P x y)" "(x y z. P x y  P y z  P x z)"
        by blast+
      moreover from a and P_1 have "¬P x y"
        by blast
      then have "P. (x y. R x y  P x y  P x y)  (x y z. P x y  P y z  P x z)  ¬P x y"
        by blast
    }
    then have "P. 
      (x y. R x y  P x y  P x y)  (x y z. P x y  P y z  P x z)  ¬P x y" 
      by blast 
  }
  note 2 = this
  {
    from 1 2 have "P. 
      (x y. R x y  P x y  P x y)  (x y z. P x y  P y z  P x z)  ¬P x y" 
      by blast
    then have "¬TC (λx y. R x y  P x y) x y" 
      unfolding TC_def  
      by (metis assms tranclp.r_into_trancl tranclp_trans)
    then have "¬(λx y. R x y  P x y)++ x y" 
      using TC_equiv_tranclp
      by fast
  }
  then show ?thesis
    by blast
qed

lemma TC_IMP_NOT_TC_CONJ:
  fixes R R' P x y
  assumes "x y. P x y  R' x y  R x y" "¬R++ x y"
  shows "¬(λx y. R' x y  P x y)++ x y" 
proof -
  from assms(2)
  have 1: "¬(λx y. R x y  P x  y)++ x y"
    using TC_IMP_NOT_TC_CONJ_1[where P="λx y. P x y"]
    by blast
  {
    {
      from 1 have  "¬TC (λx y. R x y  P x  y) x y" 
        using TC_equiv_tranclp 
        by fast
      then have "Pa.
      (x y. R x y  P x y  Pa x y)  (x y z. Pa x y  Pa y z  Pa x z) 
       ¬Pa x y"
        unfolding TC_def
        by blast
    }
    then obtain Pa where a: 
      "(x y. R x y  P x y  Pa x y)  (x y z. Pa x y  Pa y z  Pa x z)  ¬Pa x y"
      by blast
    then have "¬(Pa. (x y. R' x y  P x y  Pa x y)  (x y z. Pa x y  Pa y z  Pa x z)  Pa x y)"
      by (metis assms(1) assms(2) tranclp.r_into_trancl tranclp_trans) 
    then have "¬TC (λx y. R' x y  P x y) x y" 
      unfolding TC_def
      by blast
  }
  then show ?thesis
    using TC_equiv_tranclp
    by fast
qed

― ‹NOTE added lemma (relationScript.sml:314)› 
lemma TC_INDUCT:
  fixes R :: "'a  'a  bool" and P
  assumes "(x y. R x y  P x y)" "(x y z. P x y  P y z  P x z)" 
  shows "u v. (TC R) u v  P u v"
  using assms
  unfolding TC_def
  by metis

lemma REFL_IMP_3_CONJ_1:
  fixes R P x y
  assumes "((λx y. R x y  P x y)++ x y)"
  shows "R++ x y" 
  using assms 
proof -
  show ?thesis
    using assms TC_IMP_NOT_TC_CONJ_1
    by fast
qed

lemma REFL_IMP_3_CONJ:
  fixes R'
  assumes "reflexive R'" 
  shows "(P x y. 
    (R'++ x y)  ( ((λx y. R' x y  P x  P y)++ x y)  (z. ¬P z  R'++ x z  R'++ z y)))"
proof -
  {
    fix P
    {
      have "x y. R' x y  (λx y. R' x y  P x  P y)++ x y  (z. ¬ P z  R'++ x z  R'++ z y)" 
      proof (auto)
        fix x y
        assume P: "R' x y" "z. R'++ x z  P z  ¬ R'++ z y"
        then show "(λx y. R' x y  P x  P y)++ x y"
        proof -
          have a: "a. ¬ R' x a  ¬ R' a y  P a"
            using P(2)
            by blast
          have "reflexive R'"
            by (meson assms)
          then show ?thesis
            using a P(1)
            by (simp add: reflexive_def tranclp.r_into_trancl)
        qed
      qed
    }
    moreover {
      have "x y z. ((λx y. R' x y  P x  P y)++ x y  (z. ¬ P z  R'++ x z  R'++ z y)) 
         ((λx y. R' x y  P x  P y)++ y z  (za. ¬ P za  R'++ y za  R'++ za z)) 
         (λx y. R' x y  P x  P y)++ x z  (za. ¬ P za  R'++ x za  R'++ za z)" 
      proof (auto)
        fix x y z za
        assume P: "za. R'++ x za  P za  ¬ R'++ za z" "(λx y. R' x y  P x  P y)++ x y"
          "¬ P za" "R'++ y za" "R'++ za z" 
        then show "(λx y. R' x y  P x  P y)++ x z"
          using P
          by (meson P rtranclp_tranclp_tranclp TC_IMP_NOT_TC_CONJ_1  tranclp_into_rtranclp)
      next 
        fix x y z za
        assume P: "za. R'++ x za  P za  ¬ R'++ za z" "¬ P za" "R'++ x za" "R'++ za y" 
          "(λx y. R' x y  P x  P y)++ y z" 
        then show "(λx y. R' x y  P x  P y)++ x z"
          by (meson P TC_IMP_NOT_TC_CONJ_1 tranclp_trans)
      qed
    }
    ultimately have "u v. 
      TC R' u v 
       (λx y. R' x y  P x  P y)++ u v  (z. ¬ P z  R'++ u z  R'++ z v)"
      using TC_INDUCT[where R="R'" and
          P="λx y. ( ((λx y. R' x y  P x  P y)++ x y)  (z. ¬P z  R'++ x z  R'++ z y))"]
      by fast
  }
  then show ?thesis 
    by (simp add: TC_equiv_tranclp)
qed

lemma REFL_TC_CONJ:
  fixes R R' :: "'a  'a  bool" and P x y
  assumes "reflexive R'" "x y. P x  P y  (R' x y  R x y)" "¬(R++ x y)"
  shows "(¬(R'++ x y)  (z. ¬P z  (R')++ x z  (R')++ z y))"
  using assms
proof (cases "¬R'++ x y")
next
  case False
  then show ?thesis using assms 
      TC_IMP_NOT_TC_CONJ[where P="λx y. P x  P y"]
      REFL_IMP_3_CONJ[of R']
    by blast
qed blast

― ‹NOTE 
  This is not a trivial translation: 'TC\_INDUCT' in relationScript.sml:314 differs significantly
from 'trancl\_induct' and 'trancl\_trans\_induct' in Transitive\_Closure:375, 391›
lemma TC_CASES1_NEQ:
  fixes R x z
  assumes "R++ x z"
  shows "R x z  (y :: 'a. ¬(x = y)  ¬(y = z)  R x y  R++ y z)"
proof -
  {
    fix u v
    have "x y. R x y  R x y  (ya. x  ya  ya  y  R x ya  R++ ya y)"
      by meson
    moreover have "x y z. 
      (R x y  (ya. x  ya  ya  y  R x ya  R++ ya y)) 
       (R y z  (ya. y  ya  ya  z  R y ya  R++ ya z)) 
       R x z  (y. x  y  y  z  R x y  R++ y z)"
      by (metis tranclp.r_into_trancl tranclp_trans)
    ultimately have "TC R u v  R u v  (y. u  y  y  v  R u y  R++ y v)" 
      using TC_INDUCT[where P="λx z. R x z  (y :: 'a. ¬(x = y)  ¬(y = z)  R x y  R++ y z)"]
      by blast
  }
  then show ?thesis 
    using assms TC_equiv_tranclp
    by (simp add: TC_equiv_tranclp)
qed
end