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