src/HOL/Accessible_Part.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21404 eb85850d3eb7
child 22262 96ba62dff413
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
krauss@19564
     1
(*  Title:      HOL/Accessible_Part.thy
krauss@19564
     2
    ID:         $Id$
krauss@19564
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
krauss@19564
     4
    Copyright   1994  University of Cambridge
krauss@19564
     5
*)
krauss@19564
     6
krauss@19564
     7
header {* The accessible part of a relation *}
krauss@19564
     8
krauss@19564
     9
theory Accessible_Part
krauss@19564
    10
imports Wellfounded_Recursion
krauss@19564
    11
begin
krauss@19564
    12
krauss@19564
    13
subsection {* Inductive definition *}
krauss@19564
    14
krauss@19564
    15
text {*
krauss@19564
    16
 Inductive definition of the accessible part @{term "acc r"} of a
krauss@19564
    17
 relation; see also \cite{paulin-tlca}.
krauss@19564
    18
*}
krauss@19564
    19
krauss@19564
    20
consts
krauss@19564
    21
  acc :: "('a \<times> 'a) set => 'a set"
krauss@19564
    22
inductive "acc r"
krauss@19564
    23
  intros
krauss@19564
    24
    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
krauss@19564
    25
krauss@19564
    26
abbreviation
wenzelm@21404
    27
  termi :: "('a \<times> 'a) set => 'a set" where
krauss@19564
    28
  "termi r == acc (r\<inverse>)"
krauss@19564
    29
krauss@19564
    30
krauss@19564
    31
subsection {* Induction rules *}
krauss@19564
    32
krauss@19564
    33
theorem acc_induct:
krauss@19564
    34
  assumes major: "a \<in> acc r"
krauss@19564
    35
  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
krauss@19564
    36
  shows "P a"
krauss@19564
    37
  apply (rule major [THEN acc.induct])
krauss@19564
    38
  apply (rule hyp)
krauss@19564
    39
   apply (rule accI)
krauss@19564
    40
   apply fast
krauss@19564
    41
  apply fast
krauss@19564
    42
  done
krauss@19564
    43
krauss@19564
    44
theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
krauss@19564
    45
krauss@19564
    46
theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
krauss@19564
    47
  apply (erule acc.elims)
krauss@19564
    48
  apply fast
krauss@19564
    49
  done
krauss@19564
    50
krauss@19564
    51
lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
krauss@19564
    52
  apply (erule rtrancl_induct)
krauss@19564
    53
   apply blast
krauss@19564
    54
  apply (blast dest: acc_downward)
krauss@19564
    55
  done
krauss@19564
    56
krauss@19564
    57
theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
krauss@19564
    58
  apply (blast dest: acc_downwards_aux)
krauss@19564
    59
  done
krauss@19564
    60
krauss@19564
    61
theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
krauss@19564
    62
  apply (rule wfUNIVI)
krauss@19564
    63
  apply (induct_tac P x rule: acc_induct)
krauss@19564
    64
   apply blast
krauss@19564
    65
  apply blast
krauss@19564
    66
  done
krauss@19564
    67
krauss@19564
    68
theorem acc_wfD: "wf r ==> x \<in> acc r"
krauss@19564
    69
  apply (erule wf_induct)
krauss@19564
    70
  apply (rule accI)
krauss@19564
    71
  apply blast
krauss@19564
    72
  done
krauss@19564
    73
krauss@19564
    74
theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
krauss@19564
    75
  apply (blast intro: acc_wfI dest: acc_wfD)
krauss@19564
    76
  done
krauss@19564
    77
krauss@19564
    78
wenzelm@19669
    79
text {* Smaller relations have bigger accessible parts: *}
wenzelm@19669
    80
krauss@19564
    81
lemma acc_subset:
wenzelm@19669
    82
  assumes sub: "R1 \<subseteq> R2"
krauss@19564
    83
  shows "acc R2 \<subseteq> acc R1"
krauss@19564
    84
proof
krauss@19564
    85
  fix x assume "x \<in> acc R2"
wenzelm@19669
    86
  then show "x \<in> acc R1"
wenzelm@19669
    87
  proof (induct x)
krauss@19564
    88
    fix x
krauss@19564
    89
    assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
krauss@19564
    90
    with sub show "x \<in> acc R1"
krauss@19564
    91
      by (blast intro:accI)
krauss@19564
    92
  qed
krauss@19564
    93
qed
krauss@19564
    94
krauss@19564
    95
wenzelm@19669
    96
text {* This is a generalized induction theorem that works on
wenzelm@19669
    97
  subsets of the accessible part. *}
krauss@19564
    98
krauss@19564
    99
lemma acc_subset_induct:
krauss@19564
   100
  assumes subset: "D \<subseteq> acc R"
wenzelm@19669
   101
    and dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
wenzelm@19669
   102
    and "x \<in> D"
wenzelm@19669
   103
    and istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
wenzelm@19669
   104
  shows "P x"
krauss@19564
   105
proof -
krauss@19564
   106
  from `x \<in> D` and subset 
krauss@19564
   107
  have "x \<in> acc R" ..
wenzelm@19669
   108
  then show "P x" using `x \<in> D`
krauss@19564
   109
  proof (induct x)
krauss@19564
   110
    fix x
krauss@19564
   111
    assume "x \<in> D"
krauss@19564
   112
      and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
krauss@19564
   113
    with dcl and istep show "P x" by blast
krauss@19564
   114
  qed
krauss@19564
   115
qed
krauss@19564
   116
krauss@19564
   117
end