src/HOL/Induct/Acc.thy
changeset 10258 d549f2534e6d
parent 10257 21055ac27708
child 10259 93ec82d535f2
     1.1 --- a/src/HOL/Induct/Acc.thy	Wed Oct 18 23:35:56 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,78 +0,0 @@
     1.4 -(*  Title:      HOL/ex/Acc.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1994  University of Cambridge
     1.8 -
     1.9 -Inductive definition of acc(r)
    1.10 -
    1.11 -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    1.12 -Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    1.13 -*)
    1.14 -
    1.15 -header {* The accessible part of a relation *}
    1.16 -
    1.17 -theory Acc = Main:
    1.18 -
    1.19 -consts
    1.20 -  acc  :: "('a \<times> 'a) set => 'a set"  -- {* accessible part *}
    1.21 -
    1.22 -inductive "acc r"
    1.23 -  intros
    1.24 -    accI [rule_format]:
    1.25 -      "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    1.26 -
    1.27 -syntax
    1.28 -  termi :: "('a \<times> 'a) set => 'a set"
    1.29 -translations
    1.30 -  "termi r" == "acc (r^-1)"
    1.31 -
    1.32 -
    1.33 -theorem acc_induct:
    1.34 -  "[| a \<in> acc r;
    1.35 -      !!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x
    1.36 -  |] ==> P a"
    1.37 -proof -
    1.38 -  assume major: "a \<in> acc r"
    1.39 -  assume hyp: "!!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x"
    1.40 -  show ?thesis
    1.41 -    apply (rule major [THEN acc.induct])
    1.42 -    apply (rule hyp)
    1.43 -     apply (rule accI)
    1.44 -     apply fast
    1.45 -    apply fast
    1.46 -    done
    1.47 -qed
    1.48 -
    1.49 -theorem acc_downward: "[| b \<in> acc r; (a, b) \<in> r |] ==> a \<in> acc r"
    1.50 -  apply (erule acc.elims)
    1.51 -  apply fast
    1.52 -  done
    1.53 -
    1.54 -lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
    1.55 -  apply (erule rtrancl_induct)
    1.56 -   apply blast
    1.57 -  apply (blast dest: acc_downward)
    1.58 -  done
    1.59 -
    1.60 -theorem acc_downwards: "[| a \<in> acc r; (b, a) \<in> r^* |] ==> b \<in> acc r"
    1.61 -  apply (blast dest: acc_downwards_aux)
    1.62 -  done
    1.63 -
    1.64 -theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    1.65 -  apply (rule wfUNIVI)
    1.66 -  apply (induct_tac P x rule: acc_induct)
    1.67 -   apply blast
    1.68 -  apply blast
    1.69 -  done
    1.70 -
    1.71 -theorem acc_wfD: "wf r ==> x \<in> acc r"
    1.72 -  apply (erule wf_induct)
    1.73 -  apply (rule accI)
    1.74 -  apply blast
    1.75 -  done
    1.76 -
    1.77 -theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    1.78 -  apply (blast intro: acc_wfI dest: acc_wfD)
    1.79 -  done
    1.80 -
    1.81 -end