# Theory Confluence

Up to index of Isabelle/ZF/Resid

theory Confluence
imports Reduction
begin

    (*  Title:      Confluence.thy
        ID:         $Id: Confluence.thy,v 1.8 2005/06/17 14:15:11 haftmann Exp $
        Author:     Ole Rasmussen
        Copyright   1995  University of Cambridge
        Logic Image: ZF
    *)

    theory Confluence imports Reduction begin

    constdefs
      confluence    :: "i=>o"
        "confluence(R) ==
           ∀x y. <x,y> ∈ R --> (∀z.<x,z> ∈ R --> (∃u.<y,u> ∈ R & <z,u> ∈ R))"

      strip         :: "o"
        "strip == ∀x y. (x ===> y) -->
                        (∀z.(x =1=> z) --> (∃u.(y =1=> u) & (z===>u)))"

    (* ------------------------------------------------------------------------- *)
    (*        strip lemmas                                                       *)
    (* ------------------------------------------------------------------------- *)

    lemma strip_lemma_r:
        "[|confluence(Spar_red1)|]==> strip"
    apply (unfold confluence_def strip_def)
    apply (rule impI [THEN allI, THEN allI])
    apply (erule Spar_red.induct, fast)
    apply (fast intro: Spar_red.trans)
    done

    lemma strip_lemma_l:
        "strip==> confluence(Spar_red)"
    apply (unfold confluence_def strip_def)
    apply (rule impI [THEN allI, THEN allI])
    apply (erule Spar_red.induct, blast)
    apply clarify
    apply (blast intro: Spar_red.trans)
    done

    (* ------------------------------------------------------------------------- *)
    (*      Confluence                                                           *)
    (* ------------------------------------------------------------------------- *)

    lemma parallel_moves: "confluence(Spar_red1)"
    apply (unfold confluence_def, clarify)
    apply (frule simulation)
    apply (frule_tac n = z in simulation, clarify)
    apply (frule_tac v = va in paving)
    apply (force intro: completeness)+
    done

    lemmas confluence_parallel_reduction =
          parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]

    lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
    by (unfold confluence_def, blast intro: par_red_red red_par_red)

    lemmas confluence_beta_reduction =
           confluence_parallel_reduction [THEN lemma1, standard]

    (**** Conversion ****)

    consts
      Sconv1        :: "i"
      "<-1->"       :: "[i,i]=>o"   (infixl 50)
      Sconv         :: "i"
      "<--->"       :: "[i,i]=>o"   (infixl 50)

    translations
      "a<-1->b"    == "<a,b> ∈ Sconv1"
      "a<--->b"    == "<a,b> ∈ Sconv"

    inductive
      domains       "Sconv1" <= "lambda*lambda"
      intros
        red1:        "m -1-> n ==> m<-1->n"
        expl:        "n -1-> m ==> m<-1->n"
      type_intros    red1D1 red1D2 lambda.intros bool_typechecks

    declare Sconv1.intros [intro]

    inductive
      domains       "Sconv" <= "lambda*lambda"
      intros
        one_step:    "m<-1->n  ==> m<--->n"
        refl:        "m ∈ lambda ==> m<--->m"
        trans:       "[|m<--->n; n<--->p|] ==> m<--->p"
      type_intros    Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks

    declare Sconv.intros [intro]

    lemma conv_sym: "m<--->n ==> n<--->m"
    apply (erule Sconv.induct)
    apply (erule Sconv1.induct, blast+)
    done

    (* ------------------------------------------------------------------------- *)
    (*      Church_Rosser Theorem                                                *)
    (* ------------------------------------------------------------------------- *)

    lemma Church_Rosser: "m<--->n ==> ∃p.(m --->p) & (n ---> p)"
    apply (erule Sconv.induct)
    apply (erule Sconv1.induct)
    apply (blast intro: red1D1 redD2)
    apply (blast intro: red1D1 redD2)
    apply (blast intro: red1D1 redD2)
    apply (cut_tac confluence_beta_reduction)
    apply (unfold confluence_def)
    apply (blast intro: Sred.trans)
    done

    end

lemma strip_lemma_r:

      confluence(Spar_red1) ==> strip

lemma strip_lemma_l:

      strip ==> confluence(Spar_red)

lemma parallel_moves:

      confluence(Spar_red1)

lemmas confluence_parallel_reduction:

      confluence(Spar_red)

lemmas confluence_parallel_reduction:

      confluence(Spar_red)

lemma lemma1:

      confluence(Spar_red) ==> confluence(Sred)

lemmas confluence_beta_reduction:

      confluence(Sred)

lemmas confluence_beta_reduction:

      confluence(Sred)

lemma conv_sym:

      m <---> n ==> n <---> m

lemma Church_Rosser:

      m <---> n ==> ∃p. m ---> p ∧ n ---> p