src/HOL/Accessible_Part.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 21404 eb85850d3eb7 child 22262 96ba62dff413 permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
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 *)
7 header {* The accessible part of a relation *}
9 theory Accessible_Part
10 imports Wellfounded_Recursion
11 begin
13 subsection {* Inductive definition *}
15 text {*
16  Inductive definition of the accessible part @{term "acc r"} of a
18 *}
20 consts
21   acc :: "('a \<times> 'a) set => 'a set"
22 inductive "acc r"
23   intros
24     accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
26 abbreviation
27   termi :: "('a \<times> 'a) set => 'a set" where
28   "termi r == acc (r\<inverse>)"
31 subsection {* Induction rules *}
33 theorem acc_induct:
34   assumes major: "a \<in> acc r"
35   assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> 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
44 theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
46 theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
47   apply (erule acc.elims)
48   apply fast
49   done
51 lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
52   apply (erule rtrancl_induct)
53    apply blast
54   apply (blast dest: acc_downward)
55   done
57 theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
58   apply (blast dest: acc_downwards_aux)
59   done
61 theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
62   apply (rule wfUNIVI)
63   apply (induct_tac P x rule: acc_induct)
64    apply blast
65   apply blast
66   done
68 theorem acc_wfD: "wf r ==> x \<in> acc r"
69   apply (erule wf_induct)
70   apply (rule accI)
71   apply blast
72   done
74 theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
75   apply (blast intro: acc_wfI dest: acc_wfD)
76   done
79 text {* Smaller relations have bigger accessible parts: *}
81 lemma acc_subset:
82   assumes sub: "R1 \<subseteq> R2"
83   shows "acc R2 \<subseteq> acc R1"
84 proof
85   fix x assume "x \<in> acc R2"
86   then show "x \<in> acc R1"
87   proof (induct x)
88     fix x
89     assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
90     with sub show "x \<in> acc R1"
91       by (blast intro:accI)
92   qed
93 qed
96 text {* This is a generalized induction theorem that works on
97   subsets of the accessible part. *}
99 lemma acc_subset_induct:
100   assumes subset: "D \<subseteq> acc R"
101     and dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
102     and "x \<in> D"
103     and istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
104   shows "P x"
105 proof -
106   from `x \<in> D` and subset
107   have "x \<in> acc R" ..
108   then show "P x" using `x \<in> D`
109   proof (induct x)
110     fix x
111     assume "x \<in> D"
112       and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
113     with dcl and istep show "P x" by blast
114   qed
115 qed
117 end