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