author  obua 
Tue, 13 Sep 2005 17:05:59 +0200  
changeset 17335  7cff05c90a0e 
parent 16975  34ed8d5d4f16 
child 17615  3c5b158be33c 
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 

40 
(* 

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

42 
* have a tactic directly applied to them. 

43 
**) 

44 
fun termination_goals rules = 

16287  45 
map (Type.freeze o HOLogic.dest_Trueprop) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

48 
(* 

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

50 
* puts them into a goalstack. 

51 
**) 

52 
fun tgoalw thy defs rules = 

53 
case termination_goals rules of 

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

55 
 L => goalw_cterm defs 

56 
(Thm.cterm_of (Theory.sign_of thy) 

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

58 

59 
fun tgoal thy = tgoalw thy []; 

60 

61 
(* 

62 
* Three postprocessors are applied to the definition. It 

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

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

65 
* simplified termination conditions. 

66 
**) 

11632  67 
fun std_postprocessor strict cs ss wfs = 
68 
Prim.postprocess strict 

10769  69 
{wf_tac = REPEAT (ares_tac wfs 1), 
70 
terminator = asm_simp_tac ss 1 

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

75 

76 

77 
val concl = #2 o Rules.dest_thm; 

78 

79 
(* 

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

81 
* processing from the definition stage. 

82 
**) 

83 
local 

84 
structure R = Rules 

85 
structure U = Utils 

86 

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

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

89 

90 
fun id_thm th = 

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

92 
in lhs aconv rhs end 

93 
handle U.ERR _ => false; 

94 

95 

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

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

98 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

99 
fun mk_meta_eq r = case concl_of r of 

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

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

102 
 _ => r RS P_imp_P_eq_True 

103 

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

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

107 
fun join_assums th = 

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

109 
val tych = cterm_of sign 

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

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

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

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

114 
in 

115 
R.GEN_ALL 

116 
(R.DISCH_ALL 

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

118 
end 

119 
val gen_all = S.gen_all 

120 
in 

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

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

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

126 
val {rules, induction, nested_tcs} = 

11632  127 
std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} 
10769  128 
in 
129 
case nested_tcs 

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

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

132 
val (solved,simplified,stubborn) = 

16852  133 
fold_rev (fn th => fn (So,Si,St) => 
10769  134 
if (id_thm th) then (So, Si, th::St) else 
135 
if (solved th) then (th::So, Si, St) 

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

137 
val simplified' = map join_assums simplified 

14240  138 
val dummy = (Prim.trace_thms "solved =" solved; 
139 
Prim.trace_thms "simplified' =" simplified') 

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

10769  143 
val induction' = rewr induction 
14240  144 
val dummy = Prim.trace_thms "Simplifying the recursion rules..." 
145 
[rules] 

146 
val rules' = rewr rules 

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

10769  148 
in 
149 
{induction = induction', 

150 
rules = rules', 

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

152 
(simplified@stubborn)} 

153 
end 

154 
end; 

155 

156 

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

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

10769  160 

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

162 
val meta_outer = 

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

10769  165 

166 
(*Strip off the outer !P*) 

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

168 

14240  169 
fun tracing true _ = () 
170 
 tracing false msg = writeln msg; 

171 

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

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

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

10769  180 
val {induction, rules, tcs} = 
11632  181 
proof_stage strict cs ss wfs theory 
10769  182 
{f = f, R = R, rules = rules, 
183 
full_pats_TCs = full_pats_TCs, 

184 
TCs = TCs} 

14240  185 
val rules' = map (standard o ObjectLogic.rulify_no_asm) 
186 
(R.CONJUNCTS rules) 

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

10769  188 
rules = ListPair.zip(rules', rows), 
189 
tcs = (termination_goals rules') @ tcs} 

190 
end 

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

192 
error (mesg ^ 

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

194 

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

195 

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

196 
(* 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

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

198 
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

199 
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

200 
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

201 
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

202 
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

203 
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

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

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

206 
fun get_related_thms i = 
15570  207 
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

208 

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

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

210 
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

211 
 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

212 
 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

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

214 
[((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

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

216 
(* 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

217 
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

218 
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

219 
(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

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

221 
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

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

223 
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

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

225 
fun countlist l = 
15570  226 
(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

227 
in 
15570  228 
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

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

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

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

232 

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

233 

10769  234 
(* 
235 
* Defining a function with an associated termination relation. 

236 
**) 

11632  237 
fun define_i strict thy cs ss congs wfs fid R eqs = 
10769  238 
let val {functional,pats} = Prim.mk_functional thy eqs 
239 
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

240 
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

241 
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

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

243 
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

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

245 
in (thy, {rules = rules', induct = induct, tcs = tcs}) end; 
10769  246 

11632  247 
fun define strict thy cs ss congs wfs fid R seqs = 
16975  248 
define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs) 
10769  249 
handle U.ERR {mesg,...} => error mesg; 
250 

251 

252 
(* 

253 
* 

254 
* Definitions with synthesized termination relation 

255 
* 

256 
**) 

257 

258 
fun func_of_cond_eqn tm = 

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

260 

261 
fun defer_i thy congs fid eqs = 

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

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

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

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

266 
val induction = Prim.mk_induction theory 

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

268 
in (theory, 

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

270 
with assumptions remaining to discharge*) 

271 
standard (induction RS (rules RS conjI))) 

272 
end 

273 

274 
fun defer thy congs fid seqs = 

16975  275 
defer_i thy congs fid (map (Sign.read_term thy) seqs) 
10769  276 
handle U.ERR {mesg,...} => error mesg; 
277 
end; 

278 

279 
end; 