converted;

--- a/src/HOL/Induct/Acc.ML	Sat Sep 02 21:47:50 2000 +0200
+++ b/src/HOL/Induct/Acc.ML	Sat Sep 02 21:48:10 2000 +0200
@@ -1,53 +1,8 @@
-(*  Title:      HOL/ex/Acc
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Inductive definition of acc(r)
-
-See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
-Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
-*)
 
 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 (thm "acc.elims") 1);
-by (Fast_tac 1);
-qed "acc_downward";
-
-Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
-by (etac rtrancl_induct 1);
-by (Blast_tac 1);
- by (blast_tac (claset() addDs [acc_downward]) 1);
-no_qed();
-val lemma = result();
-
-Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
-by (blast_tac (claset() addDs [lemma]) 1);
-qed "acc_downwards";
-
-Goal "!x. x : acc(r) ==> wf(r)";
-by (rtac wfUNIVI 1);
-by (deepen_tac (claset() addEs [acc_induct]) 1 1);
-qed "acc_wfI";
-
-Goal "wf(r) ==> x : acc(r)";
-by (etac wf_induct 1);
-by (rtac accI 1);
-by (Blast_tac 1);
-qed "acc_wfD";
-
-Goal "wf(r)  =  (!x. x : acc(r))";
-by (blast_tac (claset() addIs [acc_wfI] addDs [acc_wfD]) 1);
-qed "wf_acc_iff";
+val acc_induct = thm "acc_induct";
+val acc_downward = thm "acc_downward";
+val acc_downwards = thm "acc_downwards";
+val acc_wfI = thm "acc_wfI";
+val acc_wfD = thm "acc_wfD";
+val wf_acc_iff = thm "wf_acc_iff";

--- a/src/HOL/Induct/Acc.thy	Sat Sep 02 21:47:50 2000 +0200
+++ b/src/HOL/Induct/Acc.thy	Sat Sep 02 21:48:10 2000 +0200
@@ -14,16 +14,65 @@
 theory Acc = Main:
 
 consts
-  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
+  acc  :: "('a \<times> 'a) set => 'a set"  -- {* accessible part *}
 
 inductive "acc r"
   intros
     accI [rulify_prems]:
-      "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
+      "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
 
 syntax
-  termi :: "('a * 'a)set => 'a set"
+  termi :: "('a \<times> 'a) set => 'a set"
 translations
-  "termi r" == "acc(r^-1)"
+  "termi r" == "acc (r^-1)"
+
+
+theorem acc_induct:
+  "[| a \<in> acc r;
+      !!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x
+  |] ==> P a"
+proof -
+  assume major: "a \<in> acc r"
+  assume hyp: "!!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x"
+  show ?thesis
+    apply (rule major [THEN acc.induct])
+    apply (rule hyp)
+     apply (rule accI)
+     apply fast
+    apply fast
+    done
+qed
+
+theorem acc_downward: "[| b \<in> acc r; (a, b) \<in> r |] ==> a \<in> acc r"
+  apply (erule acc.elims)
+  apply fast
+  done
+
+lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
+  apply (erule rtrancl_induct)
+   apply blast
+  apply (blast dest: acc_downward)
+  done
+
+theorem acc_downwards: "[| a \<in> acc r; (b, a) \<in> r^* |] ==> b \<in> acc r"
+  apply (blast dest: acc_downwards_aux)
+  done
+
+theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
+  apply (rule wfUNIVI)
+  apply (induct_tac P x rule: acc_induct)
+   apply blast
+  apply blast
+  done
+
+theorem acc_wfD: "wf r ==> x \<in> acc r"
+  apply (erule wf_induct)
+  apply (rule accI)
+  apply blast
+  done
+
+theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
+  apply (blast intro: acc_wfI dest: acc_wfD)
+  done
 
 end