src/ZF/Induct/Comb.thy
author wenzelm
Tue Mar 02 23:59:54 2010 +0100 (2010-03-02)
changeset 35427 ad039d29e01c
parent 35068 544867142ea4
child 46822 95f1e700b712
permissions -rw-r--r--
proper (type_)notation;
     1 (*  Title:      ZF/Induct/Comb.thy
     2     Author:     Lawrence C Paulson
     3     Copyright   1994  University of Cambridge
     4 *)
     5 
     6 header {* Combinatory Logic example: the Church-Rosser Theorem *}
     7 
     8 theory Comb imports Main begin
     9 
    10 text {*
    11   Curiously, combinators do not include free variables.
    12 
    13   Example taken from \cite{camilleri-melham}.
    14 *}
    15 
    16 subsection {* Definitions *}
    17 
    18 text {* Datatype definition of combinators @{text S} and @{text K}. *}
    19 
    20 consts comb :: i
    21 datatype comb =
    22     K
    23   | S
    24   | app ("p \<in> comb", "q \<in> comb")    (infixl "@@" 90)
    25 
    26 notation (xsymbols)
    27   app  (infixl "\<bullet>" 90)
    28 
    29 text {*
    30   Inductive definition of contractions, @{text "-1->"} and
    31   (multi-step) reductions, @{text "--->"}.
    32 *}
    33 
    34 consts
    35   contract  :: i
    36 
    37 abbreviation
    38   contract_syntax :: "[i,i] => o"    (infixl "-1->" 50)
    39   where "p -1-> q == <p,q> \<in> contract"
    40 
    41 abbreviation
    42   contract_multi :: "[i,i] => o"    (infixl "--->" 50)
    43   where "p ---> q == <p,q> \<in> contract^*"
    44 
    45 inductive
    46   domains "contract" \<subseteq> "comb \<times> comb"
    47   intros
    48     K:   "[| p \<in> comb;  q \<in> comb |] ==> K\<bullet>p\<bullet>q -1-> p"
    49     S:   "[| p \<in> comb;  q \<in> comb;  r \<in> comb |] ==> S\<bullet>p\<bullet>q\<bullet>r -1-> (p\<bullet>r)\<bullet>(q\<bullet>r)"
    50     Ap1: "[| p-1->q;  r \<in> comb |] ==> p\<bullet>r -1-> q\<bullet>r"
    51     Ap2: "[| p-1->q;  r \<in> comb |] ==> r\<bullet>p -1-> r\<bullet>q"
    52   type_intros comb.intros
    53 
    54 text {*
    55   Inductive definition of parallel contractions, @{text "=1=>"} and
    56   (multi-step) parallel reductions, @{text "===>"}.
    57 *}
    58 
    59 consts
    60   parcontract :: i
    61 
    62 abbreviation
    63   parcontract_syntax :: "[i,i] => o"    (infixl "=1=>" 50)
    64   where "p =1=> q == <p,q> \<in> parcontract"
    65 
    66 abbreviation
    67   parcontract_multi :: "[i,i] => o"    (infixl "===>" 50)
    68   where "p ===> q == <p,q> \<in> parcontract^+"
    69 
    70 inductive
    71   domains "parcontract" \<subseteq> "comb \<times> comb"
    72   intros
    73     refl: "[| p \<in> comb |] ==> p =1=> p"
    74     K:    "[| p \<in> comb;  q \<in> comb |] ==> K\<bullet>p\<bullet>q =1=> p"
    75     S:    "[| p \<in> comb;  q \<in> comb;  r \<in> comb |] ==> S\<bullet>p\<bullet>q\<bullet>r =1=> (p\<bullet>r)\<bullet>(q\<bullet>r)"
    76     Ap:   "[| p=1=>q;  r=1=>s |] ==> p\<bullet>r =1=> q\<bullet>s"
    77   type_intros comb.intros
    78 
    79 text {*
    80   Misc definitions.
    81 *}
    82 
    83 definition
    84   I :: i  where
    85   "I == S\<bullet>K\<bullet>K"
    86 
    87 definition
    88   diamond :: "i => o"  where
    89   "diamond(r) ==
    90     \<forall>x y. <x,y>\<in>r --> (\<forall>y'. <x,y'>\<in>r --> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
    91 
    92 
    93 subsection {* Transitive closure preserves the Church-Rosser property *}
    94 
    95 lemma diamond_strip_lemmaD [rule_format]:
    96   "[| diamond(r);  <x,y>:r^+ |] ==>
    97     \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
    98   apply (unfold diamond_def)
    99   apply (erule trancl_induct)
   100    apply (blast intro: r_into_trancl)
   101   apply clarify
   102   apply (drule spec [THEN mp], assumption)
   103   apply (blast intro: r_into_trancl trans_trancl [THEN transD])
   104   done
   105 
   106 lemma diamond_trancl: "diamond(r) ==> diamond(r^+)"
   107   apply (simp (no_asm_simp) add: diamond_def)
   108   apply (rule impI [THEN allI, THEN allI])
   109   apply (erule trancl_induct)
   110    apply auto
   111    apply (best intro: r_into_trancl trans_trancl [THEN transD]
   112      dest: diamond_strip_lemmaD)+
   113   done
   114 
   115 inductive_cases Ap_E [elim!]: "p\<bullet>q \<in> comb"
   116 
   117 declare comb.intros [intro!]
   118 
   119 
   120 subsection {* Results about Contraction *}
   121 
   122 text {*
   123   For type checking: replaces @{term "a -1-> b"} by @{text "a, b \<in>
   124   comb"}.
   125 *}
   126 
   127 lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
   128   and contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1]
   129   and contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2]
   130 
   131 lemma field_contract_eq: "field(contract) = comb"
   132   by (blast intro: contract.K elim!: contract_combE2)
   133 
   134 lemmas reduction_refl =
   135   field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl]
   136 
   137 lemmas rtrancl_into_rtrancl2 =
   138   r_into_rtrancl [THEN trans_rtrancl [THEN transD]]
   139 
   140 declare reduction_refl [intro!] contract.K [intro!] contract.S [intro!]
   141 
   142 lemmas reduction_rls =
   143   contract.K [THEN rtrancl_into_rtrancl2]
   144   contract.S [THEN rtrancl_into_rtrancl2]
   145   contract.Ap1 [THEN rtrancl_into_rtrancl2]
   146   contract.Ap2 [THEN rtrancl_into_rtrancl2]
   147 
   148 lemma "p \<in> comb ==> I\<bullet>p ---> p"
   149   -- {* Example only: not used *}
   150   by (unfold I_def) (blast intro: reduction_rls)
   151 
   152 lemma comb_I: "I \<in> comb"
   153   by (unfold I_def) blast
   154 
   155 
   156 subsection {* Non-contraction results *}
   157 
   158 text {* Derive a case for each combinator constructor. *}
   159 
   160 inductive_cases
   161       K_contractE [elim!]: "K -1-> r"
   162   and S_contractE [elim!]: "S -1-> r"
   163   and Ap_contractE [elim!]: "p\<bullet>q -1-> r"
   164 
   165 lemma I_contract_E: "I -1-> r ==> P"
   166   by (auto simp add: I_def)
   167 
   168 lemma K1_contractD: "K\<bullet>p -1-> r ==> (\<exists>q. r = K\<bullet>q & p -1-> q)"
   169   by auto
   170 
   171 lemma Ap_reduce1: "[| p ---> q;  r \<in> comb |] ==> p\<bullet>r ---> q\<bullet>r"
   172   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   173   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   174   apply (erule rtrancl_induct)
   175    apply (blast intro: reduction_rls)
   176   apply (erule trans_rtrancl [THEN transD])
   177   apply (blast intro: contract_combD2 reduction_rls)
   178   done
   179 
   180 lemma Ap_reduce2: "[| p ---> q;  r \<in> comb |] ==> r\<bullet>p ---> r\<bullet>q"
   181   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   182   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   183   apply (erule rtrancl_induct)
   184    apply (blast intro: reduction_rls)
   185   apply (blast intro: trans_rtrancl [THEN transD] 
   186                       contract_combD2 reduction_rls)
   187   done
   188 
   189 text {* Counterexample to the diamond property for @{text "-1->"}. *}
   190 
   191 lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
   192   by (blast intro: comb.intros contract.K comb_I)
   193 
   194 lemma KIII_contract2: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I))"
   195   by (unfold I_def) (blast intro: comb.intros contract.intros)
   196 
   197 lemma KIII_contract3: "K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I)) -1-> I"
   198   by (blast intro: comb.intros contract.K comb_I)
   199 
   200 lemma not_diamond_contract: "\<not> diamond(contract)"
   201   apply (unfold diamond_def)
   202   apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
   203     elim!: I_contract_E)
   204   done
   205 
   206 
   207 subsection {* Results about Parallel Contraction *}
   208 
   209 text {* For type checking: replaces @{text "a =1=> b"} by @{text "a, b
   210   \<in> comb"} *}
   211 lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
   212   and parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
   213   and parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
   214 
   215 lemma field_parcontract_eq: "field(parcontract) = comb"
   216   by (blast intro: parcontract.K elim!: parcontract_combE2)
   217 
   218 text {* Derive a case for each combinator constructor. *}
   219 inductive_cases
   220       K_parcontractE [elim!]: "K =1=> r"
   221   and S_parcontractE [elim!]: "S =1=> r"
   222   and Ap_parcontractE [elim!]: "p\<bullet>q =1=> r"
   223 
   224 declare parcontract.intros [intro]
   225 
   226 
   227 subsection {* Basic properties of parallel contraction *}
   228 
   229 lemma K1_parcontractD [dest!]:
   230     "K\<bullet>p =1=> r ==> (\<exists>p'. r = K\<bullet>p' & p =1=> p')"
   231   by auto
   232 
   233 lemma S1_parcontractD [dest!]:
   234     "S\<bullet>p =1=> r ==> (\<exists>p'. r = S\<bullet>p' & p =1=> p')"
   235   by auto
   236 
   237 lemma S2_parcontractD [dest!]:
   238     "S\<bullet>p\<bullet>q =1=> r ==> (\<exists>p' q'. r = S\<bullet>p'\<bullet>q' & p =1=> p' & q =1=> q')"
   239   by auto
   240 
   241 lemma diamond_parcontract: "diamond(parcontract)"
   242   -- {* Church-Rosser property for parallel contraction *}
   243   apply (unfold diamond_def)
   244   apply (rule impI [THEN allI, THEN allI])
   245   apply (erule parcontract.induct)
   246      apply (blast elim!: comb.free_elims  intro: parcontract_combD2)+
   247   done
   248 
   249 text {*
   250   \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
   251 *}
   252 
   253 lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
   254   by (induct set: contract) auto
   255 
   256 lemma reduce_imp_parreduce: "p--->q ==> p===>q"
   257   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   258   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   259   apply (erule rtrancl_induct)
   260    apply (blast intro: r_into_trancl)
   261   apply (blast intro: contract_imp_parcontract r_into_trancl
   262     trans_trancl [THEN transD])
   263   done
   264 
   265 lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
   266   apply (induct set: parcontract)
   267      apply (blast intro: reduction_rls)
   268     apply (blast intro: reduction_rls)
   269    apply (blast intro: reduction_rls)
   270   apply (blast intro: trans_rtrancl [THEN transD]
   271     Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
   272   done
   273 
   274 lemma parreduce_imp_reduce: "p===>q ==> p--->q"
   275   apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
   276   apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
   277   apply (erule trancl_induct, erule parcontract_imp_reduce)
   278   apply (erule trans_rtrancl [THEN transD])
   279   apply (erule parcontract_imp_reduce)
   280   done
   281 
   282 lemma parreduce_iff_reduce: "p===>q <-> p--->q"
   283   by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
   284 
   285 end