|
1 (* Title: TFL/post.ML |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 Second part of main module (postprocessing of TFL definitions). |
|
7 *) |
|
8 |
|
9 signature TFL = |
|
10 sig |
|
11 val trace: bool ref |
|
12 val quiet_mode: bool ref |
|
13 val message: string -> unit |
|
14 val tgoalw: theory -> thm list -> thm list -> thm list |
|
15 val tgoal: theory -> thm list -> thm list |
|
16 val std_postprocessor: claset -> simpset -> thm list -> theory -> |
|
17 {induction: thm, rules: thm, TCs: term list list} -> |
|
18 {induction: thm, rules: thm, nested_tcs: thm list} |
|
19 val define_i: theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
|
20 term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} |
|
21 val define: theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
|
22 string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} |
|
23 val defer_i: theory -> thm list -> xstring -> term list -> theory * thm |
|
24 val defer: theory -> thm list -> xstring -> string list -> theory * thm |
|
25 end; |
|
26 |
|
27 structure Tfl: TFL = |
|
28 struct |
|
29 |
|
30 structure S = USyntax |
|
31 |
|
32 |
|
33 (* messages *) |
|
34 |
|
35 val trace = Prim.trace |
|
36 |
|
37 val quiet_mode = ref false; |
|
38 fun message s = if ! quiet_mode then () else writeln s; |
|
39 |
|
40 |
|
41 (* misc *) |
|
42 |
|
43 fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT; |
|
44 |
|
45 |
|
46 (*--------------------------------------------------------------------------- |
|
47 * Extract termination goals so that they can be put it into a goalstack, or |
|
48 * have a tactic directly applied to them. |
|
49 *--------------------------------------------------------------------------*) |
|
50 fun termination_goals rules = |
|
51 map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) |
|
52 (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); |
|
53 |
|
54 (*--------------------------------------------------------------------------- |
|
55 * Finds the termination conditions in (highly massaged) definition and |
|
56 * puts them into a goalstack. |
|
57 *--------------------------------------------------------------------------*) |
|
58 fun tgoalw thy defs rules = |
|
59 case termination_goals rules of |
|
60 [] => error "tgoalw: no termination conditions to prove" |
|
61 | L => goalw_cterm defs |
|
62 (Thm.cterm_of (Theory.sign_of thy) |
|
63 (HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); |
|
64 |
|
65 fun tgoal thy = tgoalw thy []; |
|
66 |
|
67 (*--------------------------------------------------------------------------- |
|
68 * Three postprocessors are applied to the definition. It |
|
69 * attempts to prove wellfoundedness of the given relation, simplifies the |
|
70 * non-proved termination conditions, and finally attempts to prove the |
|
71 * simplified termination conditions. |
|
72 *--------------------------------------------------------------------------*) |
|
73 fun std_postprocessor cs ss wfs = |
|
74 Prim.postprocess |
|
75 {wf_tac = REPEAT (ares_tac wfs 1), |
|
76 terminator = asm_simp_tac ss 1 |
|
77 THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), |
|
78 simplifier = Rules.simpl_conv ss []}; |
|
79 |
|
80 |
|
81 |
|
82 val concl = #2 o Rules.dest_thm; |
|
83 |
|
84 (*--------------------------------------------------------------------------- |
|
85 * Postprocess a definition made by "define". This is a separate stage of |
|
86 * processing from the definition stage. |
|
87 *---------------------------------------------------------------------------*) |
|
88 local |
|
89 structure R = Rules |
|
90 structure U = Utils |
|
91 |
|
92 (* The rest of these local definitions are for the tricky nested case *) |
|
93 val solved = not o can S.dest_eq o #2 o S.strip_forall o concl |
|
94 |
|
95 fun id_thm th = |
|
96 let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); |
|
97 in lhs aconv rhs end |
|
98 handle U.ERR _ => false; |
|
99 |
|
100 |
|
101 fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); |
|
102 val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; |
|
103 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
|
104 fun mk_meta_eq r = case concl_of r of |
|
105 Const("==",_)$_$_ => r |
|
106 | _ $(Const("op =",_)$_$_) => r RS eq_reflection |
|
107 | _ => r RS P_imp_P_eq_True |
|
108 |
|
109 (*Is this the best way to invoke the simplifier??*) |
|
110 fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) |
|
111 |
|
112 fun join_assums th = |
|
113 let val {sign,...} = rep_thm th |
|
114 val tych = cterm_of sign |
|
115 val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) |
|
116 val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) |
|
117 val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) |
|
118 val cntxt = gen_union (op aconv) (cntxtl, cntxtr) |
|
119 in |
|
120 R.GEN_ALL |
|
121 (R.DISCH_ALL |
|
122 (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) |
|
123 end |
|
124 val gen_all = S.gen_all |
|
125 in |
|
126 fun proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = |
|
127 let |
|
128 val _ = message "Proving induction theorem ..." |
|
129 val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} |
|
130 val _ = message "Postprocessing ..."; |
|
131 val {rules, induction, nested_tcs} = |
|
132 std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} |
|
133 in |
|
134 case nested_tcs |
|
135 of [] => {induction=induction, rules=rules,tcs=[]} |
|
136 | L => let val dummy = message "Simplifying nested TCs ..." |
|
137 val (solved,simplified,stubborn) = |
|
138 U.itlist (fn th => fn (So,Si,St) => |
|
139 if (id_thm th) then (So, Si, th::St) else |
|
140 if (solved th) then (th::So, Si, St) |
|
141 else (So, th::Si, St)) nested_tcs ([],[],[]) |
|
142 val simplified' = map join_assums simplified |
|
143 val rewr = full_simplify (ss addsimps (solved @ simplified')); |
|
144 val induction' = rewr induction |
|
145 and rules' = rewr rules |
|
146 in |
|
147 {induction = induction', |
|
148 rules = rules', |
|
149 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) |
|
150 (simplified@stubborn)} |
|
151 end |
|
152 end; |
|
153 |
|
154 |
|
155 (*lcp: curry the predicate of the induction rule*) |
|
156 fun curry_rule rl = split_rule_var |
|
157 (head_of (HOLogic.dest_Trueprop (concl_of rl)), |
|
158 rl); |
|
159 |
|
160 (*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
|
161 val meta_outer = |
|
162 curry_rule o standard o |
|
163 rule_by_tactic (REPEAT |
|
164 (FIRSTGOAL (resolve_tac [allI, impI, conjI] |
|
165 ORELSE' etac conjE))); |
|
166 |
|
167 (*Strip off the outer !P*) |
|
168 val spec'= read_instantiate [("x","P::?'b=>bool")] spec; |
|
169 |
|
170 fun simplify_defn thy cs ss congs wfs id pats def0 = |
|
171 let val def = freezeT def0 RS meta_eq_to_obj_eq |
|
172 val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats)) |
|
173 val {lhs=f,rhs} = S.dest_eq (concl def) |
|
174 val (_,[R,_]) = S.strip_comb rhs |
|
175 val {induction, rules, tcs} = |
|
176 proof_stage cs ss wfs theory |
|
177 {f = f, R = R, rules = rules, |
|
178 full_pats_TCs = full_pats_TCs, |
|
179 TCs = TCs} |
|
180 val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules) |
|
181 in {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')), |
|
182 rules = ListPair.zip(rules', rows), |
|
183 tcs = (termination_goals rules') @ tcs} |
|
184 end |
|
185 handle U.ERR {mesg,func,module} => |
|
186 error (mesg ^ |
|
187 "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); |
|
188 |
|
189 (*--------------------------------------------------------------------------- |
|
190 * Defining a function with an associated termination relation. |
|
191 *---------------------------------------------------------------------------*) |
|
192 fun define_i thy cs ss congs wfs fid R eqs = |
|
193 let val {functional,pats} = Prim.mk_functional thy eqs |
|
194 val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional |
|
195 in (thy, simplify_defn thy cs ss congs wfs fid pats def) end; |
|
196 |
|
197 fun define thy cs ss congs wfs fid R seqs = |
|
198 define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs) |
|
199 handle U.ERR {mesg,...} => error mesg; |
|
200 |
|
201 |
|
202 (*--------------------------------------------------------------------------- |
|
203 * |
|
204 * Definitions with synthesized termination relation |
|
205 * |
|
206 *---------------------------------------------------------------------------*) |
|
207 |
|
208 fun func_of_cond_eqn tm = |
|
209 #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm))))))); |
|
210 |
|
211 fun defer_i thy congs fid eqs = |
|
212 let val {rules,R,theory,full_pats_TCs,SV,...} = |
|
213 Prim.lazyR_def thy (Sign.base_name fid) congs eqs |
|
214 val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); |
|
215 val dummy = message "Proving induction theorem ..."; |
|
216 val induction = Prim.mk_induction theory |
|
217 {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} |
|
218 in (theory, |
|
219 (*return the conjoined induction rule and recursion equations, |
|
220 with assumptions remaining to discharge*) |
|
221 standard (induction RS (rules RS conjI))) |
|
222 end |
|
223 |
|
224 fun defer thy congs fid seqs = |
|
225 defer_i thy congs fid (map (read_term thy) seqs) |
|
226 handle U.ERR {mesg,...} => error mesg; |
|
227 end; |
|
228 |
|
229 end; |