author | wenzelm |
Sat, 01 Feb 2014 18:42:46 +0100 | |
changeset 55236 | 8d61b0aa7a0d |
parent 55151 | f331472f1027 |
child 56245 | 84fc7dfa3cd4 |
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 |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
10 |
val define_i: bool -> Proof.context -> thm list -> thm list -> xstring -> term -> term list -> |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
11 |
theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
12 |
val define: bool -> Proof.context -> thm list -> thm list -> xstring -> string -> string list -> |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
13 |
theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
14 |
val defer_i: thm list -> xstring -> term list -> theory -> thm * theory |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
15 |
val defer: thm list -> xstring -> string list -> theory -> thm * theory |
23150 | 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 |
*--------------------------------------------------------------------------*) |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
37 |
fun std_postprocessor strict ctxt wfs = |
23150 | 38 |
Prim.postprocess strict |
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
39 |
{wf_tac = REPEAT (ares_tac wfs 1), |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
40 |
terminator = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset
|
41 |
asm_simp_tac ctxt 1 |
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
42 |
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42793
diff
changeset
|
43 |
fast_force_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset
|
44 |
simplifier = Rules.simpl_conv ctxt []}; |
23150 | 45 |
|
46 |
||
47 |
||
48 |
val concl = #2 o Rules.dest_thm; |
|
49 |
||
50 |
(*--------------------------------------------------------------------------- |
|
51 |
* Postprocess a definition made by "define". This is a separate stage of |
|
52 |
* processing from the definition stage. |
|
53 |
*---------------------------------------------------------------------------*) |
|
54 |
local |
|
55 |
||
56 |
(* 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
|
57 |
val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl |
23150 | 58 |
|
59 |
fun id_thm th = |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
60 |
let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th)))); |
23150 | 61 |
in lhs aconv rhs end |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
62 |
handle Utils.ERR _ => false; |
23150 | 63 |
|
30737 | 64 |
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; |
23150 | 65 |
fun mk_meta_eq r = case concl_of r of |
66 |
Const("==",_)$_$_ => r |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset
|
67 |
| _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection |
23150 | 68 |
| _ => r RS P_imp_P_eq_True |
69 |
||
70 |
(*Is this the best way to invoke the simplifier??*) |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
71 |
fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L)) |
23150 | 72 |
|
54999 | 73 |
fun join_assums ctxt th = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26478
diff
changeset
|
74 |
let val thy = Thm.theory_of_thm th |
23150 | 75 |
val tych = cterm_of thy |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *) |
33042 | 79 |
val cntxt = union (op aconv) cntxtl cntxtr |
23150 | 80 |
in |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
81 |
Rules.GEN_ALL |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
82 |
(Rules.DISCH_ALL |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
83 |
(rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th))) |
23150 | 84 |
end |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
85 |
val gen_all = USyntax.gen_all |
23150 | 86 |
in |
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
87 |
fun proof_stage strict ctxt wfs theory {f, R, rules, full_pats_TCs, TCs} = |
23150 | 88 |
let |
26478 | 89 |
val _ = writeln "Proving induction theorem ..." |
23150 | 90 |
val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} |
26478 | 91 |
val _ = writeln "Postprocessing ..."; |
23150 | 92 |
val {rules, induction, nested_tcs} = |
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
93 |
std_postprocessor strict ctxt wfs theory {rules=rules, induction=ind, TCs=TCs} |
23150 | 94 |
in |
95 |
case nested_tcs |
|
96 |
of [] => {induction=induction, rules=rules,tcs=[]} |
|
26478 | 97 |
| L => let val dummy = writeln "Simplifying nested TCs ..." |
23150 | 98 |
val (solved,simplified,stubborn) = |
99 |
fold_rev (fn th => fn (So,Si,St) => |
|
100 |
if (id_thm th) then (So, Si, th::St) else |
|
101 |
if (solved th) then (th::So, Si, St) |
|
102 |
else (So, th::Si, St)) nested_tcs ([],[],[]) |
|
54999 | 103 |
val simplified' = map (join_assums ctxt) simplified |
55236 | 104 |
val dummy = (Prim.trace_thms ctxt "solved =" solved; |
105 |
Prim.trace_thms ctxt "simplified' =" simplified') |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset
|
106 |
val rewr = full_simplify (ctxt addsimps (solved @ simplified')); |
55236 | 107 |
val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction] |
23150 | 108 |
val induction' = rewr induction |
55236 | 109 |
val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules] |
23150 | 110 |
val rules' = rewr rules |
26478 | 111 |
val _ = writeln "... Postprocessing finished"; |
23150 | 112 |
in |
113 |
{induction = induction', |
|
114 |
rules = rules', |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
115 |
tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl) |
23150 | 116 |
(simplified@stubborn)} |
117 |
end |
|
118 |
end; |
|
119 |
||
120 |
||
121 |
(*lcp: curry the predicate of the induction rule*) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset
|
122 |
fun curry_rule ctxt rl = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset
|
123 |
Split_Rule.split_rule_var ctxt (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; |
23150 | 124 |
|
125 |
(*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
|
36546 | 126 |
fun meta_outer ctxt = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset
|
127 |
curry_rule ctxt o Drule.export_without_context o |
36546 | 128 |
rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
23150 | 129 |
|
130 |
(*Strip off the outer !P*) |
|
55151 | 131 |
val spec'= Rule_Insts.read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec; |
23150 | 132 |
|
133 |
fun tracing true _ = () |
|
134 |
| tracing false msg = writeln msg; |
|
135 |
||
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
136 |
fun simplify_defn strict thy ctxt congs wfs id pats def0 = |
36546 | 137 |
let |
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
|
138 |
val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq |
23150 | 139 |
val {rules,rows,TCs,full_pats_TCs} = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
140 |
Prim.post_definition congs thy ctxt (def, pats) |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
141 |
val {lhs=f,rhs} = USyntax.dest_eq (concl def) |
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
142 |
val (_,[R,_]) = USyntax.strip_comb rhs |
55236 | 143 |
val dummy = Prim.trace_thms ctxt "congs =" congs |
23150 | 144 |
(*the next step has caused simplifier looping in some cases*) |
145 |
val {induction, rules, tcs} = |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
146 |
proof_stage strict ctxt wfs thy |
23150 | 147 |
{f = f, R = R, rules = rules, |
148 |
full_pats_TCs = full_pats_TCs, |
|
149 |
TCs = TCs} |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
150 |
val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt) |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
151 |
(Rules.CONJUNCTS rules) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
152 |
in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')), |
23150 | 153 |
rules = ListPair.zip(rules', rows), |
154 |
tcs = (termination_goals rules') @ tcs} |
|
155 |
end |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
156 |
handle Utils.ERR {mesg,func,module} => |
23150 | 157 |
error (mesg ^ |
158 |
"\n (In TFL function " ^ module ^ "." ^ func ^ ")"); |
|
159 |
||
160 |
||
161 |
(* Derive the initial equations from the case-split rules to meet the |
|
41895 | 162 |
users specification of the recursive function. *) |
23150 | 163 |
local |
164 |
fun get_related_thms i = |
|
32952 | 165 |
map_filter ((fn (r,x) => if x = i then SOME r else NONE)); |
23150 | 166 |
|
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
167 |
fun solve_eq _ (th, [], i) = error "derive_init_eqs: missing rules" |
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
168 |
| solve_eq _ (th, [a], i) = [(a, i)] |
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
169 |
| solve_eq ctxt (th, splitths, i) = |
23150 | 170 |
(writeln "Proving unsplit equation..."; |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
171 |
[((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt) |
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
172 |
(CaseSplit.splitto ctxt splitths th), i)]) |
23150 | 173 |
handle ERROR s => |
174 |
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths); |
|
175 |
in |
|
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
176 |
fun derive_init_eqs ctxt rules eqs = |
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
177 |
map (Thm.trivial o Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop) eqs |
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
178 |
|> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i)) |
41895 | 179 |
|> flat; |
23150 | 180 |
end; |
181 |
||
182 |
||
183 |
(*--------------------------------------------------------------------------- |
|
184 |
* Defining a function with an associated termination relation. |
|
185 |
*---------------------------------------------------------------------------*) |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
186 |
fun define_i strict ctxt congs wfs fid R eqs thy = |
23150 | 187 |
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
|
188 |
val (thy, def) = Prim.wfrec_definition0 thy fid R functional |
54999 | 189 |
val ctxt = Proof_Context.transfer thy ctxt |
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35625
diff
changeset
|
190 |
val (lhs, _) = Logic.dest_equals (prop_of def) |
54999 | 191 |
val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def |
23150 | 192 |
val rules' = |
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
44890
diff
changeset
|
193 |
if strict then derive_init_eqs ctxt rules eqs |
23150 | 194 |
else rules |
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
195 |
in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end; |
23150 | 196 |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
197 |
fun define strict ctxt congs wfs fid R seqs thy = |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
198 |
define_i strict ctxt congs wfs fid |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
199 |
(Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) thy |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
200 |
handle Utils.ERR {mesg,...} => error mesg; |
23150 | 201 |
|
202 |
||
203 |
(*--------------------------------------------------------------------------- |
|
204 |
* |
|
205 |
* Definitions with synthesized termination relation |
|
206 |
* |
|
207 |
*---------------------------------------------------------------------------*) |
|
208 |
||
209 |
fun func_of_cond_eqn tm = |
|
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
210 |
#1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm))))))); |
23150 | 211 |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
212 |
fun defer_i congs fid eqs thy = |
35799
7adb03f27b28
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
wenzelm
parents:
35756
diff
changeset
|
213 |
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
|
214 |
val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules)); |
26478 | 215 |
val dummy = writeln "Proving induction theorem ..."; |
23150 | 216 |
val induction = Prim.mk_induction theory |
217 |
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} |
|
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
218 |
in |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
219 |
(*return the conjoined induction rule and recursion equations, |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
220 |
with assumptions remaining to discharge*) |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
221 |
(Drule.export_without_context (induction RS (rules RS conjI)), theory) |
23150 | 222 |
end |
223 |
||
42775
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
224 |
fun defer congs fid seqs thy = |
a973f82fc885
prefer Proof.context over old-style claset/simpset;
wenzelm
parents:
42361
diff
changeset
|
225 |
defer_i congs fid (map (Syntax.read_term_global thy) seqs) thy |
41164
6854e9a40edc
avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents:
38864
diff
changeset
|
226 |
handle Utils.ERR {mesg,...} => error mesg; |
23150 | 227 |
end; |
228 |
||
229 |
end; |