author  nipkow 
Mon, 23 May 2005 11:14:58 +0200  
changeset 16042  8e15ff79851a 
parent 15574  b1d1b5bfc464 
child 16287  7a03b4b4df67 
permissions  rwrr 
10769  1 
(* Title: TFL/post.ML 
2 
ID: $Id$ 

3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
Second part of main module (postprocessing of TFL definitions). 

7 
*) 

8 

9 
signature TFL = 

10 
sig 

11 
val trace: bool ref 

12 
val quiet_mode: bool ref 

13 
val message: string > unit 

14 
val tgoalw: theory > thm list > thm list > thm list 

15 
val tgoal: theory > thm list > thm list 

11632  16 
val define_i: bool > theory > claset > simpset > thm list > thm list > xstring > 
10769  17 
term > term list > theory * {rules: (thm * int) list, induct: thm, tcs: term list} 
11632  18 
val define: bool > theory > claset > simpset > thm list > thm list > xstring > 
10769  19 
string > string list > theory * {rules: (thm * int) list, induct: thm, tcs: term list} 
20 
val defer_i: theory > thm list > xstring > term list > theory * thm 

21 
val defer: theory > thm list > xstring > string list > theory * thm 

22 
end; 

23 

24 
structure Tfl: TFL = 

25 
struct 

26 

27 
structure S = USyntax 

28 

29 

30 
(* messages *) 

31 

32 
val trace = Prim.trace 

33 

34 
val quiet_mode = ref false; 

35 
fun message s = if ! quiet_mode then () else writeln s; 

36 

37 

38 
(* misc *) 

39 

12341  40 
val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of); 
10769  41 

42 

43 
(* 

44 
* Extract termination goals so that they can be put it into a goalstack, or 

45 
* have a tactic directly applied to them. 

46 
**) 

47 
fun termination_goals rules = 

48 
map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

49 
(foldr (fn (th,A) => union_term (prems_of th, A)) [] rules); 
10769  50 

51 
(* 

52 
* Finds the termination conditions in (highly massaged) definition and 

53 
* puts them into a goalstack. 

54 
**) 

55 
fun tgoalw thy defs rules = 

56 
case termination_goals rules of 

57 
[] => error "tgoalw: no termination conditions to prove" 

58 
 L => goalw_cterm defs 

59 
(Thm.cterm_of (Theory.sign_of thy) 

60 
(HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); 

61 

62 
fun tgoal thy = tgoalw thy []; 

63 

64 
(* 

65 
* Three postprocessors are applied to the definition. It 

66 
* attempts to prove wellfoundedness of the given relation, simplifies the 

67 
* nonproved termination conditions, and finally attempts to prove the 

68 
* simplified termination conditions. 

69 
**) 

11632  70 
fun std_postprocessor strict cs ss wfs = 
71 
Prim.postprocess strict 

10769  72 
{wf_tac = REPEAT (ares_tac wfs 1), 
73 
terminator = asm_simp_tac ss 1 

13501  74 
THEN TRY (silent_arith_tac 1 ORELSE 
12488  75 
fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), 
10769  76 
simplifier = Rules.simpl_conv ss []}; 
77 

78 

79 

80 
val concl = #2 o Rules.dest_thm; 

81 

82 
(* 

83 
* Postprocess a definition made by "define". This is a separate stage of 

84 
* processing from the definition stage. 

85 
**) 

86 
local 

87 
structure R = Rules 

88 
structure U = Utils 

89 

90 
(* The rest of these local definitions are for the tricky nested case *) 

91 
val solved = not o can S.dest_eq o #2 o S.strip_forall o concl 

92 

93 
fun id_thm th = 

94 
let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); 

95 
in lhs aconv rhs end 

96 
handle U.ERR _ => false; 

97 

98 

99 
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); 

100 
val P_imp_P_iff_True = prover "P > (P= True)" RS mp; 

101 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

102 
fun mk_meta_eq r = case concl_of r of 

103 
Const("==",_)$_$_ => r 

