author  paulson 
Tue, 20 May 1997 11:40:28 +0200  
changeset 3237  4da86d44de33 
parent 3193  fafc7e815b70 
child 3296  2ee6c397003d 
permissions  rwrr 
3193  1 
(* Title: HOL/WF_Rel 
2 
ID: $Id$ 

3 
Author: Konrad Slind 

4 
Copyright 1996 TU Munich 

5 

6 
Derived wellfounded relations: inverse image, relational product, measure, ... 

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 
goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)"; 

67 
by (rtac allI 1); 

68 
by (rtac (surjective_pairing RS ssubst) 1); 

69 
by (Blast_tac 1); 

70 
qed "split_all_pair"; 

71 

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

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

74 
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); 

75 
by (rtac (wfa RS spec RS mp) 1); 

76 
by (EVERY1 [rtac allI,rtac impI]); 

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

78 
by (Blast_tac 1); 

79 
qed "wf_lex_prod"; 

80 
AddSIs [wf_lex_prod]; 

81 

82 
(* 

83 
* Wellfoundedness of relational product 

84 
**) 

85 
val [wfa,wfb] = goalw thy [wf_def,rprod_def] 

86 
"[ wf(ra); wf(rb) ] ==> wf(rprod ra rb)"; 

87 
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); 

88 
by (rtac (wfa RS spec RS mp) 1); 

89 
by (EVERY1 [rtac allI,rtac impI]); 

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

91 
by (Blast_tac 1); 

92 
qed "wf_rel_prod"; 

93 
AddSIs [wf_rel_prod]; 

94 

95 

96 
(* 

97 
* Wellfoundedness of subsets 

98 
**) 

99 

100 
goal thy "!!r. [ wf(r); p<=r ] ==> wf(p)"; 

101 
by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); 

102 
by (Fast_tac 1); 

103 
qed "wf_subset"; 

104 

105 
(* 

106 
* Wellfoundedness of the empty relation. 

107 
**) 

108 

109 
goal thy "wf({})"; 

110 
by (simp_tac (!simpset addsimps [wf_def]) 1); 

111 
qed "wf_empty"; 

112 
AddSIs [wf_empty]; 

113 

114 

115 
(* 

116 
* Transitivity of WF combinators. 

117 
**) 

118 
goalw thy [trans_def, lex_prod_def] 

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

120 
by (Simp_tac 1); 

121 
by (Blast_tac 1); 

122 
qed "trans_lex_prod"; 

123 
AddSIs [trans_lex_prod]; 

124 

125 
goalw thy [trans_def, rprod_def] 

126 
"!!R1 R2. [ trans R1; trans R2 ] ==> trans (rprod R1 R2)"; 

127 
by (Simp_tac 1); 

128 
by (Blast_tac 1); 

129 
qed "trans_rprod"; 

130 
AddSIs [trans_rprod]; 

131 

132 

133 
(* 

134 
* Wellfoundedness of proper subset on finite sets. 

135 
**) 

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

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

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

138 
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

139 
symmetric less_def])1); 
3193  140 
by (fast_tac (!claset addIs [psubset_card]) 1); 
141 
qed "wf_finite_psubset"; 

142 

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

143 
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

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

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

146 
qed "trans_finite_psubset"; 
3193  147 