author  paulson 
Fri, 23 Apr 1999 12:23:21 +0200  
changeset 6498  1ebbe18fe236 
parent 6476  92d142e58a5b 
child 6524  13410ecfce0b 
permissions  rwrr 
3302  1 
(* Title: TFL/post 
2 
ID: $Id$ 

3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
Postprocessing of TFL definitions 

7 
*) 

8 

3191  9 
signature TFL = 
10 
sig 

2112  11 
structure Prim : TFL_sig 
12 

3191  13 
val tgoalw : theory > thm list > thm list > thm list 
14 
val tgoal: theory > thm list > thm list 

2112  15 

3405  16 
val std_postprocessor : simpset > theory 
2112  17 
> {induction:thm, rules:thm, TCs:term list list} 
18 
> {induction:thm, rules:thm, nested_tcs:thm list} 

19 

3927  20 
val define_i : theory > xstring > term > term list 
3405  21 
> theory * Prim.pattern list 
3331  22 

3927  23 
val define : theory > xstring > string > string list 
3331  24 
> theory * Prim.pattern list 
2112  25 

6498  26 
val function_i : theory > xstring 
27 
> thm list (* congruence rules *) 

28 
> term list > theory * thm 

29 

30 
val function : theory > xstring 

31 
> thm list 

32 
> string list > theory * thm 

33 

3459
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

34 
val simplify_defn : simpset * thm list 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

35 
> theory * (string * Prim.pattern list) 
3191  36 
> {rules:thm list, induct:thm, tcs:term list} 
2112  37 

3191  38 
end; 
39 

40 

41 
structure Tfl: TFL = 

2112  42 
struct 
43 
structure Prim = Prim 

3391
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3331
diff
changeset

44 
structure S = USyntax 
2112  45 

6498  46 
val trace = Prim.trace 
47 

48 
(* 

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

50 
* have a tactic directly applied to them. 

51 
**) 

52 
fun termination_goals rules = 

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

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

3191  55 

6498  56 
(* 
57 
* Finds the termination conditions in (highly massaged) definition and 

58 
* puts them into a goalstack. 

59 
**) 

60 
fun tgoalw thy defs rules = 

61 
case termination_goals rules of 

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

63 
 L => goalw_cterm defs 

64 
(Thm.cterm_of (Theory.sign_of thy) 

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

66 

67 
fun tgoal thy = tgoalw thy []; 

68 

69 
(* 

70 
* Three postprocessors are applied to the definition. It 

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

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

73 
* simplified termination conditions. 

3405  74 
**) 
6498  75 
fun std_postprocessor ss = 
76 
Prim.postprocess 

77 
{WFtac = REPEAT (ares_tac [wf_empty, wf_pred_nat, 

78 
wf_measure, wf_inv_image, 

79 
wf_lex_prod, wf_less_than, wf_trancl] 1), 

80 
terminator = asm_simp_tac ss 1 

81 
THEN TRY(CLASET' (fn cs => best_tac 

82 
(cs addSDs [not0_implies_Suc] addss ss)) 1), 

83 
simplifier = Rules.simpl_conv ss []}; 

2112  84 

85 

86 

6498  87 
val concl = #2 o Rules.dest_thm; 
2112  88 

6498  89 
(* 
90 
* Defining a function with an associated termination relation. 

91 
**) 

92 
fun define_i thy fid R eqs = 

93 
let val {functional,pats} = Prim.mk_functional thy eqs 

94 
in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats) 

95 
end; 

3191  96 

6498  97 
fun define thy fid R eqs = 
98 
let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 

99 
in define_i thy fid (read thy R) (map (read thy) eqs) end 

100 
handle Utils.ERR {mesg,...} => error mesg; 

3191  101 

102 
(* 

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

104 
* processing from the definition stage. 

2112  105 
**) 
6498  106 
local 
107 
structure R = Rules 

108 
structure U = Utils 

2112  109 

6498  110 
(* The rest of these local definitions are for the tricky nested case *) 
111 
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl 

2112  112 

6498  113 
fun id_thm th = 
114 
let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) 

115 
in lhs aconv rhs 

116 
end handle _ => false 

2112  117 

6498  118 
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); 
119 
val P_imp_P_iff_True = prover "P > (P= True)" RS mp; 

120 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

121 
fun mk_meta_eq r = case concl_of r of 

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

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

124 
 _ => r RS P_imp_P_eq_True 

3405  125 

6498  126 
(*Is this the best way to invoke the simplifier??*) 
127 
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) 

2112  128 

6498  129 
fun join_assums th = 
130 
let val {sign,...} = rep_thm th 

131 
val tych = cterm_of sign 

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

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

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

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

136 
in 

137 
R.GEN_ALL 

