author  wenzelm 
Fri, 15 Sep 2000 20:22:00 +0200  
changeset 9998  09bf8fcd1c6e 
parent 9969  4753185f1dd2 
permissions  rwrr 
3193  1 
(* Title: HOL/WF_Rel 
2 
ID: $Id$ 

3 
Author: Konrad Slind 

4 
Copyright 1996 TU Munich 

5 

3296  6 
Derived WF relations: inverse image, lexicographic product, measure, ... 
3193  7 
*) 
8 

9 

10 
(* 

3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

11 
* "Less than" on the natural numbers 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

12 
**) 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

13 

5069  14 
Goalw [less_than_def] "wf less_than"; 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

15 
by (rtac (wf_pred_nat RS wf_trancl) 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

16 
qed "wf_less_than"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

17 
AddIffs [wf_less_than]; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

18 

5069  19 
Goalw [less_than_def] "trans less_than"; 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

20 
by (rtac trans_trancl 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

21 
qed "trans_less_than"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

22 
AddIffs [trans_less_than]; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

23 

5069  24 
Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

25 
by (Simp_tac 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

26 
qed "less_than_iff"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

27 
AddIffs [less_than_iff]; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

28 

9163  29 
Goal "(!!n. (ALL m. Suc m <= n > P m) ==> P n) ==> P n"; 
8254  30 
by (rtac (wf_less_than RS wf_induct) 1); 
8158  31 
by (resolve_tac (premises()) 1); 
32 
by Auto_tac; 

33 
qed_spec_mp "full_nat_induct"; 

34 

3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

35 
(* 
3193  36 
* The inverse image into a wellfounded relation is wellfounded. 
37 
**) 

38 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

39 
Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
4089  40 
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1); 
3718  41 
by (Clarify_tac 1); 
9163  42 
by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1); 
4089  43 
by (blast_tac (claset() delrules [allE]) 2); 
3193  44 
by (etac allE 1); 
45 
by (mp_tac 1); 

46 
by (Blast_tac 1); 

47 
qed "wf_inv_image"; 

48 
AddSIs [wf_inv_image]; 

49 

5069  50 
Goalw [trans_def,inv_image_def] 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

51 
"!!r. trans r ==> trans (inv_image r f)"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

52 
by (Simp_tac 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

53 
by (Blast_tac 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

54 
qed "trans_inv_image"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

55 

4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

56 

3193  57 
(* 
58 
* All measures are wellfounded. 

59 
**) 

60 

5069  61 
Goalw [measure_def] "wf (measure f)"; 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

62 
by (rtac (wf_less_than RS wf_inv_image) 1); 
3193  63 
qed "wf_measure"; 
64 
AddIffs [wf_measure]; 

65 

4643  66 
val measure_induct = standard 
67 
(asm_full_simplify (simpset() addsimps [measure_def,inv_image_def]) 

68 
(wf_measure RS wf_induct)); 

9108  69 
bind_thm ("measure_induct", measure_induct); 
4643  70 

3193  71 
(* 
72 
* Wellfoundedness of lexicographic combinations 

73 
**) 

74 

9422  75 
val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def] 
8703  76 
"[ wf(ra); wf(rb) ] ==> wf(ra <*lex*> rb)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

77 
by (EVERY1 [rtac allI,rtac impI]); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

78 
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); 
3193  79 
by (rtac (wfa RS spec RS mp) 1); 
80 
by (EVERY1 [rtac allI,rtac impI]); 

81 
by (rtac (wfb RS spec RS mp) 1); 

82 
by (Blast_tac 1); 

83 
qed "wf_lex_prod"; 

84 
AddSIs [wf_lex_prod]; 

85 

86 
(* 

87 
* Transitivity of WF combinators. 

88 
**) 

5069  89 
Goalw [trans_def, lex_prod_def] 
8703  90 
"!!R1 R2. [ trans R1; trans R2 ] ==> trans (R1 <*lex*> R2)"; 
3193  91 
by (Simp_tac 1); 
92 
by (Blast_tac 1); 

93 
qed "trans_lex_prod"; 

94 
AddSIs [trans_lex_prod]; 

95 

96 

97 
(* 

98 
* Wellfoundedness of proper subset on finite sets. 

99 
**) 

5069  100 
Goalw [finite_psubset_def] "wf(finite_psubset)"; 
3193  101 
by (rtac (wf_measure RS wf_subset) 1); 
4089  102 
by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def, 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

103 
symmetric less_def])1); 
9076  104 
by (fast_tac (claset() addSEs [psubset_card_mono]) 1); 
3193  105 
qed "wf_finite_psubset"; 
106 

5069  107 
Goalw [finite_psubset_def, trans_def] "trans finite_psubset"; 
4089  108 
by (simp_tac (simpset() addsimps [psubset_def]) 1); 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

