Theory Comb
section ‹Combinatory Logic example: the Church-Rosser Theorem›
theory Comb
imports ZF
begin
text ‹
Curiously, combinators do not include free variables.
Example taken from @{cite camilleri92}.
›
subsection ‹Definitions›
text ‹Datatype definition of combinators ‹S› and ‹K›.›
consts comb :: i
datatype comb =
K
| S
| app ("p ∈ comb", "q ∈ comb") (infixl ‹∙› 90)
text ‹
Inductive definition of contractions, ‹→⇧1› and
(multi-step) reductions, ‹→›.
›
consts contract :: i
abbreviation contract_syntax :: "[i,i] ⇒ o" (infixl ‹→⇧1› 50)
where "p →⇧1 q ≡ <p,q> ∈ contract"
abbreviation contract_multi :: "[i,i] ⇒ o" (infixl ‹→› 50)
where "p → q ≡ <p,q> ∈ contract^*"
inductive
domains "contract" ⊆ "comb × comb"
intros
K: "[| p ∈ comb; q ∈ comb |] ==> K∙p∙q →⇧1 p"
S: "[| p ∈ comb; q ∈ comb; r ∈ comb |] ==> S∙p∙q∙r →⇧1 (p∙r)∙(q∙r)"
Ap1: "[| p→⇧1q; r ∈ comb |] ==> p∙r →⇧1 q∙r"
Ap2: "[| p→⇧1q; r ∈ comb |] ==> r∙p →⇧1 r∙q"
type_intros comb.intros
text ‹
Inductive definition of parallel contractions, ‹⇛⇧1› and
(multi-step) parallel reductions, ‹⇛›.
›
consts parcontract :: i
abbreviation parcontract_syntax :: "[i,i] => o" (infixl ‹⇛⇧1› 50)
where "p ⇛⇧1 q == <p,q> ∈ parcontract"
abbreviation parcontract_multi :: "[i,i] => o" (infixl ‹⇛› 50)
where "p ⇛ q == <p,q> ∈ parcontract^+"
inductive
domains "parcontract" ⊆ "comb × comb"
intros
refl: "[| p ∈ comb |] ==> p ⇛⇧1 p"
K: "[| p ∈ comb; q ∈ comb |] ==> K∙p∙q ⇛⇧1 p"
S: "[| p ∈ comb; q ∈ comb; r ∈ comb |] ==> S∙p∙q∙r ⇛⇧1 (p∙r)∙(q∙r)"
Ap: "[| p⇛⇧1q; r⇛⇧1s |] ==> p∙r ⇛⇧1 q∙s"
type_intros comb.intros
text ‹
Misc definitions.
›
definition I :: i
where "I ≡ S∙K∙K"
definition diamond :: "i ⇒ o"
where "diamond(r) ≡
∀x y. <x,y>∈r ⟶ (∀y'. <x,y'>∈r ⟶ (∃z. <y,z>∈r & <y',z> ∈ r))"
subsection ‹Transitive closure preserves the Church-Rosser property›
lemma diamond_strip_lemmaD [rule_format]:
"[| diamond(r); <x,y>:r^+ |] ==>
∀y'. <x,y'>:r ⟶ (∃z. <y',z>: r^+ & <y,z>: r)"
apply (unfold 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 ‹Results about Contraction›
text ‹
For type checking: replaces \<^term>‹a →⇧1 b› by ‹a, b ∈
comb›.
›
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"
unfolding I_def by (blast intro: reduction_rls)
lemma comb_I: "I ∈ comb"
unfolding I_def by blast
subsection ‹Non-contraction results›
text ‹Derive a case for each combinator constructor.›
inductive_cases K_contractE [elim!]: "K →⇧1 r"
and S_contractE [elim!]: "S →⇧1 r"
and Ap_contractE [elim!]: "p∙q →⇧1 r"
lemma I_contract_E: "I →⇧1 r ==> P"
by (auto simp add: I_def)
lemma K1_contractD: "K∙p →⇧1 r ==> (∃q. r = K∙q & p →⇧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 ‹Counterexample to the diamond property for ‹→⇧1›.›
lemma KIII_contract1: "K∙I∙(I∙I) →⇧1 I"
by (blast intro: comb_I)
lemma KIII_contract2: "K∙I∙(I∙I) →⇧1 K∙I∙((K∙I)∙(K∙I))"
by (unfold I_def) (blast intro: contract.intros)
lemma KIII_contract3: "K∙I∙((K∙I)∙(K∙I)) →⇧1 I"
by (blast intro: comb_I)
lemma not_diamond_contract: "¬ diamond(contract)"
apply (unfold diamond_def)
apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
elim!: I_contract_E)
done
subsection ‹Results about Parallel Contraction›
text ‹For type checking: replaces ‹a ⇛⇧1 b› by ‹a, b
∈ comb››
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 ‹Derive a case for each combinator constructor.›
inductive_cases
K_parcontractE [elim!]: "K ⇛⇧1 r"
and S_parcontractE [elim!]: "S ⇛⇧1 r"
and Ap_parcontractE [elim!]: "p∙q ⇛⇧1 r"
declare parcontract.intros [intro]
subsection ‹Basic properties of parallel contraction›
lemma K1_parcontractD [dest!]:
"K∙p ⇛⇧1 r ==> (∃p'. r = K∙p' & p ⇛⇧1 p')"
by auto
lemma S1_parcontractD [dest!]:
"S∙p ⇛⇧1 r ==> (∃p'. r = S∙p' & p ⇛⇧1 p')"
by auto
lemma S2_parcontractD [dest!]:
"S∙p∙q ⇛⇧1 r ==> (∃p' q'. r = S∙p'∙q' & p ⇛⇧1 p' & q ⇛⇧1 q')"
by auto
lemma diamond_parcontract: "diamond(parcontract)"
apply (unfold diamond_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule parcontract.induct)
apply (blast elim!: comb.free_elims intro: parcontract_combD2)+
done
text ‹
\medskip Equivalence of \<^prop>‹p → q› and \<^prop>‹p ⇛ q›.
›
lemma contract_imp_parcontract: "p→⇧1q ==> p⇛⇧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⇛⇧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