Quelle Confluence.thy Sprache: Isabelle

theory Confluence imports
  Main
begin

section \<open>Confluence\<close>

definition semiconfluentp :: "('a \ 'a \ bool) \ bool" where
  "semiconfluentp r \ r\\ OO r\<^sup>*\<^sup>* \ r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*"

definition confluentp :: "('a \ 'a \ bool) \ bool" where
  "confluentp r \ r\\\<^sup>*\<^sup>* OO r\<^sup>*\<^sup>* \ r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*"

definition strong_confluentp :: "('a \ 'a \ bool) \ bool" where
  "strong_confluentp r \ r\\ OO r \ r\<^sup>*\<^sup>* OO (r\\)\<^sup>=\<^sup>="

lemma semiconfluentpI [intro?]:
  "semiconfluentp r" if "\x y z. \ r x y; r\<^sup>*\<^sup>* x z \ \ \u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u"
  using that unfolding semiconfluentp_def rtranclp_conversep by blast

lemma semiconfluentpD: "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "semiconfluentp r" "r x y" "r\<^sup>*\<^sup>* x z"
  using that unfolding semiconfluentp_def rtranclp_conversep by blast

lemma confluentpI:
  "confluentp r" if "\x y z. \ r\<^sup>*\<^sup>* x y; r\<^sup>*\<^sup>* x z \ \ \u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u"
  using that unfolding confluentp_def rtranclp_conversep by blast

lemma confluentpD: "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "confluentp r" "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z"
  using that unfolding confluentp_def rtranclp_conversep by blast

lemma strong_confluentpI [intro?]:
  "strong_confluentp r" if "\x y z. \ r x y; r x z \ \ \u. r\<^sup>*\<^sup>* y u \ r\<^sup>=\<^sup>= z u"
  using that unfolding strong_confluentp_def by blast

lemma strong_confluentpD: "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>=\<^sup>= z u" if "strong_confluentp r" "r x y" "r x z"
  using that unfolding strong_confluentp_def by blast

lemma semiconfluentp_imp_confluentp: "confluentp r" if r: "semiconfluentp r"
proof(rule confluentpI)
  show "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z" for x y z
    using that(2,1)
    by(induction arbitrary: y rule: converse_rtranclp_induct)
      (blast intro: rtranclp_trans dest:  r[THEN semiconfluentpD])+
qed

lemma confluentp_imp_semiconfluentp: "semiconfluentp r" if "confluentp r"
  using that by(auto intro!: semiconfluentpI dest: confluentpD[OF that])

lemma confluentp_eq_semiconfluentp: "confluentp r \ semiconfluentp r"
  by(blast intro: semiconfluentp_imp_confluentp confluentp_imp_semiconfluentp)

lemma confluentp_conv_strong_confluentp_rtranclp:
  "confluentp r \ strong_confluentp (r\<^sup>*\<^sup>*)"
  by(auto simp add: confluentp_def strong_confluentp_def rtranclp_conversep)

lemma strong_confluentp_into_semiconfluentp:
  "semiconfluentp r" if r: "strong_confluentp r"
proof
  show "\u. r\<^sup>*\<^sup>* y u \ r\<^sup>*\<^sup>* z u" if "r x y" "r\<^sup>*\<^sup>* x z" for x y z
    using that(2,1)
    apply(induction arbitrary: y rule: converse_rtranclp_induct)
    subgoal by blast
    subgoal for a b c
      by (drule (1) strong_confluentpD[OF r, of a c])(auto 10 0 intro: rtranclp_trans)
    done
qed

lemma strong_confluentp_imp_confluentp: "confluentp r" if "strong_confluentp r"
  unfolding confluentp_eq_semiconfluentp using that by(rule strong_confluentp_into_semiconfluentp)

lemma semiconfluentp_equivclp: "equivclp r = r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*" if r: "semiconfluentp r"
proof(rule antisym[rotated] r_OO_conversep_into_equivclp predicate2I)+
  show "(r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>*) x y" if "equivclp r x y" for x y using that unfolding equivclp_def rtranclp_conversep
    by(induction rule: converse_rtranclp_induct)
      (blast elim!: symclpE intro: converse_rtranclp_into_rtranclp rtranclp_trans dest: semiconfluentpD[OF r])+
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.15 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.