author  clasohm 
Wed, 04 Oct 1995 13:10:03 +0100  
changeset 1264  3eb91524b938 
parent 972  e61b058d58d2 
child 1465  5d7a7e439cec 
permissions  rwrr 
923  1 
(* Title: HOL/wf.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1992 University of Cambridge 

5 

6 
For wf.thy. Wellfounded Recursion 

7 
*) 

8 

9 
open WF; 

10 

950  11 
val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); 
923  12 
val H_cong1 = refl RS H_cong; 
13 

14 
(*Restriction to domain A. If r is wellfounded over A then wf(r)*) 

15 
val [prem1,prem2] = goalw WF.thy [wf_def] 

16 
"[ r <= Sigma A (%u.A); \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

17 
\ !!x P. [ ! x. (! y. (y,x) : r > P(y)) > P(x); x:A ] ==> P(x) ] \ 
923  18 
\ ==> wf(r)"; 
19 
by (strip_tac 1); 

20 
by (rtac allE 1); 

21 
by (assume_tac 1); 

22 
by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); 

23 
qed "wfI"; 

24 

25 
val major::prems = goalw WF.thy [wf_def] 

26 
"[ wf(r); \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

27 
\ !!x.[ ! y. (y,x): r > P(y) ] ==> P(x) \ 
923  28 
\ ] ==> P(a)"; 
29 
by (rtac (major RS spec RS mp RS spec) 1); 

30 
by (fast_tac (HOL_cs addEs prems) 1); 

31 
qed "wf_induct"; 

32 

33 
(*Perform induction on i, then prove the wf(r) subgoal using prems. *) 

34 
fun wf_ind_tac a prems i = 

35 
EVERY [res_inst_tac [("a",a)] wf_induct i, 

36 
rename_last_tac a ["1"] (i+1), 

37 
ares_tac prems i]; 

38 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

39 
val prems = goal WF.thy "[ wf(r); (a,x):r; (x,a):r ] ==> P"; 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

40 
by (subgoal_tac "! x. (a,x):r > (x,a):r > P" 1); 
923  41 
by (fast_tac (HOL_cs addIs prems) 1); 
42 
by (wf_ind_tac "a" prems 1); 

43 
by (fast_tac set_cs 1); 

44 
qed "wf_asym"; 

45 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

46 
val prems = goal WF.thy "[ wf(r); (a,a): r ] ==> P"; 
923  47 
by (rtac wf_asym 1); 
48 
by (REPEAT (resolve_tac prems 1)); 

49 
qed "wf_anti_refl"; 

50 

51 
(*transitive closure of a WF relation is WF!*) 

52 
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; 

53 
by (rewtac wf_def); 

54 
by (strip_tac 1); 

55 
(*must retain the universal formula for later use!*) 

56 
by (rtac allE 1 THEN assume_tac 1); 

57 
by (etac mp 1); 

58 
by (res_inst_tac [("a","x")] (prem RS wf_induct) 1); 

59 
by (rtac (impI RS allI) 1); 

60 
by (etac tranclE 1); 

61 
by (fast_tac HOL_cs 1); 

62 
by (fast_tac HOL_cs 1); 

63 
qed "wf_trancl"; 

64 

65 

66 
(** cut **) 

67 

68 
(*This rewrite rule works upon formulae; thus it requires explicit use of 

69 
H_cong to expose the equality*) 

70 
goalw WF.thy [cut_def] 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

71 
"(cut f r x = cut g r x) = (!y. (y,x):r > f(y)=g(y))"; 
1264  72 
by(simp_tac (!simpset addsimps [expand_fun_eq] 
73 
setloop (split_tac [expand_if])) 1); 

923  74 
qed "cut_cut_eq"; 
75 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

76 
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)"; 
1264  77 
by(Asm_simp_tac 1); 
923  78 
qed "cut_apply"; 
79 

80 

81 
(*** is_recfun ***) 

82 

83 
goalw WF.thy [is_recfun_def,cut_def] 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

84 
"!!f. [ is_recfun r a H f; ~(b,a):r ] ==> f(b) = (@z.True)"; 
923  85 
by (etac ssubst 1); 
1264  86 
by(Asm_simp_tac 1); 
923  87 
qed "is_recfun_undef"; 
88 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

89 
(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE 
923  90 
mp amd allE instantiate induction hypotheses*) 
91 
fun indhyp_tac hyps = 

92 
ares_tac (TrueI::hyps) ORELSE' 

93 
(cut_facts_tac hyps THEN' 

94 
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' 

95 
eresolve_tac [transD, mp, allE])); 

96 

97 
(*** NOTE! some simplifications need a different finish_tac!! ***) 

98 
fun indhyp_tac hyps = 

99 
resolve_tac (TrueI::refl::hyps) ORELSE' 

