1(* Title: CCL/Trancl.thy 2 Author: Martin Coen, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Transitive closure of a relation\<close> 7 8theory Trancl 9imports CCL 10begin 11 12definition trans :: "i set \<Rightarrow> o" (*transitivity predicate*) 13 where "trans(r) == (ALL x y z. <x,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <x,z>:r)" 14 15definition id :: "i set" (*the identity relation*) 16 where "id == {p. EX x. p = <x,x>}" 17 18definition relcomp :: "[i set,i set] \<Rightarrow> i set" (infixr "O" 60) (*composition of relations*) 19 where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}" 20 21definition rtrancl :: "i set \<Rightarrow> i set" ("(_^*)" [100] 100) 22 where "r^* == lfp(\<lambda>s. id Un (r O s))" 23 24definition trancl :: "i set \<Rightarrow> i set" ("(_^+)" [100] 100) 25 where "r^+ == r O rtrancl(r)" 26 27 28subsection \<open>Natural deduction for \<open>trans(r)\<close>\<close> 29 30lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)" 31 unfolding trans_def by blast 32 33lemma transD: "\<lbrakk>trans(r); <a,b>:r; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c>:r" 34 unfolding trans_def by blast 35 36 37subsection \<open>Identity relation\<close> 38 39lemma idI: "<a,a> : id" 40 apply (unfold id_def) 41 apply (rule CollectI) 42 apply (rule exI) 43 apply (rule refl) 44 done 45 46lemma idE: "\<lbrakk>p: id; \<And>x. p = <x,x> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 47 apply (unfold id_def) 48 apply (erule CollectE) 49 apply blast 50 done 51 52 53subsection \<open>Composition of two relations\<close> 54 55lemma compI: "\<lbrakk><a,b>:s; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c> : r O s" 56 unfolding relcomp_def by blast 57 58(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) 59lemma compE: "\<lbrakk>xz : r O s; \<And>x y z. \<lbrakk>xz = <x,z>; <x,y>:s; <y,z>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 60 unfolding relcomp_def by blast 61 62lemma compEpair: "\<lbrakk><a,c> : r O s; \<And>y. \<lbrakk><a,y>:s; <y,c>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 63 apply (erule compE) 64 apply (simp add: pair_inject) 65 done 66 67lemmas [intro] = compI idI 68 and [elim] = compE idE 69 and [elim!] = pair_inject 70 71lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') <= (r O s)" 72 by blast 73 74 75subsection \<open>The relation rtrancl\<close> 76 77lemma rtrancl_fun_mono: "mono(\<lambda>s. id Un (r O s))" 78 apply (rule monoI) 79 apply (rule monoI subset_refl comp_mono Un_mono)+ 80 apply assumption 81 done 82 83lemma rtrancl_unfold: "r^* = id Un (r O r^*)" 84 by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]]) 85 86(*Reflexivity of rtrancl*) 87lemma rtrancl_refl: "<a,a> : r^*" 88 apply (subst rtrancl_unfold) 89 apply blast 90 done 91 92(*Closure under composition with r*) 93lemma rtrancl_into_rtrancl: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^*" 94 apply (subst rtrancl_unfold) 95 apply blast 96 done 97 98(*rtrancl of r contains r*) 99lemma r_into_rtrancl: "<a,b> : r \<Longrightarrow> <a,b> : r^*" 100 apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl]) 101 apply assumption 102 done 103 104 105subsection \<open>standard induction rule\<close> 106 107lemma rtrancl_full_induct: 108 "\<lbrakk><a,b> : r^*; 109 \<And>x. P(<x,x>); 110 \<And>x y z. \<lbrakk>P(<x,y>); <x,y>: r^*; <y,z>: r\<rbrakk> \<Longrightarrow> P(<x,z>)\<rbrakk> 111 \<Longrightarrow> P(<a,b>)" 112 apply (erule def_induct [OF rtrancl_def]) 113 apply (rule rtrancl_fun_mono) 114 apply blast 115 done 116 117(*nice induction rule*) 118lemma rtrancl_induct: 119 "\<lbrakk><a,b> : r^*; 120 P(a); 121 \<And>y z. \<lbrakk><a,y> : r^*; <y,z> : r; P(y)\<rbrakk> \<Longrightarrow> P(z) \<rbrakk> 122 \<Longrightarrow> P(b)" 123(*by induction on this formula*) 124 apply (subgoal_tac "ALL y. <a,b> = <a,y> \<longrightarrow> P(y)") 125(*now solve first subgoal: this formula is sufficient*) 126 apply blast 127(*now do the induction*) 128 apply (erule rtrancl_full_induct) 129 apply blast 130 apply blast 131 done 132 133(*transitivity of transitive closure!! -- by induction.*) 134lemma trans_rtrancl: "trans(r^*)" 135 apply (rule transI) 136 apply (rule_tac b = z in rtrancl_induct) 137 apply (fast elim: rtrancl_into_rtrancl)+ 138 done 139 140(*elimination of rtrancl -- by induction on a special formula*) 141lemma rtranclE: 142 "\<lbrakk><a,b> : r^*; a = b \<Longrightarrow> P; \<And>y. \<lbrakk><a,y> : r^*; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 143 apply (subgoal_tac "a = b | (EX y. <a,y> : r^* \<and> <y,b> : r)") 144 prefer 2 145 apply (erule rtrancl_induct) 146 apply blast 147 apply blast 148 apply blast 149 done 150 151 152subsection \<open>The relation trancl\<close> 153 154subsubsection \<open>Conversions between trancl and rtrancl\<close> 155 156lemma trancl_into_rtrancl: "<a,b> : r^+ \<Longrightarrow> <a,b> : r^*" 157 apply (unfold trancl_def) 158 apply (erule compEpair) 159 apply (erule rtrancl_into_rtrancl) 160 apply assumption 161 done 162 163(*r^+ contains r*) 164lemma r_into_trancl: "<a,b> : r \<Longrightarrow> <a,b> : r^+" 165 unfolding trancl_def by (blast intro: rtrancl_refl) 166 167(*intro rule by definition: from rtrancl and r*) 168lemma rtrancl_into_trancl1: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^+" 169 unfolding trancl_def by blast 170 171(*intro rule from r and rtrancl*) 172lemma rtrancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^*\<rbrakk> \<Longrightarrow> <a,c> : r^+" 173 apply (erule rtranclE) 174 apply (erule subst) 175 apply (erule r_into_trancl) 176 apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1]) 177 apply (assumption | rule r_into_rtrancl)+ 178 done 179 180(*elimination of r^+ -- NOT an induction rule*) 181lemma tranclE: 182 "\<lbrakk><a,b> : r^+; 183 <a,b> : r \<Longrightarrow> P; 184 \<And>y. \<lbrakk><a,y> : r^+; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 185 apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ \<and> <y,b> : r)") 186 apply blast 187 apply (unfold trancl_def) 188 apply (erule compEpair) 189 apply (erule rtranclE) 190 apply blast 191 apply (blast intro!: rtrancl_into_trancl1) 192 done 193 194(*Transitivity of r^+. 195 Proved by unfolding since it uses transitivity of rtrancl. *) 196lemma trans_trancl: "trans(r^+)" 197 apply (unfold trancl_def) 198 apply (rule transI) 199 apply (erule compEpair)+ 200 apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]]) 201 apply assumption+ 202 done 203 204lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+" 205 apply (rule r_into_trancl [THEN trans_trancl [THEN transD]]) 206 apply assumption+ 207 done 208 209end 210