src/HOL/Induct/Comb.thy
 author urbanc Tue Jun 05 09:56:19 2007 +0200 (2007-06-05) changeset 23243 a37d3e6e8323 parent 21404 eb85850d3eb7 child 23746 a455e69c31cc permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
```     1 (*  Title:      HOL/Induct/Comb.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson
```
```     4     Copyright   1996  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {* Combinatory Logic example: the Church-Rosser Theorem *}
```
```     8
```
```     9 theory Comb imports Main begin
```
```    10
```
```    11 text {*
```
```    12   Curiously, combinators do not include free variables.
```
```    13
```
```    14   Example taken from \cite{camilleri-melham}.
```
```    15
```
```    16 HOL system proofs may be found in the HOL distribution at
```
```    17    .../contrib/rule-induction/cl.ml
```
```    18 *}
```
```    19
```
```    20 subsection {* Definitions *}
```
```    21
```
```    22 text {* Datatype definition of combinators @{text S} and @{text K}. *}
```
```    23
```
```    24 datatype comb = K
```
```    25               | S
```
```    26               | Ap comb comb (infixl "##" 90)
```
```    27
```
```    28 notation (xsymbols)
```
```    29   Ap  (infixl "\<bullet>" 90)
```
```    30
```
```    31
```
```    32 text {*
```
```    33   Inductive definition of contractions, @{text "-1->"} and
```
```    34   (multi-step) reductions, @{text "--->"}.
```
```    35 *}
```
```    36
```
```    37 consts
```
```    38   contract  :: "(comb*comb) set"
```
```    39
```
```    40 abbreviation
```
```    41   contract_rel1 :: "[comb,comb] => bool"   (infixl "-1->" 50) where
```
```    42   "x -1-> y == (x,y) \<in> contract"
```
```    43
```
```    44 abbreviation
```
```    45   contract_rel :: "[comb,comb] => bool"   (infixl "--->" 50) where
```
```    46   "x ---> y == (x,y) \<in> contract^*"
```
```    47
```
```    48 inductive contract
```
```    49   intros
```
```    50     K:     "K##x##y -1-> x"
```
```    51     S:     "S##x##y##z -1-> (x##z)##(y##z)"
```
```    52     Ap1:   "x-1->y ==> x##z -1-> y##z"
```
```    53     Ap2:   "x-1->y ==> z##x -1-> z##y"
```
```    54
```
```    55 text {*
```
```    56   Inductive definition of parallel contractions, @{text "=1=>"} and
```
```    57   (multi-step) parallel reductions, @{text "===>"}.
```
```    58 *}
```
```    59
```
```    60 consts
```
```    61   parcontract :: "(comb*comb) set"
```
```    62
```
```    63 abbreviation
```
```    64   parcontract_rel1 :: "[comb,comb] => bool"   (infixl "=1=>" 50) where
```
```    65   "x =1=> y == (x,y) \<in> parcontract"
```
```    66
```
```    67 abbreviation
```
```    68   parcontract_rel :: "[comb,comb] => bool"   (infixl "===>" 50) where
```
```    69   "x ===> y == (x,y) \<in> parcontract^*"
```
```    70
```
```    71 inductive parcontract
```
```    72   intros
```
```    73     refl:  "x =1=> x"
```
```    74     K:     "K##x##y =1=> x"
```
```    75     S:     "S##x##y##z =1=> (x##z)##(y##z)"
```
```    76     Ap:    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
```
```    77
```
```    78 text {*
```
```    79   Misc definitions.
```
```    80 *}
```
```    81
```
```    82 definition
```
```    83   I :: comb where
```
```    84   "I = S##K##K"
```
```    85
```
```    86 definition
```
```    87   diamond   :: "('a * 'a)set => bool" where
```
```    88     --{*confluence; Lambda/Commutation treats this more abstractly*}
```
```    89   "diamond(r) = (\<forall>x y. (x,y) \<in> r -->
```
```    90                   (\<forall>y'. (x,y') \<in> r -->
```
```    91                     (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))"
```
```    92
```
```    93
```
```    94 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
```
```    95
```
```    96 text{*So does the Transitive closure, with a similar proof*}
```
```    97
```
```    98 text{*Strip lemma.
```
```    99    The induction hypothesis covers all but the last diamond of the strip.*}
```
```   100 lemma diamond_strip_lemmaE [rule_format]:
```
```   101     "[| diamond(r);  (x,y) \<in> r^* |] ==>
```
```   102           \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
```
```   103 apply (unfold diamond_def)
```
```   104 apply (erule rtrancl_induct)
```
```   105 apply (meson rtrancl_refl)
```
```   106 apply (meson rtrancl_trans r_into_rtrancl)
```
```   107 done
```
```   108
```
```   109 lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)"
```
```   110 apply (simp (no_asm_simp) add: diamond_def)
```
```   111 apply (rule impI [THEN allI, THEN allI])
```
```   112 apply (erule rtrancl_induct, blast)
```
```   113 apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE)
```
```   114 done
```
```   115
```
```   116
```
```   117 subsection {* Non-contraction results *}
```
```   118
```
```   119 text {* Derive a case for each combinator constructor. *}
```
```   120
```
```   121 inductive_cases
```
```   122       K_contractE [elim!]: "K -1-> r"
```
```   123   and S_contractE [elim!]: "S -1-> r"
```
```   124   and Ap_contractE [elim!]: "p##q -1-> r"
```
```   125
```
```   126 declare contract.K [intro!] contract.S [intro!]
```
```   127 declare contract.Ap1 [intro] contract.Ap2 [intro]
```
```   128
```
```   129 lemma I_contract_E [elim!]: "I -1-> z ==> P"
```
```   130 by (unfold I_def, blast)
```
```   131
```
```   132 lemma K1_contractD [elim!]: "K##x -1-> z ==> (\<exists>x'. z = K##x' & x -1-> x')"
```
```   133 by blast
```
```   134
```
```   135 lemma Ap_reduce1 [intro]: "x ---> y ==> x##z ---> y##z"
```
```   136 apply (erule rtrancl_induct)
```
```   137 apply (blast intro: rtrancl_trans)+
```
```   138 done
```
```   139
```
```   140 lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y"
```
```   141 apply (erule rtrancl_induct)
```
```   142 apply (blast intro: rtrancl_trans)+
```
```   143 done
```
```   144
```
```   145 (** Counterexample to the diamond property for -1-> **)
```
```   146
```
```   147 lemma KIII_contract1: "K##I##(I##I) -1-> I"
```
```   148 by (rule contract.K)
```
```   149
```
```   150 lemma KIII_contract2: "K##I##(I##I) -1-> K##I##((K##I)##(K##I))"
```
```   151 by (unfold I_def, blast)
```
```   152
```
```   153 lemma KIII_contract3: "K##I##((K##I)##(K##I)) -1-> I"
```
```   154 by blast
```
```   155
```
```   156 lemma not_diamond_contract: "~ diamond(contract)"
```
```   157 apply (unfold diamond_def)
```
```   158 apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3)
```
```   159 done
```
```   160
```
```   161
```
```   162 subsection {* Results about Parallel Contraction *}
```
```   163
```
```   164 text {* Derive a case for each combinator constructor. *}
```
```   165
```
```   166 inductive_cases
```
```   167       K_parcontractE [elim!]: "K =1=> r"
```
```   168   and S_parcontractE [elim!]: "S =1=> r"
```
```   169   and Ap_parcontractE [elim!]: "p##q =1=> r"
```
```   170
```
```   171 declare parcontract.intros [intro]
```
```   172
```
```   173 (*** Basic properties of parallel contraction ***)
```
```   174
```
```   175 subsection {* Basic properties of parallel contraction *}
```
```   176
```
```   177 lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')"
```
```   178 by blast
```
```   179
```
```   180 lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')"
```
```   181 by blast
```
```   182
```
```   183 lemma S2_parcontractD [dest!]:
```
```   184      "S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')"
```
```   185 by blast
```
```   186
```
```   187 text{*The rules above are not essential but make proofs much faster*}
```
```   188
```
```   189 text{*Church-Rosser property for parallel contraction*}
```
```   190 lemma diamond_parcontract: "diamond parcontract"
```
```   191 apply (unfold diamond_def)
```
```   192 apply (rule impI [THEN allI, THEN allI])
```
```   193 apply (erule parcontract.induct, fast+)
```
```   194 done
```
```   195
```
```   196 text {*
```
```   197   \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
```
```   198 *}
```
```   199
```
```   200 lemma contract_subset_parcontract: "contract <= parcontract"
```
```   201 apply (rule subsetI)
```
```   202 apply (simp only: split_tupled_all)
```
```   203 apply (erule contract.induct, blast+)
```
```   204 done
```
```   205
```
```   206 text{*Reductions: simply throw together reflexivity, transitivity and
```
```   207   the one-step reductions*}
```
```   208
```
```   209 declare r_into_rtrancl [intro]  rtrancl_trans [intro]
```
```   210
```
```   211 (*Example only: not used*)
```
```   212 lemma reduce_I: "I##x ---> x"
```
```   213 by (unfold I_def, blast)
```
```   214
```
```   215 lemma parcontract_subset_reduce: "parcontract <= contract^*"
```
```   216 apply (rule subsetI)
```
```   217 apply (simp only: split_tupled_all)
```
```   218 apply (erule parcontract.induct, blast+)
```
```   219 done
```
```   220
```
```   221 lemma reduce_eq_parreduce: "contract^* = parcontract^*"
```
```   222 by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono]
```
```   223          parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+
```
```   224
```
```   225 lemma diamond_reduce: "diamond(contract^*)"
```
```   226 by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract)
```
```   227
```
```   228 end
```