(* Title: HOL/Induct/Comb.thy ID: $Id: Comb.thy,v 1.11 2005/06/28 13:28:04 paulson Exp $ Author: Lawrence C Paulson Copyright 1996 University of Cambridge *) header {* Combinatory Logic example: the Church-Rosser Theorem *} theory Comb imports Main begin text {* Curiously, combinators do not include free variables. Example taken from \cite{camilleri-melham}. HOL system proofs may be found in the HOL distribution at .../contrib/rule-induction/cl.ml *} subsection {* Definitions *} text {* Datatype definition of combinators @{text S} and @{text K}. *} datatype comb = K | S | "##" comb comb (infixl 90) text {* Inductive definition of contractions, @{text "-1->"} and (multi-step) reductions, @{text "--->"}. *} consts contract :: "(comb*comb) set" "-1->" :: "[comb,comb] => bool" (infixl 50) "--->" :: "[comb,comb] => bool" (infixl 50) translations "x -1-> y" == "(x,y) ∈ contract" "x ---> y" == "(x,y) ∈ contract^*" syntax (xsymbols) "op ##" :: "[comb,comb] => comb" (infixl "•" 90) inductive contract intros K: "K##x##y -1-> x" S: "S##x##y##z -1-> (x##z)##(y##z)" Ap1: "x-1->y ==> x##z -1-> y##z" Ap2: "x-1->y ==> z##x -1-> z##y" text {* Inductive definition of parallel contractions, @{text "=1=>"} and (multi-step) parallel reductions, @{text "===>"}. *} consts parcontract :: "(comb*comb) set" "=1=>" :: "[comb,comb] => bool" (infixl 50) "===>" :: "[comb,comb] => bool" (infixl 50) translations "x =1=> y" == "(x,y) ∈ parcontract" "x ===> y" == "(x,y) ∈ parcontract^*" inductive parcontract intros refl: "x =1=> x" K: "K##x##y =1=> x" S: "S##x##y##z =1=> (x##z)##(y##z)" Ap: "[| x=1=>y; z=1=>w |] ==> x##z =1=> y##w" text {* Misc definitions. *} constdefs I :: comb "I == S##K##K" diamond :: "('a * 'a)set => bool" --{*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 (simp (no_asm_simp) add: diamond_def) 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 (** Counterexample to the diamond property for -1-> **) lemma KIII_contract1: "K##I##(I##I) -1-> I" by (rule contract.K) lemma KIII_contract2: "K##I##(I##I) -1-> K##I##((K##I)##(K##I))" by (unfold I_def, blast) lemma KIII_contract3: "K##I##((K##I)##(K##I)) -1-> I" by blast lemma not_diamond_contract: "~ diamond(contract)" apply (unfold diamond_def) apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3) done subsection {* Results about Parallel Contraction *} 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 {* \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}. *} lemma contract_subset_parcontract: "contract <= parcontract" apply (rule subsetI) apply (simp only: split_tupled_all) apply (erule contract.induct, blast+) done 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^*" apply (rule subsetI) apply (simp only: split_tupled_all) apply (erule parcontract.induct, blast+) done lemma reduce_eq_parreduce: "contract^* = parcontract^*" by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono] parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+ lemma diamond_reduce: "diamond(contract^*)" by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract) end
lemma diamond_strip_lemmaE:
[| diamond r; (x, y) ∈ r*; (x, y') ∈ r |] ==> ∃z. (y', z) ∈ r* ∧ (y, z) ∈ r
lemma diamond_rtrancl:
diamond r ==> diamond (r*)
lemmas K_contractE:
K -1-> r ==> P
and S_contractE:
S -1-> r ==> P
and Ap_contractE:
[| p ## q -1-> r; p = K ## r ==> P; !!x y. [| r = x ## q ## (y ## q); p = S ## x ## y |] ==> P; !!y. [| p -1-> y; r = y ## q |] ==> P; !!y. [| q -1-> y; r = p ## y |] ==> P |] ==> P
lemma I_contract_E:
I -1-> z ==> P
lemma K1_contractD:
K ## x -1-> z ==> ∃x'. z = K ## x' ∧ x -1-> x'
lemma Ap_reduce1:
x ---> y ==> x ## z ---> y ## z
lemma Ap_reduce2:
x ---> y ==> z ## x ---> z ## y
lemma KIII_contract1:
K ## I ## (I ## I) -1-> I
lemma KIII_contract2:
K ## I ## (I ## I) -1-> K ## I ## (K ## I ## (K ## I))
lemma KIII_contract3:
K ## I ## (K ## I ## (K ## I)) -1-> I
lemma not_diamond_contract:
¬ diamond contract
lemmas K_parcontractE:
[| K =1=> r; r = K ==> P |] ==> P
and S_parcontractE:
[| S =1=> r; r = S ==> P |] ==> P
and Ap_parcontractE:
[| p ## q =1=> r; r = p ## q ==> P; p = K ## r ==> P; !!x y. [| r = x ## q ## (y ## q); p = S ## x ## y |] ==> P; !!w y. [| p =1=> y; q =1=> w; r = y ## w |] ==> P |] ==> P
lemma K1_parcontractD:
K ## x =1=> z ==> ∃x'. z = K ## x' ∧ x =1=> x'
lemma S1_parcontractD:
S ## x =1=> z ==> ∃x'. z = S ## x' ∧ x =1=> x'
lemma S2_parcontractD:
S ## x ## y =1=> z ==> ∃x' y'. z = S ## x' ## y' ∧ x =1=> x' ∧ y =1=> y'
lemma diamond_parcontract:
diamond parcontract
lemma contract_subset_parcontract:
contract ⊆ parcontract
lemma reduce_I:
I ## x ---> x
lemma parcontract_subset_reduce:
parcontract ⊆ contract*
lemma reduce_eq_parreduce:
contract* = parcontract*
lemma diamond_reduce:
diamond (contract*)