(* 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