src/HOL/Accessible_Part.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22262 96ba62dff413
child 23735 afc12f93f64f
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
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@22262
    20
inductive2
berghofe@22262
    21
  acc :: "('a => 'a => bool) => 'a => bool"
berghofe@22262
    22
  for r :: "'a => 'a => bool"
berghofe@22262
    23
  where
berghofe@22262
    24
    accI: "(!!y. r y x ==> acc r y) ==> acc r x"
krauss@19564
    25
krauss@19564
    26
abbreviation
berghofe@22262
    27
  termi :: "('a => 'a => bool) => 'a => bool" where
berghofe@22262
    28
  "termi r == acc (r\<inverse>\<inverse>)"
krauss@19564
    29
krauss@19564
    30
krauss@19564
    31
subsection {* Induction rules *}
krauss@19564
    32
krauss@19564
    33
theorem acc_induct:
berghofe@22262
    34
  assumes major: "acc r a"
berghofe@22262
    35
  assumes hyp: "!!x. acc r x ==> \<forall>y. r y x --> 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
berghofe@22262
    46
theorem acc_downward: "acc r b ==> r a b ==> acc r a"
berghofe@22262
    47
  apply (erule acc.cases)
krauss@19564
    48
  apply fast
krauss@19564
    49
  done
krauss@19564
    50
berghofe@22262
    51
lemma not_acc_down:
berghofe@22262
    52
  assumes na: "\<not> acc R x"
berghofe@22262
    53
  obtains z where "R z x" and "\<not> acc R z"
berghofe@22262
    54
proof -
berghofe@22262
    55
  assume a: "\<And>z. \<lbrakk>R z x; \<not> acc R z\<rbrakk> \<Longrightarrow> thesis"
berghofe@22262
    56
berghofe@22262
    57
  show thesis
berghofe@22262
    58
  proof (cases "\<forall>z. R z x \<longrightarrow> acc R z")
berghofe@22262
    59
    case True
berghofe@22262
    60
    hence "\<And>z. R z x \<Longrightarrow> acc R z" by auto
berghofe@22262
    61
    hence "acc R x"
berghofe@22262
    62
      by (rule accI)
berghofe@22262
    63
    with na show thesis ..
berghofe@22262
    64
  next
berghofe@22262
    65
    case False then obtain z where "R z x" and "\<not> acc R z"
berghofe@22262
    66
      by auto
berghofe@22262
    67
    with a show thesis .
berghofe@22262
    68
  qed
berghofe@22262
    69
qed
berghofe@22262
    70
berghofe@22262
    71
lemma acc_downwards_aux: "r\<^sup>*\<^sup>* b a ==> acc r a --> acc r b"
berghofe@22262
    72
  apply (erule rtrancl_induct')
krauss@19564
    73
   apply blast
krauss@19564
    74
  apply (blast dest: acc_downward)
krauss@19564
    75
  done
krauss@19564
    76
berghofe@22262
    77
theorem acc_downwards: "acc r a ==> r\<^sup>*\<^sup>* b a ==> acc r b"
krauss@19564
    78
  apply (blast dest: acc_downwards_aux)
krauss@19564
    79
  done
krauss@19564
    80
berghofe@22262
    81
theorem acc_wfI: "\<forall>x. acc r x ==> wfP r"
berghofe@22262
    82
  apply (rule wfPUNIVI)
krauss@19564
    83
  apply (induct_tac P x rule: acc_induct)
krauss@19564
    84
   apply blast
krauss@19564
    85
  apply blast
krauss@19564
    86
  done
krauss@19564
    87
berghofe@22262
    88
theorem acc_wfD: "wfP r ==> acc r x"
berghofe@22262
    89
  apply (erule wfP_induct_rule)
krauss@19564
    90
  apply (rule accI)
krauss@19564
    91
  apply blast
krauss@19564
    92
  done
krauss@19564
    93
berghofe@22262
    94
theorem wf_acc_iff: "wfP r = (\<forall>x. acc r x)"
krauss@19564
    95
  apply (blast intro: acc_wfI dest: acc_wfD)
krauss@19564
    96
  done
krauss@19564
    97
krauss@19564
    98
wenzelm@19669
    99
text {* Smaller relations have bigger accessible parts: *}
wenzelm@19669
   100
krauss@19564
   101
lemma acc_subset:
berghofe@22262
   102
  assumes sub: "R1 \<le> R2"
berghofe@22262
   103
  shows "acc R2 \<le> acc R1"
krauss@19564
   104
proof
berghofe@22262
   105
  fix x assume "acc R2 x"
berghofe@22262
   106
  then show "acc R1 x"
wenzelm@19669
   107
  proof (induct x)
krauss@19564
   108
    fix x
berghofe@22262
   109
    assume ih: "\<And>y. R2 y x \<Longrightarrow> acc R1 y"
berghofe@22262
   110
    with sub show "acc R1 x"
berghofe@22262
   111
      by (blast intro: accI)
krauss@19564
   112
  qed
krauss@19564
   113
qed
krauss@19564
   114
krauss@19564
   115
wenzelm@19669
   116
text {* This is a generalized induction theorem that works on
wenzelm@19669
   117
  subsets of the accessible part. *}
krauss@19564
   118
krauss@19564
   119
lemma acc_subset_induct:
berghofe@22262
   120
  assumes subset: "D \<le> acc R"
berghofe@22262
   121
    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
berghofe@22262
   122
    and "D x"
berghofe@22262
   123
    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
wenzelm@19669
   124
  shows "P x"
krauss@19564
   125
proof -
berghofe@22262
   126
  from subset and `D x`
berghofe@22262
   127
  have "acc R x" ..
berghofe@22262
   128
  then show "P x" using `D x`
krauss@19564
   129
  proof (induct x)
krauss@19564
   130
    fix x
berghofe@22262
   131
    assume "D x"
berghofe@22262
   132
      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
krauss@19564
   133
    with dcl and istep show "P x" by blast
krauss@19564
   134
  qed
krauss@19564
   135
qed
krauss@19564
   136
krauss@19564
   137
end