# HG changeset patch
# User berghofe
# Date 939130302 -7200
# Node ID cb353d802adef65b38227142bc5cfc3f217d35e8
# Parent  b92bbfda8de544d63b6226bb752c58f9dedb14f3
Tuned inductive definition.

diff -r b92bbfda8de5 -r cb353d802ade src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Tue Oct 05 15:31:39 1999 +0200
+++ b/src/HOL/Induct/Acc.ML	Tue Oct 05 15:31:42 1999 +0200
@@ -9,16 +9,20 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-(*The intended introduction rule*)
-val prems = goal Acc.thy
-    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
-by (fast_tac (claset() addIs prems @ 
-                             map (rewrite_rule [pred_def]) acc.intrs) 1);
-qed "accI";
+val accI = thm "acc.accI";
+
+val [major,indhyp] = Goal
+    "[| a : acc(r);                                             \
+\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
+\    |] ==> P(a)";
+by (rtac (major RS thm "acc.induct") 1);
+by (rtac indhyp 1);
+by (rtac accI 1);
+by (ALLGOALS Fast_tac);
+qed "acc_induct";
 
 Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
-by (etac acc.elim 1);
-by (rewtac pred_def);
+by (etac (thm "acc.elims") 1);
 by (Fast_tac 1);
 qed "acc_downward";
 
@@ -33,18 +37,6 @@
 by (blast_tac (claset() addDs [lemma]) 1);
 qed "acc_downwards";
 
-val [major,indhyp] = goal Acc.thy
-    "[| a : acc(r);                                             \
-\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
-\    |] ==> P(a)";
-by (rtac (major RS acc.induct) 1);
-by (rtac indhyp 1);
-by (resolve_tac acc.intrs 1);
-by (rewtac pred_def);
-by (Fast_tac 2);
-by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
-qed "acc_induct";
-
 Goal "!x. x : acc(r) ==> wf(r)";
 by (rtac wfUNIVI 1);
 by (deepen_tac (claset() addEs [acc_induct]) 1 1);
diff -r b92bbfda8de5 -r cb353d802ade src/HOL/Induct/Acc.thy
--- a/src/HOL/Induct/Acc.thy	Tue Oct 05 15:31:39 1999 +0200
+++ b/src/HOL/Induct/Acc.thy	Tue Oct 05 15:31:42 1999 +0200
@@ -9,19 +9,15 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Acc = WF + Inductive +
-
-constdefs
-  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
-  "pred x r == {y. (y,x):r}"
+theory Acc = WF + Inductive:
 
 consts
   acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
 
-inductive "acc(r)"
+inductive "acc r"
   intrs
-    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
-  monos     Pow_mono
+    accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
+
 
 syntax        termi :: "('a * 'a)set => 'a set"
 translations "termi r" == "acc(r^-1)"