src/HOL/Transitive_Closure.thy
 changeset 26179 bc5d582d6cfe parent 26174 9efd4c04eaa4 child 26271 e324f8918c98
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 28 14:04:29 2008 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 28 15:54:37 2008 +0100
1.3 @@ -87,14 +87,14 @@
1.4
1.5  lemmas rtrancl_mono = rtranclp_mono [to_set]
1.6
1.7 -theorem rtranclp_induct [consumes 1, induct set: rtranclp]:
1.8 +theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:
1.9    assumes a: "r^** a b"
1.10      and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"
1.11    shows "P b"
1.12  proof -
1.13    from a have "a = a --> P b"
1.14      by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
1.15 -  thus ?thesis by iprover
1.16 +  then show ?thesis by iprover
1.17  qed
1.18
1.19  lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]
1.20 @@ -110,13 +110,21 @@
1.21  lemma reflexive_rtrancl: "reflexive (r^*)"
1.22    by (unfold refl_def) fast
1.23
1.24 -lemma trans_rtrancl: "trans(r^*)"
1.25 -  -- {* transitivity of transitive closure!! -- by induction *}
1.26 +text {* Transitivity of transitive closure. *}
1.27 +lemma trans_rtrancl: "trans (r^*)"
1.28  proof (rule transI)
1.29    fix x y z
1.30    assume "(x, y) \<in> r\<^sup>*"
1.31    assume "(y, z) \<in> r\<^sup>*"
1.32 -  thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
1.33 +  then show "(x, z) \<in> r\<^sup>*"
1.34 +  proof induct
1.35 +    case base
1.36 +    show "(x, y) \<in> r\<^sup>*" by fact
1.37 +  next
1.38 +    case (step u v)
1.39 +    from `(x, u) \<in> r\<^sup>*` and `(u, v) \<in> r`
1.40 +    show "(x, v) \<in> r\<^sup>*" ..
1.41 +  qed
1.42  qed
1.43
1.44  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
1.45 @@ -172,11 +180,14 @@
1.46    done
1.47
1.48  lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
1.49 -by (drule rtrancl_mono, simp)
1.50 +  apply (drule rtrancl_mono)
1.51 +  apply simp
1.52 +  done
1.53
1.54  lemma rtranclp_subset: "R \<le> S ==> S \<le> R^** ==> S^** = R^**"
1.55    apply (drule rtranclp_mono)
1.56 -  apply (drule rtranclp_mono, simp)
1.57 +  apply (drule rtranclp_mono)
1.58 +  apply simp
1.59    done
1.60
1.61  lemmas rtrancl_subset = rtranclp_subset [to_set]
1.62 @@ -195,14 +206,15 @@
1.63    apply (rule sym)
1.64    apply (rule rtrancl_subset, blast, clarify)
1.65    apply (rename_tac a b)
1.66 -  apply (case_tac "a = b", blast)
1.67 +  apply (case_tac "a = b")
1.68 +   apply blast
1.69    apply (blast intro!: r_into_rtrancl)
1.70    done
1.71
1.72  lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"
1.73    apply (rule sym)
1.74    apply (rule rtranclp_subset)
1.75 -  apply blast+
1.76 +   apply blast+
1.77    done
1.78
1.79  theorem rtranclp_converseD:
1.80 @@ -216,12 +228,10 @@
1.81  lemmas rtrancl_converseD = rtranclp_converseD [to_set]
1.82
1.83  theorem rtranclp_converseI:
1.84 -  assumes r: "r^** y x"
1.85 +  assumes "r^** y x"
1.86    shows "(r^--1)^** x y"
1.87 -proof -
1.88 -  from r show ?thesis
1.89 -    by induct (iprover intro: rtranclp_trans conversepI)+
1.90 -qed
1.91 +  using assms
1.92 +  by induct (iprover intro: rtranclp_trans conversepI)+
1.93
1.94  lemmas rtrancl_converseI = rtranclp_converseI [to_set]
1.95
1.96 @@ -235,20 +245,17 @@
1.97    assumes major: "r^** a b"
1.98      and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"
1.99    shows "P a"
1.100 -proof -
1.101 -  from rtranclp_converseI [OF major]
1.102 -  show ?thesis
1.103 -    by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+
1.104 -qed
1.105 +  using rtranclp_converseI [OF major]
1.106 +  by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+
1.107
1.108  lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]
1.109
1.110  lemmas converse_rtranclp_induct2 =
1.111 -  converse_rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
1.112 +  converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,
1.113                   consumes 1, case_names refl step]
1.114
1.115  lemmas converse_rtrancl_induct2 =
1.116 -  converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
1.117 +  converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
1.118                   consumes 1, case_names refl step]
1.119
1.120  lemma converse_rtranclpE:
1.121 @@ -282,7 +289,7 @@
1.122  lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
1.124    apply (erule trancl.induct)
1.125 -  apply (iprover dest: subsetD)+
1.126 +   apply (iprover dest: subsetD)+
1.127    done
1.128
1.129  lemma r_into_trancl': "!!p. p : r ==> p : r^+"
1.130 @@ -305,34 +312,35 @@
1.131
1.132  lemma rtranclp_into_tranclp2: "[| r a b; r^** b c |] ==> r^++ a c"
1.133    -- {* intro rule from @{text r} and @{text rtrancl} *}
1.134 -  apply (erule rtranclp.cases, iprover)
1.135 +  apply (erule rtranclp.cases)
1.136 +   apply iprover
1.137    apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])
1.138 -   apply (simp | rule r_into_rtranclp)+
1.139 +    apply (simp | rule r_into_rtranclp)+
1.140    done
1.141
1.142  lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]
1.143
1.144 -lemma tranclp_induct [consumes 1, induct set: tranclp]:
1.145 -  assumes a: "r^++ a b"
1.146 +text {* Nice induction rule for @{text trancl} *}
1.147 +lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
1.148 +  assumes "r^++ a b"
1.149    and cases: "!!y. r a y ==> P y"
1.150      "!!y z. r^++ a y ==> r y z ==> P y ==> P z"
1.151    shows "P b"
1.152 -  -- {* Nice induction rule for @{text trancl} *}
1.153  proof -
1.154 -  from a have "a = a --> P b"
1.155 +  from `r^++ a b` have "a = a --> P b"
1.156      by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
1.157 -  thus ?thesis by iprover
1.158 +  then show ?thesis by iprover
1.159  qed
1.160
1.161  lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
1.162
1.163  lemmas tranclp_induct2 =
1.164 -  tranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
1.165 -                 consumes 1, case_names base step]
1.166 +  tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,
1.167 +    consumes 1, case_names base step]
1.168
1.169  lemmas trancl_induct2 =
1.170 -  trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
1.171 -                 consumes 1, case_names base step]
1.172 +  trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
1.173 +    consumes 1, case_names base step]
1.174
1.175  lemma tranclp_trans_induct:
1.176    assumes major: "r^++ x y"
1.177 @@ -353,20 +361,31 @@
1.178
1.179  lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
1.180    apply (rule subsetI)
1.181 -  apply (rule_tac p="x" in PairE, clarify)
1.182 -  apply (erule trancl_induct, auto)
1.183 +  apply (rule_tac p = x in PairE)
1.184 +  apply clarify
1.185 +  apply (erule trancl_induct)
1.186 +   apply auto
1.187    done
1.188
1.189  lemma trancl_unfold: "r^+ = r Un r O r^+"
1.190    by (auto intro: trancl_into_trancl elim: tranclE)
1.191
1.192 -lemma trans_trancl[simp]: "trans(r^+)"
1.193 -  -- {* Transitivity of @{term "r^+"} *}
1.194 +text {* Transitivity of @{term "r^+"} *}
1.195 +lemma trans_trancl [simp]: "trans (r^+)"
1.196  proof (rule transI)
1.197    fix x y z
1.198 -  assume xy: "(x, y) \<in> r^+"
1.199 +  assume "(x, y) \<in> r^+"
1.200    assume "(y, z) \<in> r^+"
1.201 -  thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+
1.202 +  then show "(x, z) \<in> r^+"
1.203 +  proof induct
1.204 +    case (base u)
1.205 +    from `(x, y) \<in> r^+` and `(y, u) \<in> r`
1.206 +    show "(x, u) \<in> r^+" ..
1.207 +  next
1.208 +    case (step u v)
1.209 +    from `(x, u) \<in> r^+` and `(u, v) \<in> r`
1.210 +    show "(x, v) \<in> r^+" ..
1.211 +  qed
1.212  qed
1.213
1.214  lemmas trancl_trans = trans_trancl [THEN transD, standard]
1.215 @@ -377,16 +396,17 @@
1.216    shows "r^++ x z" using yz xy
1.217    by induct iprover+
1.218
1.219 -lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r"
1.220 -apply(auto)
1.221 -apply(erule trancl_induct)
1.222 -apply assumption
1.223 -apply(unfold trans_def)
1.224 -apply(blast)
1.225 -done
1.226 +lemma trancl_id [simp]: "trans r \<Longrightarrow> r^+ = r"
1.227 +  apply auto
1.228 +  apply (erule trancl_induct)
1.229 +   apply assumption
1.230 +  apply (unfold trans_def)
1.231 +  apply blast
1.232 +  done
1.233
1.234 -lemma rtranclp_tranclp_tranclp: assumes r: "r^** x y"
1.235 -  shows "!!z. r^++ y z ==> r^++ x z" using r
1.236 +lemma rtranclp_tranclp_tranclp:
1.237 +  assumes "r^** x y"
1.238 +  shows "!!z. r^++ y z ==> r^++ x z" using assms
1.239    by induct (iprover intro: tranclp_trans)+
1.240
1.241  lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set]
1.242 @@ -448,7 +468,8 @@
1.243  lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
1.244
1.245  lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y"
1.246 -  apply (erule converse_tranclp_induct, auto)
1.247 +  apply (erule converse_tranclp_induct)
1.248 +   apply auto
1.249    apply (blast intro: rtranclp_trans)
1.250    done
1.251
1.252 @@ -472,7 +493,7 @@
1.253    apply (rule subsetI)
1.254    apply (simp only: split_tupled_all)
1.255    apply (erule tranclE)
1.256 -  apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
1.257 +   apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
1.258    done
1.259
1.260  lemma reflcl_tranclp [simp]: "(r^++)^== = r^**"
1.261 @@ -530,8 +551,10 @@
1.262  lemma Not_Domain_rtrancl:
1.263      "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
1.264    apply auto
1.265 -  by (erule rev_mp, erule rtrancl_induct, auto)
1.266 -
1.267 +  apply (erule rev_mp)
1.268 +  apply (erule rtrancl_induct)
1.269 +   apply auto
1.270 +  done
1.271
1.272  text {* More about converse @{text rtrancl} and @{text trancl}, should
1.273    be merged with main body. *}
1.274 @@ -539,12 +562,12 @@
1.275  lemma single_valued_confluent:
1.276    "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>
1.277    \<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*"
1.278 -apply(erule rtrancl_induct)
1.279 - apply simp
1.280 -apply(erule disjE)
1.281 - apply(blast elim:converse_rtranclE dest:single_valuedD)
1.282 -apply(blast intro:rtrancl_trans)
1.283 -done
1.284 +  apply (erule rtrancl_induct)
1.285 +  apply simp
1.286 +  apply (erule disjE)
1.287 +   apply (blast elim:converse_rtranclE dest:single_valuedD)
1.288 +  apply(blast intro:rtrancl_trans)
1.289 +  done
1.290
1.291  lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"
1.292    by (fast intro: trancl_trans)
1.293 @@ -559,7 +582,7 @@
1.294  lemma tranclp_rtranclp_tranclp:
1.295      "r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c"
1.296    apply (drule tranclpD)
1.297 -  apply (erule exE, erule conjE)
1.298 +  apply (elim exE conjE)
1.299    apply (drule rtranclp_trans, assumption)
1.300    apply (drule rtranclp_into_tranclp2, assumption, assumption)
1.301    done
```