1 (* Title: HOL/Tools/Function/fundef.ML |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 |
|
4 A package for general recursive function definitions. |
|
5 Isar commands. |
|
6 *) |
|
7 |
|
8 signature FUNDEF = |
|
9 sig |
|
10 val add_fundef : (binding * typ option * mixfix) list |
|
11 -> (Attrib.binding * term) list |
|
12 -> FundefCommon.fundef_config |
|
13 -> local_theory |
|
14 -> Proof.state |
|
15 val add_fundef_cmd : (binding * string option * mixfix) list |
|
16 -> (Attrib.binding * string) list |
|
17 -> FundefCommon.fundef_config |
|
18 -> local_theory |
|
19 -> Proof.state |
|
20 |
|
21 val termination_proof : term option -> local_theory -> Proof.state |
|
22 val termination_proof_cmd : string option -> local_theory -> Proof.state |
|
23 val termination : term option -> local_theory -> Proof.state |
|
24 val termination_cmd : string option -> local_theory -> Proof.state |
|
25 |
|
26 val setup : theory -> theory |
|
27 val get_congs : Proof.context -> thm list |
|
28 end |
|
29 |
|
30 |
|
31 structure Fundef : FUNDEF = |
|
32 struct |
|
33 |
|
34 open FundefLib |
|
35 open FundefCommon |
|
36 |
|
37 val simp_attribs = map (Attrib.internal o K) |
|
38 [Simplifier.simp_add, |
|
39 Code.add_default_eqn_attribute, |
|
40 Nitpick_Simps.add, |
|
41 Quickcheck_RecFun_Simps.add] |
|
42 |
|
43 val psimp_attribs = map (Attrib.internal o K) |
|
44 [Simplifier.simp_add, |
|
45 Nitpick_Psimps.add] |
|
46 |
|
47 fun note_theorem ((name, atts), ths) = |
|
48 LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths) |
|
49 |
|
50 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
|
51 |
|
52 fun add_simps fnames post sort extra_qualify label moreatts simps lthy = |
|
53 let |
|
54 val spec = post simps |
|
55 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
|
56 |> map (apfst (apfst extra_qualify)) |
|
57 |
|
58 val (saved_spec_simps, lthy) = |
|
59 fold_map (LocalTheory.note Thm.generatedK) spec lthy |
|
60 |
|
61 val saved_simps = maps snd saved_spec_simps |
|
62 val simps_by_f = sort saved_simps |
|
63 |
|
64 fun add_for_f fname simps = |
|
65 note_theorem ((Long_Name.qualify fname label, []), simps) #> snd |
|
66 in |
|
67 (saved_simps, |
|
68 fold2 add_for_f fnames simps_by_f lthy) |
|
69 end |
|
70 |
|
71 fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy = |
|
72 let |
|
73 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
|
74 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
|
75 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
|
76 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
|
77 val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec |
|
78 |
|
79 val defname = mk_defname fixes |
|
80 |
|
81 val ((goalstate, cont), lthy) = |
|
82 FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy |
|
83 |
|
84 fun afterqed [[proof]] lthy = |
|
85 let |
|
86 val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, |
|
87 domintros, cases, ...} = |
|
88 cont (Thm.close_derivation proof) |
|
89 |
|
90 val fnames = map (fst o fst) fixes |
|
91 val qualify = Long_Name.qualify defname |
|
92 val addsmps = add_simps fnames post sort_cont |
|
93 |
|
94 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
|
95 lthy |
|
96 |> addsmps (Binding.qualify false "partial") "psimps" |
|
97 psimp_attribs psimps |
|
98 ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps |
|
99 ||>> note_theorem ((qualify "pinduct", |
|
100 [Attrib.internal (K (RuleCases.case_names cnames)), |
|
101 Attrib.internal (K (RuleCases.consumes 1)), |
|
102 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
|
103 ||>> note_theorem ((qualify "termination", []), [termination]) |
|
104 ||> (snd o note_theorem ((qualify "cases", |
|
105 [Attrib.internal (K (RuleCases.case_names cnames))]), [cases])) |
|
106 ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros |
|
107 |
|
108 val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', |
|
109 pinducts=snd pinducts', termination=termination', |
|
110 fs=fs, R=R, defname=defname } |
|
111 val _ = |
|
112 if not is_external then () |
|
113 else Specification.print_consts lthy (K false) (map fst fixes) |
|
114 in |
|
115 lthy |
|
116 |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata) |
|
117 end |
|
118 in |
|
119 lthy |
|
120 |> is_external ? LocalTheory.set_group (serial_string ()) |
|
121 |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] |
|
122 |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd |
|
123 end |
|
124 |
|
125 val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) |
|
126 val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type" |
|
127 |
|
128 fun gen_termination_proof prep_term raw_term_opt lthy = |
|
129 let |
|
130 val term_opt = Option.map (prep_term lthy) raw_term_opt |
|
131 val data = the (case term_opt of |
|
132 SOME t => (import_fundef_data t lthy |
|
133 handle Option.Option => |
|
134 error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) |
|
135 | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function")) |
|
136 |
|
137 val FundefCtxData { termination, R, add_simps, case_names, psimps, |
|
138 pinducts, defname, ...} = data |
|
139 val domT = domain_type (fastype_of R) |
|
140 val goal = HOLogic.mk_Trueprop |
|
141 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
|
142 fun afterqed [[totality]] lthy = |
|
143 let |
|
144 val totality = Thm.close_derivation totality |
|
145 val remove_domain_condition = |
|
146 full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) |
|
147 val tsimps = map remove_domain_condition psimps |
|
148 val tinduct = map remove_domain_condition pinducts |
|
149 val qualify = Long_Name.qualify defname; |
|
150 in |
|
151 lthy |
|
152 |> add_simps I "simps" simp_attribs tsimps |> snd |
|
153 |> note_theorem |
|
154 ((qualify "induct", |
|
155 [Attrib.internal (K (RuleCases.case_names case_names))]), |
|
156 tinduct) |> snd |
|
157 end |
|
158 in |
|
159 lthy |
|
160 |> ProofContext.note_thmss "" |
|
161 [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd |
|
162 |> ProofContext.note_thmss "" |
|
163 [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
|
164 |> ProofContext.note_thmss "" |
|
165 [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]), |
|
166 [([Goal.norm_result termination], [])])] |> snd |
|
167 |> Proof.theorem_i NONE afterqed [[(goal, [])]] |
|
168 end |
|
169 |
|
170 val termination_proof = gen_termination_proof Syntax.check_term; |
|
171 val termination_proof_cmd = gen_termination_proof Syntax.read_term; |
|
172 |
|
173 fun termination term_opt lthy = |
|
174 lthy |
|
175 |> LocalTheory.set_group (serial_string ()) |
|
176 |> termination_proof term_opt; |
|
177 |
|
178 fun termination_cmd term_opt lthy = |
|
179 lthy |
|
180 |> LocalTheory.set_group (serial_string ()) |
|
181 |> termination_proof_cmd term_opt; |
|
182 |
|
183 |
|
184 (* Datatype hook to declare datatype congs as "fundef_congs" *) |
|
185 |
|
186 |
|
187 fun add_case_cong n thy = |
|
188 Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm |
|
189 (Datatype.the_info thy n |
|
190 |> #case_cong |
|
191 |> safe_mk_meta_eq))) |
|
192 thy |
|
193 |
|
194 val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) |
|
195 |
|
196 |
|
197 (* setup *) |
|
198 |
|
199 val setup = |
|
200 Attrib.setup @{binding fundef_cong} |
|
201 (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del) |
|
202 "declaration of congruence rule for function definitions" |
|
203 #> setup_case_cong |
|
204 #> FundefRelation.setup |
|
205 #> FundefCommon.Termination_Simps.setup |
|
206 |
|
207 val get_congs = FundefCtxTree.get_fundef_congs |
|
208 |
|
209 |
|
210 (* outer syntax *) |
|
211 |
|
212 local structure P = OuterParse and K = OuterKeyword in |
|
213 |
|
214 val _ = |
|
215 OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal |
|
216 (fundef_parser default_config |
|
217 >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config)); |
|
218 |
|
219 val _ = |
|
220 OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal |
|
221 (Scan.option P.term >> termination_cmd); |
|
222 |
|
223 end; |
|
224 |
|
225 |
|
226 end |
|