15 (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> |
15 (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> |
16 (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory |
16 (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory |
17 |
17 |
18 val add_nominal_function_cmd: (binding * string option * mixfix) list -> |
18 val add_nominal_function_cmd: (binding * string option * mixfix) list -> |
19 (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> |
19 (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> |
20 (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory |
20 (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory |
21 |
21 |
22 val nominal_function: (binding * typ option * mixfix) list -> |
22 val nominal_function: (binding * typ option * mixfix) list -> |
23 (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> |
23 (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> |
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 local_theory -> Proof.state |
28 bool -> local_theory -> Proof.state |
29 |
29 |
30 val setup : theory -> theory |
30 val setup : theory -> theory |
31 val get_congs : Proof.context -> thm list |
31 val get_congs : Proof.context -> thm list |
32 |
32 |
33 val get_info : Proof.context -> term -> nominal_info |
33 val get_info : Proof.context -> term -> nominal_info |
133 in |
133 in |
134 (saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
134 (saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
135 end |
135 end |
136 |
136 |
137 (* nominal *) |
137 (* nominal *) |
138 fun prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy = |
138 fun prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy = |
139 let |
139 let |
140 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
140 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
141 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
141 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
142 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
142 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
143 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
143 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
179 |
179 |
180 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
180 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
181 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
181 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
183 |
183 |
184 val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes) |
184 val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) |
185 in |
185 in |
186 (info, |
186 (info, |
187 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
187 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
188 end |
188 end |
189 in |
189 in |
190 ((goal_state, afterqed), lthy') |
190 ((goal_state, afterqed), lthy') |
191 end |
191 end |
192 |
192 |
193 fun gen_add_nominal_function is_external prep default_constraint fixspec eqns config tac lthy = |
193 fun gen_add_nominal_function do_print prep default_constraint fixspec eqns config tac lthy = |
194 let |
194 let |
195 val ((goal_state, afterqed), lthy') = |
195 val ((goal_state, afterqed), lthy') = |
196 prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy |
196 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
197 val pattern_thm = |
197 val pattern_thm = |
198 case SINGLE (tac lthy') goal_state of |
198 case SINGLE (tac lthy') goal_state of |
199 NONE => error "pattern completeness and compatibility proof failed" |
199 NONE => error "pattern completeness and compatibility proof failed" |
200 | SOME st => Goal.finish lthy' st |
200 | SOME st => Goal.finish lthy' st |
201 in |
201 in |
203 |> afterqed [[pattern_thm]] |
203 |> afterqed [[pattern_thm]] |
204 end |
204 end |
205 |
205 |
206 val add_nominal_function = |
206 val add_nominal_function = |
207 gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
207 gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
208 val add_nominal_function_cmd = gen_add_nominal_function true Specification.read_spec "_::type" |
208 fun add_nominal_function_cmd a b c d int = |
209 |
209 gen_add_nominal_function int Specification.read_spec "_::type" a b c d |
210 fun gen_nominal_function is_external prep default_constraint fixspec eqns config lthy = |
210 |
|
211 fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy = |
211 let |
212 let |
212 val ((goal_state, afterqed), lthy') = |
213 val ((goal_state, afterqed), lthy') = |
213 prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy |
214 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
214 in |
215 in |
215 lthy' |
216 lthy' |
216 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
217 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
217 |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd |
218 |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd |
218 end |
219 end |
219 |
220 |
220 val nominal_function = |
221 val nominal_function = |
221 gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
222 gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
222 val nominal_function_cmd = gen_nominal_function true Specification.read_spec "_::type" |
223 fun nominal_function_cmd a b c int = |
|
224 gen_nominal_function int Specification.read_spec "_::type" a b c |
|
225 |
223 |
226 |
224 fun add_case_cong n thy = |
227 fun add_case_cong n thy = |
225 let |
228 let |
226 val cong = #case_cong (Datatype.the_info thy n) |
229 val cong = #case_cong (Datatype.the_info thy n) |
227 |> safe_mk_meta_eq |
230 |> safe_mk_meta_eq |