author  paulson 
Thu, 01 Oct 1998 18:30:05 +0200  
changeset 5601  b6456ccd9e3e 
parent 5103  866a281a8c2a 
child 5962  0f7375e5e977 
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 

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

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

27 
> theory * (string * Prim.pattern list) 
3191  28 
> {rules:thm list, induct:thm, tcs:term list} 
2112  29 

3191  30 
(* 
31 
val function : theory > term > {theory:theory, eq_ind : thm} 

32 
val lazyR_def: theory > term > {theory:theory, eqns : thm} 

33 
**) 

2112  34 

3191  35 
end; 
36 

37 

38 
structure Tfl: TFL = 

2112  39 
struct 
40 
structure Prim = Prim 

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

41 
structure S = USyntax 
2112  42 

3191  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 = 

3405  48 
map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) 
3191  49 
(foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); 
50 

3405  51 
(* 
52 
* Finds the termination conditions in (highly massaged) definition and 

53 
* puts them into a goalstack. 

54 
**) 

55 
fun tgoalw thy defs rules = 

3497
122e80826c95
Now catches the error of calling tgoalw when there are no goals to prove,
paulson
parents:
3459
diff
changeset

56 
case termination_goals rules of 
122e80826c95
Now catches the error of calling tgoalw when there are no goals to prove,
paulson
parents:
3459
diff
changeset

57 
[] => error "tgoalw: no termination conditions to prove" 
122e80826c95
Now catches the error of calling tgoalw when there are no goals to prove,
paulson
parents:
3459
diff
changeset

58 
 L => goalw_cterm defs 
122e80826c95
Now catches the error of calling tgoalw when there are no goals to prove,
paulson
parents:
3459
diff
changeset

59 
(cterm_of (sign_of thy) 
122e80826c95
Now catches the error of calling tgoalw when there are no goals to prove,
paulson
parents:
3459
diff
changeset

60 
(HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); 
2112  61 

3405  62 
fun tgoal thy = tgoalw thy []; 
2112  63 

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

70 
fun std_postprocessor ss = 

71 
Prim.postprocess 

4805  72 
{WFtac = REPEAT (ares_tac [wf_empty, wf_measure, wf_inv_image, 
73 
wf_lex_prod, wf_less_than, wf_trancl] 1), 

3405  74 
terminator = asm_simp_tac ss 1 
4097  75 
THEN TRY(CLASET' (fn cs => best_tac 
76 
(cs addSDs [not0_implies_Suc] addss ss)) 1), 

3405  77 
simplifier = Rules.simpl_conv ss []}; 
2112  78 

79 

80 

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

81 
val concl = #2 o Rules.dest_thm; 
2112  82 

83 
(* 

3191  84 
* Defining a function with an associated termination relation. 
85 
**) 

3331  86 
fun define_i thy fid R eqs = 
4970  87 
let val dummy = Theory.requires thy "WF_Rel" "recursive function definitions" 
3191  88 
val {functional,pats} = Prim.mk_functional thy eqs 
3405  89 
in (Prim.wfrec_definition0 thy fid R functional, pats) 
3191  90 
end; 
91 

92 
(*lcp's version: takes strings; doesn't return "thm" 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

93 
(whose signature is a draft and therefore useless) *) 
3331  94 
fun define thy fid R eqs = 
3191  95 
let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
3405  96 
in define_i thy fid (read thy R) (map (read thy) eqs) end 
3191  97 
handle Utils.ERR {mesg,...} => error mesg; 
98 

99 
(* 

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

101 
* processing from the definition stage. 

2112  102 
**) 
103 
local 

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

104 
structure R = Rules 
2112  105 
structure U = Utils 
106 

3191  107 
(* The rest of these local definitions are for the tricky nested case *) 
2112  108 
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl 
109 

110 
fun id_thm th = 

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

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

112 
in lhs aconv rhs 
2112  113 
end handle _ => false 
114 

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

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

117 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

118 
fun mk_meta_eq r = case concl_of r of 

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

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

121 
 _ => r RS P_imp_P_eq_True 

3405  122 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

124 
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) 
2112  125 

126 
fun join_assums th = 

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

128 
val tych = cterm_of sign 

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

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

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

132 
val cntxt = gen_union (op aconv) (cntxtl, cntxtr) 
2112  133 
in 
3191  134 
R.GEN_ALL 
135 
(R.DISCH_ALL 

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

2112  137 
end 
138 
val gen_all = S.gen_all 

139 
in 

3405  140 
fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} = 
3271
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

141 
let val dummy = prs "Proving induction theorem.. " 
3191  142 
val ind = Prim.mk_induction theory f R full_pats_TCs 
3405  143 
val dummy = prs "Proved induction theorem.\nPostprocessing.. " 
144 
val {rules, induction, nested_tcs} = 

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

