24 local_theory -> Proof.state |
24 local_theory -> Proof.state |
25 |
25 |
26 val nominal_function_cmd: (binding * string option * mixfix) list -> |
26 val nominal_function_cmd: (binding * string option * mixfix) list -> |
27 (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> |
27 (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> |
28 bool -> local_theory -> Proof.state |
28 bool -> local_theory -> Proof.state |
29 |
|
30 val setup : theory -> theory |
|
31 val get_congs : Proof.context -> thm list |
|
32 |
29 |
33 val get_info : Proof.context -> term -> nominal_info |
30 val get_info : Proof.context -> term -> nominal_info |
34 end |
31 end |
35 |
32 |
36 |
33 |
104 |
101 |
105 |
102 |
106 val simp_attribs = map (Attrib.internal o K) |
103 val simp_attribs = map (Attrib.internal o K) |
107 [Simplifier.simp_add, |
104 [Simplifier.simp_add, |
108 Code.add_default_eqn_attribute, |
105 Code.add_default_eqn_attribute, |
109 Nitpick_Simps.add] |
106 Named_Theorems.add @{named_theorems nitpick_simp}] |
110 |
107 |
111 val psimp_attribs = map (Attrib.internal o K) |
108 val psimp_attribs = map (Attrib.internal o K) |
112 [Nitpick_Psimps.add] |
109 [Named_Theorems.add @{named_theorems nitpick_psimp}] |
113 |
110 |
114 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
111 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
115 |
112 |
116 fun add_simps fnames post sort extra_qualify label mod_binding moreatts |
113 fun add_simps fnames post sort extra_qualify label mod_binding moreatts |
117 simps lthy = |
114 simps lthy = |
157 cont (Thm.close_derivation proof) |
154 cont (Thm.close_derivation proof) |
158 |
155 |
159 val fnames = map (fst o fst) fixes |
156 val fnames = map (fst o fst) fixes |
160 fun qualify n = Binding.name n |
157 fun qualify n = Binding.name n |
161 |> Binding.qualify true defname |
158 |> Binding.qualify true defname |
162 val conceal_partial = if partials then I else Binding.conceal |
159 val concealed_partial = if partials then I else Binding.concealed |
163 |
160 |
164 val addsmps = add_simps fnames post sort_cont |
161 val addsmps = add_simps fnames post sort_cont |
165 |
162 |
166 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
163 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
167 lthy |
164 lthy |
168 |> addsmps (conceal_partial o Binding.qualify false "partial") |
165 |> addsmps (concealed_partial o Binding.qualify false "partial") |
169 "psimps" conceal_partial psimp_attribs psimps |
166 "psimps" concealed_partial psimp_attribs psimps |
170 ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
167 ||>> Local_Theory.note ((concealed_partial (qualify "pinduct"), |
171 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
168 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
172 Attrib.internal (K (Rule_Cases.consumes 1)), |
169 Attrib.internal (K (Rule_Cases.consumes 1)), |
173 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
170 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
174 ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
171 ||>> Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination]) |
175 ||> (snd o Local_Theory.note ((qualify "cases", |
172 ||> (snd o Local_Theory.note ((qualify "cases", |
176 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
173 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
177 ||> (case domintros of NONE => I | SOME thms => |
174 ||> (case domintros of NONE => I | SOME thms => |
178 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
175 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
179 |
176 |
214 let |
211 let |
215 val ((goal_state, afterqed), lthy') = |
212 val ((goal_state, afterqed), lthy') = |
216 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
213 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
217 in |
214 in |
218 lthy' |
215 lthy' |
219 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
216 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |
220 |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd |
217 |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd |
221 end |
218 end |
222 |
219 |
223 val nominal_function = |
220 val nominal_function = |
224 gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
221 gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
225 fun nominal_function_cmd a b c int = |
222 fun nominal_function_cmd a b c int = |
226 gen_nominal_function int Specification.read_spec "_::type" a b c |
223 gen_nominal_function int Specification.read_spec "_::type" a b c |
227 |
|
228 |
|
229 fun add_case_cong n thy = |
|
230 let |
|
231 val cong = #case_cong (Datatype.the_info thy n) |
|
232 |> safe_mk_meta_eq |
|
233 in |
|
234 Context.theory_map |
|
235 (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy |
|
236 end |
|
237 |
|
238 val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) |
|
239 |
|
240 |
|
241 |
|
242 (* setup *) |
|
243 |
|
244 val setup = |
|
245 Attrib.setup @{binding fundef_cong} |
|
246 (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) |
|
247 "declaration of congruence rule for function definitions" |
|
248 #> setup_case_cong |
|
249 #> Function_Common.Termination_Simps.setup |
|
250 |
|
251 val get_congs = Function_Ctx_Tree.get_function_congs |
|
252 |
224 |
253 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
225 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
254 |> the_single |> snd |
226 |> the_single |> snd |
255 |
227 |
256 |
228 |
273 end |
245 end |
274 |
246 |
275 |
247 |
276 (* nominal *) |
248 (* nominal *) |
277 val _ = |
249 val _ = |
278 Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_function"} |
250 Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function} |
279 "define general recursive nominal functions" |
251 "define general recursive nominal functions" |
280 (nominal_function_parser nominal_default_config |
252 (nominal_function_parser nominal_default_config |
281 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
253 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
282 |
254 |
283 |
255 |