55 subsubsection{*Equivalences between @{term wf} and @{term wf_on}*} |
55 subsubsection{*Equivalences between @{term wf} and @{term wf_on}*} |
56 |
56 |
57 lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" |
57 lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" |
58 by (unfold wf_def wf_on_def, force) |
58 by (unfold wf_def wf_on_def, force) |
59 |
59 |
60 lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)"; |
60 lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)" |
61 by (simp add: wf_on_def subset_Int_iff) |
61 by (simp add: wf_on_def subset_Int_iff) |
62 |
62 |
63 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)" |
63 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)" |
64 by (unfold wf_def wf_on_def, fast) |
64 by (unfold wf_def wf_on_def, fast) |
65 |
65 |
103 |
103 |
104 subsubsection{*Well-founded Induction*} |
104 subsubsection{*Well-founded Induction*} |
105 |
105 |
106 text{*Consider the least @{term z} in @{term "domain(r)"} such that |
106 text{*Consider the least @{term z} in @{term "domain(r)"} such that |
107 @{term "P(z)"} does not hold...*} |
107 @{term "P(z)"} does not hold...*} |
108 lemma wf_induct [induct set: wf]: |
108 lemma wf_induct_raw: |
109 "[| wf(r); |
109 "[| wf(r); |
110 !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |] |
110 !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |] |
111 ==> P(a)" |
111 ==> P(a)" |
112 apply (unfold wf_def) |
112 apply (unfold wf_def) |
113 apply (erule_tac x = "{z \<in> domain(r). ~ P(z)}" in allE) |
113 apply (erule_tac x = "{z \<in> domain(r). ~ P(z)}" in allE) |
114 apply blast |
114 apply blast |
115 done |
115 done |
116 |
116 |
117 lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf] |
117 lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf] |
118 |
118 |
119 text{*The form of this rule is designed to match @{text wfI}*} |
119 text{*The form of this rule is designed to match @{text wfI}*} |
120 lemma wf_induct2: |
120 lemma wf_induct2: |
121 "[| wf(r); a \<in> A; field(r)<=A; |
121 "[| wf(r); a \<in> A; field(r)<=A; |
122 !!x.[| x \<in> A; \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |] |
122 !!x.[| x \<in> A; \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |] |
126 done |
126 done |
127 |
127 |
128 lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A" |
128 lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A" |
129 by blast |
129 by blast |
130 |
130 |
131 lemma wf_on_induct [consumes 2, induct set: wf_on]: |
131 lemma wf_on_induct_raw [consumes 2, induct set: wf_on]: |
132 "[| wf[A](r); a \<in> A; |
132 "[| wf[A](r); a \<in> A; |
133 !!x.[| x \<in> A; \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |
133 !!x.[| x \<in> A; \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |
134 |] ==> P(a)" |
134 |] ==> P(a)" |
135 apply (unfold wf_on_def) |
135 apply (unfold wf_on_def) |
136 apply (erule wf_induct2, assumption) |
136 apply (erule wf_induct2, assumption) |
137 apply (rule field_Int_square, blast) |
137 apply (rule field_Int_square, blast) |
138 done |
138 done |
139 |
139 |
140 lemmas wf_on_induct_rule = |
140 lemmas wf_on_induct = |
141 wf_on_induct [rule_format, consumes 2, induct set: wf_on] |
141 wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on] |
142 |
142 |
143 |
143 |
144 text{*If @{term r} allows well-founded induction |
144 text{*If @{term r} allows well-founded induction |
145 then we have @{term "wf(r)"}.*} |
145 then we have @{term "wf(r)"}.*} |
146 lemma wfI: |
146 lemma wfI: |
295 apply (rule fun_extension) |
295 apply (rule fun_extension) |
296 apply (blast intro: is_recfun_type) |
296 apply (blast intro: is_recfun_type) |
297 apply (rule lam_type [THEN restrict_type2]) |
297 apply (rule lam_type [THEN restrict_type2]) |
298 apply blast |
298 apply blast |
299 apply (blast dest: transD) |
299 apply (blast dest: transD) |
|
300 apply atomize |
300 apply (frule spec [THEN mp], assumption) |
301 apply (frule spec [THEN mp], assumption) |
301 apply (subgoal_tac "<xa,a1> \<in> r") |
302 apply (subgoal_tac "<xa,a1> \<in> r") |
302 apply (drule_tac x1 = xa in spec [THEN mp], assumption) |
303 apply (drule_tac x1 = xa in spec [THEN mp], assumption) |
303 apply (simp add: vimage_singleton_iff |
304 apply (simp add: vimage_singleton_iff |
304 apply_recfun is_recfun_cut) |
305 apply_recfun is_recfun_cut) |