Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Induct/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 7 kB

Quelle Comb.thy Sprache: Isabelle

(*  Title:      HOL/Induct/Comb.thy
    Author:     Lawrence C Paulson
    Copyright   1996  University of Cambridge
*)

section \<open>Combinatory Logic example: the Church-Rosser Theorem\<close>

theory Comb
imports Main
begin

text \<open>
  Combinator terms do not have free variables.
  Example taken from \<^cite>\<open>camilleri92\<close>.
\<close>

subsection \<open>Definitions\<close>

text \<open>Datatype definition of combinators \<open>S\<close> and \<open>K\<close>.\<close>

datatype comb = K
              | S
              | Ap comb comb (infixl \<open>\<bullet>\<close> 90)

text \<open>
  Inductive definition of contractions, \<open>\<rightarrow>\<^sup>1\<close> and
  (multi-step) reductions, \<open>\<rightarrow>\<close>.
\<close>

inductive contract1 :: "[comb,comb] \ bool" (infixl \\\<^sup>1\ 50)
  where
    K:     "K\x\y \\<^sup>1 x"
  | S:     "S\x\y\z \\<^sup>1 (x\z)\(y\z)"
  | Ap1:   "x \\<^sup>1 y \ x\z \\<^sup>1 y\z"
  | Ap2:   "x \\<^sup>1 y \ z\x \\<^sup>1 z\y"

abbreviation
  contract :: "[comb,comb] \ bool" (infixl \\\ 50) where
  "contract \ contract1\<^sup>*\<^sup>*"

text \<open>
  Inductive definition of parallel contractions, \<open>\<Rrightarrow>\<^sup>1\<close> and
  (multi-step) parallel reductions, \<open>\<Rrightarrow>\<close>.
\<close>

inductive parcontract1 :: "[comb,comb] \ bool" (infixl \\\<^sup>1\ 50)
  where
    refl:  "x \\<^sup>1 x"
  | K:     "K\x\y \\<^sup>1 x"
  | S:     "S\x\y\z \\<^sup>1 (x\z)\(y\z)"
  | Ap:    "\x \\<^sup>1 y; z \\<^sup>1 w\ \ x\z \\<^sup>1 y\w"

abbreviation
  parcontract :: "[comb,comb] \ bool" (infixl \\\ 50) where
  "parcontract \ parcontract1\<^sup>*\<^sup>*"

text \<open>
  Misc definitions.
\<close>

definition
  I :: comb where
  "I \ S\K\K"

