src/HOL/Library/Accessible_Part.thy
author wenzelm
Sat Apr 08 22:51:06 2006 +0200 (2006-04-08)
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
permissions -rw-r--r--
refined 'abbreviation';
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@19363
    26
abbreviation
wenzelm@10248
    27
  termi :: "('a \<times> 'a) set => 'a set"
wenzelm@19086
    28
  "termi r == acc (r\<inverse>)"
wenzelm@10248
    29
wenzelm@10248
    30
wenzelm@10248
    31
subsection {* Induction rules *}
wenzelm@10248
    32
wenzelm@10734
    33
theorem acc_induct:
wenzelm@18241
    34
  assumes major: "a \<in> acc r"
wenzelm@18241
    35
  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
wenzelm@18241
    36
  shows "P a"
wenzelm@18241
    37
  apply (rule major [THEN acc.induct])
wenzelm@18241
    38
  apply (rule hyp)
wenzelm@18241
    39
   apply (rule accI)
wenzelm@18241
    40
   apply fast
wenzelm@18241
    41
  apply fast
wenzelm@18241
    42
  done
wenzelm@10248
    43
wenzelm@10734
    44
theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
wenzelm@10734
    45
wenzelm@10248
    46
theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
wenzelm@10248
    47
  apply (erule acc.elims)
wenzelm@10248
    48
  apply fast
wenzelm@10248
    49
  done
wenzelm@10248
    50
wenzelm@10388
    51
lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
wenzelm@10248
    52
  apply (erule rtrancl_induct)
wenzelm@10248
    53
   apply blast
wenzelm@10248
    54
  apply (blast dest: acc_downward)
wenzelm@10248
    55
  done
wenzelm@10248
    56
wenzelm@10388
    57
theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
wenzelm@10248
    58
  apply (blast dest: acc_downwards_aux)
wenzelm@10248
    59
  done
wenzelm@10248
    60
wenzelm@10248
    61
theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
wenzelm@10248
    62
  apply (rule wfUNIVI)
wenzelm@10248
    63
  apply (induct_tac P x rule: acc_induct)
wenzelm@10248
    64
   apply blast
wenzelm@10248
    65
  apply blast
wenzelm@10248
    66
  done
wenzelm@10248
    67
wenzelm@10248
    68
theorem acc_wfD: "wf r ==> x \<in> acc r"
wenzelm@10248
    69
  apply (erule wf_induct)
wenzelm@10248
    70
  apply (rule accI)
wenzelm@10248
    71
  apply blast
wenzelm@10248
    72
  done
wenzelm@10248
    73
wenzelm@10248
    74
theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
wenzelm@10248
    75
  apply (blast intro: acc_wfI dest: acc_wfD)
wenzelm@10248
    76
  done
wenzelm@10248
    77
wenzelm@10248
    78
end