author | wenzelm |
Sun, 07 Feb 2010 19:33:34 +0100 | |
changeset 35021 | c839a4c670c6 |
parent 33832 | cff42395c246 |
child 35365 | 2fcd08c62495 |
permissions | -rw-r--r-- |
23150 | 1 |
(* Title: HOL/Tools/TFL/post.ML |
2 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
3 |
Copyright 1997 University of Cambridge |
|
4 |
||
5 |
Second part of main module (postprocessing of TFL definitions). |
|
6 |
*) |
|
7 |
||
8 |
signature TFL = |
|
9 |
sig |
|
10 |
val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
|
11 |
term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} |
|
12 |
val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
|
13 |
string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} |
|
14 |
val defer_i: theory -> thm list -> xstring -> term list -> theory * thm |
|
15 |
val defer: theory -> thm list -> xstring -> string list -> theory * thm |
|
16 |
end; |
|
17 |
||
18 |
structure Tfl: TFL = |
|
19 |
struct |
|
20 |
||
21 |
structure S = USyntax |
|
22 |
||
23 |
(* misc *) |
|
24 |
||
25 |
(*--------------------------------------------------------------------------- |
|
26 |
* Extract termination goals so that they can be put it into a goalstack, or |
|
27 |
* have a tactic directly applied to them. |
|
28 |
*--------------------------------------------------------------------------*) |
|
29 |
fun termination_goals rules = |
|
33832 | 30 |
map (Type.legacy_freeze o HOLogic.dest_Trueprop) |
33339 | 31 |
(fold_rev (union (op aconv) o prems_of) rules []); |
23150 | 32 |
|
33 |
(*--------------------------------------------------------------------------- |
|
34 |
* Three postprocessors are applied to the definition. It |
|
35 |
* attempts to prove wellfoundedness of the given relation, simplifies the |
|
36 |
* non-proved termination conditions, and finally attempts to prove the |
|
37 |
* simplified termination conditions. |
|
38 |
*--------------------------------------------------------------------------*) |
|
39 |
fun std_postprocessor strict cs ss wfs = |
|
40 |
Prim.postprocess strict |
|
41 |
{wf_tac = REPEAT (ares_tac wfs 1), |
|
42 |
terminator = asm_simp_tac ss 1 |
|
30686
47a32dd1b86e
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents:
30364
diff
changeset
|
43 |
THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE |
23880 | 44 |
fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), |
23150 | 45 |
simplifier = Rules.simpl_conv ss []}; |
46 |
||
47 |
||
48 |
||
49 |
val concl = #2 o Rules.dest_thm; |
|
50 |
||
51 |
(*--------------------------------------------------------------------------- |
|
52 |
* Postprocess a definition made by "define". This is a separate stage of |
|
53 |
* processing from the definition stage. |
|
54 |
*---------------------------------------------------------------------------*) |
|
55 |
local |
|
56 |
structure R = Rules |
|
57 |
structure U = Utils |
|
58 |
||
59 |
(* The rest of these local definitions are for the tricky nested case *) |
|
60 |
val solved = not o can S.dest_eq o #2 o S.strip_forall o concl |
|
61 |
||
62 |
fun id_thm th = |
|
63 |
let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); |
|
64 |
in lhs aconv rhs end |
|
65 |
handle U.ERR _ => false; |
|
66 |
||
30737 | 67 |
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; |
23150 | 68 |
fun mk_meta_eq r = case concl_of r of |
69 |
Const("==",_)$_$_ => r |
|
70 |
| _ $(Const("op =",_)$_$_) => r RS eq_reflection |
|
71 |
| _ => r RS P_imp_P_eq_True |
|
72 |
||
73 |
(*Is this the best way to invoke the simplifier??*) |
|
33317 | 74 |
fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) |
23150 | 75 |
|
76 |
fun join_assums th = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26478
diff
changeset
|
77 |
let val thy = Thm.theory_of_thm th |
23150 | 78 |
val tych = cterm_of thy |
79 |
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) |
|
80 |
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) |
|
81 |
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) |
|
33042 | 82 |
val cntxt = union (op aconv) cntxtl cntxtr |
23150 | 83 |
in |
84 |
R.GEN_ALL |
|
85 |
(R.DISCH_ALL |
|
86 |
(rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) |
|
87 |
end |
|
88 |
val gen_all = S.gen_all |
|
89 |
in |
|
90 |
fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = |
|
91 |
let |
|
26478 | 92 |
val _ = writeln "Proving induction theorem ..." |
23150 | 93 |
val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} |
26478 | 94 |
val _ = writeln "Postprocessing ..."; |
23150 | 95 |
val {rules, induction, nested_tcs} = |
96 |
std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} |
|
97 |
in |
|
98 |
case nested_tcs |
|
99 |
of [] => {induction=induction, rules=rules,tcs=[]} |
|
26478 | 100 |
| L => let val dummy = writeln "Simplifying nested TCs ..." |
23150 | 101 |
val (solved,simplified,stubborn) = |
102 |
fold_rev (fn th => fn (So,Si,St) => |
|
103 |
if (id_thm th) then (So, Si, th::St) else |
|
104 |
if (solved th) then (th::So, Si, St) |
|
105 |
else (So, th::Si, St)) nested_tcs ([],[],[]) |
|
106 |
val simplified' = map join_assums simplified |
|
107 |
val dummy = (Prim.trace_thms "solved =" solved; |
|
108 |
Prim.trace_thms "simplified' =" simplified') |
|
109 |
val rewr = full_simplify (ss addsimps (solved @ simplified')); |
|
110 |
val dummy = Prim.trace_thms "Simplifying the induction rule..." |
|
111 |
[induction] |
|
112 |
val induction' = rewr induction |
|
113 |
val dummy = Prim.trace_thms "Simplifying the recursion rules..." |
|
114 |
[rules] |
|
115 |
val rules' = rewr rules |
|
26478 | 116 |
val _ = writeln "... Postprocessing finished"; |
23150 | 117 |
in |
118 |
{induction = induction', |
|
119 |
rules = rules', |
|
120 |
tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) |
|
121 |
(simplified@stubborn)} |
|
122 |
end |
|
123 |
end; |
|
124 |
||
125 |
||
126 |
(*lcp: curry the predicate of the induction rule*) |
|
127 |
fun curry_rule rl = |
|
128 |
SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; |
|
129 |
||
130 |
(*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
|
131 |
val meta_outer = |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset
|
132 |
curry_rule o Drule.export_without_context o |
23150 | 133 |
rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
134 |
||
135 |
(*Strip off the outer !P*) |
|
27239 | 136 |
val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; |
23150 | 137 |
|
138 |
fun tracing true _ = () |
|
139 |
| tracing false msg = writeln msg; |
|
140 |
||
141 |
fun simplify_defn strict thy cs ss congs wfs id pats def0 = |
|
142 |
let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq |
|
143 |
val {rules,rows,TCs,full_pats_TCs} = |
|
144 |
Prim.post_definition congs (thy, (def,pats)) |
|
145 |
val {lhs=f,rhs} = S.dest_eq (concl def) |
|
146 |
val (_,[R,_]) = S.strip_comb rhs |
|
147 |
val dummy = Prim.trace_thms "congs =" congs |
|
148 |
(*the next step has caused simplifier looping in some cases*) |
|
149 |
val {induction, rules, tcs} = |
|
150 |
proof_stage strict cs ss wfs thy |
|
151 |
{f = f, R = R, rules = rules, |
|
152 |
full_pats_TCs = full_pats_TCs, |
|
153 |
TCs = TCs} |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset
|
154 |
val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm) |
23150 | 155 |
(R.CONJUNCTS rules) |
156 |
in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')), |
|
157 |
rules = ListPair.zip(rules', rows), |
|
158 |
tcs = (termination_goals rules') @ tcs} |
|
159 |
end |
|
160 |
handle U.ERR {mesg,func,module} => |
|
161 |
error (mesg ^ |
|
162 |
"\n (In TFL function " ^ module ^ "." ^ func ^ ")"); |
|
163 |
||
164 |
||
165 |
(* Derive the initial equations from the case-split rules to meet the |
|
166 |
users specification of the recursive function. |
|
167 |
Note: We don't do this if the wf conditions fail to be solved, as each |
|
168 |
case may have a different wf condition. We could group the conditions |
|
169 |
together and say that they must be true to solve the general case, |
|
170 |
but that would hide from the user which sub-case they were related |
|
171 |
to. Probably this is not important, and it would work fine, but, for now, I |
|
172 |
prefer leaving more fine-grain control to the user. |
|
173 |
-- Lucas Dixon, Aug 2004 *) |
|
174 |
local |
|
175 |
fun get_related_thms i = |
|
32952 | 176 |
map_filter ((fn (r,x) => if x = i then SOME r else NONE)); |
23150 | 177 |
|
178 |
fun solve_eq (th, [], i) = |
|
179 |
error "derive_init_eqs: missing rules" |
|
180 |
| solve_eq (th, [a], i) = [(a, i)] |
|
181 |
| solve_eq (th, splitths as (_ :: _), i) = |
|
182 |
(writeln "Proving unsplit equation..."; |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset
|
183 |
[((Drule.export_without_context o ObjectLogic.rulify_no_asm) |
23150 | 184 |
(CaseSplit.splitto splitths th), i)]) |
185 |
(* if there's an error, pretend nothing happened with this definition |
|
186 |
We should probably print something out so that the user knows...? *) |
|
187 |
handle ERROR s => |
|
188 |
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths); |
|
189 |
in |
|
190 |
fun derive_init_eqs sgn rules eqs = |
|
191 |
let |
|
33245 | 192 |
val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) eqs |
193 |
fun countlist l = |
|
194 |
rev (snd (fold (fn e => fn (i, L) => (i + 1, (e, i) :: L)) l (0, []))) |
|
23150 | 195 |
in |
33245 | 196 |
maps (fn (e, i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths) |
23150 | 197 |
end; |
198 |
end; |
|
199 |
||
200 |
||
201 |
(*--------------------------------------------------------------------------- |
|
202 |
* Defining a function with an associated termination relation. |
|
203 |
*---------------------------------------------------------------------------*) |
|
204 |
fun define_i strict thy cs ss congs wfs fid R eqs = |
|
205 |
let val {functional,pats} = Prim.mk_functional thy eqs |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
206 |
val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional |
23150 | 207 |
val {induct, rules, tcs} = |
208 |
simplify_defn strict thy cs ss congs wfs fid pats def |
|
209 |
val rules' = |
|
210 |
if strict then derive_init_eqs thy rules eqs |
|
211 |
else rules |
|
212 |
in (thy, {rules = rules', induct = induct, tcs = tcs}) end; |
|
213 |
||
214 |
fun define strict thy cs ss congs wfs fid R seqs = |
|
24707 | 215 |
define_i strict thy cs ss congs wfs fid |
216 |
(Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs) |
|
23150 | 217 |
handle U.ERR {mesg,...} => error mesg; |
218 |
||
219 |
||
220 |
(*--------------------------------------------------------------------------- |
|
221 |
* |
|
222 |
* Definitions with synthesized termination relation |
|
223 |
* |
|
224 |
*---------------------------------------------------------------------------*) |
|
225 |
||
226 |
fun func_of_cond_eqn tm = |
|
227 |
#1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm))))))); |
|
228 |
||
229 |
fun defer_i thy congs fid eqs = |
|
230 |
let val {rules,R,theory,full_pats_TCs,SV,...} = |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
231 |
Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs |
23150 | 232 |
val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); |
26478 | 233 |
val dummy = writeln "Proving induction theorem ..."; |
23150 | 234 |
val induction = Prim.mk_induction theory |
235 |
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} |
|
236 |
in (theory, |
|
237 |
(*return the conjoined induction rule and recursion equations, |
|
238 |
with assumptions remaining to discharge*) |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33832
diff
changeset
|
239 |
Drule.export_without_context (induction RS (rules RS conjI))) |
23150 | 240 |
end |
241 |
||
242 |
fun defer thy congs fid seqs = |
|
24707 | 243 |
defer_i thy congs fid (map (Syntax.read_term_global thy) seqs) |
23150 | 244 |
handle U.ERR {mesg,...} => error mesg; |
245 |
end; |
|
246 |
||
247 |
end; |