src/HOL/Wellfounded_Relations.thy
 author krauss Fri Sep 14 22:21:46 2007 +0200 (2007-09-14) changeset 24575 8b5c5eb7df87 parent 22261 9e185f78e7d4 child 24853 aab5798e5a33 permissions -rw-r--r--
added "<*mlex*>" which lexicographically combines a measure function with a relation
1 (*  ID:   \$Id\$
4 *)
8 theory Wellfounded_Relations
9 imports Finite_Set
10 begin
12 text{*Derived WF relations such as inverse image, lexicographic product and
13 measure. The simple relational product, in which @{term "(x',y')"} precedes
14 @{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
15 lexicographic product, and therefore does not need to be defined separately.*}
17 constdefs
18  less_than :: "(nat*nat)set"
19     "less_than == pred_nat^+"
21  measure   :: "('a => nat) => ('a * 'a)set"
22     "measure == inv_image less_than"
24  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
25                (infixr "<*lex*>" 80)
26     "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
28  finite_psubset  :: "('a set * 'a set) set"
29    --{* finite proper subset*}
30     "finite_psubset == {(A,B). A < B & finite B}"
32  same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
33     "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
34    --{*For @{text rec_def} declarations where the first n parameters
35        stay unchanged in the recursive call.
36        See @{text "Library/While_Combinator.thy"} for an application.*}
41 subsection{*Measure Functions make Wellfounded Relations*}
43 subsubsection{*`Less than' on the natural numbers*}
45 lemma wf_less_than [iff]: "wf less_than"
46 by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
48 lemma trans_less_than [iff]: "trans less_than"
49 by (simp add: less_than_def trans_trancl)
51 lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
52 by (simp add: less_than_def less_def)
54 lemma full_nat_induct:
55   assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
56   shows "P n"
57 apply (rule wf_less_than [THEN wf_induct])
58 apply (rule ih, auto)
59 done
61 subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
63 lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
64 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
65 apply clarify
66 apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
67 prefer 2 apply (blast del: allE)
68 apply (erule allE)
69 apply (erule (1) notE impE)
70 apply blast
71 done
73 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
74   by (auto simp:inv_image_def)
76 subsubsection{*Finally, All Measures are Wellfounded.*}
78 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
81 lemma wf_measure [iff]: "wf (measure f)"
82 apply (unfold measure_def)
83 apply (rule wf_less_than [THEN wf_inv_image])
84 done
86 lemma measure_induct_rule [case_names less]:
87   fixes f :: "'a \<Rightarrow> nat"
88   assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
89   shows "P a"
90 proof -
91   have "wf (measure f)" ..
92   then show ?thesis
93   proof induct
94     case (less x)
95     show ?case
96     proof (rule step)
97       fix y
98       assume "f y < f x"
99       hence "(y, x) \<in> measure f" by simp
100       thus "P y" by (rule less)
101     qed
102   qed
103 qed
105 lemma measure_induct:
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"
108   by (rule measure_induct_rule [of f P a]) iprover
111 subsection{*Other Ways of Constructing Wellfounded Relations*}
113 text{*Wellfoundedness of lexicographic combinations*}
114 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
115 apply (unfold wf_def lex_prod_def)
116 apply (rule allI, rule impI)
117 apply (simp (no_asm_use) only: split_paired_All)
118 apply (drule spec, erule mp)
119 apply (rule allI, rule impI)
120 apply (drule spec, erule mp, blast)
121 done
123 lemma in_lex_prod[simp]:
124   "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
125   by (auto simp:lex_prod_def)
127 text {* lexicographic combinations with measure functions *}
129 definition
130   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
131 where
132   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
134 lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
135 unfolding mlex_prod_def
136 by auto
138 lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
139 unfolding mlex_prod_def by simp
141 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
142 unfolding mlex_prod_def by auto
145 text{*Transitivity of WF combinators.*}
146 lemma trans_lex_prod [intro!]:
147     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
148 by (unfold trans_def lex_prod_def, blast)
150 subsubsection{*Wellfoundedness of proper subset on finite sets.*}
151 lemma wf_finite_psubset: "wf(finite_psubset)"
152 apply (unfold finite_psubset_def)
153 apply (rule wf_measure [THEN wf_subset])
154 apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])
155 apply (fast elim!: psubset_card_mono)
156 done
158 lemma trans_finite_psubset: "trans finite_psubset"
159 by (simp add: finite_psubset_def psubset_def trans_def, blast)
162 subsubsection{*Wellfoundedness of finite acyclic relations*}
164 text{*This proof belongs in this theory because it needs Finite.*}
166 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
167 apply (erule finite_induct, blast)
168 apply (simp (no_asm_simp) only: split_tupled_all)
169 apply simp
170 done
172 lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
173 apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
174 apply (erule acyclic_converse [THEN iffD2])
175 done
177 lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
178 by (blast intro: finite_acyclic_wf wf_acyclic)
181 subsubsection{*Wellfoundedness of @{term same_fst}*}
183 lemma same_fstI [intro!]:
184      "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
187 lemma wf_same_fst:
188   assumes prem: "(!!x. P x ==> wf(R x))"
189   shows "wf(same_fst P R)"
190 apply (simp cong del: imp_cong add: wf_def same_fst_def)
191 apply (intro strip)
192 apply (rename_tac a b)
193 apply (case_tac "wf (R a)")
194  apply (erule_tac a = b in wf_induct, blast)
195 apply (blast intro: prem)
196 done
199 subsection{*Weakly decreasing sequences (w.r.t. some well-founded order)
200    stabilize.*}
202 text{*This material does not appear to be used any longer.*}
204 lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
205 apply (induct_tac "k", simp_all)
206 apply (blast intro: rtrancl_trans)
207 done
209 lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]
210       ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
211 apply (erule wf_induct, clarify)
212 apply (case_tac "EX j. (f (m+j), f m) : r^+")
213  apply clarify
214  apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
215   apply clarify
216   apply (rule_tac x = "j+i" in exI)
218 apply (rule_tac x = 0 in exI, clarsimp)
219 apply (drule_tac i = m and k = k in lemma1)
220 apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
221 done
223 lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]
224       ==> EX i. ALL k. f (i+k) = f i"
225 apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
226 done
228 (* special case of the theorem above: <= *)
229 lemma weak_decr_stable:
230      "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
231 apply (rule_tac r = pred_nat in wf_weak_decr_stable)
233 apply (intro wf_trancl wf_pred_nat)
234 done
237 ML
238 {*
239 val less_than_def = thm "less_than_def";
240 val measure_def = thm "measure_def";
241 val lex_prod_def = thm "lex_prod_def";
242 val finite_psubset_def = thm "finite_psubset_def";
244 val wf_less_than = thm "wf_less_than";
245 val trans_less_than = thm "trans_less_than";
246 val less_than_iff = thm "less_than_iff";
247 val full_nat_induct = thm "full_nat_induct";
248 val wf_inv_image = thm "wf_inv_image";
249 val wf_measure = thm "wf_measure";
250 val measure_induct = thm "measure_induct";
251 val wf_lex_prod = thm "wf_lex_prod";
252 val trans_lex_prod = thm "trans_lex_prod";
253 val wf_finite_psubset = thm "wf_finite_psubset";
254 val trans_finite_psubset = thm "trans_finite_psubset";
255 val finite_acyclic_wf = thm "finite_acyclic_wf";
256 val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse";
257 val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite";
258 val wf_weak_decr_stable = thm "wf_weak_decr_stable";
259 val weak_decr_stable = thm "weak_decr_stable";
260 val same_fstI = thm "same_fstI";
261 val wf_same_fst = thm "wf_same_fst";
262 *}
265 end