1(* Title: ZF/ex/Commutation.thy 2 Author: Tobias Nipkow & Sidi Ould Ehmety 3 Copyright 1995 TU Muenchen 4 5Commutation theory for proving the Church Rosser theorem. 6*) 7 8theory Commutation imports ZF begin 9 10definition 11 square :: "[i, i, i, i] => o" where 12 "square(r,s,t,u) == 13 (\<forall>a b. <a,b> \<in> r \<longrightarrow> (\<forall>c. <a, c> \<in> s \<longrightarrow> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))" 14 15definition 16 commute :: "[i, i] => o" where 17 "commute(r,s) == square(r,s,s,r)" 18 19definition 20 diamond :: "i=>o" where 21 "diamond(r) == commute(r, r)" 22 23definition 24 strip :: "i=>o" where 25 "strip(r) == commute(r^*, r)" 26 27definition 28 Church_Rosser :: "i => o" where 29 "Church_Rosser(r) == (\<forall>x y. <x,y> \<in> (r \<union> converse(r))^* \<longrightarrow> 30 (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))" 31 32definition 33 confluent :: "i=>o" where 34 "confluent(r) == diamond(r^*)" 35 36 37lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)" 38 unfolding square_def by blast 39 40lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)" 41 unfolding square_def by blast 42 43 44lemma square_rtrancl: 45 "square(r,s,s,t) ==> field(s)<=field(t) ==> square(r^*,s,s,t^*)" 46apply (unfold square_def, clarify) 47apply (erule rtrancl_induct) 48apply (blast intro: rtrancl_refl) 49apply (blast intro: rtrancl_into_rtrancl) 50done 51 52(* A special case of square_rtrancl_on *) 53lemma diamond_strip: 54 "diamond(r) ==> strip(r)" 55apply (unfold diamond_def commute_def strip_def) 56apply (rule square_rtrancl, simp_all) 57done 58 59(*** commute ***) 60 61lemma commute_sym: "commute(r,s) ==> commute(s,r)" 62 unfolding commute_def by (blast intro: square_sym) 63 64lemma commute_rtrancl: 65 "commute(r,s) ==> field(r)=field(s) ==> commute(r^*,s^*)" 66apply (unfold commute_def) 67apply (rule square_rtrancl) 68apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) 69apply (simp_all add: rtrancl_field) 70done 71 72 73lemma confluentD: "confluent(r) ==> diamond(r^*)" 74by (simp add: confluent_def) 75 76lemma strip_confluent: "strip(r) ==> confluent(r)" 77apply (unfold strip_def confluent_def diamond_def) 78apply (drule commute_rtrancl) 79apply (simp_all add: rtrancl_field) 80done 81 82lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r \<union> s, t)" 83 unfolding commute_def square_def by blast 84 85lemma diamond_Un: 86 "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r \<union> s)" 87 unfolding diamond_def by (blast intro: commute_Un commute_sym) 88 89lemma diamond_confluent: 90 "diamond(r) ==> confluent(r)" 91apply (unfold diamond_def confluent_def) 92apply (erule commute_rtrancl, simp) 93done 94 95lemma confluent_Un: 96 "[| confluent(r); confluent(s); commute(r^*, s^*); 97 relation(r); relation(s) |] ==> confluent(r \<union> s)" 98apply (unfold confluent_def) 99apply (rule rtrancl_Un_rtrancl [THEN subst], auto) 100apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD]) 101done 102 103 104lemma diamond_to_confluence: 105 "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)" 106apply (drule rtrancl_subset [symmetric], assumption) 107apply (simp_all add: confluent_def) 108apply (blast intro: diamond_confluent [THEN confluentD]) 109done 110 111 112(*** Church_Rosser ***) 113 114lemma Church_Rosser1: 115 "Church_Rosser(r) ==> confluent(r)" 116apply (unfold confluent_def Church_Rosser_def square_def 117 commute_def diamond_def, auto) 118apply (drule converseI) 119apply (simp (no_asm_use) add: rtrancl_converse [symmetric]) 120apply (drule_tac x = b in spec) 121apply (drule_tac x1 = c in spec [THEN mp]) 122apply (rule_tac b = a in rtrancl_trans) 123apply (blast intro: rtrancl_mono [THEN subsetD])+ 124done 125 126 127lemma Church_Rosser2: 128 "confluent(r) ==> Church_Rosser(r)" 129apply (unfold confluent_def Church_Rosser_def square_def 130 commute_def diamond_def, auto) 131apply (frule fieldI1) 132apply (simp add: rtrancl_field) 133apply (erule rtrancl_induct, auto) 134apply (blast intro: rtrancl_refl) 135apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+ 136done 137 138 139lemma Church_Rosser: "Church_Rosser(r) \<longleftrightarrow> confluent(r)" 140 by (blast intro: Church_Rosser1 Church_Rosser2) 141 142end 143