17456

1 
(* Title: CCL/Trancl.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 
*)


6 

17456

7 
header {* Transitive closure of a relation *}


8 


9 
theory Trancl


10 
imports CCL


11 
begin

0

12 


13 
consts

17456

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


15 
id :: "i set"


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


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

24825

18 
relcomp :: "[i set,i set] => i set" (infixr "O" 60)

0

19 

17456

20 
axioms


21 
trans_def: "trans(r) == (ALL x y z. <x,y>:r > <y,z>:r > <x,z>:r)"

24825

22 
relcomp_def: (*composition of relations*)

17456

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


24 
id_def: (*the identity relation*)


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


26 
rtrancl_def: "r^* == lfp(%s. id Un (r O s))"


27 
trancl_def: "r^+ == r O rtrancl(r)"


28 

20140

29 


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


31 


32 
lemma transI:


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


34 
unfolding trans_def by blast


35 


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


37 
unfolding trans_def by blast


38 


39 


40 
subsection {* Identity relation *}


41 


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


43 
apply (unfold id_def)


44 
apply (rule CollectI)


45 
apply (rule exI)


46 
apply (rule refl)


47 
done


48 


49 
lemma idE:


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


51 
apply (unfold id_def)


52 
apply (erule CollectE)


53 
apply blast


54 
done


55 


56 


57 
subsection {* Composition of two relations *}


58 


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

24825

60 
unfolding relcomp_def by blast

20140

61 


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


63 
lemma compE:


64 
"[ xz : r O s;


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


66 
] ==> P"

24825

67 
unfolding relcomp_def by blast

20140

68 


69 
lemma compEpair:


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


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


72 
] ==> P"


73 
apply (erule compE)


74 
apply (simp add: pair_inject)


75 
done


76 


77 
lemmas [intro] = compI idI


78 
and [elim] = compE idE


79 
and [elim!] = pair_inject


80 


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


82 
by blast


83 


84 


85 
subsection {* The relation rtrancl *}


86 


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


88 
apply (rule monoI)


89 
apply (rule monoI subset_refl comp_mono Un_mono)+


90 
apply assumption


91 
done


92 


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


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


95 


96 
(*Reflexivity of rtrancl*)


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


98 
apply (subst rtrancl_unfold)


99 
apply blast


100 
done


101 


102 
(*Closure under composition with r*)


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


104 
apply (subst rtrancl_unfold)


105 
apply blast


106 
done


107 


108 
(*rtrancl of r contains r*)


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


110 
apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])


111 
apply assumption


112 
done


113 


114 


115 
subsection {* standard induction rule *}


116 


117 
lemma rtrancl_full_induct:


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


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


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


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


122 
apply (erule def_induct [OF rtrancl_def])


123 
apply (rule rtrancl_fun_mono)


124 
apply blast


125 
done


126 


127 
(*nice induction rule*)


128 
lemma rtrancl_induct:


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


130 
P(a);


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


132 
==> P(b)"


133 
(*by induction on this formula*)


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


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


136 
apply blast


137 
(*now do the induction*)


138 
apply (erule rtrancl_full_induct)


139 
apply blast


140 
apply blast


141 
done


142 


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


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


145 
apply (rule transI)


146 
apply (rule_tac b = z in rtrancl_induct)


147 
apply (fast elim: rtrancl_into_rtrancl)+


148 
done


149 


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


151 
lemma rtranclE:


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


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


154 
==> P"


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


156 
prefer 2


157 
apply (erule rtrancl_induct)


158 
apply blast


159 
apply blast


160 
apply blast


161 
done


162 


163 


164 
subsection {* The relation trancl *}


165 


166 
subsubsection {* Conversions between trancl and rtrancl *}


167 


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


169 
apply (unfold trancl_def)


170 
apply (erule compEpair)


171 
apply (erule rtrancl_into_rtrancl)


172 
apply assumption


173 
done


174 


175 
(*r^+ contains r*)


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


177 
unfolding trancl_def by (blast intro: rtrancl_refl)


178 


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


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


181 
unfolding trancl_def by blast


182 


183 
(*intro rule from r and rtrancl*)


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


185 
apply (erule rtranclE)


186 
apply (erule subst)


187 
apply (erule r_into_trancl)


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


189 
apply (assumption  rule r_into_rtrancl)+


190 
done


191 


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


193 
lemma tranclE:


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


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


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


197 
] ==> P"


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


199 
apply blast


200 
apply (unfold trancl_def)


201 
apply (erule compEpair)


202 
apply (erule rtranclE)


203 
apply blast


204 
apply (blast intro!: rtrancl_into_trancl1)


205 
done


206 


207 
(*Transitivity of r^+.


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


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


210 
apply (unfold trancl_def)


211 
apply (rule transI)


212 
apply (erule compEpair)+


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


214 
apply assumption+


215 
done


216 


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


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


219 
apply assumption+


220 
done

0

221 


222 
end