138 
(R.DISCH_ALL 

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

140 
end 

141 
val gen_all = S.gen_all 

142 
in 

143 
fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} = 

144 
let val dummy = writeln "Proving induction theorem.. " 

145 
val ind = Prim.mk_induction theory 

146 
{fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} 

147 
val dummy = writeln "Proved induction theorem.\nPostprocessing.. " 

148 
val {rules, induction, nested_tcs} = 

149 
std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} 

150 
in 

151 
case nested_tcs 

152 
of [] => (writeln "Postprocessing done."; 

153 
{induction=induction, rules=rules,tcs=[]}) 

154 
 L => let val dummy = writeln "Simplifying nested TCs.. " 

155 
val (solved,simplified,stubborn) = 

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

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

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

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

160 
val simplified' = map join_assums simplified 

161 
val rewr = full_simplify (ss addsimps (solved @ simplified')); 

162 
val induction' = rewr induction 

163 
and rules' = rewr rules 

164 
val dummy = writeln "Postprocessing done." 

165 
in 

166 
{induction = induction', 

167 
rules = rules', 

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

169 
(simplified@stubborn)} 

170 
end 

171 
end; 

3191  172 

173 

6498  174 
(*lcp: curry the predicate of the induction rule*) 
175 
fun curry_rule rl = split_rule_var 

176 
(head_of (HOLogic.dest_Trueprop (concl_of rl)), 

177 
rl); 

3191  178 

6498  179 
(*lcp: put a theorem into Isabelle form, using metalevel connectives*) 
180 
val meta_outer = 

181 
curry_rule o standard o 

182 
rule_by_tactic (REPEAT 

183 
(FIRSTGOAL (resolve_tac [allI, impI, conjI] 

184 
ORELSE' etac conjE))); 

2112  185 

6498  186 
(*Strip off the outer !P*) 
187 
val spec'= read_instantiate [("x","P::?'b=>bool")] spec; 

3459
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

188 

6498  189 
val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; 
190 

191 
(*Convert conclusion from = to ==*) 

192 
val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); 

3459
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

193 

6498  194 
(* 
195 
* Install the basic context notions. Others (for nat and list and prod) 

196 
* have already been added in thry.sml 

197 
**) 

198 
fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = 

199 
let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy))) 

200 
("Recursive definition " ^ id ^ 

201 
" would clash with the theory of the same name!") 

202 
val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq 

203 
val {theory,rules,TCs,full_pats_TCs,patterns} = 

204 
Prim.post_definition (Prim.congs tflCongs) 

205 
(thy, (def,pats)) 

206 
val {lhs=f,rhs} = S.dest_eq(concl def) 

207 
val (_,[R,_]) = S.strip_comb rhs 

208 
val ss' = ss addsimps Prim.default_simps 

209 
val {induction, rules, tcs} = 

210 
proof_stage ss' theory 

211 
{f = f, R = R, rules = rules, 

212 
full_pats_TCs = full_pats_TCs, 

213 
TCs = TCs} 

214 
val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) 

215 
in {induct = meta_outer 

216 
(normalize_thm [RSspec,RSmp] (induction RS spec')), 

217 
rules = rules', 

218 
tcs = (termination_goals rules') @ tcs} 

219 
end 

220 
handle Utils.ERR {mesg,func,module} => 

221 
error (mesg ^ 

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

2112  223 

3191  224 
(* 
225 
* 

6498  226 
* Definitions with synthesized termination relation 
3191  227 
* 
228 
**) 

6498  229 

230 
local open USyntax 

231 
in 

232 
fun func_of_cond_eqn tm = 

233 
#1(strip_comb(#lhs(dest_eq(#2 (strip_forall(#2(strip_imp tm))))))) 

234 
end; 

235 

236 
fun function_i thy fid congs eqs = 

237 
let val dum = Theory.requires thy "WF_Rel" "recursive function definitions" 

238 
val {rules,R,theory,full_pats_TCs,SV,...} = 

239 
Prim.lazyR_def thy fid congs eqs 

240 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) 

241 
val dummy = writeln "Definition made.\nProving induction theorem.. " 

242 
val induction = Prim.mk_induction theory 

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

244 
val dummy = writeln "Induction theorem proved." 

245 
in (theory, 

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

247 
with assumptions remaining to discharge*) 

248 
standard (induction RS (rules RS conjI))) 

249 
end 

250 

251 
fun function thy fid congs seqs = 

252 
let val _ = writeln ("Deferred recursive function " ^ fid) 

253 
fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 

254 
in function_i thy fid congs (map (read thy) seqs) end 

255 
handle Utils.ERR {mesg,...} => error mesg; 

256 

257 
end; 

258 

2112  259 
end; 