definition
  diamond   :: "([comb,comb] \ bool) \ bool" where
    \<comment> \<open>confluence; Lambda/Commutation treats this more abstractly\<close>
  "diamond r \ \x y. r x y \
                  (\<forall>y'. r x y' \<longrightarrow>
                    (\<exists>z. r y z \<and> r y' z))"

subsection \<open>Reflexive/Transitive closure preserves Church-Rosser property\<close>

text\<open>Remark: So does the Transitive closure, with a similar proof\<close>

text\<open>Strip lemma.
   The induction hypothesis covers all but the last diamond of the strip.\<close>
lemma strip_lemma [rule_format]:
  assumes "diamond r" and r: "r\<^sup>*\<^sup>* x y" "r x y'"
  shows "\z. r\<^sup>*\<^sup>* y' z \ r y z"
  using r
proof (induction rule: rtranclp_induct)
  case base
  then show ?case
    by blast
next
  case (step y z)
  then show ?case
    using \<open>diamond r\<close> unfolding diamond_def
    by (metis rtranclp.rtrancl_into_rtrancl)
qed

proposition diamond_rtrancl:
  assumes "diamond r"
  shows "diamond(r\<^sup>*\<^sup>*)"
  unfolding diamond_def
proof (intro strip)
  fix x y y'
  assume "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x y'"
  then show "\z. r\<^sup>*\<^sup>* y z \ r\<^sup>*\<^sup>* y' z"
  proof (induction rule: rtranclp_induct)
    case base
    then show ?case
      by blast
  next
    case (step y z)
    then show ?case
      by (meson assms strip_lemma rtranclp.rtrancl_into_rtrancl)
  qed
qed

subsection \<open>Non-contraction results\<close>

text \<open>Derive a case for each combinator constructor.\<close>

inductive_cases
  K_contractE [elim!]: "K \\<^sup>1 r"
  and S_contractE [elim!]: "S \\<^sup>1 r"
  and Ap_contractE [elim!]: "p\q \\<^sup>1 r"

declare contract1.K [intro!] contract1.S [intro!]
declare contract1.Ap1 [intro] contract1.Ap2 [intro]

lemma I_contract_E [iff]: "\ I \\<^sup>1 z"
  unfolding I_def by blast

lemma K1_contractD [elim!]: "K\x \\<^sup>1 z \ (\x'. z = K\x' \ x \\<^sup>1 x')"
  by blast

lemma Ap_reduce1 [intro]: "x \ y \ x\z \ y\z"
  by (induction rule: rtranclp_induct; blast intro: rtranclp_trans)

lemma Ap_reduce2 [intro]: "x \ y \ z\x \ z\y"
  by (induction rule: rtranclp_induct; blast intro: rtranclp_trans)

text \<open>Counterexample to the diamond property for \<^term>\<open>x \<rightarrow>\<^sup>1 y\<close>\<close>

lemma not_diamond_contract: "\ diamond(contract1)"
  unfolding diamond_def by (metis S_contractE contract1.K)

subsection \<open>Results about Parallel Contraction\<close>

text \<open>Derive a case for each combinator constructor.\<close>

inductive_cases
      K_parcontractE [elim!]: "K \\<^sup>1 r"
  and S_parcontractE [elim!]: "S \\<^sup>1 r"
  and Ap_parcontractE [elim!]: "p\q \\<^sup>1 r"

declare parcontract1.intros [intro]

subsection \<open>Basic properties of parallel contraction\<close>
text\<open>The rules below are not essential but make proofs much faster\<close>

lemma K1_parcontractD [dest!]: "K\x \\<^sup>1 z \ (\x'. z = K\x' \ x \\<^sup>1 x')"
  by blast

lemma S1_parcontractD [dest!]: "S\x \\<^sup>1 z \ (\x'. z = S\x' \ x \\<^sup>1 x')"
  by blast

lemma S2_parcontractD [dest!]: "S\x\y \\<^sup>1 z \ (\x' y'. z = S\x'\y' \ x \\<^sup>1 x' \ y \\<^sup>1 y')"
  by blast

text\<open>Church-Rosser property for parallel contraction\<close>
proposition diamond_parcontract: "diamond parcontract1"
proof -
  have "(\z. w \\<^sup>1 z \ y' \\<^sup>1 z)" if "y \\<^sup>1 w" "y \\<^sup>1 y'" for w y y'
    using that by (induction arbitrary: y' rule: parcontract1.induct) fast+
  then show ?thesis
    by (auto simp: diamond_def)
qed

subsection \<open>Equivalence of \<^prop>\<open>p \<rightarrow> q\<close> and \<^prop>\<open>p \<Rrightarrow> q\<close>.\<close>

lemma contract_imp_parcontract: "x \\<^sup>1 y \ x \\<^sup>1 y"
  by (induction rule: contract1.induct; blast)

text\<open>Reductions: simply throw together reflexivity, transitivity and
  the one-step reductions\<close>

proposition reduce_I: "I\x \ x"
  unfolding I_def
  by (meson contract1.K contract1.S r_into_rtranclp rtranclp.rtrancl_into_rtrancl)

lemma parcontract_imp_reduce: "x \\<^sup>1 y \ x \ y"
proof (induction rule: parcontract1.induct)
  case (Ap x y z w)
  then show ?case
    by (meson Ap_reduce1 Ap_reduce2 rtranclp_trans)
qed auto

lemma reduce_eq_parreduce: "x \ y \ x \ y"
  by (metis contract_imp_parcontract parcontract_imp_reduce predicate2I rtranclp_subset)

theorem diamond_reduce: "diamond(contract)"
  using diamond_parcontract diamond_rtrancl reduce_eq_parreduce by presburger

end

quality96%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

über den Urheber dieser Seite

Die Firma ist wie angegeben erreichbar.

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.