1 structure Tfl |
1 signature TFL = |
2 :sig |
2 sig |
3 structure Prim : TFL_sig |
3 structure Prim : TFL_sig |
4 |
4 |
5 val tgoalw : theory -> thm list -> thm -> thm list |
5 val tgoalw : theory -> thm list -> thm list -> thm list |
6 val tgoal: theory -> thm -> thm list |
6 val tgoal: theory -> thm list -> thm list |
7 |
7 |
8 val WF_TAC : thm list -> tactic |
8 val WF_TAC : thm list -> tactic |
9 |
9 |
10 val simplifier : thm -> thm |
10 val simplifier : thm -> thm |
11 val std_postprocessor : theory |
11 val std_postprocessor : theory |
12 -> {induction:thm, rules:thm, TCs:term list list} |
12 -> {induction:thm, rules:thm, TCs:term list list} |
13 -> {induction:thm, rules:thm, nested_tcs:thm list} |
13 -> {induction:thm, rules:thm, nested_tcs:thm list} |
14 |
14 |
15 val rfunction : theory |
15 val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list) |
16 -> (thm list -> thm -> thm) |
16 val define : theory -> string -> string list -> theory * Prim.pattern list |
17 -> term -> term |
17 |
18 -> {induction:thm, rules:thm, |
18 val simplify_defn : theory * (string * Prim.pattern list) |
19 tcs:term list, theory:theory} |
19 -> {rules:thm list, induct:thm, tcs:term list} |
20 |
20 |
21 val Rfunction : theory -> term -> term |
21 (*------------------------------------------------------------------------- |
22 -> {induction:thm, rules:thm, |
22 val function : theory -> term -> {theory:theory, eq_ind : thm} |
23 theory:theory, tcs:term list} |
23 val lazyR_def: theory -> term -> {theory:theory, eqns : thm} |
24 |
24 *-------------------------------------------------------------------------*) |
25 val function : theory -> term -> {theory:theory, eq_ind : thm} |
|
26 val lazyR_def : theory -> term -> {theory:theory, eqns : thm} |
|
27 |
25 |
28 val tflcongs : theory -> thm list |
26 val tflcongs : theory -> thm list |
29 |
27 |
30 end = |
28 end; |
|
29 |
|
30 |
|
31 structure Tfl: TFL = |
31 struct |
32 struct |
32 structure Prim = Prim |
33 structure Prim = Prim |
33 |
34 structure S = Prim.USyntax |
34 fun tgoalw thy defs thm = |
35 |
35 let val L = Prim.termination_goals thm |
36 (*--------------------------------------------------------------------------- |
|
37 * Extract termination goals so that they can be put it into a goalstack, or |
|
38 * have a tactic directly applied to them. |
|
39 *--------------------------------------------------------------------------*) |
|
40 fun termination_goals rules = |
|
41 map (Logic.freeze_vars o S.drop_Trueprop) |
|
42 (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); |
|
43 |
|
44 (*--------------------------------------------------------------------------- |
|
45 * Finds the termination conditions in (highly massaged) definition and |
|
46 * puts them into a goalstack. |
|
47 *--------------------------------------------------------------------------*) |
|
48 fun tgoalw thy defs rules = |
|
49 let val L = termination_goals rules |
36 open USyntax |
50 open USyntax |
37 val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L)) |
51 val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L)) |
38 in goalw_cterm defs g |
52 in goalw_cterm defs g |
39 end; |
53 end; |
40 |
54 |
41 val tgoal = Utils.C tgoalw []; |
55 val tgoal = Utils.C tgoalw []; |
42 |
56 |
|
57 (*--------------------------------------------------------------------------- |
|
58 * Simple wellfoundedness prover. |
|
59 *--------------------------------------------------------------------------*) |
43 fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) |
60 fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) |
44 val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, |
61 val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, |
45 wf_pred_nat, wf_pred_list, wf_trancl]; |
62 wf_pred_nat, wf_pred_list, wf_trancl]; |
46 |
63 |
47 val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def, |
64 val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def, |
48 fst_conv,snd_conv, |
65 fst_conv,snd_conv, |
49 mem_Collect_eq,lessI]) 1 |
66 mem_Collect_eq,lessI]) 1 |
50 THEN TRY(fast_tac set_cs 1); |
67 THEN TRY(fast_tac set_cs 1); |
51 |
68 |
|
69 val length_Cons = prove_goal List.thy "length(h#t) = Suc(length t)" |
|
70 (fn _ => [Simp_tac 1]); |
|
71 |
52 val simpls = [less_eq RS eq_reflection, |
72 val simpls = [less_eq RS eq_reflection, |
53 lex_prod_def, measure_def, inv_image_def, |
73 lex_prod_def, measure_def, inv_image_def, |
54 fst_conv RS eq_reflection, snd_conv RS eq_reflection, |
74 fst_conv RS eq_reflection, snd_conv RS eq_reflection, |
55 mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)]; |
75 mem_Collect_eq RS eq_reflection, length_Cons RS eq_reflection]; |
56 |
76 |
|
77 (*--------------------------------------------------------------------------- |
|
78 * Does some standard things with the termination conditions of a definition: |
|
79 * attempts to prove wellfoundedness of the given relation; simplifies the |
|
80 * non-proven termination conditions; and finally attempts to prove the |
|
81 * simplified termination conditions. |
|
82 *--------------------------------------------------------------------------*) |
57 val std_postprocessor = Prim.postprocess{WFtac = WFtac, |
83 val std_postprocessor = Prim.postprocess{WFtac = WFtac, |
58 terminator = terminator, |
84 terminator = terminator, |
59 simplifier = Prim.Rules.simpl_conv simpls}; |
85 simplifier = Prim.Rules.simpl_conv simpls}; |
60 |
86 |
61 val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ |
87 val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ |
62 [pred_nat_def,pred_list_def]); |
88 [pred_nat_def,pred_list_def]); |
|
89 |
63 fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); |
90 fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); |
64 |
91 |
65 |
92 |
66 local structure S = Prim.USyntax |
|
67 in |
|
68 fun func_of_cond_eqn tm = |
|
69 #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm))))))) |
|
70 end; |
|
71 |
|
72 |
|
73 val concl = #2 o Prim.Rules.dest_thm; |
93 val concl = #2 o Prim.Rules.dest_thm; |
74 |
94 |
75 (*--------------------------------------------------------------------------- |
95 (*--------------------------------------------------------------------------- |
76 * Defining a function with an associated termination relation. Lots of |
96 * Defining a function with an associated termination relation. |
77 * postprocessing takes place. |
97 *---------------------------------------------------------------------------*) |
|
98 fun define_i thy R eqs = |
|
99 let val dummy = require_thy thy "WF_Rel" "recursive function definitions"; |
|
100 |
|
101 val {functional,pats} = Prim.mk_functional thy eqs |
|
102 val (thm,thry) = Prim.wfrec_definition0 thy R functional |
|
103 in (thry,(thm,pats)) |
|
104 end; |
|
105 |
|
106 (*lcp's version: takes strings; doesn't return "thm" |
|
107 (whose signature is a draft and therefore useless) *) |
|
108 fun define thy R eqs = |
|
109 let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) |
|
110 val (thy',(_,pats)) = |
|
111 define_i thy (read thy R) |
|
112 (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs)) |
|
113 in (thy',pats) end |
|
114 handle Utils.ERR {mesg,...} => error mesg; |
|
115 |
|
116 (*--------------------------------------------------------------------------- |
|
117 * Postprocess a definition made by "define". This is a separate stage of |
|
118 * processing from the definition stage. |
78 *---------------------------------------------------------------------------*) |
119 *---------------------------------------------------------------------------*) |
79 local |
120 local |
80 structure S = Prim.USyntax |
|
81 structure R = Prim.Rules |
121 structure R = Prim.Rules |
82 structure U = Utils |
122 structure U = Utils |
83 |
123 |
|
124 (* The rest of these local definitions are for the tricky nested case *) |
84 val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl |
125 val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl |
85 |
126 |
86 fun id_thm th = |
127 fun id_thm th = |
87 let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) |
128 let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) |
88 in S.aconv lhs rhs |
129 in S.aconv lhs rhs |
94 fun mk_meta_eq r = case concl_of r of |
135 fun mk_meta_eq r = case concl_of r of |
95 Const("==",_)$_$_ => r |
136 Const("==",_)$_$_ => r |
96 | _$(Const("op =",_)$_$_) => r RS eq_reflection |
137 | _$(Const("op =",_)$_$_) => r RS eq_reflection |
97 | _ => r RS P_imp_P_eq_True |
138 | _ => r RS P_imp_P_eq_True |
98 fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L)) |
139 fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L)) |
|
140 fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss)) |
99 |
141 |
100 fun join_assums th = |
142 fun join_assums th = |
101 let val {sign,...} = rep_thm th |
143 let val {sign,...} = rep_thm th |
102 val tych = cterm_of sign |
144 val tych = cterm_of sign |
103 val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) |
145 val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) |
104 val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) |
146 val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) |
105 val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) |
147 val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) |
106 val cntxt = U.union S.aconv cntxtl cntxtr |
148 val cntxt = U.union S.aconv cntxtl cntxtr |
107 in |
149 in |
108 R.GEN_ALL |
150 R.GEN_ALL |
109 (R.DISCH_ALL |
151 (R.DISCH_ALL |
110 (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) |
152 (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) |
111 end |
153 end |
112 val gen_all = S.gen_all |
154 val gen_all = S.gen_all |
113 in |
155 in |
114 fun rfunction theory reducer R eqs = |
156 (*--------------------------------------------------------------------------- |
115 let val _ = prs "Making definition.. " |
157 * The "reducer" argument is |
116 val {rules,theory, full_pats_TCs, |
158 * (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); |
117 TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} |
159 *---------------------------------------------------------------------------*) |
118 val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules)) |
160 fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} = |
119 val _ = prs "Definition made.\n" |
161 let val dummy = output(std_out, "Proving induction theorem.. ") |
120 val _ = prs "Proving induction theorem.. " |
162 val ind = Prim.mk_induction theory f R full_pats_TCs |
121 val ind = Prim.mk_induction theory f R full_pats_TCs |
163 val dummy = output(std_out, "Proved induction theorem.\n") |
122 val _ = prs "Proved induction theorem.\n" |
164 val pp = std_postprocessor theory |
123 val pp = std_postprocessor theory |
165 val dummy = output(std_out, "Postprocessing.. ") |
124 val _ = prs "Postprocessing.. " |
166 val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs} |
125 val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs} |
167 in |
126 val normal_tcs = Prim.termination_goals rules |
168 case nested_tcs |
127 in |
169 of [] => (output(std_out, "Postprocessing done.\n"); |
128 case nested_tcs |
170 {induction=induction, rules=rules,tcs=[]}) |
129 of [] => (prs "Postprocessing done.\n"; |
171 | L => let val dummy = output(std_out, "Simplifying nested TCs.. ") |
130 {theory=theory, induction=induction, rules=rules,tcs=normal_tcs}) |
|
131 | L => let val _ = prs "Simplifying nested TCs.. " |
|
132 val (solved,simplified,stubborn) = |
172 val (solved,simplified,stubborn) = |
133 U.itlist (fn th => fn (So,Si,St) => |
173 U.itlist (fn th => fn (So,Si,St) => |
134 if (id_thm th) then (So, Si, th::St) else |
174 if (id_thm th) then (So, Si, th::St) else |
135 if (solved th) then (th::So, Si, St) |
175 if (solved th) then (th::So, Si, St) |
136 else (So, th::Si, St)) nested_tcs ([],[],[]) |
176 else (So, th::Si, St)) nested_tcs ([],[],[]) |
137 val simplified' = map join_assums simplified |
177 val simplified' = map join_assums simplified |
138 val induction' = reducer (solved@simplified') induction |
178 val induction' = reducer (solved@simplified') induction |
139 val rules' = reducer (solved@simplified') rules |
179 val rules' = reducer (solved@simplified') rules |
140 val _ = prs "Postprocessing done.\n" |
180 val dummy = output(std_out, "Postprocessing done.\n") |
141 in |
181 in |
142 {induction = induction', |
182 {induction = induction', |
143 rules = rules', |
183 rules = rules', |
144 tcs = normal_tcs @ |
184 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) |
145 map (gen_all o S.rhs o #2 o S.strip_forall o concl) |
185 (simplified@stubborn)} |
146 (simplified@stubborn), |
|
147 theory = theory} |
|
148 end |
186 end |
149 end |
187 end handle (e as Utils.ERR _) => Utils.Raise e |
150 handle (e as Utils.ERR _) => Utils.Raise e |
188 | e => print_exn e; |
151 | e => print_exn e |
189 |
152 |
190 |
153 |
191 (*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
154 fun Rfunction thry = |
192 val meta_outer = |
155 rfunction thry |
193 standard o rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI])); |
156 (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); |
194 |
157 |
195 |
158 |
196 (*Strip off the outer !P*) |
|
197 val spec'= read_instantiate [("x","P::?'b=>bool")] spec; |
|
198 |
|
199 |
|
200 fun simplify_defn (thy,(id,pats)) = |
|
201 let val def = freezeT(get_def thy id RS meta_eq_to_obj_eq) |
|
202 val {theory,rules,TCs,full_pats_TCs,patterns} = |
|
203 Prim.post_definition (thy,(def,pats)) |
|
204 val {lhs=f,rhs} = S.dest_eq(concl def) |
|
205 val (_,[R,_]) = S.strip_comb rhs |
|
206 val {induction, rules, tcs} = |
|
207 proof_stage theory reducer |
|
208 {f = f, R = R, rules = rules, |
|
209 full_pats_TCs = full_pats_TCs, |
|
210 TCs = TCs} |
|
211 val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) |
|
212 in {induct = meta_outer |
|
213 (normalize_thm [RSspec,RSmp] (induction RS spec')), |
|
214 rules = rules', |
|
215 tcs = (termination_goals rules') @ tcs} |
|
216 end |
|
217 handle Utils.ERR {mesg,...} => error mesg |
159 end; |
218 end; |
160 |
219 |
161 |
220 (*--------------------------------------------------------------------------- |
162 local structure R = Prim.Rules |
221 * |
|
222 * Definitions with synthesized termination relation temporarily |
|
223 * deleted -- it's not clear how to integrate this facility with |
|
224 * the Isabelle theory file scheme, which restricts |
|
225 * inference at theory-construction time. |
|
226 * |
|
227 |
|
228 local fun floutput s = (output(std_out,s); flush_out std_out) |
|
229 structure R = Prim.Rules |
163 in |
230 in |
164 fun function theory eqs = |
231 fun function theory eqs = |
165 let val _ = prs "Making definition.. " |
232 let val dummy = floutput "Making definition.. " |
166 val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs |
233 val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs |
167 val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) |
234 val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) |
168 val _ = prs "Definition made.\n" |
235 val dummy = floutput "Definition made.\n" |
169 val _ = prs "Proving induction theorem.. " |
236 val dummy = floutput "Proving induction theorem.. " |
170 val induction = Prim.mk_induction theory f R full_pats_TCs |
237 val induction = Prim.mk_induction theory f R full_pats_TCs |
171 val _ = prs "Induction theorem proved.\n" |
238 val dummy = floutput "Induction theorem proved.\n" |
172 in {theory = theory, |
239 in {theory = theory, |
173 eq_ind = standard (induction RS (rules RS conjI))} |
240 eq_ind = standard (induction RS (rules RS conjI))} |
174 end |
241 end |
175 handle (e as Utils.ERR _) => Utils.Raise e |
242 handle (e as Utils.ERR _) => Utils.Raise e |
176 | e => print_exn e |
243 | e => print_exn e |