--- a/src/HOL/Accessible_Part.thy Thu Apr 24 16:53:04 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,167 +0,0 @@
-(* 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