diff -r 5e7c4a45d8bb -r adda1dc18bb8 src/HOL/Induct/Acc.thy --- 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 \ 'a) set => 'a set" -- {* accessible part *} inductive "acc r" intros accI [rulify_prems]: - "ALL y. (y, x) : r --> y : acc r ==> x : acc r" + "\y. (y, x) \ r --> y \ acc r ==> x \ acc r" syntax - termi :: "('a * 'a)set => 'a set" + termi :: "('a \ 'a) set => 'a set" translations - "termi r" == "acc(r^-1)" + "termi r" == "acc (r^-1)" + + +theorem acc_induct: + "[| a \ acc r; + !!x. [| x \ acc r; \y. (y, x) \ r --> P y |] ==> P x + |] ==> P a" +proof - + assume major: "a \ acc r" + assume hyp: "!!x. [| x \ acc r; \y. (y, x) \ 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 \ acc r; (a, b) \ r |] ==> a \ acc r" + apply (erule acc.elims) + apply fast + done + +lemma acc_downwards_aux: "(b, a) \ r^* ==> a \ acc r --> b \ acc r" + apply (erule rtrancl_induct) + apply blast + apply (blast dest: acc_downward) + done + +theorem acc_downwards: "[| a \ acc r; (b, a) \ r^* |] ==> b \ acc r" + apply (blast dest: acc_downwards_aux) + done + +theorem acc_wfI: "\x. x \ 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 \ acc r" + apply (erule wf_induct) + apply (rule accI) + apply blast + done + +theorem wf_acc_iff: "wf r = (\x. x \ acc r)" + apply (blast intro: acc_wfI dest: acc_wfD) + done end