author  wenzelm 
Wed, 25 Aug 1999 20:49:02 +0200  
changeset 7357  d0e16da40ea2 
parent 7262  a05dc63ca29b 
child 8526  0be2c98f15a7 
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 

7262  11 

12 
val trace : bool ref 

13 

2112  14 
structure Prim : TFL_sig 
6524  15 
val quiet_mode : bool ref 
16 
val message : string > unit 

2112  17 

3191  18 
val tgoalw : theory > thm list > thm list > thm list 
19 
val tgoal: theory > thm list > thm list 

2112  20 

3405  21 
val std_postprocessor : simpset > theory 
2112  22 
> {induction:thm, rules:thm, TCs:term list list} 
23 
> {induction:thm, rules:thm, nested_tcs:thm list} 

24 

7262  25 
val define_i : theory > xstring > term 
26 
> simpset * thm list (*allows special simplication*) 

27 
> term list 

28 
> theory * {rules:thm list, induct:thm, tcs:term list} 

3331  29 

7262  30 
val define : theory > xstring > string 
31 
> simpset * thm list 

32 
> string list 

33 
> theory * {rules:thm list, induct:thm, tcs:term list} 

2112  34 

7262  35 
val defer_i : theory > xstring 
6498  36 
> thm list (* congruence rules *) 
37 
> term list > theory * thm 

38 

7262  39 
val defer : theory > xstring 
6498  40 
> thm list 
41 
> string list > theory * thm 

42 

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

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

44 
> theory * (string * Prim.pattern list) 
3191  45 
> {rules:thm list, induct:thm, tcs:term list} 
2112  46 

3191  47 
end; 
48 

49 

50 
structure Tfl: TFL = 

2112  51 
struct 
52 
structure Prim = Prim 

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

53 
structure S = USyntax 
2112  54 

6524  55 
(* messages *) 
56 

57 
val quiet_mode = ref false; 

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

59 

6498  60 
val trace = Prim.trace 
61 

62 
(* 

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

64 
* have a tactic directly applied to them. 

65 
**) 

66 
fun termination_goals rules = 

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

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

3191  69 

6498  70 
(* 
71 
* Finds the termination conditions in (highly massaged) definition and 

72 
* puts them into a goalstack. 

73 
**) 

74 
fun tgoalw thy defs rules = 

75 
case termination_goals rules of 

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

77 
 L => goalw_cterm defs 

78 
(Thm.cterm_of (Theory.sign_of thy) 

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

80 

81 
fun tgoal thy = tgoalw thy []; 

82 

83 
(* 

84 
* Three postprocessors are applied to the definition. It 

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

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

87 
* simplified termination conditions. 

3405  88 
**) 
6498  89 
fun std_postprocessor ss = 
90 
Prim.postprocess 

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

92 
wf_measure, wf_inv_image, 

93 
wf_lex_prod, wf_less_than, wf_trancl] 1), 

94 
terminator = asm_simp_tac ss 1 

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

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

97 
simplifier = Rules.simpl_conv ss []}; 

2112  98 

99 

100 

6498  101 
val concl = #2 o Rules.dest_thm; 
2112  102 

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

105 
* processing from the definition stage. 

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

109 
structure U = Utils 

2112  110 

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

2112  113 

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

116 
in lhs aconv rhs 

117 
end handle _ => false 

2112  118 

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

121 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

122 
fun mk_meta_eq r = case concl_of r of 

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

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

125 
 _ => r RS P_imp_P_eq_True 

3405  126 

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

2112  129 

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

132 
val tych = cterm_of sign 

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

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

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

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

137 
in 

138 
R.GEN_ALL 

139 
(R.DISCH_ALL 

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

141 
end 

142 
val gen_all = S.gen_all 

143 
in 

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

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

7262  148 
val dummy = (message "Proved induction theorem."; 
149 
message "Postprocessing ..."); 

6498  150 
val {rules, induction, nested_tcs} = 
151 
std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} 

152 
in 

153 
case nested_tcs 

6524  154 
of [] => (message "Postprocessing done."; 
6498  155 
{induction=induction, rules=rules,tcs=[]}) 
6524  156 
 L => let val dummy = message "Simplifying nested TCs ..." 
6498  157 
val (solved,simplified,stubborn) = 
158 
U.itlist (fn th => fn (So,Si,St) => 

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

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

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

162 
val simplified' = map join_assums simplified 

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

164 
val induction' = rewr induction 

165 
and rules' = rewr rules 

6524  166 
val dummy = message "Postprocessing done." 
6498  167 
in 
168 
{induction = induction', 

169 
rules = rules', 

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

171 
(simplified@stubborn)} 

172 
end 

173 
end; 

3191  174 

175 

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

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

179 
rl); 

3191  180 

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

183 
curry_rule o standard o 

184 
rule_by_tactic (REPEAT 

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

186 
ORELSE' etac conjE))); 

2112  187 

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

190 

7262  191 
(*this function could be combined with define_i lcp*) 
6498  192 
fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = 
193 
let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy))) 

194 
("Recursive definition " ^ id ^ 

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

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

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

198 
Prim.post_definition (Prim.congs tflCongs) 

199 
(thy, (def,pats)) 

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

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

202 
val ss' = ss addsimps Prim.default_simps 

203 
val {induction, rules, tcs} = 

204 
proof_stage ss' theory 

205 
{f = f, R = R, rules = rules, 

206 
full_pats_TCs = full_pats_TCs, 

207 
TCs = TCs} 

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

209 
in {induct = meta_outer 

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

211 
rules = rules', 

212 
tcs = (termination_goals rules') @ tcs} 

213 
end 

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

215 
error (mesg ^ 

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

2112  217 

3191  218 
(* 
7262  219 
* Defining a function with an associated termination relation. 
220 
**) 

221 
fun define_i thy fid R ss_congs eqs = 

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

223 
val thy = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional 

224 
in (thy, simplify_defn ss_congs (thy, (fid, pats))) 

225 
end; 

226 

227 
fun define thy fid R ss_congs seqs = 

228 
let val _ = writeln ("Recursive function " ^ fid) 

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

230 
in define_i thy fid (read R) ss_congs (map read seqs) end 

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

232 

233 

234 
(* 

3191  235 
* 
6498  236 
* Definitions with synthesized termination relation 
3191  237 
* 
238 
**) 

6498  239 

240 
local open USyntax 

241 
in 

242 
fun func_of_cond_eqn tm = 

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

244 
end; 

245 

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

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

6498  249 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) 
7262  250 
val dummy = (message "Definition made."; 
251 
message "Proving induction theorem ..."); 

6498  252 
val induction = Prim.mk_induction theory 
253 
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} 

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

257 
with assumptions remaining to discharge*) 

258 
standard (induction RS (rules RS conjI))) 

259 
end 

260 

6554  261 
fun defer thy fid congs seqs = 
7262  262 
let val read = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
263 
in defer_i thy fid congs (map read seqs) end 

6498  264 
handle Utils.ERR {mesg,...} => error mesg; 
265 
end; 

266 

2112  267 
end; 