src/HOL/Induct/Acc.thy
author wenzelm
Thu Sep 07 21:10:11 2000 +0200 (2000-09-07)
changeset 9906 5c027cca6262
parent 9802 adda1dc18bb8
child 9941 fe05af7ec816
permissions -rw-r--r--
updated attribute names;
     1 (*  Title:      HOL/ex/Acc.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Inductive definition of acc(r)
     7 
     8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
     9 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    10 *)
    11 
    12 header {* The accessible part of a relation *}
    13 
    14 theory Acc = Main:
    15 
    16 consts
    17   acc  :: "('a \<times> 'a) set => 'a set"  -- {* accessible part *}
    18 
    19 inductive "acc r"
    20   intros
    21     accI [rulified]:
    22       "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    23 
    24 syntax
    25   termi :: "('a \<times> 'a) set => 'a set"
    26 translations
    27   "termi r" == "acc (r^-1)"
    28 
    29 
    30 theorem acc_induct:
    31   "[| a \<in> acc r;
    32       !!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x
    33   |] ==> P a"
    34 proof -
    35   assume major: "a \<in> acc r"
    36   assume hyp: "!!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x"
    37   show ?thesis
    38     apply (rule major [THEN acc.induct])
    39     apply (rule hyp)
    40      apply (rule accI)
    41      apply fast
    42     apply fast
    43     done
    44 qed
    45 
    46 theorem acc_downward: "[| b \<in> acc r; (a, b) \<in> r |] ==> a \<in> acc r"
    47   apply (erule acc.elims)
    48   apply fast
    49   done
    50 
    51 lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
    52   apply (erule rtrancl_induct)
    53    apply blast
    54   apply (blast dest: acc_downward)
    55   done
    56 
    57 theorem acc_downwards: "[| a \<in> acc r; (b, a) \<in> r^* |] ==> b \<in> acc r"
    58   apply (blast dest: acc_downwards_aux)
    59   done
    60 
    61 theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    62   apply (rule wfUNIVI)
    63   apply (induct_tac P x rule: acc_induct)
    64    apply blast
    65   apply blast
    66   done
    67 
    68 theorem acc_wfD: "wf r ==> x \<in> acc r"
    69   apply (erule wf_induct)
    70   apply (rule accI)
    71   apply blast
    72   done
    73 
    74 theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    75   apply (blast intro: acc_wfI dest: acc_wfD)
    76   done
    77 
    78 end