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