author  nipkow 
Thu, 05 Jun 1997 14:39:22 +0200  
changeset 3413  c1f63cc3a768 
parent 3296  2ee6c397003d 
child 3436  d68dbb8f22d3 
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 
open WF_Rel; 

10 

11 

12 
(* 

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

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

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

15 

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

16 
goalw thy [less_than_def] "wf less_than"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

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

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

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

20 

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

21 
goalw thy [less_than_def] "trans less_than"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

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

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

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

25 

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

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

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

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

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

30 

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

31 
(* 
3193  32 
* The inverse image into a wellfounded relation is wellfounded. 
33 
**) 

34 

35 
goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 

36 
by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1); 

37 
by (Step_tac 1); 

38 
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1); 

39 
by (blast_tac (!claset delrules [allE]) 2); 

40 
by (etac allE 1); 

41 
by (mp_tac 1); 

42 
by (Blast_tac 1); 

43 
qed "wf_inv_image"; 

44 
AddSIs [wf_inv_image]; 

45 

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

46 
goalw thy [trans_def,inv_image_def] 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

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

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

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

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

51 

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

52 

3193  53 
(* 
54 
* All measures are wellfounded. 

55 
**) 

56 

57 
goalw thy [measure_def] "wf (measure f)"; 

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

58 
by (rtac (wf_less_than RS wf_inv_image) 1); 
3193  59 
qed "wf_measure"; 
60 
AddIffs [wf_measure]; 

61 

62 
(* 

63 
* Wellfoundedness of lexicographic combinations 

64 
**) 

65 

66 
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] 

67 
"[ wf(ra); wf(rb) ] ==> wf(ra**rb)"; 

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

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

69 
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); 
3193  70 
by (rtac (wfa RS spec RS mp) 1); 
71 
by (EVERY1 [rtac allI,rtac impI]); 

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

73 
by (Blast_tac 1); 

74 
qed "wf_lex_prod"; 

75 
AddSIs [wf_lex_prod]; 

76 

77 
(* 

78 
* Transitivity of WF combinators. 

79 
**) 

80 
goalw thy [trans_def, lex_prod_def] 

81 
"!!R1 R2. [ trans R1; trans R2 ] ==> trans (R1 ** R2)"; 

82 
by (Simp_tac 1); 

83 
by (Blast_tac 1); 

84 
qed "trans_lex_prod"; 

85 
AddSIs [trans_lex_prod]; 

86 

87 

88 
(* 

89 
* Wellfoundedness of proper subset on finite sets. 

90 
**) 

91 
goalw thy [finite_psubset_def] "wf(finite_psubset)"; 

92 
by (rtac (wf_measure RS wf_subset) 1); 

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

93 
by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def, 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

94 
symmetric less_def])1); 
3193  95 
by (fast_tac (!claset addIs [psubset_card]) 1); 
96 
qed "wf_finite_psubset"; 

97 

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

98 
goalw thy [finite_psubset_def, trans_def] "trans finite_psubset"; 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

99 
by (simp_tac (!simpset addsimps [psubset_def]) 1); 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3193
diff
changeset

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

101 
qed "trans_finite_psubset"; 
3193  102 

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

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

104 
* Wellfoundedness of finite acyclic relations 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

105 
* Cannot go into WF because it needs Finite 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

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

107 

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

108 
goal thy "!!r. finite r ==> acyclic r > wf r"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

109 
be finite_induct 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

110 
by(Blast_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

111 
by(split_all_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

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

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

114 

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

115 
goal thy "!!r. finite r ==> wf r = acyclic r"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

116 
by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

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

118 

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

119 

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

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

121 
* A relation is wellfounded iff it has no infinite descending chain 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

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

123 

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

124 
goalw thy [wf_eq_minimal RS eq_reflection] 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

125 
"wf r = (~(? f. !i. (f(Suc i),f i) : r))"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

126 
br iffI 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

127 
br notI 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

128 
be exE 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

129 
by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

130 
by(Blast_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

131 
be swap 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

132 
by(Asm_full_simp_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

133 
be exE 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

134 
be swap 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

135 
br impI 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

136 
be swap 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

137 
be exE 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

138 
by(rename_tac "x" 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

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

140 
"!i. nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i) : Q & \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

141 
\ (nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i),\ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

142 
\ nat_rec x (%i y. @z. z:Q & (z,y):r) i): r" 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

143 
by(Blast_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

144 
br allI 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

145 
by(induct_tac "i" 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

146 
by(Asm_simp_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

147 
by(subgoal_tac "? y. y : Q & (y,x):r" 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

148 
by(Blast_tac 2); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

149 
be exE 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

150 
be selectI 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

151 
by(subgoal_tac "? y.y:Q & (y,nat_rec x (%i y. @z. z:Q & (z,y):r)(Suc i)):r" 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

152 
by(Blast_tac 2); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

153 
by(Asm_full_simp_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

154 
be exE 1; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

155 
(* `be selectI 1' takes a long time; hence the instantiation: *) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

156 
by (eres_inst_tac[("P","%u.u:Q & (u,?v):r")]selectI 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3296
diff
changeset

157 
qed "wf_iff_no_infinite_down_chain"; 