104 |
104 |
105 lemma measure_induct: |
105 lemma measure_induct: |
106 fixes f :: "'a \<Rightarrow> nat" |
106 fixes f :: "'a \<Rightarrow> nat" |
107 shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a" |
107 shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a" |
108 by (rule measure_induct_rule [of f P a]) iprover |
108 by (rule measure_induct_rule [of f P a]) iprover |
|
109 |
|
110 (* Should go into Finite_Set, but needs measure. |
|
111 Maybe move Wf_Rel before Finite_Set and finite_psubset to Finite_set? |
|
112 *) |
|
113 lemma (in linorder) |
|
114 finite_linorder_induct[consumes 1, case_names empty insert]: |
|
115 "finite A \<Longrightarrow> P {} \<Longrightarrow> |
|
116 (!!A b. finite A \<Longrightarrow> ALL a:A. a \<^loc>< b \<Longrightarrow> P A \<Longrightarrow> P(insert b A)) |
|
117 \<Longrightarrow> P A" |
|
118 proof (induct A rule: measure_induct[where f=card]) |
|
119 fix A :: "'a set" |
|
120 assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow> |
|
121 (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a\<^loc><b) \<longrightarrow> P A \<longrightarrow> P (insert b A)) |
|
122 \<longrightarrow> P B" |
|
123 and "finite A" and "P {}" |
|
124 and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a \<^loc>< b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" |
|
125 show "P A" |
|
126 proof cases |
|
127 assume "A = {}" thus "P A" using `P {}` by simp |
|
128 next |
|
129 let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B" |
|
130 assume "A \<noteq> {}" |
|
131 with `finite A` have "Max A : A" by auto |
|
132 hence A: "?A = A" using insert_Diff_single insert_absorb by auto |
|
133 note card_Diff1_less[OF `finite A` `Max A : A`] |
|
134 moreover have "finite ?B" using `finite A` by simp |
|
135 ultimately have "P ?B" using `P {}` step IH by blast |
|
136 moreover have "\<forall>a\<in>?B. a \<^loc>< Max A" |
|
137 using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp |
|
138 ultimately show "P A" |
|
139 using A insert_Diff_single step[OF `finite ?B`] by fastsimp |
|
140 qed |
|
141 qed |
109 |
142 |
110 |
143 |
111 subsection{*Other Ways of Constructing Wellfounded Relations*} |
144 subsection{*Other Ways of Constructing Wellfounded Relations*} |
112 |
145 |
113 text{*Wellfoundedness of lexicographic combinations*} |
146 text{*Wellfoundedness of lexicographic combinations*} |