17456

1 
(* Title: CCL/Trancl.thy

1474

2 
Author: Martin Coen, Cambridge University Computer Laboratory

0

3 
Copyright 1993 University of Cambridge


4 
*)


5 

17456

6 
header {* Transitive closure of a relation *}


7 


8 
theory Trancl


9 
imports CCL


10 
begin

0

11 

42156

12 
definition trans :: "i set => o" (*transitivity predicate*)


13 
where "trans(r) == (ALL x y z. <x,y>:r > <y,z>:r > <x,z>:r)"


14 


15 
definition id :: "i set" (*the identity relation*)


16 
where "id == {p. EX x. p = <x,x>}"

0

17 

42156

18 
definition relcomp :: "[i set,i set] => i set" (infixr "O" 60) (*composition of relations*)


19 
where "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"


20 


21 
definition rtrancl :: "i set => i set" ("(_^*)" [100] 100)


22 
where "r^* == lfp(%s. id Un (r O s))"


23 


24 
definition trancl :: "i set => i set" ("(_^+)" [100] 100)


25 
where "r^+ == r O rtrancl(r)"

17456

26 

20140

27 


28 
subsection {* Natural deduction for @{text "trans(r)"} *}


29 


30 
lemma transI:


31 
"(!! x y z. [ <x,y>:r; <y,z>:r ] ==> <x,z>:r) ==> trans(r)"


32 
unfolding trans_def by blast


33 


34 
lemma transD: "[ trans(r); <a,b>:r; <b,c>:r ] ==> <a,c>:r"


35 
unfolding trans_def by blast


36 


37 


38 
subsection {* Identity relation *}


39 


40 
lemma idI: "<a,a> : id"


41 
apply (unfold id_def)


42 
apply (rule CollectI)


43 
apply (rule exI)


44 
apply (rule refl)


45 
done


46 


47 
lemma idE:


48 
"[ p: id; !!x.[ p = <x,x> ] ==> P ] ==> P"


49 
apply (unfold id_def)


50 
apply (erule CollectE)


51 
apply blast


52 
done


53 


54 


55 
subsection {* Composition of two relations *}


56 


57 
lemma compI: "[ <a,b>:s; <b,c>:r ] ==> <a,c> : r O s"

24825

58 
unfolding relcomp_def by blast

20140

59 


60 
(*proof requires higherlevel assumptions or a delaying of hyp_subst_tac*)


61 
lemma compE:


62 
"[ xz : r O s;


63 
!!x y z. [ xz = <x,z>; <x,y>:s; <y,z>:r ] ==> P


64 
] ==> P"

24825

65 
unfolding relcomp_def by blast

20140

66 


67 
lemma compEpair:


68 
"[ <a,c> : r O s;


69 
!!y. [ <a,y>:s; <y,c>:r ] ==> P


70 
] ==> P"


71 
apply (erule compE)


72 
apply (simp add: pair_inject)


73 
done


74 


75 
lemmas [intro] = compI idI


76 
and [elim] = compE idE


77 
and [elim!] = pair_inject


78 


79 
lemma comp_mono: "[ r'<=r; s'<=s ] ==> (r' O s') <= (r O s)"


80 
by blast


81 


82 


83 
subsection {* The relation rtrancl *}


84 


85 
lemma rtrancl_fun_mono: "mono(%s. id Un (r O s))"


86 
apply (rule monoI)


87 
apply (rule monoI subset_refl comp_mono Un_mono)+


88 
apply assumption


89 
done


90 


91 
lemma rtrancl_unfold: "r^* = id Un (r O r^*)"


92 
by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]])


93 


94 
(*Reflexivity of rtrancl*)


95 
lemma rtrancl_refl: "<a,a> : r^*"


96 
apply (subst rtrancl_unfold)


97 
apply blast


98 
done


99 


100 
(*Closure under composition with r*)


101 
lemma rtrancl_into_rtrancl: "[ <a,b> : r^*; <b,c> : r ] ==> <a,c> : r^*"


102 
apply (subst rtrancl_unfold)


103 
apply blast


104 
done


105 


106 
(*rtrancl of r contains r*)


107 
lemma r_into_rtrancl: "[ <a,b> : r ] ==> <a,b> : r^*"


108 
apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])


109 
apply assumption


110 
done


111 


112 


113 
subsection {* standard induction rule *}


114 


115 
lemma rtrancl_full_induct:


