The accessible part of a relation (from HOL/Induct/Acc);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Accessible_Part.ML	Wed Oct 18 23:28:02 2000 +0200
@@ -0,0 +1,8 @@
+
+val accI = thm "acc.accI";
+val acc_induct = thm "acc_induct";
+val acc_downward = thm "acc_downward";
+val acc_downwards = thm "acc_downwards";
+val acc_wfI = thm "acc_wfI";
+val acc_wfD = thm "acc_wfD";
+val wf_acc_iff = thm "wf_acc_iff";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Accessible_Part.thy	Wed Oct 18 23:28:02 2000 +0200
@@ -0,0 +1,83 @@
+(*  Title:      HOL/Library/Accessible_Part.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+*)
+
+header {*
+ \title{The accessible part of a relation}
+ \author{Lawrence C Paulson}
+*}
+
+theory Accessible_Part = Main:
+
+
+subsection {* Inductive definition *}
+
+text {*
+ Inductive definition of the accessible part @{term "acc r"} of a
+ relation; see also \cite{paulin-tlca}.
+*}
+
+consts
+  acc :: "('a \<times> 'a) set => 'a set"
+inductive "acc r"
+  intros
+    accI [rule_format]: "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
+
+syntax
+  termi :: "('a \<times> 'a) set => 'a set"
+translations
+  "termi r" == "acc (r^-1)"
+
+
+subsection {* Induction rules *}
+
+theorem acc_induct [induct set: acc]:
+  "a \<in> acc r ==>
+    (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
+proof -
+  assume major: "a \<in> acc r"
+  assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
+  show ?thesis
+    apply (rule major [THEN acc.induct])
+    apply (rule hyp)
+     apply (rule accI)
+     apply fast
+    apply fast
+    done
+qed
+
+theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
+  apply (erule acc.elims)
+  apply fast
+  done
+
+lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
+  apply (erule rtrancl_induct)
+   apply blast
+  apply (blast dest: acc_downward)
+  done
+
+theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r^* ==> b \<in> acc r"
+  apply (blast dest: acc_downwards_aux)
+  done
+
+theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
+  apply (rule wfUNIVI)
+  apply (induct_tac P x rule: acc_induct)
+   apply blast
+  apply blast
+  done
+
+theorem acc_wfD: "wf r ==> x \<in> acc r"
+  apply (erule wf_induct)
+  apply (rule accI)
+  apply blast
+  done
+
+theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
+  apply (blast intro: acc_wfI dest: acc_wfD)
+  done
+
+end