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