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