104 
 _ $(Const("op =",_)$_$_) => r RS eq_reflection 

105 
 _ => r RS P_imp_P_eq_True 

106 

107 
(*Is this the best way to invoke the simplifier??*) 

15570  108 
fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L)) 
10769  109 

110 
fun join_assums th = 

111 
let val {sign,...} = rep_thm th 

112 
val tych = cterm_of sign 

113 
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) 

114 
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) 

115 
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) 

116 
val cntxt = gen_union (op aconv) (cntxtl, cntxtr) 

117 
in 

118 
R.GEN_ALL 

119 
(R.DISCH_ALL 

120 
(rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) 

121 
end 

122 
val gen_all = S.gen_all 

123 
in 

11632  124 
fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = 
10769  125 
let 
126 
val _ = message "Proving induction theorem ..." 

127 
val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} 

128 
val _ = message "Postprocessing ..."; 

129 
val {rules, induction, nested_tcs} = 

11632  130 
std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} 
10769  131 
in 
132 
case nested_tcs 

133 
of [] => {induction=induction, rules=rules,tcs=[]} 

134 
 L => let val dummy = message "Simplifying nested TCs ..." 

135 
val (solved,simplified,stubborn) = 

136 
U.itlist (fn th => fn (So,Si,St) => 

137 
if (id_thm th) then (So, Si, th::St) else 

138 
if (solved th) then (th::So, Si, St) 

139 
else (So, th::Si, St)) nested_tcs ([],[],[]) 

140 
val simplified' = map join_assums simplified 

14240  141 
val dummy = (Prim.trace_thms "solved =" solved; 
142 
Prim.trace_thms "simplified' =" simplified') 

10769  143 
val rewr = full_simplify (ss addsimps (solved @ simplified')); 
14240  144 
val dummy = Prim.trace_thms "Simplifying the induction rule..." 
145 
[induction] 

10769  146 
val induction' = rewr induction 
14240  147 
val dummy = Prim.trace_thms "Simplifying the recursion rules..." 
148 
[rules] 

149 
val rules' = rewr rules 

150 
val _ = message "... Postprocessing finished"; 

10769  151 
in 
152 
{induction = induction', 

153 
rules = rules', 

154 
tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) 

155 
(simplified@stubborn)} 

156 
end 

157 
end; 

158 

159 

160 
(*lcp: curry the predicate of the induction rule*) 

11038  161 
fun curry_rule rl = 
162 
SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl); 

10769  163 

164 
(*lcp: put a theorem into Isabelle form, using metalevel connectives*) 

165 
val meta_outer = 

11038  166 
curry_rule o standard o 
167 
rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); 

10769  168 

169 
(*Strip off the outer !P*) 

170 
val spec'= read_instantiate [("x","P::?'b=>bool")] spec; 

171 

14240  172 
fun tracing true _ = () 
173 
 tracing false msg = writeln msg; 

174 

11632  175 
fun simplify_defn strict thy cs ss congs wfs id pats def0 = 
10769  176 
let val def = freezeT def0 RS meta_eq_to_obj_eq 
14240  177 
val {theory,rules,rows,TCs,full_pats_TCs} = 
178 
Prim.post_definition congs (thy, (def,pats)) 

10769  179 
val {lhs=f,rhs} = S.dest_eq (concl def) 
180 
val (_,[R,_]) = S.strip_comb rhs 

14240  181 
val dummy = Prim.trace_thms "congs =" congs 
182 
(*the next step has caused simplifier looping in some cases*) 

10769  183 
val {induction, rules, tcs} = 
11632  184 
proof_stage strict cs ss wfs theory 
10769  185 
{f = f, R = R, rules = rules, 
186 
full_pats_TCs = full_pats_TCs, 

187 
TCs = TCs} 

14240  188 
val rules' = map (standard o ObjectLogic.rulify_no_asm) 
189 
(R.CONJUNCTS rules) 

190 
in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')), 

