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