src/CCL/Trancl.thy
changeset 20140 98acc6d0fab6
parent 17456 bcf7544875b2
child 24825 c4f13ab78f9d
     1.1 --- a/src/CCL/Trancl.thy	Mon Jul 17 18:42:38 2006 +0200
     1.2 +++ b/src/CCL/Trancl.thy	Tue Jul 18 02:22:38 2006 +0200
     1.3 @@ -26,6 +26,197 @@
     1.4    rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"
     1.5    trancl_def:      "r^+ == r O rtrancl(r)"
     1.6  
     1.7 -ML {* use_legacy_bindings (the_context ()) *}
     1.8 +
     1.9 +subsection {* Natural deduction for @{text "trans(r)"} *}
    1.10 +
    1.11 +lemma transI:
    1.12 +  "(!! x y z. [| <x,y>:r;  <y,z>:r |] ==> <x,z>:r) ==> trans(r)"
    1.13 +  unfolding trans_def by blast
    1.14 +
    1.15 +lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"
    1.16 +  unfolding trans_def by blast
    1.17 +
    1.18 +
    1.19 +subsection {* Identity relation *}
    1.20 +
    1.21 +lemma idI: "<a,a> : id"
    1.22 +  apply (unfold id_def)
    1.23 +  apply (rule CollectI)
    1.24 +  apply (rule exI)
    1.25 +  apply (rule refl)
    1.26 +  done
    1.27 +
    1.28 +lemma idE:
    1.29 +    "[| p: id;  !!x.[| p = <x,x> |] ==> P |] ==>  P"
    1.30 +  apply (unfold id_def)
    1.31 +  apply (erule CollectE)
    1.32 +  apply blast
    1.33 +  done
    1.34 +
    1.35 +
    1.36 +subsection {* Composition of two relations *}
    1.37 +
    1.38 +lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
    1.39 +  unfolding comp_def by blast
    1.40 +
    1.41 +(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.42 +lemma compE:
    1.43 +    "[| xz : r O s;
    1.44 +        !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P
    1.45 +     |] ==> P"
    1.46 +  unfolding comp_def by blast
    1.47 +
    1.48 +lemma compEpair:
    1.49 +  "[| <a,c> : r O s;
    1.50 +      !!y. [| <a,y>:s;  <y,c>:r |] ==> P
    1.51 +   |] ==> P"
    1.52 +  apply (erule compE)
    1.53 +  apply (simp add: pair_inject)
    1.54 +  done
    1.55 +
    1.56 +lemmas [intro] = compI idI
    1.57 +  and [elim] = compE idE
    1.58 +  and [elim!] = pair_inject
    1.59 +
    1.60 +lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
    1.61 +  by blast
    1.62 +
    1.63 +
    1.64 +subsection {* The relation rtrancl *}
    1.65 +
    1.66 +lemma rtrancl_fun_mono: "mono(%s. id Un (r O s))"
    1.67 +  apply (rule monoI)
    1.68 +  apply (rule monoI subset_refl comp_mono Un_mono)+
    1.69 +  apply assumption
    1.70 +  done
    1.71 +
    1.72 +lemma rtrancl_unfold: "r^* = id Un (r O r^*)"
    1.73 +  by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]])
    1.74 +
    1.75 +(*Reflexivity of rtrancl*)
    1.76 +lemma rtrancl_refl: "<a,a> : r^*"
    1.77 +  apply (subst rtrancl_unfold)
    1.78 +  apply blast
    1.79 +  done
    1.80 +
    1.81 +(*Closure under composition with r*)
    1.82 +lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
    1.83 +  apply (subst rtrancl_unfold)
    1.84 +  apply blast
    1.85 +  done
    1.86 +
    1.87 +(*rtrancl of r contains r*)
    1.88 +lemma r_into_rtrancl: "[| <a,b> : r |] ==> <a,b> : r^*"
    1.89 +  apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
    1.90 +  apply assumption
    1.91 +  done
    1.92 +
    1.93 +
    1.94 +subsection {* standard induction rule *}
    1.95 +
    1.96 +lemma rtrancl_full_induct:
    1.97 +  "[| <a,b> : r^*;
    1.98 +      !!x. P(<x,x>);
    1.99 +      !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]
   1.100 +   ==>  P(<a,b>)"
   1.101 +  apply (erule def_induct [OF rtrancl_def])
   1.102 +   apply (rule rtrancl_fun_mono)
   1.103 +  apply blast
   1.104 +  done
   1.105 +
   1.106 +(*nice induction rule*)
   1.107 +lemma rtrancl_induct:
   1.108 +  "[| <a,b> : r^*;
   1.109 +      P(a);
   1.110 +      !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z) |]
   1.111 +    ==> P(b)"
   1.112 +(*by induction on this formula*)
   1.113 +  apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)")
   1.114 +(*now solve first subgoal: this formula is sufficient*)
   1.115 +  apply blast
   1.116 +(*now do the induction*)
   1.117 +  apply (erule rtrancl_full_induct)
   1.118 +   apply blast
   1.119 +  apply blast
   1.120 +  done
   1.121 +
   1.122 +(*transitivity of transitive closure!! -- by induction.*)
   1.123 +lemma trans_rtrancl: "trans(r^*)"
   1.124 +  apply (rule transI)
   1.125 +  apply (rule_tac b = z in rtrancl_induct)
   1.126 +    apply (fast elim: rtrancl_into_rtrancl)+
   1.127 +  done
   1.128 +
   1.129 +(*elimination of rtrancl -- by induction on a special formula*)
   1.130 +lemma rtranclE:
   1.131 +  "[| <a,b> : r^*;  (a = b) ==> P;
   1.132 +      !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |]
   1.133 +   ==> P"
   1.134 +  apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)")
   1.135 +   prefer 2
   1.136 +   apply (erule rtrancl_induct)
   1.137 +    apply blast
   1.138 +   apply blast
   1.139 +  apply blast
   1.140 +  done
   1.141 +
   1.142 +
   1.143 +subsection {* The relation trancl *}
   1.144 +
   1.145 +subsubsection {* Conversions between trancl and rtrancl *}
   1.146 +
   1.147 +lemma trancl_into_rtrancl: "[| <a,b> : r^+ |] ==> <a,b> : r^*"
   1.148 +  apply (unfold trancl_def)
   1.149 +  apply (erule compEpair)
   1.150 +  apply (erule rtrancl_into_rtrancl)
   1.151 +  apply assumption
   1.152 +  done
   1.153 +
   1.154 +(*r^+ contains r*)
   1.155 +lemma r_into_trancl: "[| <a,b> : r |] ==> <a,b> : r^+"
   1.156 +  unfolding trancl_def by (blast intro: rtrancl_refl)
   1.157 +
   1.158 +(*intro rule by definition: from rtrancl and r*)
   1.159 +lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
   1.160 +  unfolding trancl_def by blast
   1.161 +
   1.162 +(*intro rule from r and rtrancl*)
   1.163 +lemma rtrancl_into_trancl2: "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+"
   1.164 +  apply (erule rtranclE)
   1.165 +   apply (erule subst)
   1.166 +   apply (erule r_into_trancl)
   1.167 +  apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1])
   1.168 +    apply (assumption | rule r_into_rtrancl)+
   1.169 +  done
   1.170 +
   1.171 +(*elimination of r^+ -- NOT an induction rule*)
   1.172 +lemma tranclE:
   1.173 +  "[| <a,b> : r^+;
   1.174 +      <a,b> : r ==> P;
   1.175 +      !!y.[| <a,y> : r^+;  <y,b> : r |] ==> P
   1.176 +   |] ==> P"
   1.177 +  apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)")
   1.178 +   apply blast
   1.179 +  apply (unfold trancl_def)
   1.180 +  apply (erule compEpair)
   1.181 +  apply (erule rtranclE)
   1.182 +   apply blast
   1.183 +  apply (blast intro!: rtrancl_into_trancl1)
   1.184 +  done
   1.185 +
   1.186 +(*Transitivity of r^+.
   1.187 +  Proved by unfolding since it uses transitivity of rtrancl. *)
   1.188 +lemma trans_trancl: "trans(r^+)"
   1.189 +  apply (unfold trancl_def)
   1.190 +  apply (rule transI)
   1.191 +  apply (erule compEpair)+
   1.192 +  apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]])
   1.193 +    apply assumption+
   1.194 +  done
   1.195 +
   1.196 +lemma trancl_into_trancl2: "[| <a,b> : r;  <b,c> : r^+ |]   ==>  <a,c> : r^+"
   1.197 +  apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
   1.198 +   apply assumption+
   1.199 +  done
   1.200  
   1.201  end