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