109 
by (Blast_tac 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

110 
qed "trans_finite_psubset"; 
3193  111 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

112 
(* 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

113 
* Wellfoundedness of finite acyclic relations 
5144  114 
* Cannot go into WF because it needs Finite. 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

115 
**) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

116 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

117 
Goal "finite r ==> acyclic r > wf r"; 
3457  118 
by (etac finite_induct 1); 
119 
by (Blast_tac 1); 

120 
by (split_all_tac 1); 

121 
by (Asm_full_simp_tac 1); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

122 
qed_spec_mp "finite_acyclic_wf"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

123 

7031  124 
Goal "[finite r; acyclic r] ==> wf (r^1)"; 
125 
by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1); 

126 
by (etac (acyclic_converse RS iffD2) 1); 

127 
qed "finite_acyclic_wf_converse"; 

4749  128 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

129 
Goal "finite r ==> wf r = acyclic r"; 
4089  130 
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

131 
qed "wf_iff_acyclic_if_finite"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

132 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

133 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

134 
(* 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

135 
* A relation is wellfounded iff it has no infinite descending chain 
5144  136 
* Cannot go into WF because it needs type nat. 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

137 
**) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

138 

5069  139 
Goalw [wf_eq_minimal RS eq_reflection] 
9163  140 
"wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))"; 
3457  141 
by (rtac iffI 1); 
142 
by (rtac notI 1); 

143 
by (etac exE 1); 

9163  144 
by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1); 
3457  145 
by (Blast_tac 1); 
146 
by (etac swap 1); 

3446
a14e5451f613
Addition of not_imp (which pushes negation into implication) as a default
paulson
parents:
3436
diff
changeset

147 
by (Asm_full_simp_tac 1); 
3718  148 
by (Clarify_tac 1); 
9163  149 
by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); 
3436
d68dbb8f22d3
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
nipkow
parents:
3413
diff
changeset

150 
by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); 
3457  151 
by (rtac allI 1); 
152 
by (Simp_tac 1); 

9998  153 
by (rtac someI2_ex 1); 
3457  154 
by (Blast_tac 1); 
155 
by (Blast_tac 1); 

156 
by (rtac allI 1); 

157 
by (induct_tac "n" 1); 

158 
by (Asm_simp_tac 1); 

159 
by (Simp_tac 1); 

9998  160 
by (rtac someI2_ex 1); 
3457  161 
by (Blast_tac 1); 
162 
by (Blast_tac 1); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

163 
qed "wf_iff_no_infinite_down_chain"; 
6803  164 

165 
(* 

166 
* Weakly decreasing sequences (w.r.t. some wellfounded order) stabilize. 

167 
**) 

168 

9163  169 
Goal "[ ALL i. (f (Suc i), f i) : r^* ] ==> (f (i+k), f i) : r^*"; 
6803  170 
by (induct_tac "k" 1); 
171 
by (ALLGOALS Simp_tac); 

172 
by (blast_tac (claset() addIs [rtrancl_trans]) 1); 

173 
val lemma = result(); 

174 

9163  175 
Goal "[ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ] \ 
176 
\ ==> ALL m. f m = x > (EX i. ALL k. f (m+i+k) = f (m+i))"; 

6803  177 
by (etac wf_induct 1); 
178 
by (Clarify_tac 1); 

9163  179 
by (case_tac "EX j. (f (m+j), f m) : r^+" 1); 
6803  180 
by (Clarify_tac 1); 
9163  181 
by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1); 
6803  182 
by (Clarify_tac 1); 
183 
by (res_inst_tac [("x","j+i")] exI 1); 

184 
by (asm_full_simp_tac (simpset() addsimps add_ac) 1); 

185 
by (Blast_tac 1); 

186 
by (res_inst_tac [("x","0")] exI 1); 

187 
by (Clarsimp_tac 1); 

188 
by (dres_inst_tac [("i","m"), ("k","k")] lemma 1); 

9163  189 
by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1); 
6803  190 
val lemma = result(); 
191 

9163  192 
Goal "[ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ] \ 
193 
\ ==> EX i. ALL k. f (i+k) = f i"; 

6803  194 
by (dres_inst_tac [("x","0")] (lemma RS spec) 1); 
195 
by Auto_tac; 

196 
qed "wf_weak_decr_stable"; 

197 

198 
(* special case: <= *) 

199 

200 
Goal "(m, n) : pred_nat^* = (m <= n)"; 

201 
by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 

202 
delsimps [reflcl_trancl]) 1); 

203 
by (arith_tac 1); 

204 
qed "le_eq"; 

205 

9163  206 
Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"; 
6803  207 
by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1); 
208 
by (asm_simp_tac (simpset() addsimps [le_eq]) 1); 

209 
by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1)); 

210 
qed "weak_decr_stable"; 

9443  211 

212 
(* 

213 
* Wellfoundedness of same_fst 

214 
**) 

215 

216 
val prems = goalw thy [same_fst_def] 

217 
"(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)"; 

218 
by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1); 

219 
by(strip_tac 1); 

220 
by(rename_tac "a b" 1); 

221 
by(case_tac "wf(R a)" 1); 

222 
by (eres_inst_tac [("a","b")] wf_induct 1); 

223 
by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]); 

224 
by(Blast_tac 1); 

225 
by(blast_tac (claset() addIs prems) 1); 

226 
qed "wf_same_fstI"; 