|
1 (* Nominal Mutual Functions |
|
2 Author: Christian Urban |
|
3 |
|
4 heavily based on the code of Alexander Krauss |
|
5 (code forked on 14 January 2011) |
|
6 |
|
7 Main entry points to the nominal function package. |
|
8 *) |
|
9 |
|
10 signature NOMINAL_FUNCTION = |
|
11 sig |
|
12 include FUNCTION_DATA |
|
13 |
|
14 val add_nominal_function: (binding * typ option * mixfix) list -> |
|
15 (Attrib.binding * term) list -> Function_Common.function_config -> |
|
16 (Proof.context -> tactic) -> local_theory -> info * local_theory |
|
17 |
|
18 val add_nominal_function_cmd: (binding * string option * mixfix) list -> |
|
19 (Attrib.binding * string) list -> Function_Common.function_config -> |
|
20 (Proof.context -> tactic) -> local_theory -> info * local_theory |
|
21 |
|
22 val nominal_function: (binding * typ option * mixfix) list -> |
|
23 (Attrib.binding * term) list -> Function_Common.function_config -> |
|
24 local_theory -> Proof.state |
|
25 |
|
26 val nominal_function_cmd: (binding * string option * mixfix) list -> |
|
27 (Attrib.binding * string) list -> Function_Common.function_config -> |
|
28 local_theory -> Proof.state |
|
29 |
|
30 val setup : theory -> theory |
|
31 val get_congs : Proof.context -> thm list |
|
32 |
|
33 val get_info : Proof.context -> term -> info |
|
34 end |
|
35 |
|
36 |
|
37 structure Nominal_Function : NOMINAL_FUNCTION = |
|
38 struct |
|
39 |
|
40 open Function_Lib |
|
41 open Function_Common |
|
42 |
|
43 val simp_attribs = map (Attrib.internal o K) |
|
44 [Simplifier.simp_add, |
|
45 Code.add_default_eqn_attribute, |
|
46 Nitpick_Simps.add] |
|
47 |
|
48 val psimp_attribs = map (Attrib.internal o K) |
|
49 [Nitpick_Psimps.add] |
|
50 |
|
51 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
|
52 |
|
53 fun add_simps fnames post sort extra_qualify label mod_binding moreatts |
|
54 simps lthy = |
|
55 let |
|
56 val spec = post simps |
|
57 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
|
58 |> map (apfst (apfst extra_qualify)) |
|
59 |
|
60 val (saved_spec_simps, lthy) = |
|
61 fold_map Local_Theory.note spec lthy |
|
62 |
|
63 val saved_simps = maps snd saved_spec_simps |
|
64 val simps_by_f = sort saved_simps |
|
65 |
|
66 fun add_for_f fname simps = |
|
67 Local_Theory.note |
|
68 ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
|
69 #> snd |
|
70 in |
|
71 (saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
|
72 end |
|
73 |
|
74 (* nominal *) |
|
75 fun prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy = |
|
76 let |
|
77 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
|
78 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
|
79 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
|
80 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
|
81 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
|
82 |
|
83 val defname = mk_defname fixes |
|
84 val FunctionConfig {partials, tailrec, default, ...} = config |
|
85 val _ = |
|
86 if tailrec then Output.legacy_feature |
|
87 "'function (tailrec)' command. Use 'partial_function (tailrec)'." |
|
88 else () |
|
89 val _ = |
|
90 if is_some default then Output.legacy_feature |
|
91 "'function (default)'. Use 'partial_function'." |
|
92 else () |
|
93 |
|
94 val ((goal_state, cont), lthy') = |
|
95 Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy |
|
96 |
|
97 fun afterqed [[proof]] lthy = |
|
98 let |
|
99 val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, |
|
100 termination, domintros, cases, ...} = |
|
101 cont (Thm.close_derivation proof) |
|
102 |
|
103 val fnames = map (fst o fst) fixes |
|
104 fun qualify n = Binding.name n |
|
105 |> Binding.qualify true defname |
|
106 val conceal_partial = if partials then I else Binding.conceal |
|
107 |
|
108 val addsmps = add_simps fnames post sort_cont |
|
109 |
|
110 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
|
111 lthy |
|
112 |> addsmps (conceal_partial o Binding.qualify false "partial") |
|
113 "psimps" conceal_partial psimp_attribs psimps |
|
114 ||> (case trsimps of NONE => I | SOME thms => |
|
115 addsmps I "simps" I simp_attribs thms #> snd |
|
116 #> Spec_Rules.add Spec_Rules.Equational (fs, thms)) |
|
117 ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
|
118 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
|
119 Attrib.internal (K (Rule_Cases.consumes 1)), |
|
120 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
|
121 ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
|
122 ||> (snd o Local_Theory.note ((qualify "cases", |
|
123 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
|
124 ||> (case domintros of NONE => I | SOME thms => |
|
125 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
|
126 |
|
127 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
|
128 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
|
129 fs=fs, R=R, defname=defname, is_partial=true } |
|
130 |
|
131 val _ = |
|
132 if not is_external then () |
|
133 else Specification.print_consts lthy (K false) (map fst fixes) |
|
134 in |
|
135 (info, |
|
136 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
|
137 end |
|
138 in |
|
139 ((goal_state, afterqed), lthy') |
|
140 end |
|
141 |
|
142 fun gen_add_nominal_function is_external prep default_constraint fixspec eqns config tac lthy = |
|
143 let |
|
144 val ((goal_state, afterqed), lthy') = |
|
145 prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy |
|
146 val pattern_thm = |
|
147 case SINGLE (tac lthy') goal_state of |
|
148 NONE => error "pattern completeness and compatibility proof failed" |
|
149 | SOME st => Goal.finish lthy' st |
|
150 in |
|
151 lthy' |
|
152 |> afterqed [[pattern_thm]] |
|
153 end |
|
154 |
|
155 val add_nominal_function = |
|
156 gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
|
157 val add_nominal_function_cmd = gen_add_nominal_function true Specification.read_spec "_::type" |
|
158 |
|
159 fun gen_nominal_function is_external prep default_constraint fixspec eqns config lthy = |
|
160 let |
|
161 val ((goal_state, afterqed), lthy') = |
|
162 prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy |
|
163 in |
|
164 lthy' |
|
165 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
|
166 |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd |
|
167 end |
|
168 |
|
169 val nominal_function = |
|
170 gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
|
171 val nominal_function_cmd = gen_nominal_function true Specification.read_spec "_::type" |
|
172 |
|
173 fun add_case_cong n thy = |
|
174 let |
|
175 val cong = #case_cong (Datatype.the_info thy n) |
|
176 |> safe_mk_meta_eq |
|
177 in |
|
178 Context.theory_map |
|
179 (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy |
|
180 end |
|
181 |
|
182 val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) |
|
183 |
|
184 |
|
185 (* setup *) |
|
186 |
|
187 val setup = |
|
188 Attrib.setup @{binding fundef_cong} |
|
189 (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) |
|
190 "declaration of congruence rule for function definitions" |
|
191 #> setup_case_cong |
|
192 #> Function_Relation.setup |
|
193 #> Function_Common.Termination_Simps.setup |
|
194 |
|
195 val get_congs = Function_Ctx_Tree.get_function_congs |
|
196 |
|
197 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
|
198 |> the_single |> snd |
|
199 |
|
200 |
|
201 (* outer syntax *) |
|
202 |
|
203 (* nominal *) |
|
204 val _ = |
|
205 Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions" |
|
206 Keyword.thy_goal |
|
207 (function_parser default_config |
|
208 >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) |
|
209 |
|
210 |
|
211 end |