rtranclp_induct, tranclp_induct: added case_names;
authorwenzelm
Thu Feb 28 15:54:37 2008 +0100 (2008-02-28)
changeset 26179bc5d582d6cfe
parent 26178 3396ba6d0823
child 26180 cc85eaab20f6
rtranclp_induct, tranclp_induct: added case_names;
tuned proofs;
src/HOL/Transitive_Closure.thy
     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.123    apply (simp add: split_tupled_all)
   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