# Theory Comb

Up to index of Isabelle/ZF/Induct

theory Comb
imports Main
begin

    (*  Title:      ZF/Induct/Comb.thy
        ID:         $Id: Comb.thy,v 1.7 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson
        Copyright   1994  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}.
    *}

    subsection {* Definitions *}

    text {* Datatype definition of combinators @{text S} and @{text K}. *}

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

    text {*
      Inductive definition of contractions, @{text "-1->"} and
      (multi-step) reductions, @{text "--->"}.
    *}

    consts
      contract  :: i
    syntax
      "_contract"       :: "[i,i] => o"    (infixl "-1->" 50)
      "_contract_multi" :: "[i,i] => o"    (infixl "--->" 50)
    translations
      "p -1-> q" == "<p,q> ∈ contract"
      "p ---> q" == "<p,q> ∈ contract^*"

    syntax (xsymbols)
      "comb.app"    :: "[i, i] => i"             (infixl "•" 90)

    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-1->q;  r ∈ comb |] ==> p•r -1-> q•r"
        Ap2: "[| p-1->q;  r ∈ comb |] ==> r•p -1-> r•q"
      type_intros comb.intros

    text {*
      Inductive definition of parallel contractions, @{text "=1=>"} and
      (multi-step) parallel reductions, @{text "===>"}.
    *}

    consts
      parcontract :: i
    syntax
      "_parcontract" :: "[i,i] => o"    (infixl "=1=>" 50)
      "_parcontract_multi" :: "[i,i] => o"    (infixl "===>" 50)
    translations
      "p =1=> q" == "<p,q> ∈ parcontract"
      "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=1=>q;  r=1=>s |] ==> p•r =1=> q•s"
      type_intros comb.intros

    text {*
      Misc definitions.
    *}

    constdefs
      I :: i
      "I == S•K•K"

      diamond :: "i => o"
      "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"

    declare comb.intros [intro!]

    subsection {* Results about Contraction *}

    text {*
      For type checking: replaces @{term "a -1-> b"} by @{text "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"
      -- {* Example only: not used *}
      by (unfold I_def) (blast intro: reduction_rls)

    lemma comb_I: "I ∈ comb"
      by (unfold I_def) 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 @{text "-1->"}. *}

    lemma KIII_contract1: "K•I•(I•I) -1-> I"
      by (blast intro: comb.intros contract.K comb_I)

    lemma KIII_contract2: "K•I•(I•I) -1-> K•I•((K•I)•(K•I))"
      by (unfold I_def) (blast intro: comb.intros contract.intros)

    lemma KIII_contract3: "K•I•((K•I)•(K•I)) -1-> I"
      by (blast intro: comb.intros contract.K 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 @{text "a =1=> b"} by @{text "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)"
      -- {* Church-Rosser property for parallel contraction *}
      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-1->q ==> p=1=>q"
      by (erule contract.induct) 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=1=>q ==> p--->q"
      apply (erule parcontract.induct)
         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

### Definitions

### Transitive closure preserves the Church-Rosser property

lemma diamond_strip_lemmaD:

      [| diamond(r); ⟨x, y⟩ ∈ r^+; ⟨x, y'⟩ ∈ r |] ==> ∃z. ⟨y', z⟩ ∈ r^+ ∧ ⟨y, z⟩ ∈ r

lemma diamond_trancl:

      diamond(r) ==> diamond(r^+)

lemmas Ap_E:

      [| comb.app(p, q) ∈ comb; [| p ∈ comb; q ∈ comb |] ==> Q |] ==> Q

### Results about Contraction

lemmas contract_combE2:

      [| a -1-> b; [| a ∈ comb; b ∈ comb |] ==> P |] ==> P

and contract_combD1:

      a -1-> b ==> a ∈ comb

and contract_combD2:

      a -1-> b ==> b ∈ comb

lemmas contract_combE2:

      [| a -1-> b; [| a ∈ comb; b ∈ comb |] ==> P |] ==> P

and contract_combD1:

      a -1-> b ==> a ∈ comb

and contract_combD2:

      a -1-> b ==> b ∈ comb

lemma field_contract_eq:

      field(contract) = comb

lemmas reduction_refl:

      a ∈ comb ==> a ---> a

lemmas reduction_refl:

      a ∈ comb ==> a ---> a

lemmas rtrancl_into_rtrancl2:

      [| ⟨a, b⟩ ∈ r1; ⟨b, c⟩ ∈ r1^* |] ==> ⟨a, c⟩ ∈ r1^*

lemmas rtrancl_into_rtrancl2:

      [| ⟨a, b⟩ ∈ r1; ⟨b, c⟩ ∈ r1^* |] ==> ⟨a, c⟩ ∈ r1^*

lemmas reduction_rls:

      [| b ∈ comb; q3 ∈ comb; b ---> c |] ==> comb.app(comb.app(K, b), q3) ---> c

      [| p3 ∈ comb; q3 ∈ comb; r3 ∈ comb;
         comb.app(comb.app(p3, r3), comb.app(q3, r3)) ---> c |]
      ==> comb.app(comb.app(comb.app(S, p3), q3), r3) ---> c

      [| p3 -1-> q3; r3 ∈ comb; comb.app(q3, r3) ---> c |] ==> comb.app(p3, r3) ---> c

      [| p3 -1-> q3; r3 ∈ comb; comb.app(r3, q3) ---> c |] ==> comb.app(r3, p3) ---> c

lemmas reduction_rls:

      [| b ∈ comb; q3 ∈ comb; b ---> c |] ==> comb.app(comb.app(K, b), q3) ---> c

      [| p3 ∈ comb; q3 ∈ comb; r3 ∈ comb;
         comb.app(comb.app(p3, r3), comb.app(q3, r3)) ---> c |]
      ==> comb.app(comb.app(comb.app(S, p3), q3), r3) ---> c

      [| p3 -1-> q3; r3 ∈ comb; comb.app(q3, r3) ---> c |] ==> comb.app(p3, r3) ---> c

      [| p3 -1-> q3; r3 ∈ comb; comb.app(r3, q3) ---> c |] ==> comb.app(r3, p3) ---> c

lemma

      p ∈ comb ==> comb.app(I, p) ---> p

lemma comb_I:

      I ∈ comb

### Non-contraction results

lemmas K_contractE:

      K -1-> r ==> Q

and S_contractE:

      S -1-> r ==> Q

and Ap_contractE:

      [| comb.app(p, q) -1-> r; [| r ∈ comb; q ∈ comb; p = comb.app(K, r) |] ==> Q;
         !!p q. [| p ∈ comb; q ∈ comb; q ∈ comb;
                   r = comb.app(comb.app(p, q), comb.app(q, q));
                   p = comb.app(comb.app(S, p), q) |]
                ==> Q;
         !!q. [| p -1-> q; q ∈ comb; r = comb.app(q, q) |] ==> Q;
         !!q. [| q -1-> q; p ∈ comb; r = comb.app(p, q) |] ==> Q |]
      ==> Q

lemma I_contract_E:

      I -1-> r ==> P

lemma K1_contractD:

      comb.app(K, p) -1-> r ==> ∃q. r = comb.app(K, q) ∧ p -1-> q

lemma Ap_reduce1:

      [| p ---> q; r ∈ comb |] ==> comb.app(p, r) ---> comb.app(q, r)

lemma Ap_reduce2:

      [| p ---> q; r ∈ comb |] ==> comb.app(r, p) ---> comb.app(r, q)

lemma KIII_contract1:

      comb.app(comb.app(K, I), comb.app(I, I)) -1-> I

lemma KIII_contract2:

      comb.app(comb.app(K, I), comb.app(I, I)) -1->
      comb.app(comb.app(K, I), comb.app(comb.app(K, I), comb.app(K, I)))

lemma KIII_contract3:

      comb.app(comb.app(K, I), comb.app(comb.app(K, I), comb.app(K, I))) -1-> I

lemma not_diamond_contract:

      ¬ diamond(contract)

### Results about Parallel Contraction

lemmas parcontract_combE2:

      [| a =1=> b; [| a ∈ comb; b ∈ comb |] ==> P |] ==> P

and parcontract_combD1:

      a =1=> b ==> a ∈ comb

and parcontract_combD2:

      a =1=> b ==> b ∈ comb

lemmas parcontract_combE2:

      [| a =1=> b; [| a ∈ comb; b ∈ comb |] ==> P |] ==> P

and parcontract_combD1:

      a =1=> b ==> a ∈ comb

and parcontract_combD2:

      a =1=> b ==> b ∈ comb

lemma field_parcontract_eq:

      field(parcontract) = comb

lemmas K_parcontractE:

      [| K =1=> r; [| K ∈ comb; r = K |] ==> Q |] ==> Q

and S_parcontractE:

      [| S =1=> r; [| S ∈ comb; r = S |] ==> Q |] ==> Q

and Ap_parcontractE:

      [| comb.app(p, q) =1=> r; [| comb.app(p, q) ∈ comb; r = comb.app(p, q) |] ==> Q;
         [| r ∈ comb; q ∈ comb; p = comb.app(K, r) |] ==> Q;
         !!p q. [| p ∈ comb; q ∈ comb; q ∈ comb;
                   r = comb.app(comb.app(p, q), comb.app(q, q));
                   p = comb.app(comb.app(S, p), q) |]
                ==> Q;
         !!q s. [| p =1=> q; q =1=> s; r = comb.app(q, s) |] ==> Q |]
      ==> Q

### Basic properties of parallel contraction

lemma K1_parcontractD:

      comb.app(K, p) =1=> r ==> ∃p'. r = comb.app(K, p') ∧ p =1=> p'

lemma S1_parcontractD:

      comb.app(S, p) =1=> r ==> ∃p'. r = comb.app(S, p') ∧ p =1=> p'

lemma S2_parcontractD:

      comb.app(comb.app(S, p), q) =1=> r
      ==> ∃p' q'. r = comb.app(comb.app(S, p'), q') ∧ p =1=> p' ∧ q =1=> q'

lemma diamond_parcontract:

      diamond(parcontract)

lemma contract_imp_parcontract:

      p -1-> q ==> p =1=> q

lemma reduce_imp_parreduce:

      p ---> q ==> p ===> q

lemma parcontract_imp_reduce:

      p =1=> q ==> p ---> q

lemma parreduce_imp_reduce:

      p ===> q ==> p ---> q

lemma parreduce_iff_reduce:

      p ===> q <-> p ---> q