Quelle Comb.thy Sprache: Isabelle

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

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

theory Comb
imports ZF
begin

text \<open>
  Curiously, combinators do not include 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>

consts comb :: i
datatype comb =
  K
| S
| app ("p \ comb", "q \ comb") (infixl \\\ 90)

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

consts contract  :: i
abbreviation contract_syntax :: "[i,i] \ o" (infixl \\\<^sup>1\ 50)
  where "p \\<^sup>1 q \ \p,q\ \ contract"

abbreviation contract_multi :: "[i,i] \ o" (infixl \\\ 50)
  where "p \ q \ \p,q\ \ contract^*"

inductive
  domains "contract" \<subseteq> "comb \<times> comb"
  intros
    K:   "\p \ comb; q \ comb\ \ K\p\q \\<^sup>1 p"
    S:   "\p \ comb; q \ comb; r \ comb\ \ S\p\q\r \\<^sup>1 (p\r)\(q\r)"
    Ap1: "\p\\<^sup>1q; r \ comb\ \ p\r \\<^sup>1 q\r"
    Ap2: "\p\\<^sup>1q; r \ comb\ \ r\p \\<^sup>1 r\q"
  type_intros comb.intros

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

consts parcontract :: i

abbreviation parcontract_syntax :: "[i,i] \ o" (infixl \\\<^sup>1\ 50)
  where "p \\<^sup>1 q \ \p,q\ \ parcontract"

abbreviation parcontract_multi :: "[i,i] \ o" (infixl \\\ 50)
  where "p \ q \ \p,q\ \ parcontract^+"

inductive
  domains "parcontract" \<subseteq> "comb \<times> comb"
  intros
    refl: "\p \ comb\ \ p \\<^sup>1 p"
    K:    "\p \ comb; q \ comb\ \ K\p\q \\<^sup>1 p"
    S:    "\p \ comb; q \ comb; r \ comb\ \ S\p\q\r \\<^sup>1 (p\r)\(q\r)"
    Ap:   "\p\\<^sup>1q; r\\<^sup>1s\ \ p\r \\<^sup>1 q\s"
  type_intros comb.intros

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

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

definition diamond :: "i \ o"
  where "diamond(r) \
    \<forall>x y. \<langle>x,y\<rangle>\<in>r \<longrightarrow> (\<forall>y'. <x,y'>\<in>r \<longrightarrow> (\<exists>z. \<langle>y,z\<rangle>\<in>r \<and> <y',z> \<in> r))"

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

lemma diamond_strip_lemmaD [rule_format]:
  "\diamond(r); \x,y\:r^+\ \
    \<forall>y'. <x,y'>:r \<longrightarrow> (\<exists>z. <y',z>: r^+ \<and> \<langle>y,z\<rangle>: r)"
    unfolding diamond_def
  apply (erule trancl_induct)
   apply (blast intro: r_into_trancl)
  apply clarify
  apply (drule spec [THEN mp], assumption)
  apply (blast intro: r_into_trancl trans_trancl [THEN transD])
  done

lemma diamond_trancl: "diamond(r) \ diamond(r^+)"
  apply (simp (no_asm_simp) add: diamond_def)
  apply (rule impI [THEN allI, THEN allI])
  apply (erule trancl_induct)
   apply auto
   apply (best intro: r_into_trancl trans_trancl [THEN transD]
     dest: diamond_strip_lemmaD)+
  done

inductive_cases Ap_E [elim!]: "p\q \ comb"

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

text \<open>
  For type checking: replaces \<^term>\<open>a \<rightarrow>\<^sup>1 b\<close> by \<open>a, b \<in>
  comb\<close>.
\<close>

lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
  and contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1]
  and contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2]

lemma field_contract_eq: "field(contract) = comb"
  by (blast intro: contract.K elim!: contract_combE2)

lemmas reduction_refl =
  field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl]

lemmas rtrancl_into_rtrancl2 =
  r_into_rtrancl [THEN trans_rtrancl [THEN transD]]

declare reduction_refl [intro!] contract.K [intro!] contract.S [intro!]

lemmas reduction_rls =
  contract.K [THEN rtrancl_into_rtrancl2]
  contract.S [THEN rtrancl_into_rtrancl2]
  contract.Ap1 [THEN rtrancl_into_rtrancl2]
  contract.Ap2 [THEN rtrancl_into_rtrancl2]

