Quelle Confluence.thy Sprache: Isabelle

(*  Title:      ZF/Resid/Confluence.thy
    Author:     Ole Rasmussen
    Copyright   1995  University of Cambridge
*)

theory Confluence imports Reduction begin

definition
  confluence    :: "i\o" where
    "confluence(R) \
       \<forall>x y. \<langle>x,y\<rangle> \<in> R \<longrightarrow> (\<forall>z.\<langle>x,z\<rangle> \<in> R \<longrightarrow> (\<exists>u.\<langle>y,u\<rangle> \<in> R \<and> \<langle>z,u\<rangle> \<in> R))"

definition
  strip         :: "o"  where
    "strip \ \x y. (x =\ y) \
                    (\<forall>z.(x =1\<Rightarrow> z) \<longrightarrow> (\<exists>u.(y =1\<Rightarrow> u) \<and> (z=\<Longrightarrow>u)))"

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

lemma strip_lemma_r:
    "\confluence(Spar_red1)\\ strip"
  unfolding 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)"
  unfolding 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]

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]

(**** Conversion ****)

consts
  Sconv1        :: "i"
  Sconv         :: "i"

abbreviation
  Sconv1_rel (infixl \<open><-1->\<close> 50) where
  "a<-1->b \ \a,b\ \ Sconv1"

abbreviation
  Sconv_rel (infixl \<open><-\<longrightarrow>\<close> 50) where
  "a<-\b \ \a,b\ \ Sconv"

inductive
  domains       "Sconv1" \<subseteq> "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" \<subseteq> "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)
  unfolding confluence_def
apply (blast intro: Sred.trans)
done

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.