7 Main entry points to the nominal function package. |
7 Main entry points to the nominal function package. |
8 *) |
8 *) |
9 |
9 |
10 signature NOMINAL_FUNCTION = |
10 signature NOMINAL_FUNCTION = |
11 sig |
11 sig |
12 include FUNCTION_DATA |
12 include NOMINAL_FUNCTION_DATA |
13 |
13 |
14 val add_nominal_function: (binding * typ option * mixfix) list -> |
14 val add_nominal_function: (binding * typ option * mixfix) list -> |
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 -> 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 -> info * local_theory |
20 (Proof.context -> tactic) -> 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 |
28 local_theory -> Proof.state |
28 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 -> info |
33 val get_info : Proof.context -> term -> nominal_info |
34 end |
34 end |
35 |
35 |
36 |
36 |
37 structure Nominal_Function : NOMINAL_FUNCTION = |
37 structure Nominal_Function : NOMINAL_FUNCTION = |
38 struct |
38 struct |
150 val ((goal_state, cont), lthy') = |
150 val ((goal_state, cont), lthy') = |
151 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
151 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
152 |
152 |
153 fun afterqed [[proof]] lthy = |
153 fun afterqed [[proof]] lthy = |
154 let |
154 let |
155 val FunctionResult {fs, R, psimps, simple_pinducts, |
155 val NominalFunctionResult {fs, R, psimps, simple_pinducts, |
156 termination, domintros, cases, ...} = |
156 termination, domintros, cases, eqvts, ...} = |
157 cont (Thm.close_derivation proof) |
157 cont (Thm.close_derivation proof) |
|
158 |
|
159 val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps)) |
|
160 val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts)) |
158 |
161 |
159 val fnames = map (fst o fst) fixes |
162 val fnames = map (fst o fst) fixes |
160 fun qualify n = Binding.name n |
163 fun qualify n = Binding.name n |
161 |> Binding.qualify true defname |
164 |> Binding.qualify true defname |
162 val conceal_partial = if partials then I else Binding.conceal |
165 val conceal_partial = if partials then I else Binding.conceal |
177 ||> (case domintros of NONE => I | SOME thms => |
180 ||> (case domintros of NONE => I | SOME thms => |
178 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
181 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
179 |
182 |
180 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
183 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
181 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
184 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
182 fs=fs, R=R, defname=defname, is_partial=true } |
185 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
|
186 |
|
187 val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps')) |
183 |
188 |
184 val _ = |
189 val _ = |
185 if not is_external then () |
190 if not is_external then () |
186 else Specification.print_consts lthy (K false) (map fst fixes) |
191 else Specification.print_consts lthy (K false) (map fst fixes) |
187 in |
192 in |