author  paulson 
Fri, 20 Aug 2004 12:20:09 +0200  
changeset 15150  c7af682b9ee5 
parent 14240  d3843feb9de7 
child 15171  e0cd537c4325 
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) 

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

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??*) 

108 
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) 

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 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

206 
prefer leaving more finegrain control to the user. *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

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

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

209 
mapfilter ((fn (r,x) => if x = i then Some r else None)); 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

210 

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

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

212 
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

213 
 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

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

215 
[((standard o ObjectLogic.rulify_no_asm) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

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

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

218 
We should probably print something out so that the user knows...? *) 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

219 
handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; 
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 = 
c7af682b9ee5
fix to eliminate excessive casesplits in the recursion equations, by Luca Dixon
paulson
parents:
14240
diff
changeset

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

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

228 
flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) 
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 

11632  240 
in (thy, simplify_defn strict thy cs ss congs wfs fid pats def) end; 
10769  241 

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

10769  244 
handle U.ERR {mesg,...} => error mesg; 
245 

246 

247 
(* 

248 
* 

249 
* Definitions with synthesized termination relation 

250 
* 

251 
**) 

252 

253 
fun func_of_cond_eqn tm = 

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

255 

256 
fun defer_i thy congs fid eqs = 

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

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

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

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

261 
val induction = Prim.mk_induction theory 

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

263 
in (theory, 

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

265 
with assumptions remaining to discharge*) 

266 
standard (induction RS (rules RS conjI))) 

267 
end 

268 

269 
fun defer thy congs fid seqs = 

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

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

272 
end; 

273 

274 
end; 