100 
(cut_facts_tac hyps THEN' 

101 
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' 

102 
eresolve_tac [transD, mp, allE])); 

1264  103 
val wf_super_ss = !simpset setsolver indhyp_tac; 
923  104 

105 
val prems = goalw WF.thy [is_recfun_def,cut_def] 

106 
"[ wf(r); trans(r); is_recfun r a H f; is_recfun r b H g ] ==> \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

107 
\ (x,a):r > (x,b):r > f(x)=g(x)"; 
923  108 
by (cut_facts_tac prems 1); 
109 
by (etac wf_induct 1); 

110 
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); 

111 
by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); 

112 
qed "is_recfun_equal_lemma"; 

113 
bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp)); 

114 

115 

116 
val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] 

117 
"[ wf(r); trans(r); \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

118 
\ is_recfun r a H f; is_recfun r b H g; (b,a):r ] ==> \ 
923  119 
\ cut f r b = g"; 
120 
val gundef = recgb RS is_recfun_undef 

121 
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); 

122 
by (cut_facts_tac prems 1); 

123 
by (rtac ext 1); 

124 
by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg] 

125 
setloop (split_tac [expand_if])) 1); 

126 
qed "is_recfun_cut"; 

127 

128 
(*** Main Existence Lemma  Basic Properties of the_recfun ***) 

129 

130 
val prems = goalw WF.thy [the_recfun_def] 

131 
"is_recfun r a H f ==> is_recfun r a H (the_recfun r a H)"; 

132 
by (res_inst_tac [("P", "is_recfun r a H")] selectI 1); 

133 
by (resolve_tac prems 1); 

134 
qed "is_the_recfun"; 

135 

136 
val prems = goal WF.thy 

137 
"[ wf(r); trans(r) ] ==> is_recfun r a H (the_recfun r a H)"; 

138 
by (cut_facts_tac prems 1); 

139 
by (wf_ind_tac "a" prems 1); 

140 
by (res_inst_tac [("f", "cut (%y. wftrec r y H) r a1")] is_the_recfun 1); 

141 
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); 

142 
by (rtac (cut_cut_eq RS ssubst) 1); 

143 
(*Applying the substitution: must keep the quantified assumption!!*) 

144 
by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac, 

145 
etac (mp RS ssubst), atac]); 

146 
by (fold_tac [is_recfun_def]); 

147 
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cut_cut_eq]) 1); 

148 
qed "unfold_the_recfun"; 

149 

150 

151 
(*Beware incompleteness of unification!*) 

152 
val prems = goal WF.thy 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

153 
"[ wf(r); trans(r); (c,a):r; (c,b):r ] \ 
923  154 
\ ==> the_recfun r a H c = the_recfun r b H c"; 
155 
by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1)); 

156 
qed "the_recfun_equal"; 

157 

158 
val prems = goal WF.thy 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

159 
"[ wf(r); trans(r); (b,a):r ] \ 
923  160 
\ ==> cut (the_recfun r a H) r b = the_recfun r b H"; 
161 
by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1)); 

162 
qed "the_recfun_cut"; 

163 

164 
(*** Unfolding wftrec ***) 

165 

166 
goalw WF.thy [wftrec_def] 

167 
"!!r. [ wf(r); trans(r) ] ==> \ 

168 
\ wftrec r a H = H a (cut (%x.wftrec r x H) r a)"; 

169 
by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun), 

170 
REPEAT o atac, rtac H_cong1]); 

1264  171 
by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1); 
923  172 
qed "wftrec"; 
173 

174 
(*Unused but perhaps interesting*) 

175 
val prems = goal WF.thy 

176 
"[ wf(r); trans(r); !!f x. H x (cut f r x) = H x f ] ==> \ 

177 
\ wftrec r a H = H a (%x.wftrec r x H)"; 

178 
by (rtac (wftrec RS trans) 1); 

179 
by (REPEAT (resolve_tac prems 1)); 

180 
qed "wftrec2"; 

181 

182 
(** Removal of the premise trans(r) **) 

183 

184 
goalw WF.thy [wfrec_def] 

185 
"!!r. wf(r) ==> wfrec r a H = H a (cut (%x.wfrec r x H) r a)"; 

186 
by (etac (wf_trancl RS wftrec RS ssubst) 1); 

187 
by (rtac trans_trancl 1); 

188 
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) 

1264  189 
by (simp_tac (!simpset addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1); 
923  190 
qed "wfrec"; 
191 

192 
(*This form avoids giant explosions in proofs. NOTE USE OF == *) 

193 
val rew::prems = goal WF.thy 

194 
"[ !!x. f(x)==wfrec r x H; wf(r) ] ==> f(a) = H a (cut (%x.f(x)) r a)"; 

195 
by (rewtac rew); 

196 
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); 

197 
qed "def_wfrec"; 