lemma "p \ comb \ I\p \ p"
  \<comment> \<open>Example only: not used\<close>
  unfolding I_def by (blast intro: reduction_rls)

lemma comb_I: "I \ comb"
  unfolding I_def by blast

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"

lemma I_contract_E: "I \\<^sup>1 r \ P"
  by (auto simp add: I_def)

lemma K1_contractD: "K\p \\<^sup>1 r \ (\q. r = K\q \ p \\<^sup>1 q)"
  by auto

lemma Ap_reduce1: "\p \ q; r \ comb\ \ p\r \ q\r"
  apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
  apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
  apply (erule rtrancl_induct)
   apply (blast intro: reduction_rls)
  apply (erule trans_rtrancl [THEN transD])
  apply (blast intro: contract_combD2 reduction_rls)
  done

lemma Ap_reduce2: "\p \ q; r \ comb\ \ r\p \ r\q"
  apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
  apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
  apply (erule rtrancl_induct)
   apply (blast intro: reduction_rls)
  apply (blast intro: trans_rtrancl [THEN transD]
                      contract_combD2 reduction_rls)
  done

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

lemma KIII_contract1: "K\I\(I\I) \\<^sup>1 I"
  by (blast intro: comb_I)

lemma KIII_contract2: "K\I\(I\I) \\<^sup>1 K\I\((K\I)\(K\I))"
  by (unfold I_def) (blast intro: contract.intros)

lemma KIII_contract3: "K\I\((K\I)\(K\I)) \\<^sup>1 I"
  by (blast intro: comb_I)

lemma not_diamond_contract: "\ diamond(contract)"
    unfolding diamond_def
  apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
    elim!: I_contract_E)
  done

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

text \<open>For type checking: replaces \<open>a \<Rrightarrow>\<^sup>1 b\<close> by \<open>a, b
  \<in> comb\<close>\<close>
lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
  and parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
  and parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]

lemma field_parcontract_eq: "field(parcontract) = comb"
  by (blast intro: parcontract.K elim!: parcontract_combE2)

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 parcontract.intros [intro]

subsection \<open>Basic properties of parallel contraction\<close>

lemma K1_parcontractD [dest!]:
    "K\p \\<^sup>1 r \ (\p'. r = K\p' \ p \\<^sup>1 p')"
  by auto

lemma S1_parcontractD [dest!]:
    "S\p \\<^sup>1 r \ (\p'. r = S\p' \ p \\<^sup>1 p')"
  by auto

lemma S2_parcontractD [dest!]:
    "S\p\q \\<^sup>1 r \ (\p' q'. r = S\p'\q' \ p \\<^sup>1 p' \ q \\<^sup>1 q')"
  by auto

lemma diamond_parcontract: "diamond(parcontract)"
  \<comment> \<open>Church-Rosser property for parallel contraction\<close>
    unfolding diamond_def
  apply (rule impI [THEN allI, THEN allI])
  apply (erule parcontract.induct)
     apply (blast elim!: comb.free_elims  intro: parcontract_combD2)+
  done

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

lemma contract_imp_parcontract: "p\\<^sup>1q \ p\\<^sup>1q"
  by (induct set: contract) auto

lemma reduce_imp_parreduce: "p\q \ p\q"
  apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
  apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
  apply (erule rtrancl_induct)
   apply (blast intro: r_into_trancl)
  apply (blast intro: contract_imp_parcontract r_into_trancl
    trans_trancl [THEN transD])
  done

lemma parcontract_imp_reduce: "p\\<^sup>1q \ p\q"
  apply (induct set: parcontract)
     apply (blast intro: reduction_rls)
    apply (blast intro: reduction_rls)
   apply (blast intro: reduction_rls)
  apply (blast intro: trans_rtrancl [THEN transD]
    Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
  done

lemma parreduce_imp_reduce: "p\q \ p\q"
  apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
  apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
  apply (erule trancl_induct, erule parcontract_imp_reduce)
  apply (erule trans_rtrancl [THEN transD])
  apply (erule parcontract_imp_reduce)
  done

lemma parreduce_iff_reduce: "p\q \ p\q"
  by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)

end

quality95%

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