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 


12 
consts

17456

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


14 
id :: "i set"


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


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

24825

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

0

18 

17456

19 
axioms


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

24825

21 
relcomp_def: (*composition of relations*)

17456

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


23 
id_def: (*the identity relation*)


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


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


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


27 

20140

28 


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


30 


31 
lemma transI:


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


33 
unfolding trans_def by blast


34 


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


36 
unfolding trans_def by blast


37 


38 


39 
subsection {* Identity relation *}


40 


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


42 
apply (unfold id_def)


43 
apply (rule CollectI)


44 
apply (rule exI)


45 
apply (rule refl)


46 
done


47 


48 
lemma idE:


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


50 
apply (unfold id_def)


51 
apply (erule CollectE)


52 
apply blast


53 
done


54 


55 


56 
subsection {* Composition of two relations *}


57 


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

24825

59 
unfolding relcomp_def by blast

20140

60 


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


62 
lemma compE:


63 
"[ xz : r O s;


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


65 
] ==> P"

24825

66 
unfolding relcomp_def by blast

20140

67 


68 
lemma compEpair:


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


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


71 
] ==> P"


72 
apply (erule compE)


73 
apply (simp add: pair_inject)


74 
done


75 


76 
lemmas [intro] = compI idI


77 
and [elim] = compE idE


78 
and [elim!] = pair_inject


79 


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


81 
by blast


82 


83 


84 
subsection {* The relation rtrancl *}


85 


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


87 
apply (rule monoI)


88 
apply (rule monoI subset_refl comp_mono Un_mono)+


89 
apply assumption


90 
done


91 


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


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


94 


95 
(*Reflexivity of rtrancl*)


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


97 
apply (subst rtrancl_unfold)


98 
apply blast


99 
done


100 


101 
(*Closure under composition with r*)


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


103 
apply (subst rtrancl_unfold)


104 
apply blast


105 
done


106 


107 
(*rtrancl of r contains r*)


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


109 
apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])


110 
apply assumption


111 
done


112 


113 


114 
subsection {* standard induction rule *}


115 


116 
lemma rtrancl_full_induct:


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


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


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


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


121 
apply (erule def_induct [OF rtrancl_def])


122 
apply (rule rtrancl_fun_mono)


123 
apply blast


124 
done


125 


126 
(*nice induction rule*)


127 
lemma rtrancl_induct:


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


129 
P(a);


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


131 
==> P(b)"


132 
(*by induction on this formula*)


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


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


135 
apply blast


136 
(*now do the induction*)


137 
apply (erule rtrancl_full_induct)


138 
apply blast


139 
apply blast


140 
done


141 


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


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


144 
apply (rule transI)


145 
apply (rule_tac b = z in rtrancl_induct)


146 
apply (fast elim: rtrancl_into_rtrancl)+


147 
done


148 


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


150 
lemma rtranclE:


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


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


153 
==> P"


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


155 
prefer 2


156 
apply (erule rtrancl_induct)


157 
apply blast


158 
apply blast


159 
apply blast


160 
done


161 


162 


163 
subsection {* The relation trancl *}


164 


165 
subsubsection {* Conversions between trancl and rtrancl *}


166 


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


168 
apply (unfold trancl_def)


169 
apply (erule compEpair)


170 
apply (erule rtrancl_into_rtrancl)


171 
apply assumption


172 
done


173 


174 
(*r^+ contains r*)


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


176 
unfolding trancl_def by (blast intro: rtrancl_refl)


177 


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


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


180 
unfolding trancl_def by blast


181 


182 
(*intro rule from r and rtrancl*)


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


184 
apply (erule rtranclE)


185 
apply (erule subst)


186 
apply (erule r_into_trancl)


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


188 
apply (assumption  rule r_into_rtrancl)+


189 
done


190 


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


192 
lemma tranclE:


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


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


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


196 
] ==> P"


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


198 
apply blast


199 
apply (unfold trancl_def)


200 
apply (erule compEpair)


201 
apply (erule rtranclE)


202 
apply blast


203 
apply (blast intro!: rtrancl_into_trancl1)


204 
done


205 


206 
(*Transitivity of r^+.


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


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


209 
apply (unfold trancl_def)


210 
apply (rule transI)


211 
apply (erule compEpair)+


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


213 
apply assumption+


214 
done


215 


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


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


218 
apply assumption+


219 
done

0

220 


221 
end