10769  191 
rules = ListPair.zip(rules', rows), 
192 
tcs = (termination_goals rules') @ tcs} 

193 
end 

194 
handle U.ERR {mesg,func,module} => 

195 
error (mesg ^ 

196 
"\n (In TFL function " ^ module ^ "." ^ func ^ ")"); 

197 

15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

198 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

199 
(* Derive the initial equations from the casesplit rules to meet the 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

200 
users specification of the recursive function. 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

201 
Note: We don't do this if the wf conditions fail to be solved, as each 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

202 
case may have a different wf condition. We could group the conditions 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

203 
together and say that they must be true to solve the general case, 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

204 
but that would hide from the user which subcase they were related 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

205 
to. Probably this is not important, and it would work fine, but, for now, I 
15171
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

206 
prefer leaving more finegrain control to the user. 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

207 
 Lucas Dixon, Aug 2004 *) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

208 
local 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

209 
fun get_related_thms i = 
15570  210 
List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE)); 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

211 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

212 
fun solve_eq (th, [], i) = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

213 
raise ERROR_MESSAGE "derive_init_eqs: missing rules" 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

214 
 solve_eq (th, [a], i) = [(a, i)] 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

215 
 solve_eq (th, splitths as (_ :: _), i) = 
15171
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

216 
(writeln "Proving unsplit equation..."; 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

217 
[((standard o ObjectLogic.rulify_no_asm) 
15171
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

218 
(CaseSplit.splitto splitths th), i)]) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

219 
(* if there's an error, pretend nothing happened with this definition 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

220 
We should probably print something out so that the user knows...? *) 
15171
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

221 
handle ERROR_MESSAGE s => 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

222 
(writeln ("WARNING:post.ML:solve_eq: " ^ s); map (fn x => (x,i)) splitths); 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

223 
in 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

224 
fun derive_init_eqs sgn rules eqs = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

225 
let 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

226 
val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

227 
eqs 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

228 
fun countlist l = 
15570  229 
(rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

230 
in 
15570  231 
List.concat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) 
15150
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

232 
(countlist eqths)) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

233 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

234 
end; 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

235 

c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

236 

10769  237 
(* 
238 
* Defining a function with an associated termination relation. 

239 
**) 

11632  240 
fun define_i strict thy cs ss congs wfs fid R eqs = 
10769  241 
let val {functional,pats} = Prim.mk_functional thy eqs 
242 
val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional 

15171
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

243 
val {induct, rules, tcs} = 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

244 
simplify_defn strict thy cs ss congs wfs fid pats def 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

245 
val rules' = 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

246 
if strict then derive_init_eqs (Theory.sign_of thy) rules eqs 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

247 
else rules 
e0cd537c4325
added code to make use of case splitting to prove the specification equations for recursive definitions.
dixon
parents:
15150
diff
changeset

248 
in (thy, {rules = rules', induct = induct, tcs = tcs}) end; 
10769  249 

11632  250 
fun define strict thy cs ss congs wfs fid R seqs = 
251 
define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs) 

10769  252 
handle U.ERR {mesg,...} => error mesg; 
253 

254 

255 
(* 

256 
* 

257 
* Definitions with synthesized termination relation 

258 
* 

259 
**) 

260 

261 
fun func_of_cond_eqn tm = 

262 
#1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm))))))); 

263 

264 
fun defer_i thy congs fid eqs = 

265 
let val {rules,R,theory,full_pats_TCs,SV,...} = 

266 
Prim.lazyR_def thy (Sign.base_name fid) congs eqs 

267 
val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); 

268 
val dummy = message "Proving induction theorem ..."; 

269 
val induction = Prim.mk_induction theory 

270 
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} 

271 
in (theory, 

272 
(*return the conjoined induction rule and recursion equations, 

273 
with assumptions remaining to discharge*) 

274 
standard (induction RS (rules RS conjI))) 

275 
end 

276 

277 
fun defer thy congs fid seqs = 

278 
defer_i thy congs fid (map (read_term thy) seqs) 

279 
handle U.ERR {mesg,...} => error mesg; 

280 
end; 

281 

282 
end; 