(*  Title:      HOL/Accessible_Part.thy

     ID:         $Id$

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     Copyright   1994  University of Cambridge

 *)

 header {* The accessible part of a relation *}

 theory Accessible_Part

 imports Wellfounded_Recursion

 begin

 subsection {* Inductive definition *}

 text {*

  Inductive definition of the accessible part @{term "acc r"} of a

  relation; see also \cite{paulin-tlca}.

 *}

 inductive_set

   acc :: "('a * 'a) set => 'a set"

   for r :: "('a * 'a) set"

   where

     accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"

 abbreviation

   termip :: "('a => 'a => bool) => 'a => bool" where

   "termip r == accp (r\<inverse>\<inverse>)"

 abbreviation

   termi :: "('a * 'a) set => 'a set" where

   "termi r == acc (r\<inverse>)"

 lemmas accpI = accp.accI

 subsection {* Induction rules *}

 theorem accp_induct:

   assumes major: "accp r a"

   assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"

   shows "P a"

   apply (rule major [THEN accp.induct])

   apply (rule hyp)

    apply (rule accp.accI)

    apply fast

   apply fast

   done

 theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]

 theorem accp_downward: "accp r b ==> r a b ==> accp r a"

   apply (erule accp.cases)

   apply fast

   done

 lemma not_accp_down:

   assumes na: "\<not> accp R x"

   obtains z where "R z x" and "\<not> accp R z"

 proof -

   assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"

   show thesis

   proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")

     case True

     hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto

     hence "accp R x"

       by (rule accp.accI)

     with na show thesis ..

   next

     case False then obtain z where "R z x" and "\<not> accp R z"

       by auto

     with a show thesis .

   qed

 qed

 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"

   apply (erule rtranclp_induct)

    apply blast

   apply (blast dest: accp_downward)

   done

 theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"

   apply (blast dest: accp_downwards_aux)

   done

 theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"

   apply (rule wfPUNIVI)

   apply (induct_tac P x rule: accp_induct)

    apply blast

   apply blast

   done

 theorem accp_wfPD: "wfP r ==> accp r x"

   apply (erule wfP_induct_rule)

   apply (rule accp.accI)

   apply blast

   done

 theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"

   apply (blast intro: accp_wfPI dest: accp_wfPD)

   done

 text {* Smaller relations have bigger accessible parts: *}

 lemma accp_subset:

   assumes sub: "R1 \<le> R2"

   shows "accp R2 \<le> accp R1"

 proof

   fix x assume "accp R2 x"

   then show "accp R1 x"

   proof (induct x)

     fix x

     assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"

     with sub show "accp R1 x"

       by (blast intro: accp.accI)

   qed

 qed

 text {* This is a generalized induction theorem that works on

   subsets of the accessible part. *}

 lemma accp_subset_induct:

   assumes subset: "D \<le> accp R"

     and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"

     and "D x"

     and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"

   shows "P x"

 proof -

   from subset and `D x`

   have "accp R x" ..

   then show "P x" using `D x`

   proof (induct x)

     fix x

     assume "D x"

       and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"

     with dcl and istep show "P x" by blast

   qed

 qed

 text {* Set versions of the above theorems *}

 lemmas acc_induct = accp_induct [to_set]

 lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]

 lemmas acc_downward = accp_downward [to_set]

 lemmas not_acc_down = not_accp_down [to_set]

 lemmas acc_downwards_aux = accp_downwards_aux [to_set]

 lemmas acc_downwards = accp_downwards [to_set]

 lemmas acc_wfI = accp_wfPI [to_set]

 lemmas acc_wfD = accp_wfPD [to_set]

 lemmas wf_acc_iff = wfP_accp_iff [to_set]

 lemmas acc_subset = accp_subset [to_set]

 lemmas acc_subset_induct = accp_subset_induct [to_set]

 end