511 ((all_fvs, ordered_fvs), lthy'') |
511 ((all_fvs, ordered_fvs), lthy'') |
512 end |
512 end |
513 *} |
513 *} |
514 |
514 |
515 ML {* |
515 ML {* |
516 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
516 fun define_alpha (dt_info : Datatype_Aux.info) bindsall bns fv_frees lthy = |
517 let |
517 let |
518 val thy = ProofContext.theory_of lthy; |
518 val thy = ProofContext.theory_of lthy; |
519 val {descr, sorts, ...} = dt_info; |
519 val {descr, sorts, ...} = dt_info; |
520 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
520 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
521 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
|
522 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
|
523 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
|
524 val fv_frees = map Free (fv_names ~~ fv_types); |
|
525 (* TODO: We need a transitive closure, but instead we do this hack considering |
521 (* TODO: We need a transitive closure, but instead we do this hack considering |
526 all binding functions as recursive or not *) |
522 all binding functions as recursive or not *) |
527 val nr_bns = |
523 val nr_bns = |
528 if (non_rec_binds bindsall) = [] then [] |
524 if (non_rec_binds bindsall) = [] then [] |
529 else map (fn (bn, _, _) => bn) bns; |
525 else map (fn (bn, _, _) => bn) bns; |
530 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
|
531 val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; |
|
532 val fvbns = map snd bn_fv_bns; |
|
533 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
|
534 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
526 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
535 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
527 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
536 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
528 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
537 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
529 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
538 (* We assume that a bn is either recursive or not *) |
530 (* We assume that a bn is either recursive or not *) |
540 val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = |
532 val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = |
541 alpha_bns dt_info alpha_frees bns bns_rec |
533 alpha_bns dt_info alpha_frees bns bns_rec |
542 val alpha_bn_frees = map snd bn_alpha_bns; |
534 val alpha_bn_frees = map snd bn_alpha_bns; |
543 val alpha_bn_types = map fastype_of alpha_bn_frees; |
535 val alpha_bn_types = map fastype_of alpha_bn_frees; |
544 |
536 |
545 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
537 fun alpha_constr ith_dtyp (cname, dts) bindcs = |
546 let |
538 let |
547 val Ts = map (typ_of_dtyp descr sorts) dts; |
539 val Ts = map (typ_of_dtyp descr sorts) dts; |
548 val bindslen = length bindcs |
540 val bindslen = length bindcs |
549 val pi_strs_same = replicate bindslen "pi" |
541 val pi_strs_same = replicate bindslen "pi" |
550 val pi_strs = Name.variant_list [] pi_strs_same; |
542 val pi_strs = Name.variant_list [] pi_strs_same; |
551 val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; |
543 val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; |
552 val bind_pis_gath = bindcs ~~ pis; |
544 val bind_pis_gath = bindcs ~~ pis; |
553 val bind_pis = un_gather_binds_cons bind_pis_gath; |
545 val bind_pis = un_gather_binds_cons bind_pis_gath; |
554 val bindcs = map fst bind_pis; |
|
555 val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); |
546 val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); |
556 val args = map Free (names ~~ Ts); |
547 val args = map Free (names ~~ Ts); |
557 val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); |
548 val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); |
558 val args2 = map Free (names2 ~~ Ts); |
549 val args2 = map Free (names2 ~~ Ts); |
559 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
550 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
560 val fv_c = nth fv_frees ith_dtyp; |
|
561 val alpha = nth alpha_frees ith_dtyp; |
551 val alpha = nth alpha_frees ith_dtyp; |
562 val arg_nos = 0 upto (length dts - 1) |
552 val arg_nos = 0 upto (length dts - 1) |
563 fun fv_bind args (NONE, i, _, _) = |
553 fun fv_bind args (NONE, i, _, _) = |
564 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
554 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
565 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
555 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
567 if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else |
557 if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else |
568 (* TODO goes the code for preiously defined nominal datatypes *) |
558 (* TODO goes the code for preiously defined nominal datatypes *) |
569 @{term "{} :: atom set"} |
559 @{term "{} :: atom set"} |
570 | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) |
560 | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) |
571 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
561 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
572 fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant) |
|
573 fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE |
|
574 | find_nonrec_binder _ _ = NONE |
|
575 fun fv_arg ((dt, x), arg_no) = |
|
576 case get_first (find_nonrec_binder arg_no) bindcs of |
|
577 SOME f => |
|
578 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
|
579 SOME fv_bn => fv_bn $ x |
|
580 | NONE => error "bn specified in a non-rec binding but not in bn list") |
|
581 | NONE => |
|
582 let |
|
583 val arg = |
|
584 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
|
585 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
|
586 if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else |
|
587 if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else |
|
588 (* TODO goes the code for preiously defined nominal datatypes *) |
|
589 @{term "{} :: atom set"}; |
|
590 (* If i = j then we generate it only once *) |
|
591 val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
|
592 val sub = fv_binds_as_set args relevant |
|
593 in |
|
594 mk_diff arg sub |
|
595 end; |
|
596 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
597 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
|
598 val alpha_rhs = |
562 val alpha_rhs = |
599 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
563 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
600 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
564 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
601 let |
565 let |
602 val rel_in_simp_binds = filter (fn ((NONE, i, _, _), _) => i = arg_no | _ => false) bind_pis; |
566 val rel_in_simp_binds = filter (fn ((NONE, i, _, _), _) => i = arg_no | _ => false) bind_pis; |
667 val alpha_lhss = mk_conjl alphas |
631 val alpha_lhss = mk_conjl alphas |
668 val alpha_lhss_ex = |
632 val alpha_lhss_ex = |
669 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
633 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
670 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
634 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
671 in |
635 in |
672 (fv_eq, alpha_eq) |
636 alpha_eq |
673 end; |
637 end; |
674 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
638 fun alpha_eq (i, (_, _, constrs)) binds = map2i (alpha_constr i) constrs binds; |
675 val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) |
639 val alphaeqs = map2i alpha_eq descr (gather_binds bindsall) |
676 val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) |
640 val alpha_eqs = flat alphaeqs |
677 val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; |
|
678 fun filter_fun (_, b) = b mem rel_bns_nos; |
|
679 val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) |
|
680 val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) |
|
681 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
|
682 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
|
683 val fv_names_all = fv_names_fst @ fv_bn_names; |
|
684 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
641 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
685 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
642 val (alphas, lthy') = (Inductive.add_inductive_i |
686 val (fvs, lthy') = (Primrec.add_primrec |
|
687 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
|
688 val (fvs2, lthy'') = |
|
689 if fv_eqs_snd = [] then (([], []), lthy') else |
|
690 (Primrec.add_primrec |
|
691 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') |
|
692 val (alphas, lthy''') = (Inductive.add_inductive_i |
|
693 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
643 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
694 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
644 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
695 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) |
645 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) |
696 (alpha_types @ alpha_bn_types)) [] |
646 (alpha_types @ alpha_bn_types)) [] |
697 (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') |
647 (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy) |
698 val ordered_fvs = fv_frees @ fvbns; |
648 in |
699 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
649 (alphas, lthy') |
700 in |
650 end |
701 (((all_fvs, ordered_fvs), alphas), lthy''') |
651 *} |
702 end |
652 |
703 *} |
653 end |
704 |
|
705 end |
|