converted theory Transitive_Closure;
authorwenzelm
Wed Jan 09 17:48:40 2002 +0100 (2002-01-09)
changeset 12691d21db58bcdc2
parent 12690 ac3fa7c05e5a
child 12692 df42e9a53a02
converted theory Transitive_Closure;
src/HOL/IsaMakefile
src/HOL/Transitive_Closure.ML
src/HOL/Transitive_Closure.thy
src/HOL/Transitive_Closure_lemmas.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Jan 09 17:42:49 2002 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jan 09 17:48:40 2002 +0100
     1.3 @@ -18,7 +18,6 @@
     1.4    HOL-CTL \
     1.5    HOL-GroupTheory \
     1.6        HOL-Real-HahnBanach \
     1.7 -      HOL-Real-Hyperreal \
     1.8        HOL-Real-ex \
     1.9    HOL-Hoare \
    1.10    HOL-IMP \
    1.11 @@ -101,7 +100,7 @@
    1.12    Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
    1.13    Tools/record_package.ML Tools/split_rule.ML \
    1.14    Tools/svc_funcs.ML Tools/typedef_package.ML \
    1.15 -  Transitive_Closure.thy Transitive_Closure_lemmas.ML Typedef.thy \
    1.16 +  Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.17    Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
    1.18    Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
    1.19    document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Transitive_Closure.ML	Wed Jan 09 17:48:40 2002 +0100
     2.3 @@ -0,0 +1,50 @@
     2.4 +
     2.5 +(* legacy ML bindings *)
     2.6 +
     2.7 +val converse_rtranclE = thm "converse_rtranclE";
     2.8 +val converse_rtranclE2 = thm "converse_rtranclE2";
     2.9 +val converse_rtrancl_induct = thm "converse_rtrancl_induct";
    2.10 +val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";
    2.11 +val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";
    2.12 +val converse_trancl_induct = thm "converse_trancl_induct";
    2.13 +val irrefl_tranclI = thm "irrefl_tranclI";
    2.14 +val irrefl_trancl_rD = thm "irrefl_trancl_rD";
    2.15 +val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";
    2.16 +val r_into_rtrancl = thm "r_into_rtrancl";
    2.17 +val r_into_trancl = thm "r_into_trancl";
    2.18 +val rtranclE = thm "rtranclE";
    2.19 +val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
    2.20 +val rtrancl_converse = thm "rtrancl_converse";
    2.21 +val rtrancl_converseD = thm "rtrancl_converseD";
    2.22 +val rtrancl_converseI = thm "rtrancl_converseI";
    2.23 +val rtrancl_idemp = thm "rtrancl_idemp";
    2.24 +val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";
    2.25 +val rtrancl_induct = thm "rtrancl_induct";
    2.26 +val rtrancl_induct2 = thm "rtrancl_induct2";
    2.27 +val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
    2.28 +val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
    2.29 +val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
    2.30 +val rtrancl_mono = thm "rtrancl_mono";
    2.31 +val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";
    2.32 +val rtrancl_refl = thm "rtrancl_refl";
    2.33 +val rtrancl_reflcl = thm "rtrancl_reflcl";
    2.34 +val rtrancl_subset = thm "rtrancl_subset";
    2.35 +val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";
    2.36 +val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    2.37 +val rtrancl_trans = thm "rtrancl_trans";
    2.38 +val tranclD = thm "tranclD";
    2.39 +val tranclE = thm "tranclE";
    2.40 +val trancl_converse = thm "trancl_converse";
    2.41 +val trancl_converseD = thm "trancl_converseD";
    2.42 +val trancl_converseI = thm "trancl_converseI";
    2.43 +val trancl_def = thm "trancl_def";
    2.44 +val trancl_induct = thm "trancl_induct";
    2.45 +val trancl_insert = thm "trancl_insert";
    2.46 +val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    2.47 +val trancl_into_trancl2 = thm "trancl_into_trancl2";
    2.48 +val trancl_mono = thm "trancl_mono";
    2.49 +val trancl_subset_Sigma = thm "trancl_subset_Sigma";
    2.50 +val trancl_trans = thm "trancl_trans";
    2.51 +val trancl_trans_induct = thm "trancl_trans_induct";
    2.52 +val trans_rtrancl = thm "trans_rtrancl";
    2.53 +val trans_trancl = thm "trans_trancl";
     3.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 09 17:42:49 2002 +0100
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 09 17:48:40 2002 +0100
     3.3 @@ -2,48 +2,394 @@
     3.4      ID:         $Id$
     3.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.6      Copyright   1992  University of Cambridge
     3.7 -
     3.8 -Relfexive and Transitive closure of a relation
     3.9 -
    3.10 -rtrancl is reflexive/transitive closure;
    3.11 -trancl  is transitive closure
    3.12 -reflcl  is reflexive closure
    3.13 -
    3.14 -These postfix operators have MAXIMUM PRIORITY, forcing their operands
    3.15 -to be atomic.
    3.16  *)
    3.17  
    3.18 -theory Transitive_Closure = Inductive
    3.19 -files ("Transitive_Closure_lemmas.ML"):
    3.20 +header {* Reflexive and Transitive closure of a relation *}
    3.21 +
    3.22 +theory Transitive_Closure = Inductive:
    3.23 +
    3.24 +text {*
    3.25 +  @{text rtrancl} is reflexive/transitive closure,
    3.26 +  @{text trancl} is transitive closure,
    3.27 +  @{text reflcl} is reflexive closure.
    3.28 +
    3.29 +  These postfix operators have \emph{maximum priority}, forcing their
    3.30 +  operands to be atomic.
    3.31 +*}
    3.32  
    3.33  consts
    3.34 -  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    3.35 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^*)" [1000] 999)
    3.36  
    3.37  inductive "r^*"
    3.38 -intros
    3.39 -  rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    3.40 -  rtrancl_into_rtrancl:        "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"
    3.41 +  intros
    3.42 +    rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    3.43 +    rtrancl_into_rtrancl: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
    3.44  
    3.45  constdefs
    3.46 -  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    3.47 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    3.48    "r^+ ==  r O rtrancl r"
    3.49  
    3.50  syntax
    3.51 -  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
    3.52 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    3.53  translations
    3.54 -  "r^=" == "r Un Id"
    3.55 +  "r^=" == "r \<union> Id"
    3.56  
    3.57  syntax (xsymbols)
    3.58 -  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    3.59 -  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    3.60 -  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    3.61 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    3.62 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    3.63 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    3.64 +
    3.65 +
    3.66 +subsection {* Reflexive-transitive closure *}
    3.67 +
    3.68 +lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    3.69 +  -- {* @{text rtrancl} of @{text r} contains @{text r} *}
    3.70 +  apply (simp only: split_tupled_all)
    3.71 +  apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
    3.72 +  done
    3.73 +
    3.74 +lemma rtrancl_mono: "r \<subseteq> s ==> r^* \<subseteq> s^*"
    3.75 +  -- {* monotonicity of @{text rtrancl} *}
    3.76 +  apply (rule subsetI)
    3.77 +  apply (simp only: split_tupled_all)
    3.78 +  apply (erule rtrancl.induct)
    3.79 +   apply (rule_tac [2] rtrancl_into_rtrancl)
    3.80 +    apply blast+
    3.81 +  done
    3.82 +
    3.83 +theorem rtrancl_induct [consumes 1]:
    3.84 +  (assumes a: "(a, b) : r^*"
    3.85 +    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
    3.86 +  "P b"
    3.87 +proof -
    3.88 +  from a have "a = a --> P b"
    3.89 +    by (induct "%x y. x = a --> P y" a b rule: rtrancl.induct)
    3.90 +      (rules intro: cases)+
    3.91 +  thus ?thesis by rules
    3.92 +qed
    3.93 +
    3.94 +ML_setup {*
    3.95 +  bind_thm ("rtrancl_induct2", split_rule
    3.96 +    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
    3.97 +*}
    3.98 +
    3.99 +lemma trans_rtrancl: "trans(r^*)"
   3.100 +  -- {* transitivity of transitive closure!! -- by induction *}
   3.101 +  apply (unfold trans_def)
   3.102 +  apply safe
   3.103 +  apply (erule_tac b = z in rtrancl_induct)
   3.104 +   apply (blast intro: rtrancl_into_rtrancl)+
   3.105 +  done
   3.106 +
   3.107 +lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   3.108 +
   3.109 +lemma rtranclE:
   3.110 +  "[| (a::'a,b) : r^*;  (a = b) ==> P;
   3.111 +      !!y.[| (a,y) : r^*; (y,b) : r |] ==> P
   3.112 +   |] ==> P"
   3.113 +  -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
   3.114 +proof -
   3.115 +  assume major: "(a::'a,b) : r^*"
   3.116 +  case rule_context
   3.117 +  show ?thesis
   3.118 +    apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
   3.119 +     apply (rule_tac [2] major [THEN rtrancl_induct])
   3.120 +      prefer 2 apply (blast!)
   3.121 +      prefer 2 apply (blast!)
   3.122 +    apply (erule asm_rl exE disjE conjE prems)+
   3.123 +    done
   3.124 +qed
   3.125 +
   3.126 +lemmas converse_rtrancl_into_rtrancl = r_into_rtrancl [THEN rtrancl_trans, standard]
   3.127 +
   3.128 +text {*
   3.129 +  \medskip More @{term "r^*"} equations and inclusions.
   3.130 +*}
   3.131 +
   3.132 +lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
   3.133 +  apply auto
   3.134 +  apply (erule rtrancl_induct)
   3.135 +   apply (rule rtrancl_refl)
   3.136 +  apply (blast intro: rtrancl_trans)
   3.137 +  done
   3.138 +
   3.139 +lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
   3.140 +  apply (rule set_ext)
   3.141 +  apply (simp only: split_tupled_all)
   3.142 +  apply (blast intro: rtrancl_trans)
   3.143 +  done
   3.144 +
   3.145 +lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
   3.146 +  apply (drule rtrancl_mono)
   3.147 +  apply simp
   3.148 +  done
   3.149 +
   3.150 +lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
   3.151 +  apply (drule rtrancl_mono)
   3.152 +  apply (drule rtrancl_mono)
   3.153 +  apply simp
   3.154 +  apply blast
   3.155 +  done
   3.156 +
   3.157 +lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"
   3.158 +  by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD])
   3.159 +
   3.160 +lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*"
   3.161 +  by (blast intro!: rtrancl_subset intro: r_into_rtrancl)
   3.162 +
   3.163 +lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
   3.164 +  apply (rule sym)
   3.165 +  apply (rule rtrancl_subset)
   3.166 +   apply blast
   3.167 +  apply clarify
   3.168 +  apply (rename_tac a b)
   3.169 +  apply (case_tac "a = b")
   3.170 +   apply blast
   3.171 +  apply (blast intro!: r_into_rtrancl)
   3.172 +  done
   3.173 +
   3.174 +lemma rtrancl_converseD: "(x, y) \<in> (r^-1)^* ==> (y, x) \<in> r^*"
   3.175 +  apply (erule rtrancl_induct)
   3.176 +   apply (rule rtrancl_refl)
   3.177 +  apply (blast intro: rtrancl_trans)
   3.178 +  done
   3.179 +
   3.180 +lemma rtrancl_converseI: "(y, x) \<in> r^* ==> (x, y) \<in> (r^-1)^*"
   3.181 +  apply (erule rtrancl_induct)
   3.182 +   apply (rule rtrancl_refl)
   3.183 +  apply (blast intro: rtrancl_trans)
   3.184 +  done
   3.185 +
   3.186 +lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   3.187 +  by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
   3.188 +
   3.189 +lemma converse_rtrancl_induct:
   3.190 +  "[| (a,b) : r^*; P(b);
   3.191 +      !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]
   3.192 +    ==> P(a)"
   3.193 +proof -
   3.194 +  assume major: "(a,b) : r^*"
   3.195 +  case rule_context
   3.196 +  show ?thesis
   3.197 +    apply (rule major [THEN rtrancl_converseI, THEN rtrancl_induct])
   3.198 +     apply assumption
   3.199 +    apply (blast! dest!: rtrancl_converseD)
   3.200 +  done
   3.201 +qed
   3.202 +
   3.203 +ML_setup {*
   3.204 +  bind_thm ("converse_rtrancl_induct2", split_rule
   3.205 +    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
   3.206 +*}
   3.207 +
   3.208 +lemma converse_rtranclE:
   3.209 +  "[| (x,z):r^*;
   3.210 +      x=z ==> P;
   3.211 +      !!y. [| (x,y):r; (y,z):r^* |] ==> P
   3.212 +   |] ==> P"
   3.213 +proof -
   3.214 +  assume major: "(x,z):r^*"
   3.215 +  case rule_context
   3.216 +  show ?thesis
   3.217 +    apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
   3.218 +     apply (rule_tac [2] major [THEN converse_rtrancl_induct])
   3.219 +      prefer 2 apply (blast!)
   3.220 +     prefer 2 apply (blast!)
   3.221 +    apply (erule asm_rl exE disjE conjE prems)+
   3.222 +    done
   3.223 +qed
   3.224 +
   3.225 +ML_setup {*
   3.226 +  bind_thm ("converse_rtranclE2", split_rule
   3.227 +    (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE")));
   3.228 +*}
   3.229 +
   3.230 +lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"
   3.231 +  by (blast elim: rtranclE converse_rtranclE
   3.232 +    intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
   3.233 +
   3.234 +
   3.235 +subsection {* Transitive closure *}
   3.236  
   3.237 -use "Transitive_Closure_lemmas.ML"
   3.238 +lemma trancl_mono: "p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   3.239 +  apply (unfold trancl_def)
   3.240 +  apply (blast intro: rtrancl_mono [THEN subsetD])
   3.241 +  done
   3.242 +
   3.243 +text {*
   3.244 +  \medskip Conversions between @{text trancl} and @{text rtrancl}.
   3.245 +*}
   3.246 +
   3.247 +lemma trancl_into_rtrancl: "!!p. p \<in> r^+ ==> p \<in> r^*"
   3.248 +  apply (unfold trancl_def)
   3.249 +  apply (simp only: split_tupled_all)
   3.250 +  apply (erule rel_compEpair)
   3.251 +  apply (assumption | rule rtrancl_into_rtrancl)+
   3.252 +  done
   3.253 +
   3.254 +lemma r_into_trancl [intro]: "!!p. p \<in> r ==> p \<in> r^+"
   3.255 +  -- {* @{text "r^+"} contains @{text r} *}
   3.256 +  apply (unfold trancl_def)
   3.257 +  apply (simp only: split_tupled_all)
   3.258 +  apply (assumption | rule rel_compI rtrancl_refl)+
   3.259 +  done
   3.260 +
   3.261 +lemma rtrancl_into_trancl1: "(a, b) \<in> r^* ==> (b, c) \<in> r ==> (a, c) \<in> r^+"
   3.262 +  -- {* intro rule by definition: from @{text rtrancl} and @{text r} *}
   3.263 +  by (auto simp add: trancl_def)
   3.264 +
   3.265 +lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   3.266 +  -- {* intro rule from @{text r} and @{text rtrancl} *}
   3.267 +  apply (erule rtranclE)
   3.268 +   apply (blast intro: r_into_trancl)
   3.269 +  apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
   3.270 +   apply (assumption | rule r_into_rtrancl)+
   3.271 +  done
   3.272 +
   3.273 +lemma trancl_induct:
   3.274 +  "[| (a,b) : r^+;
   3.275 +      !!y.  [| (a,y) : r |] ==> P(y);
   3.276 +      !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)
   3.277 +   |] ==> P(b)"
   3.278 +  -- {* Nice induction rule for @{text trancl} *}
   3.279 +proof -
   3.280 +  assume major: "(a, b) : r^+"
   3.281 +  case rule_context
   3.282 +  show ?thesis
   3.283 +    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
   3.284 +    txt {* by induction on this formula *}
   3.285 +    apply (subgoal_tac "ALL z. (y,z) : r --> P (z)")
   3.286 +     txt {* now solve first subgoal: this formula is sufficient *}
   3.287 +     apply blast
   3.288 +    apply (erule rtrancl_induct)
   3.289 +    apply (blast intro: rtrancl_into_trancl1 prems)+
   3.290 +    done
   3.291 +qed
   3.292 +
   3.293 +lemma trancl_trans_induct:
   3.294 +  "[| (x,y) : r^+;
   3.295 +      !!x y. (x,y) : r ==> P x y;
   3.296 +      !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z
   3.297 +   |] ==> P x y"
   3.298 +  -- {* Another induction rule for trancl, incorporating transitivity *}
   3.299 +proof -
   3.300 +  assume major: "(x,y) : r^+"
   3.301 +  case rule_context
   3.302 +  show ?thesis
   3.303 +    by (blast intro: r_into_trancl major [THEN trancl_induct] prems)
   3.304 +qed
   3.305 +
   3.306 +lemma tranclE:
   3.307 +  "[| (a::'a,b) : r^+;
   3.308 +      (a,b) : r ==> P;
   3.309 +      !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P
   3.310 +   |] ==> P"
   3.311 +  -- {* elimination of @{text "r^+"} -- \emph{not} an induction rule *}
   3.312 +proof -
   3.313 +  assume major: "(a::'a,b) : r^+"
   3.314 +  case rule_context
   3.315 +  show ?thesis
   3.316 +    apply (subgoal_tac "(a::'a, b) : r | (EX y. (a,y) : r^+ & (y,b) : r)")
   3.317 +     apply (erule asm_rl disjE exE conjE prems)+
   3.318 +    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
   3.319 +    apply (erule rtranclE)
   3.320 +     apply blast
   3.321 +    apply (blast intro!: rtrancl_into_trancl1)
   3.322 +    done
   3.323 +qed
   3.324  
   3.325 +lemma trans_trancl: "trans(r^+)"
   3.326 +  -- {* Transitivity of @{term "r^+"} *}
   3.327 +  -- {* Proved by unfolding since it uses transitivity of @{text rtrancl} *}
   3.328 +  apply (unfold trancl_def)
   3.329 +  apply (rule transI)
   3.330 +  apply (erule rel_compEpair)+
   3.331 +  apply (rule rtrancl_into_rtrancl [THEN rtrancl_trans [THEN rel_compI]])
   3.332 +  apply assumption+
   3.333 +  done
   3.334 +
   3.335 +lemmas trancl_trans = trans_trancl [THEN transD, standard]
   3.336 +
   3.337 +lemma rtrancl_trancl_trancl: "(x, y) \<in> r^* ==> (y, z) \<in> r^+ ==> (x, z) \<in> r^+"
   3.338 +  apply (unfold trancl_def)
   3.339 +  apply (blast intro: rtrancl_trans)
   3.340 +  done
   3.341 +
   3.342 +lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   3.343 +  by (erule transD [OF trans_trancl r_into_trancl])
   3.344 +
   3.345 +lemma trancl_insert:
   3.346 +  "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
   3.347 +  -- {* primitive recursion for @{text trancl} over finite relations *}
   3.348 +  apply (rule equalityI)
   3.349 +   apply (rule subsetI)
   3.350 +   apply (simp only: split_tupled_all)
   3.351 +   apply (erule trancl_induct)
   3.352 +    apply blast
   3.353 +   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
   3.354 +  apply (rule subsetI)
   3.355 +  apply (blast intro: trancl_mono rtrancl_mono
   3.356 +    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   3.357 +  done
   3.358 +
   3.359 +lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   3.360 +  apply (unfold trancl_def)
   3.361 +  apply (simp add: rtrancl_converse converse_rel_comp)
   3.362 +  apply (simp add: rtrancl_converse [symmetric] r_comp_rtrancl_eq)
   3.363 +  done
   3.364 +
   3.365 +lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x,y) \<in> (r^-1)^+"
   3.366 +  by (simp add: trancl_converse)
   3.367 +
   3.368 +lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   3.369 +  by (simp add: trancl_converse)
   3.370 +
   3.371 +lemma converse_trancl_induct:
   3.372 +  "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
   3.373 +      !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]
   3.374 +    ==> P(a)"
   3.375 +proof -
   3.376 +  assume major: "(a,b) : r^+"
   3.377 +  case rule_context
   3.378 +  show ?thesis
   3.379 +    apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
   3.380 +     apply (rule prems)
   3.381 +     apply (erule converseD)
   3.382 +    apply (blast intro: prems dest!: trancl_converseD)
   3.383 +    done
   3.384 +qed
   3.385 +
   3.386 +lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
   3.387 +  apply (erule converse_trancl_induct)
   3.388 +   apply auto
   3.389 +  apply (blast intro: rtrancl_trans)
   3.390 +  done
   3.391 +
   3.392 +lemma irrefl_tranclI: "r^-1 \<inter> r^+ = {} ==> (x, x) \<notin> r^+"
   3.393 +  apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \<noteq> y")
   3.394 +   apply fast
   3.395 +  apply (intro strip)
   3.396 +  apply (erule trancl_induct)
   3.397 +   apply (auto intro: r_into_trancl)
   3.398 +  done
   3.399 +
   3.400 +lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
   3.401 +  by (blast dest: r_into_trancl)
   3.402 +
   3.403 +lemma trancl_subset_Sigma_aux:
   3.404 +    "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
   3.405 +  apply (erule rtrancl_induct)
   3.406 +   apply auto
   3.407 +  done
   3.408 +
   3.409 +lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   3.410 +  apply (unfold trancl_def)
   3.411 +  apply (blast dest!: trancl_subset_Sigma_aux)
   3.412 +  done
   3.413  
   3.414  lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
   3.415    apply safe
   3.416 -  apply (erule trancl_into_rtrancl)
   3.417 +   apply (erule trancl_into_rtrancl)
   3.418    apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   3.419    done
   3.420  
   3.421 @@ -70,7 +416,7 @@
   3.422    by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
   3.423  
   3.424  
   3.425 -(* should be merged with the main body of lemmas: *)
   3.426 +text {* @{text Domain} and @{text Range} *}
   3.427  
   3.428  lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
   3.429    by blast
   3.430 @@ -91,24 +437,26 @@
   3.431    by (simp add: Range_def trancl_converse [symmetric])
   3.432  
   3.433  lemma Not_Domain_rtrancl:
   3.434 -	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
   3.435 - apply (auto)
   3.436 - by (erule rev_mp, erule rtrancl_induct, auto)
   3.437 +    "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
   3.438 +  apply auto
   3.439 +  by (erule rev_mp, erule rtrancl_induct, auto)
   3.440 +
   3.441  
   3.442 -(* more about converse rtrancl and trancl, should be merged with main body *)
   3.443 +text {* More about converse @{text rtrancl} and @{text trancl}, should
   3.444 +  be merged with main body. *}
   3.445  
   3.446 -lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
   3.447 +lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"
   3.448    by (fast intro: trancl_trans)
   3.449  
   3.450  lemma trancl_into_trancl [rule_format]:
   3.451 -  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+"
   3.452 -  apply (erule trancl_induct)   
   3.453 +    "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+"
   3.454 +  apply (erule trancl_induct)
   3.455     apply (fast intro: r_r_into_trancl)
   3.456    apply (fast intro: r_r_into_trancl trancl_trans)
   3.457    done
   3.458  
   3.459  lemma trancl_rtrancl_trancl:
   3.460 -  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+"
   3.461 +    "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r\<^sup>* ==> (a, c) \<in> r\<^sup>+"
   3.462    apply (drule tranclD)
   3.463    apply (erule exE, erule conjE)
   3.464    apply (drule rtrancl_trans, assumption)
   3.465 @@ -116,10 +464,11 @@
   3.466    apply assumption
   3.467    done
   3.468  
   3.469 -lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans 
   3.470 -                 trancl_into_trancl trancl_into_trancl2
   3.471 -                 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   3.472 -                 rtrancl_trancl_trancl trancl_rtrancl_trancl
   3.473 +lemmas transitive_closure_trans [trans] =
   3.474 +  r_r_into_trancl trancl_trans rtrancl_trans
   3.475 +  trancl_into_trancl trancl_into_trancl2
   3.476 +  rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   3.477 +  rtrancl_trancl_trancl trancl_rtrancl_trancl
   3.478  
   3.479  declare trancl_into_rtrancl [elim]
   3.480  
     4.1 --- a/src/HOL/Transitive_Closure_lemmas.ML	Wed Jan 09 17:42:49 2002 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,333 +0,0 @@
     4.4 -(*  Title:      HOL/Transitive_Closure_lemmas.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1992  University of Cambridge
     4.8 -
     4.9 -Theorems about the transitive closure of a relation
    4.10 -*)
    4.11 -
    4.12 -val rtrancl_refl = thm "rtrancl_refl";
    4.13 -val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
    4.14 -val trancl_def = thm "trancl_def";
    4.15 -
    4.16 -
    4.17 -(** The relation rtrancl **)
    4.18 -
    4.19 -section "^*";
    4.20 -
    4.21 -(*rtrancl of r contains r*)
    4.22 -Goal "!!p. p : r ==> p : r^*";
    4.23 -by (split_all_tac 1);
    4.24 -by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    4.25 -qed "r_into_rtrancl";
    4.26 -
    4.27 -AddIs [r_into_rtrancl];
    4.28 -
    4.29 -(*monotonicity of rtrancl*)
    4.30 -Goal "r <= s ==> r^* <= s^*";
    4.31 -by (rtac subsetI 1);
    4.32 -by (split_all_tac 1);
    4.33 -by (etac (thm "rtrancl.induct") 1);
    4.34 -by (rtac rtrancl_into_rtrancl 2);
    4.35 -by (ALLGOALS Blast_tac);
    4.36 -qed "rtrancl_mono";
    4.37 -
    4.38 -(*nice induction rule*)
    4.39 -val major::prems = Goal
    4.40 -    "[| (a::'a,b) : r^*;    \
    4.41 -\       P(a); \
    4.42 -\       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
    4.43 -\     ==> P(b)";
    4.44 -by (rtac (read_instantiate [("P","%x y. x = a --> P y")]
    4.45 -  (major RS thm "rtrancl.induct") RS mp) 1);
    4.46 -by (ALLGOALS (blast_tac (claset() addIs prems)));
    4.47 -qed "rtrancl_induct";
    4.48 -
    4.49 -bind_thm ("rtrancl_induct2", split_rule
    4.50 -  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
    4.51 -
    4.52 -(*transitivity of transitive closure!! -- by induction.*)
    4.53 -Goalw [trans_def] "trans(r^*)";
    4.54 -by Safe_tac;
    4.55 -by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    4.56 -by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    4.57 -qed "trans_rtrancl";
    4.58 -
    4.59 -bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
    4.60 -
    4.61 -
    4.62 -(*elimination of rtrancl -- by induction on a special formula*)
    4.63 -val major::prems = Goal
    4.64 -    "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
    4.65 -\       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
    4.66 -\    |] ==> P";
    4.67 -by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
    4.68 -by (rtac (major RS rtrancl_induct) 2);
    4.69 -by (blast_tac (claset() addIs prems) 2);
    4.70 -by (blast_tac (claset() addIs prems) 2);
    4.71 -by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    4.72 -qed "rtranclE";
    4.73 -
    4.74 -bind_thm ("converse_rtrancl_into_rtrancl", r_into_rtrancl RS rtrancl_trans);
    4.75 -
    4.76 -(*** More r^* equations and inclusions ***)
    4.77 -
    4.78 -Goal "(r^*)^* = r^*";
    4.79 -by Auto_tac;
    4.80 -by (etac rtrancl_induct 1);
    4.81 -by (rtac rtrancl_refl 1);
    4.82 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
    4.83 -qed "rtrancl_idemp";
    4.84 -Addsimps [rtrancl_idemp];
    4.85 -
    4.86 -Goal "R^* O R^* = R^*";
    4.87 -by (rtac set_ext 1);
    4.88 -by (split_all_tac 1);
    4.89 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
    4.90 -qed "rtrancl_idemp_self_comp";
    4.91 -Addsimps [rtrancl_idemp_self_comp];
    4.92 -
    4.93 -Goal "r <= s^* ==> r^* <= s^*";
    4.94 -by (dtac rtrancl_mono 1);
    4.95 -by (Asm_full_simp_tac 1);
    4.96 -qed "rtrancl_subset_rtrancl";
    4.97 -
    4.98 -Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
    4.99 -by (dtac rtrancl_mono 1);
   4.100 -by (dtac rtrancl_mono 1);
   4.101 -by (Asm_full_simp_tac 1);
   4.102 -by (Blast_tac 1);
   4.103 -qed "rtrancl_subset";
   4.104 -
   4.105 -Goal "(R^* Un S^*)^* = (R Un S)^*";
   4.106 -by (blast_tac (claset() addSIs [rtrancl_subset]
   4.107 -                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   4.108 -qed "rtrancl_Un_rtrancl";
   4.109 -
   4.110 -Goal "(R^=)^* = R^*";
   4.111 -by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
   4.112 -qed "rtrancl_reflcl";
   4.113 -Addsimps [rtrancl_reflcl];
   4.114 -
   4.115 -Goal "(r - Id)^* = r^*";
   4.116 -by (rtac sym 1);
   4.117 -by (rtac rtrancl_subset 1);
   4.118 - by (Blast_tac 1);
   4.119 -by (Clarify_tac 1);
   4.120 -by (rename_tac "a b" 1);
   4.121 -by (case_tac "a=b" 1);
   4.122 - by (Blast_tac 1);
   4.123 -by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
   4.124 -qed "rtrancl_r_diff_Id";
   4.125 -
   4.126 -Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
   4.127 -by (etac rtrancl_induct 1);
   4.128 -by (rtac rtrancl_refl 1);
   4.129 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   4.130 -qed "rtrancl_converseD";
   4.131 -
   4.132 -Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
   4.133 -by (etac rtrancl_induct 1);
   4.134 -by (rtac rtrancl_refl 1);
   4.135 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   4.136 -qed "rtrancl_converseI";
   4.137 -
   4.138 -Goal "(r^-1)^* = (r^*)^-1";
   4.139 -(*blast_tac fails: the split_all_tac wrapper must be called to convert
   4.140 -  the set element to a pair*)
   4.141 -by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
   4.142 -qed "rtrancl_converse";
   4.143 -
   4.144 -val major::prems = Goal
   4.145 -    "[| (a,b) : r^*; P(b); \
   4.146 -\       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
   4.147 -\     ==> P(a)";
   4.148 -by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
   4.149 -by (resolve_tac prems 1);
   4.150 -by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
   4.151 -qed "converse_rtrancl_induct";
   4.152 -
   4.153 -bind_thm ("converse_rtrancl_induct2", split_rule
   4.154 -  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
   4.155 -
   4.156 -val major::prems = Goal
   4.157 - "[| (x,z):r^*; \
   4.158 -\    x=z ==> P; \
   4.159 -\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
   4.160 -\ |] ==> P";
   4.161 -by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
   4.162 -by (rtac (major RS converse_rtrancl_induct) 2);
   4.163 -by (blast_tac (claset() addIs prems) 2);
   4.164 -by (blast_tac (claset() addIs prems) 2);
   4.165 -by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   4.166 -qed "converse_rtranclE";
   4.167 -
   4.168 -bind_thm ("converse_rtranclE2", split_rule
   4.169 -  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
   4.170 -
   4.171 -Goal "r O r^* = r^* O r";
   4.172 -by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
   4.173 -	               addIs [rtrancl_into_rtrancl, converse_rtrancl_into_rtrancl]) 1);
   4.174 -qed "r_comp_rtrancl_eq";
   4.175 -
   4.176 -
   4.177 -(**** The relation trancl ****)
   4.178 -
   4.179 -section "^+";
   4.180 -
   4.181 -Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
   4.182 -by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
   4.183 -qed "trancl_mono";
   4.184 -
   4.185 -(** Conversions between trancl and rtrancl **)
   4.186 -
   4.187 -Goalw [trancl_def]
   4.188 -    "!!p. p : r^+ ==> p : r^*";
   4.189 -by (split_all_tac 1);
   4.190 -by (etac rel_compEpair 1);
   4.191 -by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
   4.192 -qed "trancl_into_rtrancl";
   4.193 -
   4.194 -(*r^+ contains r*)
   4.195 -Goalw [trancl_def]
   4.196 -   "!!p. p : r ==> p : r^+";
   4.197 -by (split_all_tac 1);
   4.198 -by (REPEAT (ares_tac [prem,rel_compI,rtrancl_refl] 1));
   4.199 -qed "r_into_trancl";
   4.200 -AddIs [r_into_trancl];
   4.201 -
   4.202 -(*intro rule by definition: from rtrancl and r*)
   4.203 -Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
   4.204 -by Auto_tac;
   4.205 -qed "rtrancl_into_trancl1";
   4.206 -
   4.207 -(*intro rule from r and rtrancl*)
   4.208 -Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
   4.209 -by (etac rtranclE 1);
   4.210 -by (blast_tac (claset() addIs [r_into_trancl]) 1);
   4.211 -by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
   4.212 -by (REPEAT (ares_tac [r_into_rtrancl] 1));
   4.213 -qed "rtrancl_into_trancl2";
   4.214 -
   4.215 -(*Nice induction rule for trancl*)
   4.216 -val major::prems = Goal
   4.217 -  "[| (a,b) : r^+;                                      \
   4.218 -\     !!y.  [| (a,y) : r |] ==> P(y);                   \
   4.219 -\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
   4.220 -\  |] ==> P(b)";
   4.221 -by (rtac (rewrite_rule [trancl_def] major  RS  rel_compEpair) 1);
   4.222 -(*by induction on this formula*)
   4.223 -by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
   4.224 -(*now solve first subgoal: this formula is sufficient*)
   4.225 -by (Blast_tac 1);
   4.226 -by (etac rtrancl_induct 1);
   4.227 -by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
   4.228 -qed "trancl_induct";
   4.229 -
   4.230 -(*Another induction rule for trancl, incorporating transitivity.*)
   4.231 -val major::prems = Goal
   4.232 - "[| (x,y) : r^+; \
   4.233 -\    !!x y. (x,y) : r ==> P x y; \
   4.234 -\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
   4.235 -\ |] ==> P x y";
   4.236 -by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
   4.237 -qed "trancl_trans_induct";
   4.238 -
   4.239 -(*elimination of r^+ -- NOT an induction rule*)
   4.240 -val major::prems = Goal
   4.241 -    "[| (a::'a,b) : r^+;  \
   4.242 -\       (a,b) : r ==> P; \
   4.243 -\       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
   4.244 -\    |] ==> P";
   4.245 -by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
   4.246 -by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
   4.247 -by (rtac (rewrite_rule [trancl_def] major RS rel_compEpair) 1);
   4.248 -by (etac rtranclE 1);
   4.249 -by (Blast_tac 1);
   4.250 -by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
   4.251 -qed "tranclE";
   4.252 -
   4.253 -(*Transitivity of r^+.
   4.254 -  Proved by unfolding since it uses transitivity of rtrancl. *)
   4.255 -Goalw [trancl_def] "trans(r^+)";
   4.256 -by (rtac transI 1);
   4.257 -by (REPEAT (etac rel_compEpair 1));
   4.258 -by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS rel_compI)) 1);
   4.259 -by (REPEAT (assume_tac 1));
   4.260 -qed "trans_trancl";
   4.261 -
   4.262 -bind_thm ("trancl_trans", trans_trancl RS transD);
   4.263 -
   4.264 -Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
   4.265 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   4.266 -qed "rtrancl_trancl_trancl";
   4.267 -
   4.268 -(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
   4.269 -bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
   4.270 -
   4.271 -(* primitive recursion for trancl over finite relations: *)
   4.272 -Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
   4.273 -by (rtac equalityI 1);
   4.274 - by (rtac subsetI 1);
   4.275 - by (split_all_tac 1);
   4.276 - by (etac trancl_induct 1);
   4.277 -  by (blast_tac (claset() addIs [r_into_trancl]) 1);
   4.278 - by (blast_tac (claset() addIs
   4.279 -     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
   4.280 -by (rtac subsetI 1);
   4.281 -by (blast_tac (claset() addIs
   4.282 -     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
   4.283 -      impOfSubs rtrancl_mono, trancl_mono]) 1);
   4.284 -qed "trancl_insert";
   4.285 -
   4.286 -Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
   4.287 -by (simp_tac (simpset() addsimps [rtrancl_converse,converse_rel_comp]) 1);
   4.288 -by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
   4.289 -				  r_comp_rtrancl_eq]) 1);
   4.290 -qed "trancl_converse";
   4.291 -
   4.292 -Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
   4.293 -by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   4.294 -qed "trancl_converseI";
   4.295 -
   4.296 -Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
   4.297 -by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   4.298 -qed "trancl_converseD";
   4.299 -
   4.300 -val major::prems = Goal
   4.301 -    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
   4.302 -\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
   4.303 -\     ==> P(a)";
   4.304 -by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
   4.305 - by (resolve_tac prems 1);
   4.306 - by (etac converseD 1);
   4.307 -by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
   4.308 -qed "converse_trancl_induct";
   4.309 -
   4.310 -Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
   4.311 -by (etac converse_trancl_induct 1);
   4.312 -by Auto_tac;
   4.313 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   4.314 -qed "tranclD";
   4.315 -
   4.316 -(*Unused*)
   4.317 -Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
   4.318 -by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
   4.319 -by (Fast_tac 1);
   4.320 -by (strip_tac 1);
   4.321 -by (etac trancl_induct 1);
   4.322 -by (auto_tac (claset() addIs [r_into_trancl], simpset()));
   4.323 -qed "irrefl_tranclI";
   4.324 -
   4.325 -Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
   4.326 -by (blast_tac (claset() addDs [r_into_trancl]) 1);
   4.327 -qed "irrefl_trancl_rD";
   4.328 -
   4.329 -Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
   4.330 -by (etac rtrancl_induct 1);
   4.331 -by Auto_tac;
   4.332 -val lemma = result();
   4.333 -
   4.334 -Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
   4.335 -by (blast_tac (claset() addSDs [lemma]) 1);
   4.336 -qed "trancl_subset_Sigma";