# Theory Commutation

Up to index of Isabelle/HOL/Lambda

theory Commutation
imports Main
begin

    (*  Title:      HOL/Lambda/Commutation.thy
        ID:         $Id: Commutation.thy,v 1.16 2005/09/22 21:56:35 nipkow Exp $
        Author:     Tobias Nipkow
        Copyright   1995  TU Muenchen
    *)

    header {* Abstract commutation and confluence notions *}

    theory Commutation imports Main begin

    subsection {* Basic definitions *}

    constdefs
      square :: "[('a × 'a) set, ('a × 'a) set, ('a × 'a) set, ('a × 'a) set] => bool"
      "square R S T U ==
        ∀x y. (x, y) ∈ R --> (∀z. (x, z) ∈ S --> (∃u. (y, u) ∈ T ∧ (z, u) ∈ U))"

      commute :: "[('a × 'a) set, ('a × 'a) set] => bool"
      "commute R S == square R S S R"

      diamond :: "('a × 'a) set => bool"
      "diamond R == commute R R"

      Church_Rosser :: "('a × 'a) set => bool"
      "Church_Rosser R ==
        ∀x y. (x, y) ∈ (R ∪ R^-1)^* --> (∃z. (x, z) ∈ R^* ∧ (y, z) ∈ R^*)"

    syntax
      confluent :: "('a × 'a) set => bool"
    translations
      "confluent R" == "diamond (R^*)"

    subsection {* Basic lemmas *}

    subsubsection {* square *}

    lemma square_sym: "square R S T U ==> square S R U T"
      apply (unfold square_def)
      apply blast
      done

    lemma square_subset:
        "[| square R S T U; T ⊆ T' |] ==> square R S T' U"
      apply (unfold square_def)
      apply blast
      done

    lemma square_reflcl:
        "[| square R S T (R^=); S ⊆ T |] ==> square (R^=) S T (R^=)"
      apply (unfold square_def)
      apply blast
      done

    lemma square_rtrancl:
        "square R S S T ==> square (R^*) S S (T^*)"
      apply (unfold square_def)
      apply (intro strip)
      apply (erule rtrancl_induct)
       apply blast
      apply (blast intro: rtrancl_into_rtrancl)
      done

    lemma square_rtrancl_reflcl_commute:
        "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
      apply (unfold commute_def)
      apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
        elim: r_into_rtrancl)
      done

    subsubsection {* commute *}

    lemma commute_sym: "commute R S ==> commute S R"
      apply (unfold commute_def)
      apply (blast intro: square_sym)
      done

    lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
      apply (unfold commute_def)
      apply (blast intro: square_rtrancl square_sym)
      done

    lemma commute_Un:
        "[| commute R T; commute S T |] ==> commute (R ∪ S) T"
      apply (unfold commute_def square_def)
      apply blast
      done

    subsubsection {* diamond, confluence, and union *}

    lemma diamond_Un:
        "[| diamond R; diamond S; commute R S |] ==> diamond (R ∪ S)"
      apply (unfold diamond_def)
      apply (assumption | rule commute_Un commute_sym)+
      done

    lemma diamond_confluent: "diamond R ==> confluent R"
      apply (unfold diamond_def)
      apply (erule commute_rtrancl)
      done

    lemma square_reflcl_confluent:
        "square R R (R^=) (R^=) ==> confluent R"
      apply (unfold diamond_def)
      apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
        elim: square_subset)
      done

    lemma confluent_Un:
        "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R ∪ S)"
      apply (rule rtrancl_Un_rtrancl [THEN subst])
      apply (blast dest: diamond_Un intro: diamond_confluent)
      done

    lemma diamond_to_confluence:
        "[| diamond R; T ⊆ R; R ⊆ T^* |] ==> confluent T"
      apply (force intro: diamond_confluent
        dest: rtrancl_subset [symmetric])
      done

    subsection {* Church-Rosser *}

    lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
      apply (unfold square_def commute_def diamond_def Church_Rosser_def)
      apply (tactic {* safe_tac HOL_cs *})
       apply (tactic {*
         blast_tac (HOL_cs addIs
           [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
           rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
      apply (erule rtrancl_induct)
       apply blast
      apply (blast del: rtrancl_refl intro: rtrancl_trans)
      done

    subsection {* Newman's lemma *}

    text {* Proof by Stefan Berghofer *}

    theorem newman:
      assumes wf: "wf (R¯)"
      and lc: "!!a b c. (a, b) ∈ R ==> (a, c) ∈ R ==>
        ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*"
      shows "!!b c. (a, b) ∈ R* ==> (a, c) ∈ R* ==>
        ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*"
      using wf
    proof induct
      case (less x b c)
      have xc: "(x, c) ∈ R*" .
      have xb: "(x, b) ∈ R*" . thus ?case
      proof (rule converse_rtranclE)
        assume "x = b"
        with xc have "(b, c) ∈ R*" by simp
        thus ?thesis by iprover
      next
        fix y
        assume xy: "(x, y) ∈ R"
        assume yb: "(y, b) ∈ R*"
        from xc show ?thesis
        proof (rule converse_rtranclE)
          assume "x = c"
          with xb have "(c, b) ∈ R*" by simp
          thus ?thesis by iprover
        next
          fix y'
          assume y'c: "(y', c) ∈ R*"
          assume xy': "(x, y') ∈ R"
          with xy have "∃u. (y, u) ∈ R* ∧ (y', u) ∈ R*" by (rule lc)
          then obtain u where yu: "(y, u) ∈ R*" and y'u: "(y', u) ∈ R*" by iprover
          from xy have "(y, x) ∈ R¯" ..
          from this and yb yu have "∃d. (b, d) ∈ R* ∧ (u, d) ∈ R*" by (rule less)
          then obtain v where bv: "(b, v) ∈ R*" and uv: "(u, v) ∈ R*" by iprover
          from xy' have "(y', x) ∈ R¯" ..
          moreover from y'u and uv have "(y', v) ∈ R*" by (rule rtrancl_trans)
          moreover note y'c
          ultimately have "∃d. (v, d) ∈ R* ∧ (c, d) ∈ R*" by (rule less)
          then obtain w where vw: "(v, w) ∈ R*" and cw: "(c, w) ∈ R*" by iprover
          from bv vw have "(b, w) ∈ R*" by (rule rtrancl_trans)
          with cw show ?thesis by iprover
        qed
      qed
    qed

    text {*
      \medskip Alternative version.  Partly automated by Tobias
      Nipkow. Takes 2 minutes (2002).

      This is the maximal amount of automation possible at the moment.
    *}

    theorem newman':
      assumes wf: "wf (R¯)"
      and lc: "!!a b c. (a, b) ∈ R ==> (a, c) ∈ R ==>
        ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*"
      shows "!!b c. (a, b) ∈ R* ==> (a, c) ∈ R* ==>
                   ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*"
    using wf
    proof induct
      case (less x b c)
      have IH: "!!y b c. [|(y,x) ∈ R¯; (y,b) ∈ R*; (y,c) ∈ R*|]
                         ==> ∃d. (b,d) ∈ R* ∧ (c,d) ∈ R*" by(rule less)
      have xc: "(x, c) ∈ R*" .
      have xb: "(x, b) ∈ R*" .
      thus ?case
      proof (rule converse_rtranclE)
        assume "x = b"
        with xc have "(b, c) ∈ R*" by simp
        thus ?thesis by iprover
      next
        fix y
        assume xy: "(x, y) ∈ R"
        assume yb: "(y, b) ∈ R*"
        from xc show ?thesis
        proof (rule converse_rtranclE)
          assume "x = c"
          with xb have "(c, b) ∈ R*" by simp
          thus ?thesis by iprover
        next
          fix y'
          assume y'c: "(y', c) ∈ R*"
          assume xy': "(x, y') ∈ R"
          with xy obtain u where u: "(y, u) ∈ R*" "(y', u) ∈ R*"
            by (blast dest:lc)
          from yb u y'c show ?thesis
            by(blast del: rtrancl_refl
                     intro:rtrancl_trans
                     dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
        qed
      qed
    qed

    end

### Basic definitions

### Basic lemmas

#### square

lemma square_sym:

      square R S T U ==> square S R U T

lemma square_subset:

      [| square R S T U; T ⊆ T' |] ==> square R S T' U

lemma square_reflcl:

      [| square R S T (R=); S ⊆ T |] ==> square (R=) S T (R=)

lemma square_rtrancl:

      square R S S T ==> square (R*) S S (T*)

lemma square_rtrancl_reflcl_commute:

      square R S (S*) (R=) ==> commute (R*) (S*)

#### commute

lemma commute_sym:

      commute R S ==> commute S R

lemma commute_rtrancl:

      commute R S ==> commute (R*) (S*)

lemma commute_Un:

      [| commute R T; commute S T |] ==> commute (R ∪ S) T

#### diamond, confluence, and union

lemma diamond_Un:

      [| diamond R; diamond S; commute R S |] ==> diamond (R ∪ S)

lemma diamond_confluent:

      diamond R ==> confluent R

lemma square_reflcl_confluent:

      square R R (R=) (R=) ==> confluent R

lemma confluent_Un:

      [| confluent R; confluent S; commute (R*) (S*) |] ==> confluent (R ∪ S)

lemma diamond_to_confluence:

      [| diamond R; T ⊆ R; R ⊆ T* |] ==> confluent T

### Church-Rosser

lemma Church_Rosser_confluent:

      Church_Rosser R = confluent R

### Newman's lemma

theorem newman:

      [| wf (R^-1);
         !!a b c. [| (a, b) ∈ R; (a, c) ∈ R |] ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*;
         (a, b) ∈ R*; (a, c) ∈ R* |]
      ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*

theorem newman':

      [| wf (R^-1);
         !!a b c. [| (a, b) ∈ R; (a, c) ∈ R |] ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*;
         (a, b) ∈ R*; (a, c) ∈ R* |]
      ==> ∃d. (b, d) ∈ R* ∧ (c, d) ∈ R*