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
```