equal
deleted
inserted
replaced
70 apply blast |
70 apply blast |
71 done |
71 done |
72 |
72 |
73 |
73 |
74 subsubsection{*Finally, All Measures are Wellfounded.*} |
74 subsubsection{*Finally, All Measures are Wellfounded.*} |
|
75 |
|
76 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)" |
|
77 by (auto simp:measure_def inv_image_def) |
75 |
78 |
76 lemma wf_measure [iff]: "wf (measure f)" |
79 lemma wf_measure [iff]: "wf (measure f)" |
77 apply (unfold measure_def) |
80 apply (unfold measure_def) |
78 apply (rule wf_less_than [THEN wf_inv_image]) |
81 apply (rule wf_less_than [THEN wf_inv_image]) |
79 done |
82 done |
89 case (less x) |
92 case (less x) |
90 show ?case |
93 show ?case |
91 proof (rule step) |
94 proof (rule step) |
92 fix y |
95 fix y |
93 assume "f y < f x" |
96 assume "f y < f x" |
94 then have "(y, x) \<in> measure f" |
97 hence "(y, x) \<in> measure f" by simp |
95 by (simp add: measure_def inv_image_def) |
98 thus "P y" by (rule less) |
96 then show "P y" by (rule less) |
|
97 qed |
99 qed |
98 qed |
100 qed |
99 qed |
101 qed |
100 |
102 |
101 lemma measure_induct: |
103 lemma measure_induct: |