116 
"[ <a,b> : r^*;


117 
!!x. P(<x,x>);


118 
!!x y z.[ P(<x,y>); <x,y>: r^*; <y,z>: r ] ==> P(<x,z>) ]


119 
==> P(<a,b>)"


120 
apply (erule def_induct [OF rtrancl_def])


121 
apply (rule rtrancl_fun_mono)


122 
apply blast


123 
done


124 


125 
(*nice induction rule*)


126 
lemma rtrancl_induct:


127 
"[ <a,b> : r^*;


128 
P(a);


129 
!!y z.[ <a,y> : r^*; <y,z> : r; P(y) ] ==> P(z) ]


130 
==> P(b)"


131 
(*by induction on this formula*)


132 
apply (subgoal_tac "ALL y. <a,b> = <a,y> > P(y)")


133 
(*now solve first subgoal: this formula is sufficient*)


134 
apply blast


135 
(*now do the induction*)


136 
apply (erule rtrancl_full_induct)


137 
apply blast


138 
apply blast


139 
done


140 


141 
(*transitivity of transitive closure!!  by induction.*)


142 
lemma trans_rtrancl: "trans(r^*)"


143 
apply (rule transI)


144 
apply (rule_tac b = z in rtrancl_induct)


145 
apply (fast elim: rtrancl_into_rtrancl)+


146 
done


147 


148 
(*elimination of rtrancl  by induction on a special formula*)


149 
lemma rtranclE:


150 
"[ <a,b> : r^*; (a = b) ==> P;


151 
!!y.[ <a,y> : r^*; <y,b> : r ] ==> P ]


152 
==> P"


153 
apply (subgoal_tac "a = b  (EX y. <a,y> : r^* & <y,b> : r)")


154 
prefer 2


155 
apply (erule rtrancl_induct)


156 
apply blast


157 
apply blast


158 
apply blast


159 
done


160 


161 


162 
subsection {* The relation trancl *}


163 


164 
subsubsection {* Conversions between trancl and rtrancl *}


165 


166 
lemma trancl_into_rtrancl: "[ <a,b> : r^+ ] ==> <a,b> : r^*"


167 
apply (unfold trancl_def)


168 
apply (erule compEpair)


169 
apply (erule rtrancl_into_rtrancl)


170 
apply assumption


171 
done


172 


173 
(*r^+ contains r*)


174 
lemma r_into_trancl: "[ <a,b> : r ] ==> <a,b> : r^+"


175 
unfolding trancl_def by (blast intro: rtrancl_refl)


176 


177 
(*intro rule by definition: from rtrancl and r*)


178 
lemma rtrancl_into_trancl1: "[ <a,b> : r^*; <b,c> : r ] ==> <a,c> : r^+"


179 
unfolding trancl_def by blast


180 


181 
(*intro rule from r and rtrancl*)


182 
lemma rtrancl_into_trancl2: "[ <a,b> : r; <b,c> : r^* ] ==> <a,c> : r^+"


183 
apply (erule rtranclE)


184 
apply (erule subst)


185 
apply (erule r_into_trancl)


186 
apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1])


187 
apply (assumption  rule r_into_rtrancl)+


188 
done


189 


190 
(*elimination of r^+  NOT an induction rule*)


191 
lemma tranclE:


192 
"[ <a,b> : r^+;


193 
<a,b> : r ==> P;


194 
!!y.[ <a,y> : r^+; <y,b> : r ] ==> P


195 
] ==> P"


196 
apply (subgoal_tac "<a,b> : r  (EX y. <a,y> : r^+ & <y,b> : r)")


197 
apply blast


198 
apply (unfold trancl_def)


199 
apply (erule compEpair)


200 
apply (erule rtranclE)


201 
apply blast


202 
apply (blast intro!: rtrancl_into_trancl1)


203 
done


204 


205 
(*Transitivity of r^+.


206 
Proved by unfolding since it uses transitivity of rtrancl. *)


207 
lemma trans_trancl: "trans(r^+)"


208 
apply (unfold trancl_def)


209 
apply (rule transI)


210 
apply (erule compEpair)+


211 
apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]])


212 
apply assumption+


213 
done


214 


215 
lemma trancl_into_trancl2: "[ <a,b> : r; <b,c> : r^+ ] ==> <a,c> : r^+"


216 
apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])


217 
apply assumption+


218 
done

0

219 


220 
end
