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
     1 (*  Title:      HOL/Accessible_Part.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 *)
     6 
     7 header {* The accessible part of a relation *}
     8 
     9 theory Accessible_Part
    10 imports Wellfounded_Recursion
    11 begin
    12 
    13 subsection {* Inductive definition *}
    14 
    15 text {*
    16  Inductive definition of the accessible part @{term "acc r"} of a
    17  relation; see also \cite{paulin-tlca}.
    18 *}
    19 
    20 inductive2
    21   acc :: "('a => 'a => bool) => 'a => bool"
    22   for r :: "'a => 'a => bool"
    23   where
    24     accI: "(!!y. r y x ==> acc r y) ==> acc r x"
    25 
    26 abbreviation
    27   termi :: "('a => 'a => bool) => 'a => bool" where
    28   "termi r == acc (r\<inverse>\<inverse>)"
    29 
    30 
    31 subsection {* Induction rules *}
    32 
    33 theorem acc_induct:
    34   assumes major: "acc r a"
    35   assumes hyp: "!!x. acc r x ==> \<forall>y. r y x --> P y ==> P x"
    36   shows "P a"
    37   apply (rule major [THEN acc.induct])
    38   apply (rule hyp)
    39    apply (rule accI)
    40    apply fast
    41   apply fast
    42   done
    43 
    44 theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
    45 
    46 theorem acc_downward: "acc r b ==> r a b ==> acc r a"
    47   apply (erule acc.cases)
    48   apply fast
    49   done
    50 
    51 lemma not_acc_down:
    52   assumes na: "\<not> acc R x"
    53   obtains z where "R z x" and "\<not> acc R z"
    54 proof -
    55   assume a: "\<And>z. \<lbrakk>R z x; \<not> acc R z\<rbrakk> \<Longrightarrow> thesis"
    56 
    57   show thesis
    58   proof (cases "\<forall>z. R z x \<longrightarrow> acc R z")
    59     case True
    60     hence "\<And>z. R z x \<Longrightarrow> acc R z" by auto
    61     hence "acc R x"
    62       by (rule accI)
    63     with na show thesis ..
    64   next
    65     case False then obtain z where "R z x" and "\<not> acc R z"
    66       by auto
    67     with a show thesis .
    68   qed
    69 qed
    70 
    71 lemma acc_downwards_aux: "r\<^sup>*\<^sup>* b a ==> acc r a --> acc r b"
    72   apply (erule rtrancl_induct')
    73    apply blast
    74   apply (blast dest: acc_downward)
    75   done
    76 
    77 theorem acc_downwards: "acc r a ==> r\<^sup>*\<^sup>* b a ==> acc r b"
    78   apply (blast dest: acc_downwards_aux)
    79   done
    80 
    81 theorem acc_wfI: "\<forall>x. acc r x ==> wfP r"
    82   apply (rule wfPUNIVI)
    83   apply (induct_tac P x rule: acc_induct)
    84    apply blast
    85   apply blast
    86   done
    87 
    88 theorem acc_wfD: "wfP r ==> acc r x"
    89   apply (erule wfP_induct_rule)
    90   apply (rule accI)
    91   apply blast
    92   done
    93 
    94 theorem wf_acc_iff: "wfP r = (\<forall>x. acc r x)"
    95   apply (blast intro: acc_wfI dest: acc_wfD)
    96   done
    97 
    98 
    99 text {* Smaller relations have bigger accessible parts: *}
   100 
   101 lemma acc_subset:
   102   assumes sub: "R1 \<le> R2"
   103   shows "acc R2 \<le> acc R1"
   104 proof
   105   fix x assume "acc R2 x"
   106   then show "acc R1 x"
   107   proof (induct x)
   108     fix x
   109     assume ih: "\<And>y. R2 y x \<Longrightarrow> acc R1 y"
   110     with sub show "acc R1 x"
   111       by (blast intro: accI)
   112   qed
   113 qed
   114 
   115 
   116 text {* This is a generalized induction theorem that works on
   117   subsets of the accessible part. *}
   118 
   119 lemma acc_subset_induct:
   120   assumes subset: "D \<le> acc R"
   121     and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
   122     and "D x"
   123     and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   124   shows "P x"
   125 proof -
   126   from subset and `D x`
   127   have "acc R x" ..
   128   then show "P x" using `D x`
   129   proof (induct x)
   130     fix x
   131     assume "D x"
   132       and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   133     with dcl and istep show "P x" by blast
   134   qed
   135 qed
   136 
   137 end