221 in |
221 in |
222 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
222 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
223 end |
223 end |
224 *} |
224 *} |
225 |
225 |
226 |
226 ML {* val restricted_nominal=ref true *} |
227 ML {* |
227 |
|
228 ML {* |
228 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
229 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
229 let |
230 let |
230 val thy = ProofContext.theory_of lthy |
231 val thy = ProofContext.theory_of lthy |
231 val thy_name = Context.theory_name thy |
232 val thy_name = Context.theory_name thy |
232 val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) = |
233 val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) = |
265 val alpha_intros = #intrs alpha; |
266 val alpha_intros = #intrs alpha; |
266 val alpha_cases_loc = #elims alpha |
267 val alpha_cases_loc = #elims alpha |
267 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
268 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
268 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
269 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
269 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
270 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
270 (* val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
271 in |
|
272 if !restricted_nominal then |
|
273 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
|
274 else |
|
275 let |
|
276 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
271 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
277 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
272 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
278 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
|
279 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
|
280 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
273 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
281 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
274 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
282 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
275 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
283 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
276 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
284 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
277 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
285 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
323 val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
331 val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
324 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
332 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
325 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
333 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
326 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
334 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
327 val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; |
335 val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; |
328 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;*) |
336 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
329 in |
337 val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt; |
330 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
338 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
331 end |
339 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
332 *} |
340 in |
333 ML fold |
341 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) |
334 ML name_of_typ |
342 end |
|
343 end |
|
344 *} |
335 |
345 |
336 ML {* |
346 ML {* |
337 (* parsing the datatypes and declaring *) |
347 (* parsing the datatypes and declaring *) |
338 (* constructors in the local theory *) |
348 (* constructors in the local theory *) |
339 fun prepare_dts dt_strs lthy = |
349 fun prepare_dts dt_strs lthy = |