author | bulwahn |
Fri, 18 Mar 2011 18:19:42 +0100 | |
changeset 42025 | cb5b1e85b32e |
parent 41895 | a2e9af953b90 |
child 42361 | 23f352990944 |
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 -> |
|
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35625
diff
changeset
|
11 |
term -> term list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} |
23150 | 12 |
val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35625
diff
changeset
|
13 |
string -> string list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} |
23150 | 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 |
(* misc *) |
|
22 |
||
23 |
(*--------------------------------------------------------------------------- |
|
24 |
* Extract termination goals so that they can be put it into a goalstack, or |
|
25 |
* have a tactic directly applied to them. |
|
26 |
*--------------------------------------------------------------------------*) |
|
27 |
fun termination_goals rules = |
|
33832 | 28 |
map (Type.legacy_freeze o HOLogic.dest_Trueprop) |
33339 | 29 |
(fold_rev (union (op aconv) o prems_of) rules []); |
23150 | 30 |
|
31 |
(*--------------------------------------------------------------------------- |
|
32 |
* Three postprocessors are applied to the definition. It |
|
33 |
* attempts to prove wellfoundedness of the given relation, simplifies the |
|
34 |
* non-proved termination conditions, and finally attempts to prove the |
|
35 |
* simplified termination conditions. |
|
36 |
*--------------------------------------------------------------------------*) |
|
37 |
fun std_postprocessor strict cs ss wfs = |
|
38 |
Prim.postprocess strict |
|
39 |
{wf_tac = REPEAT (ares_tac wfs 1), |
|
40 |
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
|
41 |
THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE |
23880 | 42 |
fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), |
23150 | 43 |
simplifier = Rules.simpl_conv ss []}; |
44 |
||
45 |
||
46 |
||
47 |
val concl = #2 o Rules.dest_thm; |
|
48 |
||
49 |
(*--------------------------------------------------------------------------- |
|
50 |
* Postprocess a definition made by "define". This is a separate stage of |
|
51 |
* processing from the definition stage. |
|
52 |
*---------------------------------------------------------------------------*) |
|
53 |
local |
|
54 |
||
55 |
(* The rest of these local definitions are for the tricky nested case *) |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
56 |
val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl |
23150 | 57 |
|
58 |
fun id_thm th = |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
59 |
let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th)))); |
23150 | 60 |
in lhs aconv rhs end |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
61 |
handle Utils.ERR _ => false; |
23150 | 62 |
|
30737 | 63 |
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; |
23150 | 64 |
fun mk_meta_eq r = case concl_of r of |
65 |
Const("==",_)$_$_ => r |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset
|
66 |
| _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection |
23150 | 67 |
| _ => r RS P_imp_P_eq_True |
68 |
||
69 |
(*Is this the best way to invoke the simplifier??*) |
|
33317 | 70 |
fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) |
23150 | 71 |
|
72 |
fun join_assums th = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26478
diff
changeset
|
73 |
let val thy = Thm.theory_of_thm th |
23150 | 74 |
val tych = cterm_of thy |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
75 |
val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th))) |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
76 |
val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *) |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
77 |
val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *) |
33042 | 78 |
val cntxt = union (op aconv) cntxtl cntxtr |
23150 | 79 |
in |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
80 |
Rules.GEN_ALL |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
81 |
(Rules.DISCH_ALL |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
82 |
(rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th))) |
23150 | 83 |
end |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
84 |
val gen_all = USyntax.gen_all |
23150 | 85 |
in |
86 |
fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = |
|
87 |
let |
|
26478 | 88 |
val _ = writeln "Proving induction theorem ..." |
23150 | 89 |
val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} |
26478 | 90 |
val _ = writeln "Postprocessing ..."; |
23150 | 91 |
val {rules, induction, nested_tcs} = |
92 |
std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} |
|
93 |
in |
|
94 |
case nested_tcs |
|
95 |
of [] => {induction=induction, rules=rules,tcs=[]} |
|
26478 | 96 |
| L => let val dummy = writeln "Simplifying nested TCs ..." |
23150 | 97 |
val (solved,simplified,stubborn) = |
98 |
fold_rev (fn th => fn (So,Si,St) => |
|
99 |
if (id_thm th) then (So, Si, th::St) else |
|
100 |
if (solved th) then (th::So, Si, St) |
|
101 |
else (So, th::Si, St)) nested_tcs ([],[],[]) |
|
102 |
val simplified' = map join_assums simplified |
|
103 |
val dummy = (Prim.trace_thms "solved =" solved; |
|
104 |
Prim.trace_thms "simplified' =" simplified') |
|
105 |
val rewr = full_simplify (ss addsimps (solved @ simplified')); |
|
106 |
val dummy = Prim.trace_thms "Simplifying the induction rule..." |
|
107 |
[induction] |
|
108 |
val induction' = rewr induction |
|
109 |
val dummy = Prim.trace_thms "Simplifying the recursion rules..." |
|
110 |
[rules] |
|
111 |
val rules' = rewr rules |
|
26478 | 112 |
val _ = writeln "... Postprocessing finished"; |
23150 | 113 |
in |
114 |
{induction = induction', |
|
115 |
rules = rules', |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
116 |
tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl) |
23150 | 117 |
(simplified@stubborn)} |
118 |
end |
|
119 |
end; |
|
120 |
||
121 |
||
122 |
(*lcp: curry the predicate of the induction rule*) |
|
123 |
fun curry_rule rl = |
|
35365 | 124 |
Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; |
23150 | 125 |
|
126 |
(*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
|
36546 | 127 |
fun meta_outer ctxt = |
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
|
128 |
curry_rule o Drule.export_without_context o |
36546 | 129 |
rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
23150 | 130 |
|
131 |
(*Strip off the outer !P*) |
|
27239 | 132 |
val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; |
23150 | 133 |
|
134 |
fun tracing true _ = () |
|
135 |
| tracing false msg = writeln msg; |
|
136 |
||
137 |
fun simplify_defn strict thy cs ss congs wfs id pats def0 = |
|
36546 | 138 |
let |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36546
diff
changeset
|
139 |
val ctxt = ProofContext.init_global thy |
36616
712724c32ac8
replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
wenzelm
parents:
36615
diff
changeset
|
140 |
val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq |
23150 | 141 |
val {rules,rows,TCs,full_pats_TCs} = |
142 |
Prim.post_definition congs (thy, (def,pats)) |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
143 |
val {lhs=f,rhs} = USyntax.dest_eq (concl def) |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
144 |
val (_,[R,_]) = USyntax.strip_comb rhs |
23150 | 145 |
val dummy = Prim.trace_thms "congs =" congs |
146 |
(*the next step has caused simplifier looping in some cases*) |
|
147 |
val {induction, rules, tcs} = |
|
148 |
proof_stage strict cs ss wfs thy |
|
149 |
{f = f, R = R, rules = rules, |
|
150 |
full_pats_TCs = full_pats_TCs, |
|
151 |
TCs = TCs} |
|
35625 | 152 |
val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm) |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
153 |
(Rules.CONJUNCTS rules) |
36546 | 154 |
in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')), |
23150 | 155 |
rules = ListPair.zip(rules', rows), |
156 |
tcs = (termination_goals rules') @ tcs} |
|
157 |
end |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
158 |
handle Utils.ERR {mesg,func,module} => |
23150 | 159 |
error (mesg ^ |
160 |
"\n (In TFL function " ^ module ^ "." ^ func ^ ")"); |
|
161 |
||
162 |
||
163 |
(* Derive the initial equations from the case-split rules to meet the |
|
41895 | 164 |
users specification of the recursive function. *) |
23150 | 165 |
local |
166 |
fun get_related_thms i = |
|
32952 | 167 |
map_filter ((fn (r,x) => if x = i then SOME r else NONE)); |
23150 | 168 |
|
41895 | 169 |
fun solve_eq (th, [], i) = error "derive_init_eqs: missing rules" |
23150 | 170 |
| solve_eq (th, [a], i) = [(a, i)] |
41895 | 171 |
| solve_eq (th, splitths, i) = |
23150 | 172 |
(writeln "Proving unsplit equation..."; |
35625 | 173 |
[((Drule.export_without_context o Object_Logic.rulify_no_asm) |
23150 | 174 |
(CaseSplit.splitto splitths th), i)]) |
175 |
handle ERROR s => |
|
176 |
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths); |
|
177 |
in |
|
41895 | 178 |
fun derive_init_eqs thy rules eqs = |
179 |
map (Thm.trivial o Thm.cterm_of thy o HOLogic.mk_Trueprop) eqs |
|
180 |
|> map_index (fn (i, e) => solve_eq (e, (get_related_thms i rules), i)) |
|
181 |
|> flat; |
|
23150 | 182 |
end; |
183 |
||
184 |
||
185 |
(*--------------------------------------------------------------------------- |
|
186 |
* Defining a function with an associated termination relation. |
|
187 |
*---------------------------------------------------------------------------*) |
|
188 |
fun define_i strict thy cs ss congs wfs fid R eqs = |
|
189 |
let val {functional,pats} = Prim.mk_functional thy eqs |
|
35799
7adb03f27b28
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
wenzelm
parents:
35756
diff
changeset
|
190 |
val (thy, def) = Prim.wfrec_definition0 thy fid R functional |
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35625
diff
changeset
|
191 |
val (lhs, _) = Logic.dest_equals (prop_of def) |
23150 | 192 |
val {induct, rules, tcs} = |
193 |
simplify_defn strict thy cs ss congs wfs fid pats def |
|
194 |
val rules' = |
|
195 |
if strict then derive_init_eqs thy rules eqs |
|
196 |
else rules |
|
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35625
diff
changeset
|
197 |
in (thy, {lhs = lhs, rules = rules', induct = induct, tcs = tcs}) end; |
23150 | 198 |
|
199 |
fun define strict thy cs ss congs wfs fid R seqs = |
|
24707 | 200 |
define_i strict thy cs ss congs wfs fid |
201 |
(Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs) |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
202 |
handle Utils.ERR {mesg,...} => error mesg; |
23150 | 203 |
|
204 |
||
205 |
(*--------------------------------------------------------------------------- |
|
206 |
* |
|
207 |
* Definitions with synthesized termination relation |
|
208 |
* |
|
209 |
*---------------------------------------------------------------------------*) |
|
210 |
||
211 |
fun func_of_cond_eqn tm = |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
212 |
#1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm))))))); |
23150 | 213 |
|
214 |
fun defer_i thy congs fid eqs = |
|
35799
7adb03f27b28
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
wenzelm
parents:
35756
diff
changeset
|
215 |
let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
216 |
val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules)); |
26478 | 217 |
val dummy = writeln "Proving induction theorem ..."; |
23150 | 218 |
val induction = Prim.mk_induction theory |
219 |
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} |
|
220 |
in (theory, |
|
221 |
(*return the conjoined induction rule and recursion equations, |
|
222 |
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
|
223 |
Drule.export_without_context (induction RS (rules RS conjI))) |
23150 | 224 |
end |
225 |
||
226 |
fun defer thy congs fid seqs = |
|
24707 | 227 |
defer_i thy congs fid (map (Syntax.read_term_global thy) seqs) |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
228 |
handle Utils.ERR {mesg,...} => error mesg; |
23150 | 229 |
end; |
230 |
||
231 |
end; |