src/HOL/Library/Accessible_Part.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10734 66604af28f94
child 14706 71590b7733b7
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Library/Accessible_Part.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 *)
     6 
     7 header {*
     8  \title{The accessible part of a relation}
     9  \author{Lawrence C Paulson}
    10 *}
    11 
    12 theory Accessible_Part = Main:
    13 
    14 
    15 subsection {* Inductive definition *}
    16 
    17 text {*
    18  Inductive definition of the accessible part @{term "acc r"} of a
    19  relation; see also \cite{paulin-tlca}.
    20 *}
    21 
    22 consts
    23   acc :: "('a \<times> 'a) set => 'a set"
    24 inductive "acc r"
    25   intros
    26     accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    27 
    28 syntax
    29   termi :: "('a \<times> 'a) set => 'a set"
    30 translations
    31   "termi r" == "acc (r\<inverse>)"
    32 
    33 
    34 subsection {* Induction rules *}
    35 
    36 theorem acc_induct:
    37   "a \<in> acc r ==>
    38     (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
    39 proof -
    40   assume major: "a \<in> acc r"
    41   assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
    42   show ?thesis
    43     apply (rule major [THEN acc.induct])
    44     apply (rule hyp)
    45      apply (rule accI)
    46      apply fast
    47     apply fast
    48     done
    49 qed
    50 
    51 theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
    52 
    53 theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
    54   apply (erule acc.elims)
    55   apply fast
    56   done
    57 
    58 lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
    59   apply (erule rtrancl_induct)
    60    apply blast
    61   apply (blast dest: acc_downward)
    62   done
    63 
    64 theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
    65   apply (blast dest: acc_downwards_aux)
    66   done
    67 
    68 theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    69   apply (rule wfUNIVI)
    70   apply (induct_tac P x rule: acc_induct)
    71    apply blast
    72   apply blast
    73   done
    74 
    75 theorem acc_wfD: "wf r ==> x \<in> acc r"
    76   apply (erule wf_induct)
    77   apply (rule accI)
    78   apply blast
    79   done
    80 
    81 theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    82   apply (blast intro: acc_wfI dest: acc_wfD)
    83   done
    84 
    85 end