# HG changeset patch
# User berghofe
# Date 990537131 -7200
# Node ID cd2c27a23df10bde9911a8f0115023e374657933
# Parent  680ebd093cfed628ba65ec77234525fe47a608c2
Transitive closure is now defined via "inductive".

diff -r 680ebd093cfe -r cd2c27a23df1 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue May 22 15:11:43 2001 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue May 22 15:12:11 2001 +0200
@@ -13,13 +13,18 @@
 to be atomic.
 *)
 
-theory Transitive_Closure = Lfp + Relation
+theory Transitive_Closure = Inductive
 files ("Transitive_Closure_lemmas.ML"):
 
+consts
+  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
+
+inductive "r^*"
+intros
+  rtrancl_refl [intro!, simp]: "(a, a) : r^*"
+  rtrancl_into_rtrancl:        "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"
+
 constdefs
-  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
-  "r^* == lfp (%s. Id Un (r O s))"
-
   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
   "r^+ ==  r O rtrancl r"
 
@@ -89,5 +94,11 @@
 	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
  apply (auto)
  by (erule rev_mp, erule rtrancl_induct, auto)
- 
+
+
+declare rtrancl_induct [induct set: rtrancl]
+declare rtranclE [cases set: rtrancl]
+declare trancl_induct [induct set: trancl]
+declare tranclE [cases set: trancl]
+
 end
diff -r 680ebd093cfe -r cd2c27a23df1 src/HOL/Transitive_Closure_lemmas.ML
--- a/src/HOL/Transitive_Closure_lemmas.ML	Tue May 22 15:11:43 2001 +0200
+++ b/src/HOL/Transitive_Closure_lemmas.ML	Tue May 22 15:12:11 2001 +0200
@@ -6,7 +6,8 @@
 Theorems about the transitive closure of a relation
 *)
 
-val rtrancl_def = thm "rtrancl_def";
+val rtrancl_refl = thm "rtrancl_refl";
+val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
 val trancl_def = thm "trancl_def";
 
 
@@ -14,29 +15,6 @@
 
 section "^*";
 
-Goal "mono(%s. Id Un (r O s))";
-by (rtac monoI 1);
-by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
-qed "rtrancl_fun_mono";
-
-bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
-
-(*Reflexivity of rtrancl*)
-Goal "(a,a) : r^*";
-by (stac rtrancl_unfold 1);
-by (Blast_tac 1);
-qed "rtrancl_refl";
-
-Addsimps [rtrancl_refl];
-AddSIs   [rtrancl_refl];
-
-
-(*Closure under composition with r*)
-Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
-by (stac rtrancl_unfold 1);
-by (Blast_tac 1);
-qed "rtrancl_into_rtrancl";
-
 (*rtrancl of r contains r*)
 Goal "!!p. p : r ==> p : r^*";
 by (split_all_tac 1);
@@ -46,35 +24,23 @@
 AddIs [r_into_rtrancl];
 
 (*monotonicity of rtrancl*)
-Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
-by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
+Goal "r <= s ==> r^* <= s^*";
+by (rtac subsetI 1);
+by (split_all_tac 1);
+by (etac (thm "rtrancl.induct") 1);
+by (rtac rtrancl_into_rtrancl 2);
+by (ALLGOALS Blast_tac);
 qed "rtrancl_mono";
 
-(** standard induction rule **)
-
-val major::prems = Goal 
-  "[| (a,b) : r^*; \
-\     !!x. P(x,x); \
-\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
-\  ==>  P(a,b)";
-by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "rtrancl_full_induct";
-
 (*nice induction rule*)
 val major::prems = Goal
     "[| (a::'a,b) : r^*;    \
 \       P(a); \
 \       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
 \     ==> P(b)";
-(*by induction on this formula*)
-by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
-(*now solve first subgoal: this formula is sufficient*)
-by (Blast_tac 1);
-(*now do the induction*)
-by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (blast_tac (claset() addIs prems) 1);
-by (blast_tac (claset() addIs prems) 1);
+by (rtac (read_instantiate [("P","%x y. x = a --> P y")]
+  (major RS thm "rtrancl.induct") RS mp) 1);
+by (ALLGOALS (blast_tac (claset() addIs prems)));
 qed "rtrancl_induct";
 
 bind_thm ("rtrancl_induct2", split_rule