285 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
286 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
286 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
287 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
287 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
288 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
288 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
289 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
289 val thy = Local_Theory.exit_global lthy2; |
290 val thy = Local_Theory.exit_global lthy2; |
|
291 val thy_name = Context.theory_name thy |
290 val lthy3 = Theory_Target.init NONE thy; |
292 val lthy3 = Theory_Target.init NONE thy; |
291 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
293 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
292 |
294 |
293 val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
295 val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
294 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
296 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
301 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
303 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
302 (rel_distinct ~~ alpha_ts_nobn)); |
304 (rel_distinct ~~ alpha_ts_nobn)); |
303 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
305 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
304 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
306 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
305 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
307 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
306 val _ = tracing "Proving equivariance"; |
308 val _ = warning "Proving equivariance"; |
307 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
309 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
308 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
310 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
309 in |
311 fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy |
310 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy6) |
312 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
|
313 val _ = warning "Proving equivalence"; |
|
314 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
|
315 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; |
|
316 val alpha_equivp = |
|
317 build_equivps alpha_ts reflps alpha_induct |
|
318 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
|
319 val qty_binds = map (fn (_, b, _, _) => b) dts; |
|
320 val qty_names = map Name.of_binding qty_binds; |
|
321 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
|
322 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
|
323 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
|
324 val raw_consts = |
|
325 flat (map (fn (i, (_, _, l)) => |
|
326 map (fn (cname, dts) => |
|
327 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
|
328 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
|
329 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
|
330 val _ = warning "Proving respects"; |
|
331 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
|
332 val (bns_rsp_pre, lthy9) = fold_map ( |
|
333 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
|
334 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
|
335 val bns_rsp = flat (map snd bns_rsp_pre); |
|
336 (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*) |
|
337 fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy |
|
338 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
|
339 val (fv_rsp_pre, lthy10) = fold_map |
|
340 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
|
341 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
|
342 val fv_rsp = flat (map snd fv_rsp_pre); |
|
343 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
|
344 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
|
345 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
|
346 (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 |
|
347 fun const_rsp_tac _ = |
|
348 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
|
349 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
|
350 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
|
351 const_rsp_tac) raw_consts lthy11a |
|
352 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
|
353 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
|
354 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
|
355 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
|
356 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
|
357 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
|
358 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
|
359 val _ = warning "Lifting permutations"; |
|
360 val thy = Local_Theory.exit_global lthy12c; |
|
361 val perm_names = map (fn x => "permute_" ^ x) qty_names |
|
362 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
|
363 val lthy13 = Theory_Target.init NONE thy'; |
|
364 val q_name = space_implode "_" qty_names; |
|
365 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
|
366 val _ = warning "Lifting induction"; |
|
367 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
|
368 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct); |
|
369 fun note_suffix s th ctxt = |
|
370 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
|
371 fun note_simp_suffix s th ctxt = |
|
372 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
|
373 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
|
374 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
|
375 val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct |
|
376 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
|
377 val q_perm = map (lift_thm qtys lthy14) raw_perm_def; |
|
378 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
|
379 val q_fv = map (lift_thm qtys lthy15) fv_def; |
|
380 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
|
381 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
|
382 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
|
383 val _ = warning "Lifting eq-iff"; |
|
384 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
|
385 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
|
386 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
|
387 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
|
388 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
|
389 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
|
390 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
|
391 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
|
392 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
|
393 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
|
394 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
|
395 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
|
396 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
|
397 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
|
398 val _ = warning "Supports"; |
|
399 val supports = map (prove_supports lthy20 q_perm) consts; |
|
400 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
|
401 val thy3 = Local_Theory.exit_global lthy20; |
|
402 val _ = warning "Instantiating FS"; |
|
403 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
|
404 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
|
405 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
|
406 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
|
407 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
|
408 val _ = warning "Support Equations"; |
|
409 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; |
|
410 val lthy23 = note_suffix "supp" q_supp lthy22; |
|
411 in |
|
412 (0, lthy23) |
311 end |
413 end |
312 *} |
414 *} |
313 |
415 |
314 section {* Preparing and parsing of the specification *} |
416 section {* Preparing and parsing of the specification *} |
315 |
417 |
537 | "b_fnclauses (S fc) = (b_fnclause fc)" |
642 | "b_fnclauses (S fc) = (b_fnclause fc)" |
538 | "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" |
643 | "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)" |
539 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
644 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
540 | "b_fnclause (K x pat exp) = [atom x]" |
645 | "b_fnclause (K x pat exp) = [atom x]" |
541 |
646 |
542 typ exp_raw |
647 thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn |
543 typ pat_raw |
648 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
544 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
649 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
545 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
650 thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct |
546 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
651 thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm |
547 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps |
|
548 thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros |
|
549 |
652 |
550 nominal_datatype ty = |
653 nominal_datatype ty = |
551 Var "name" |
654 Vr "name" |
552 | Fun "ty" "ty" |
655 | Fn "ty" "ty" |
|
656 and tys = |
|
657 Al xs::"name fset" t::"ty" bind_res xs in t |
|
658 |
|
659 thm ty_tys.fv[simplified ty_tys.supp] |
|
660 thm ty_tys.eq_iff |
|
661 |
|
662 (* some further tests *) |
|
663 |
|
664 nominal_datatype ty = |
|
665 Vr "name" |
|
666 | Fn "ty" "ty" |
553 |
667 |
554 nominal_datatype tys = |
668 nominal_datatype tys = |
555 All xs::"name fset" ty::"ty_raw" bind_res xs in ty |
669 All xs::"name fset" ty::"ty_raw" bind_res xs in ty |
556 thm fv_tys_raw.simps |
|
557 thm alpha_tys_raw.intros |
|
558 thm eqvts |
|
559 |
|
560 (* some further tests *) |
|
561 |
670 |
562 nominal_datatype lam2 = |
671 nominal_datatype lam2 = |
563 Var2 "name" |
672 Var2 "name" |
564 | App2 "lam2" "lam2 list" |
673 | App2 "lam2" "lam2 list" |
565 | Lam2 x::"name" t::"lam2" bind x in t |
674 | Lam2 x::"name" t::"lam2" bind x in t |