src/HOL/Library/Accessible_Part.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 18241 afdba6b3e383
permissions -rw-r--r--
import -> imports
     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 {* The accessible part of a relation *}
     8 
     9 theory Accessible_Part
    10 imports Main
    11 begin
    12 
    13 subsection {* Inductive definition *}
    14 
    15 text {*
    16  Inductive definition of the accessible part @{term "acc r"} of a
    17  relation; see also \cite{paulin-tlca}.
    18 *}
    19 
    20 consts
    21   acc :: "('a \<times> 'a) set => 'a set"
    22 inductive "acc r"
    23   intros
    24     accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    25 
    26 syntax
    27   termi :: "('a \<times> 'a) set => 'a set"
    28 translations
    29   "termi r" == "acc (r\<inverse>)"
    30 
    31 
    32 subsection {* Induction rules *}
    33 
    34 theorem acc_induct:
    35   "a \<in> acc r ==>
    36     (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
    37 proof -
    38   assume major: "a \<in> acc r"
    39   assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
    40   show ?thesis
    41     apply (rule major [THEN acc.induct])
    42     apply (rule hyp)
    43      apply (rule accI)
    44      apply fast
    45     apply fast
    46     done
    47 qed
    48 
    49 theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
    50 
    51 theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
    52   apply (erule acc.elims)
    53   apply fast
    54   done
    55 
    56 lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
    57   apply (erule rtrancl_induct)
    58    apply blast
    59   apply (blast dest: acc_downward)
    60   done
    61 
    62 theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
    63   apply (blast dest: acc_downwards_aux)
    64   done
    65 
    66 theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    67   apply (rule wfUNIVI)
    68   apply (induct_tac P x rule: acc_induct)
    69    apply blast
    70   apply blast
    71   done
    72 
    73 theorem acc_wfD: "wf r ==> x \<in> acc r"
    74   apply (erule wf_induct)
    75   apply (rule accI)
    76   apply blast
    77   done
    78 
    79 theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    80   apply (blast intro: acc_wfI dest: acc_wfD)
    81   done
    82 
    83 end