3191  146 
in 
147 
case nested_tcs 

3271
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

148 
of [] => (writeln "Postprocessing done."; 
3191  149 
{induction=induction, rules=rules,tcs=[]}) 
3271
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

150 
 L => let val dummy = prs "Simplifying nested TCs.. " 
2112  151 
val (solved,simplified,stubborn) = 
152 
U.itlist (fn th => fn (So,Si,St) => 

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

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

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

156 
val simplified' = map join_assums simplified 

3572
5ec1589eac1b
Replaced clumsy rewriting by the new function simplify on thms.
nipkow
parents:
3556
diff
changeset

157 
val rewr = full_simplify (ss addsimps (solved @ simplified')); 
3405  158 
val induction' = rewr induction 
159 
and rules' = rewr rules 

3271
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

160 
val dummy = writeln "Postprocessing done." 
2112  161 
in 
162 
{induction = induction', 

163 
rules = rules', 

3191  164 
tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) 
165 
(simplified@stubborn)} 

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

167 
end; 
3191  168 

169 

3302  170 
(*lcp: curry the predicate of the induction rule*) 
5103  171 
fun curry_rule rl = split_rule_var 
3271
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

172 
(head_of (HOLogic.dest_Trueprop (concl_of rl)), 
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

173 
rl); 
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

174 

3191  175 
(*lcp: put a theorem into Isabelle form, using metalevel connectives*) 
176 
val meta_outer = 

3302  177 
curry_rule o standard o 
3271
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

178 
rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI] 
b873969b05d3
Basis library input/output primitives; currying the induction rule;
paulson
parents:
3245
diff
changeset

179 
ORELSE' etac conjE)); 
3191  180 

181 
(*Strip off the outer !P*) 

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

2112  183 

3405  184 
val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; 
2112  185 

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

186 
(*Convert conclusion from = to ==*) 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

187 
val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

188 

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

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

190 
* Install the basic context notions. Others (for nat and list and prod) 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

191 
* have already been added in thry.sml 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

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

193 
val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong]; 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

194 

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

195 
fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = 
3978  196 
let val dummy = deny (id mem (Sign.stamp_names_of (sign_of thy))) 
3208  197 
("Recursive definition " ^ id ^ 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

198 
" would clash with the theory of the same name!") 
3405  199 
val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq 
200 
val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs) 

3191  201 
val {theory,rules,TCs,full_pats_TCs,patterns} = 
3459
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

202 
Prim.post_definition 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

203 
(ss', defaultTflCongs @ eq_reflect_list tflCongs) 
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

204 
(thy, (def,pats)) 
3191  205 
val {lhs=f,rhs} = S.dest_eq(concl def) 
206 
val (_,[R,_]) = S.strip_comb rhs 

207 
val {induction, rules, tcs} = 

3405  208 
proof_stage ss' theory 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

209 
{f = f, R = R, rules = rules, 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

210 
full_pats_TCs = full_pats_TCs, 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

211 
TCs = TCs} 
3191  212 
val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) 
213 
in {induct = meta_outer 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

214 
(normalize_thm [RSspec,RSmp] (induction RS spec')), 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

215 
rules = rules', 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3208
diff
changeset

216 
tcs = (termination_goals rules') @ tcs} 
3191  217 
end 
3391
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3331
diff
changeset

218 
handle Utils.ERR {mesg,func,module} => 
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3331
diff
changeset

219 
error (mesg ^ 
3405  220 
"\n (In TFL function " ^ module ^ "." ^ func ^ ")"); 
2112  221 
end; 
222 

3191  223 
(* 
224 
* 

225 
* Definitions with synthesized termination relation temporarily 

226 
* deleted  it's not clear how to integrate this facility with 

227 
* the Isabelle theory file scheme, which restricts 

228 
* inference at theoryconstruction time. 

229 
* 

2112  230 

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

231 
local structure R = Rules 
2112  232 
in 
233 
fun function theory eqs = 

3208  234 
let val dummy = prs "Making definition.. " 
2112  235 
val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs 
236 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) 

3208  237 
val dummy = prs "Definition made.\n" 
238 
val dummy = prs "Proving induction theorem.. " 

2112  239 
val induction = Prim.mk_induction theory f R full_pats_TCs 
3208  240 
val dummy = prs "Induction theorem proved.\n" 
2112  241 
in {theory = theory, 
242 
eq_ind = standard (induction RS (rules RS conjI))} 

243 
end 

244 
end; 

245 

246 

247 
fun lazyR_def theory eqs = 

248 
let val {rules,theory, ...} = Prim.lazyR_def theory eqs 

249 
in {eqns=rules, theory=theory} 

250 
end 

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

251 
handle e => print_exn e; 
3191  252 
* 
253 
* 

254 
**) 

2112  255 
end; 