68 lemmas wfP_induct = wf_induct [to_pred] |
68 lemmas wfP_induct = wf_induct [to_pred] |
69 |
69 |
70 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
70 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
71 |
71 |
72 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
72 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
|
73 |
|
74 lemma wf_on_iff_wf: "wf_on A r \<longleftrightarrow> wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}" |
|
75 proof (rule iffI) |
|
76 assume wf: "wf_on A r" |
|
77 show "wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}" |
|
78 unfolding wf_def |
|
79 proof (intro allI impI ballI) |
|
80 fix P x |
|
81 assume IH: "\<forall>x. (\<forall>y. (y, x) \<in> {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A} \<longrightarrow> P y) \<longrightarrow> P x" |
|
82 show "P x" |
|
83 proof (cases "x \<in> A") |
|
84 case True |
|
85 show ?thesis |
|
86 using wf |
|
87 proof (induction x rule: wf_on_induct) |
|
88 case in_set |
|
89 thus ?case |
|
90 using True . |
|
91 next |
|
92 case (less x) |
|
93 thus ?case |
|
94 by (auto intro: IH[rule_format]) |
|
95 qed |
|
96 next |
|
97 case False |
|
98 then show ?thesis |
|
99 by (auto intro: IH[rule_format]) |
|
100 qed |
|
101 qed |
|
102 next |
|
103 assume wf: "wf {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A}" |
|
104 show "wf_on A r" |
|
105 unfolding wf_on_def |
|
106 proof (intro allI impI ballI) |
|
107 fix P x |
|
108 assume IH: "\<forall>x\<in>A. (\<forall>y\<in>A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x" and "x \<in> A" |
|
109 show "P x" |
|
110 using wf \<open>x \<in> A\<close> |
|
111 proof (induction x rule: wf_on_induct) |
|
112 case in_set |
|
113 show ?case |
|
114 by simp |
|
115 next |
|
116 case (less y) |
|
117 hence "\<And>z. (z, y) \<in> r \<Longrightarrow> z \<in> A \<Longrightarrow> P z" |
|
118 by simp |
|
119 thus ?case |
|
120 using IH[rule_format, OF \<open>y \<in> A\<close>] by simp |
|
121 qed |
|
122 qed |
|
123 qed |
73 |
124 |
74 |
125 |
75 subsection \<open>Introduction Rules\<close> |
126 subsection \<open>Introduction Rules\<close> |
76 |
127 |
77 lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r" |
128 lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r" |