src/HOL/Induct/Acc.ML

 Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
 by (etac acc.elim 1);
 by (rewtac pred_def);
 by (Fast_tac 1);
 qed "acc_downward";
+
+Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
+be rtrancl_induct 1;
+by(Blast_tac 1);
+ by(blast_tac (claset() addDs [acc_downward]) 1);
+val lemma = result();
+Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
+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)";