src/HOL/Accessible_Part.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23818 cfe8d4bf749a
permissions -rw-r--r--
Name.uu, Name.aT;
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
berghofe@23735
    20
inductive_set
berghofe@23735
    21
  acc :: "('a * 'a) set => 'a set"
berghofe@23735
    22
  for r :: "('a * 'a) set"
berghofe@22262
    23
  where
berghofe@23735
    24
    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"
krauss@19564
    25
krauss@19564
    26
abbreviation
berghofe@23735
    27
  termip :: "('a => 'a => bool) => 'a => bool" where
berghofe@23735
    28
  "termip r == accp (r\<inverse>\<inverse>)"
berghofe@23735
    29
berghofe@23735
    30
abbreviation
berghofe@23735
    31
  termi :: "('a * 'a) set => 'a set" where
berghofe@23735
    32
  "termi r == acc (r\<inverse>)"
krauss@19564
    33
krauss@23818
    34
lemmas accpI = accp.accI
krauss@19564
    35
krauss@19564
    36
subsection {* Induction rules *}
krauss@19564
    37
berghofe@23735
    38
theorem accp_induct:
berghofe@23735
    39
  assumes major: "accp r a"
berghofe@23735
    40
  assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
krauss@19564
    41
  shows "P a"
berghofe@23735
    42
  apply (rule major [THEN accp.induct])
krauss@19564
    43
  apply (rule hyp)
berghofe@23735
    44
   apply (rule accp.accI)
krauss@19564
    45
   apply fast
krauss@19564
    46
  apply fast
krauss@19564
    47
  done
krauss@19564
    48
berghofe@23735
    49
theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
krauss@19564
    50
berghofe@23735
    51
theorem accp_downward: "accp r b ==> r a b ==> accp r a"
berghofe@23735
    52
  apply (erule accp.cases)
krauss@19564
    53
  apply fast
krauss@19564
    54
  done
krauss@19564
    55
berghofe@23735
    56
lemma not_accp_down:
berghofe@23735
    57
  assumes na: "\<not> accp R x"
berghofe@23735
    58
  obtains z where "R z x" and "\<not> accp R z"
berghofe@22262
    59
proof -
berghofe@23735
    60
  assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
berghofe@22262
    61
berghofe@22262
    62
  show thesis
berghofe@23735
    63
  proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
berghofe@22262
    64
    case True
berghofe@23735
    65
    hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto
berghofe@23735
    66
    hence "accp R x"
berghofe@23735
    67
      by (rule accp.accI)
berghofe@22262
    68
    with na show thesis ..
berghofe@22262
    69
  next
berghofe@23735
    70
    case False then obtain z where "R z x" and "\<not> accp R z"
berghofe@22262
    71
      by auto
berghofe@22262
    72
    with a show thesis .
berghofe@22262
    73
  qed
berghofe@22262
    74
qed
berghofe@22262
    75
berghofe@23735
    76
lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"
berghofe@23735
    77
  apply (erule rtranclp_induct)
krauss@19564
    78
   apply blast
berghofe@23735
    79
  apply (blast dest: accp_downward)
krauss@19564
    80
  done
krauss@19564
    81
berghofe@23735
    82
theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"
berghofe@23735
    83
  apply (blast dest: accp_downwards_aux)
krauss@19564
    84
  done
krauss@19564
    85
berghofe@23735
    86
theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
berghofe@22262
    87
  apply (rule wfPUNIVI)
berghofe@23735
    88
  apply (induct_tac P x rule: accp_induct)
krauss@19564
    89
   apply blast
krauss@19564
    90
  apply blast
krauss@19564
    91
  done
krauss@19564
    92
berghofe@23735
    93
theorem accp_wfPD: "wfP r ==> accp r x"
berghofe@22262
    94
  apply (erule wfP_induct_rule)
berghofe@23735
    95
  apply (rule accp.accI)
krauss@19564
    96
  apply blast
krauss@19564
    97
  done
krauss@19564
    98
berghofe@23735
    99
theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
berghofe@23735
   100
  apply (blast intro: accp_wfPI dest: accp_wfPD)
krauss@19564
   101
  done
krauss@19564
   102
krauss@19564
   103
wenzelm@19669
   104
text {* Smaller relations have bigger accessible parts: *}
wenzelm@19669
   105
berghofe@23735
   106
lemma accp_subset:
berghofe@22262
   107
  assumes sub: "R1 \<le> R2"
berghofe@23735
   108
  shows "accp R2 \<le> accp R1"
krauss@19564
   109
proof
berghofe@23735
   110
  fix x assume "accp R2 x"
berghofe@23735
   111
  then show "accp R1 x"
wenzelm@19669
   112
  proof (induct x)
krauss@19564
   113
    fix x
berghofe@23735
   114
    assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
berghofe@23735
   115
    with sub show "accp R1 x"
berghofe@23735
   116
      by (blast intro: accp.accI)
krauss@19564
   117
  qed
krauss@19564
   118
qed
krauss@19564
   119
krauss@19564
   120
wenzelm@19669
   121
text {* This is a generalized induction theorem that works on
wenzelm@19669
   122
  subsets of the accessible part. *}
krauss@19564
   123
berghofe@23735
   124
lemma accp_subset_induct:
berghofe@23735
   125
  assumes subset: "D \<le> accp R"
berghofe@22262
   126
    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
berghofe@22262
   127
    and "D x"
berghofe@22262
   128
    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
wenzelm@19669
   129
  shows "P x"
krauss@19564
   130
proof -
berghofe@22262
   131
  from subset and `D x`
berghofe@23735
   132
  have "accp R x" ..
berghofe@22262
   133
  then show "P x" using `D x`
krauss@19564
   134
  proof (induct x)
krauss@19564
   135
    fix x
berghofe@22262
   136
    assume "D x"
berghofe@22262
   137
      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
krauss@19564
   138
    with dcl and istep show "P x" by blast
krauss@19564
   139
  qed
krauss@19564
   140
qed
krauss@19564
   141
berghofe@23735
   142
berghofe@23735
   143
text {* Set versions of the above theorems *}
berghofe@23735
   144
berghofe@23735
   145
lemmas acc_induct = accp_induct [to_set]
berghofe@23735
   146
berghofe@23735
   147
lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
berghofe@23735
   148
berghofe@23735
   149
lemmas acc_downward = accp_downward [to_set]
berghofe@23735
   150
berghofe@23735
   151
lemmas not_acc_down = not_accp_down [to_set]
berghofe@23735
   152
berghofe@23735
   153
lemmas acc_downwards_aux = accp_downwards_aux [to_set]
berghofe@23735
   154
berghofe@23735
   155
lemmas acc_downwards = accp_downwards [to_set]
berghofe@23735
   156
berghofe@23735
   157
lemmas acc_wfI = accp_wfPI [to_set]
berghofe@23735
   158
berghofe@23735
   159
lemmas acc_wfD = accp_wfPD [to_set]
berghofe@23735
   160
berghofe@23735
   161
lemmas wf_acc_iff = wfP_accp_iff [to_set]
berghofe@23735
   162
berghofe@23735
   163
lemmas acc_subset = accp_subset [to_set]
berghofe@23735
   164
berghofe@23735
   165
lemmas acc_subset_induct = accp_subset_induct [to_set]
berghofe@23735
   166
krauss@19564
   167
end