# Theory Comb

theory Comb
imports Main
```(*  Title:      HOL/Induct/Comb.thy
Author:     Lawrence C Paulson
*)

section ‹Combinatory Logic example: the Church-Rosser Theorem›

theory Comb
imports Main
begin

text ‹
Curiously, combinators do not include free variables.

Example taken from @{cite camilleri92}.
›

subsection ‹Definitions›

text ‹Datatype definition of combinators ‹S› and ‹K›.›

datatype comb = K
| S
| Ap comb comb (infixl "∙" 90)

text ‹
Inductive definition of contractions, ‹→⇧1› and
(multi-step) reductions, ‹→›.
›

inductive_set contract :: "(comb*comb) set"
and contract_rel1 :: "[comb,comb] ⇒ bool"  (infixl "→⇧1" 50)
where
"x →⇧1 y == (x,y) ∈ contract"
| K:     "K∙x∙y →⇧1 x"
| S:     "S∙x∙y∙z →⇧1 (x∙z)∙(y∙z)"
| Ap1:   "x→⇧1y ⟹ x∙z →⇧1 y∙z"
| Ap2:   "x→⇧1y ⟹ z∙x →⇧1 z∙y"

abbreviation
contract_rel :: "[comb,comb] ⇒ bool"   (infixl "→" 50) where
"x → y == (x,y) ∈ contract⇧*"

text ‹
Inductive definition of parallel contractions, ‹⇛⇧1› and
(multi-step) parallel reductions, ‹⇛›.
›

inductive_set parcontract :: "(comb*comb) set"
and parcontract_rel1 :: "[comb,comb] ⇒ bool"  (infixl "⇛⇧1" 50)
where
"x ⇛⇧1 y == (x,y) ∈ parcontract"
| refl:  "x ⇛⇧1 x"
| K:     "K∙x∙y ⇛⇧1 x"
| S:     "S∙x∙y∙z ⇛⇧1 (x∙z)∙(y∙z)"
| Ap:    "[| x⇛⇧1y;  z⇛⇧1w |] ==> x∙z ⇛⇧1 y∙w"

abbreviation
parcontract_rel :: "[comb,comb] ⇒ bool"   (infixl "⇛" 50) where
"x ⇛ y == (x,y) ∈ parcontract⇧*"

text ‹
Misc definitions.
›

definition
I :: comb where
"I = S∙K∙K"

definition
diamond   :: "('a * 'a)set ⇒ bool" where
― ‹confluence; Lambda/Commutation treats this more abstractly›
"diamond(r) = (∀x y. (x,y) ∈ r -->
(∀y'. (x,y') ∈ r -->
(∃z. (y,z) ∈ r & (y',z) ∈ r)))"

subsection ‹Reflexive/Transitive closure preserves Church-Rosser property›

text‹So does the Transitive closure, with a similar proof›

text‹Strip lemma.
The induction hypothesis covers all but the last diamond of the strip.›
lemma diamond_strip_lemmaE [rule_format]:
"[| diamond(r);  (x,y) ∈ r⇧* |] ==>
∀y'. (x,y') ∈ r --> (∃z. (y',z) ∈ r⇧* & (y,z) ∈ r)"
apply (unfold diamond_def)
apply (erule rtrancl_induct)
apply (meson rtrancl_refl)
apply (meson rtrancl_trans r_into_rtrancl)
done

lemma diamond_rtrancl: "diamond(r) ⟹ diamond(r⇧*)"
apply (rule impI [THEN allI, THEN allI])
apply (erule rtrancl_induct, blast)
apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE)
done

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"

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

lemma I_contract_E [elim!]: "I →⇧1 z ⟹ P"
by (unfold I_def, blast)

lemma K1_contractD [elim!]: "K∙x →⇧1 z ⟹ (∃x'. z = K∙x' & x →⇧1 x')"
by blast

lemma Ap_reduce1 [intro]: "x → y ⟹ x∙z → y∙z"
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_trans)+
done

lemma Ap_reduce2 [intro]: "x → y ⟹ z∙x → z∙y"
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_trans)+
done

text ‹Counterexample to the diamond property for @{term "x →⇧1 y"}›

lemma not_diamond_contract: "~ diamond(contract)"
by (unfold diamond_def, metis S_contractE contract.K)

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]

(*** Basic properties of parallel contraction ***)

subsection ‹Basic properties of parallel contraction›

lemma K1_parcontractD [dest!]: "K∙x ⇛⇧1 z ⟹ (∃x'. z = K∙x' & x ⇛⇧1 x')"
by blast

lemma S1_parcontractD [dest!]: "S∙x ⇛⇧1 z ⟹ (∃x'. z = S∙x' & x ⇛⇧1 x')"
by blast

lemma S2_parcontractD [dest!]:
"S∙x∙y ⇛⇧1 z ⟹ (∃x' y'. z = S∙x'∙y' & x ⇛⇧1 x' & y ⇛⇧1 y')"
by blast

text‹The rules above are not essential but make proofs much faster›

text‹Church-Rosser property for parallel contraction›
lemma diamond_parcontract: "diamond parcontract"
apply (unfold diamond_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule parcontract.induct, fast+)
done

text ‹
┉
Equivalence of @{prop "p → q"} and @{prop "p ⇛ q"}.
›

lemma contract_subset_parcontract: "contract ⊆ parcontract"
by (auto, erule contract.induct, blast+)

text‹Reductions: simply throw together reflexivity, transitivity and
the one-step reductions›

declare r_into_rtrancl [intro]  rtrancl_trans [intro]

(*Example only: not used*)
lemma reduce_I: "I∙x → x"
by (unfold I_def, blast)

lemma parcontract_subset_reduce: "parcontract ⊆ contract⇧*"
by (auto, erule parcontract.induct, blast+)

lemma reduce_eq_parreduce: "contract⇧* = parcontract⇧*"
by (metis contract_subset_parcontract parcontract_subset_reduce rtrancl_subset)

theorem diamond_reduce: "diamond(contract⇧*)"
by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract)

end
```