author  wenzelm 
Thu, 01 Jul 1999 21:19:45 +0200  
changeset 6874  747f656e04ec 
parent 6554  5be3f13193d7 
child 7262  a05dc63ca29b 
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 
6524  12 
val quiet_mode : bool ref 
13 
val message : string > unit 

2112  14 

3191  15 
val tgoalw : theory > thm list > thm list > thm list 
16 
val tgoal: theory > thm list > thm list 

2112  17 

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

21 

6554  22 
val define_i : theory > string > term > term list 
3405  23 
> theory * Prim.pattern list 
3331  24 

6554  25 
val define : theory > string > string > string list 
3331  26 
> theory * Prim.pattern list 
2112  27 

6554  28 
val defer_i : theory > string 
6498  29 
> thm list (* congruence rules *) 
30 
> term list > theory * thm 

31 

6554  32 
val defer : theory > string 
6498  33 
> thm list 
34 
> string list > theory * thm 

35 

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

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

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

3191  40 
end; 
41 

42 

43 
structure Tfl: TFL = 

2112  44 
struct 
45 
structure Prim = Prim 

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

46 
structure S = USyntax 
2112  47 

6524  48 

49 
(* messages *) 

50 

51 
val quiet_mode = ref false; 

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

53 

6498  54 
val trace = Prim.trace 
55 

56 
(* 

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

58 
* have a tactic directly applied to them. 

59 
**) 

60 
fun termination_goals rules = 

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

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

3191  63 

6498  64 
(* 
65 
* Finds the termination conditions in (highly massaged) definition and 

66 
* puts them into a goalstack. 

67 
**) 

68 
fun tgoalw thy defs rules = 

69 
case termination_goals rules of 

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

71 
 L => goalw_cterm defs 

72 
(Thm.cterm_of (Theory.sign_of thy) 

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

74 

75 
fun tgoal thy = tgoalw thy []; 

76 

77 
(* 

78 
* Three postprocessors are applied to the definition. It 

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

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

81 
* simplified termination conditions. 

3405  82 
**) 
6498  83 
fun std_postprocessor ss = 
84 
Prim.postprocess 

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

86 
wf_measure, wf_inv_image, 

87 
wf_lex_prod, wf_less_than, wf_trancl] 1), 

88 
terminator = asm_simp_tac ss 1 

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

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

91 
simplifier = Rules.simpl_conv ss []}; 

2112  92 

93 

94 

6498  95 
val concl = #2 o Rules.dest_thm; 
2112  96 

6498  97 
(* 
98 
* Defining a function with an associated termination relation. 

99 
**) 

100 
fun define_i thy fid R eqs = 

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

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

103 
end; 

3191  104 

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

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

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

3191  109 

110 
(* 

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

112 
* processing from the definition stage. 

2112  113 
**) 
6498  114 
local 
115 
structure R = Rules 

116 
structure U = Utils 

2112  117 

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

2112  120 

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

123 
in lhs aconv rhs 

124 
end handle _ => false 

2112  125 

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

128 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

129 
fun mk_meta_eq r = case concl_of r of 

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

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

132 
 _ => r RS P_imp_P_eq_True 

3405  133 

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

2112  136 

6498  137 
fun join_assums th = 
138 
let val {sign,...} = rep_thm th 

139 
val tych = cterm_of sign 

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

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

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

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

144 
in 

145 
R.GEN_ALL 

146 
(R.DISCH_ALL 

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

148 
end 

149 
val gen_all = S.gen_all 

150 
in 

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

6524  152 
let val dummy = message "Proving induction theorem ..." 
6498  153 
val ind = Prim.mk_induction theory 
154 
{fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} 

6524  155 
val dummy = (message "Proved induction theorem."; message "Postprocessing ..."); 
6498  156 
val {rules, induction, nested_tcs} = 
157 
std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} 

158 
in 

159 
case nested_tcs 

6524  160 
of [] => (message "Postprocessing done."; 
6498  161 
{induction=induction, rules=rules,tcs=[]}) 
6524  162 
 L => let val dummy = message "Simplifying nested TCs ..." 
6498  163 
val (solved,simplified,stubborn) = 
164 
U.itlist (fn th => fn (So,Si,St) => 

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

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

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

168 
val simplified' = map join_assums simplified 

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

170 
val induction' = rewr induction 

171 
and rules' = rewr rules 

6524  172 
val dummy = message "Postprocessing done." 
6498  173 
in 
174 
{induction = induction', 

175 
rules = rules', 

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

177 
(simplified@stubborn)} 

178 
end 

179 
end; 

3191  180 

181 

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

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

185 
rl); 

3191  186 

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

189 
curry_rule o standard o 

190 
rule_by_tactic (REPEAT 

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

192 
ORELSE' etac conjE))); 

2112  193 

6498  194 
(*Strip off the outer !P*) 
195 
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

196 

6498  197 
val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; 
198 

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

200 
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

201 

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

204 
* have already been added in thry.sml 

205 
**) 

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

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

208 
("Recursive definition " ^ id ^ 

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

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

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

212 
Prim.post_definition (Prim.congs tflCongs) 

213 
(thy, (def,pats)) 

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

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

216 
val ss' = ss addsimps Prim.default_simps 

217 
val {induction, rules, tcs} = 

218 
proof_stage ss' theory 

219 
{f = f, R = R, rules = rules, 

220 
full_pats_TCs = full_pats_TCs, 

221 
TCs = TCs} 

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

223 
in {induct = meta_outer 

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

225 
rules = rules', 

226 
tcs = (termination_goals rules') @ tcs} 

227 
end 

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

229 
error (mesg ^ 

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

2112  231 

3191  232 
(* 
233 
* 

6498  234 
* Definitions with synthesized termination relation 
3191  235 
* 
236 
**) 

6498  237 

238 
local open USyntax 

239 
in 

240 
fun func_of_cond_eqn tm = 

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

242 
end; 

243 

6554  244 
fun defer_i thy fid congs eqs = 
245 
let val {rules,R,theory,full_pats_TCs,SV,...} = 

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

6498  247 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) 
6524  248 
val dummy = (message "Definition made."; message "Proving induction theorem ..."); 
6498  249 
val induction = Prim.mk_induction theory 
250 
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} 

6524  251 
val dummy = message "Induction theorem proved." 
6498  252 
in (theory, 
253 
(*return the conjoined induction rule and recursion equations, 

254 
with assumptions remaining to discharge*) 

255 
standard (induction RS (rules RS conjI))) 

256 
end 

257 

6554  258 
fun defer thy fid congs seqs = 
259 
let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 

260 
in defer_i thy fid congs (map (read thy) seqs) end 

6498  261 
handle Utils.ERR {mesg,...} => error mesg; 
262 

263 
end; 

264 

2112  265 
end; 