545 case dt'' of |
545 case dt'' of |
546 DtRec k => list_all (map (pair "x") Us, |
546 DtRec k => list_all (map (pair "x") Us, |
547 HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k), |
547 HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k), |
548 T --> HOLogic.boolT) $ free')) :: prems |
548 T --> HOLogic.boolT) $ free')) :: prems |
549 | _ => prems, |
549 | _ => prems, |
550 snd (foldr mk_abs_fun (j', free) Ts) :: ts) |
550 snd (List.foldr mk_abs_fun (j', free) Ts) :: ts) |
551 end; |
551 end; |
552 |
552 |
553 val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs; |
553 val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs; |
554 val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $ |
554 val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $ |
555 list_comb (Const (cname, map fastype_of ts ---> T), ts)) |
555 list_comb (Const (cname, map fastype_of ts ---> T), ts)) |
556 in Logic.list_implies (prems, concl) |
556 in Logic.list_implies (prems, concl) |
557 end; |
557 end; |
558 |
558 |
714 in |
714 in |
715 Const ("Nominal.abs_fun", T --> U --> T --> |
715 Const ("Nominal.abs_fun", T --> U --> T --> |
716 Type ("Nominal.noption", [U])) $ x $ t |
716 Type ("Nominal.noption", [U])) $ x $ t |
717 end; |
717 end; |
718 |
718 |
719 val (ty_idxs, _) = foldl |
719 val (ty_idxs, _) = List.foldl |
720 (fn ((i, ("Nominal.noption", _, _)), p) => p |
720 (fn ((i, ("Nominal.noption", _, _)), p) => p |
721 | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; |
721 | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; |
722 |
722 |
723 fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) |
723 fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) |
724 | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) |
724 | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) |
736 | (i, (s, dts, constrs)) => |
736 | (i, (s, dts, constrs)) => |
737 let |
737 let |
738 val SOME index = AList.lookup op = ty_idxs i; |
738 val SOME index = AList.lookup op = ty_idxs i; |
739 val (constrs1, constrs2) = ListPair.unzip |
739 val (constrs1, constrs2) = ListPair.unzip |
740 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname))) |
740 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname))) |
741 (foldl_map (fn (dts, dt) => |
741 (Library.foldl_map (fn (dts, dt) => |
742 let val (dts', dt') = strip_option dt |
742 let val (dts', dt') = strip_option dt |
743 in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) |
743 in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) |
744 ([], cargs))) constrs) |
744 ([], cargs))) constrs) |
745 in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)), |
745 in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)), |
746 (index, constrs2)) |
746 (index, constrs2)) |
778 (dts ~~ (j upto j + length dts - 1)) |
778 (dts ~~ (j upto j + length dts - 1)) |
779 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts) |
779 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts) |
780 in |
780 in |
781 (j + length dts + 1, |
781 (j + length dts + 1, |
782 xs @ x :: l_args, |
782 xs @ x :: l_args, |
783 foldr mk_abs_fun |
783 List.foldr mk_abs_fun |
784 (case dt of |
784 (case dt of |
785 DtRec k => if k < length new_type_names then |
785 DtRec k => if k < length new_type_names then |
786 Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt --> |
786 Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt --> |
787 typ_of_dtyp descr sorts dt) $ x |
787 typ_of_dtyp descr sorts dt) $ x |
788 else error "nested recursion not (yet) supported" |
788 else error "nested recursion not (yet) supported" |
789 | _ => x) xs :: r_args) |
789 | _ => x) xs :: r_args) |
790 end |
790 end |
791 |
791 |
792 val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs; |
792 val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs; |
793 val abs_name = Sign.intern_const thy ("Abs_" ^ tname); |
793 val abs_name = Sign.intern_const thy ("Abs_" ^ tname); |
794 val rep_name = Sign.intern_const thy ("Rep_" ^ tname); |
794 val rep_name = Sign.intern_const thy ("Rep_" ^ tname); |
795 val constrT = map fastype_of l_args ---> T; |
795 val constrT = map fastype_of l_args ---> T; |
796 val lhs = list_comb (Const (cname, constrT), l_args); |
796 val lhs = list_comb (Const (cname, constrT), l_args); |
797 val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args); |
797 val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args); |
907 (j + length dts + 1, |
907 (j + length dts + 1, |
908 xs @ x :: l_args, |
908 xs @ x :: l_args, |
909 map perm (xs @ [x]) @ r_args) |
909 map perm (xs @ [x]) @ r_args) |
910 end |
910 end |
911 |
911 |
912 val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts; |
912 val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts; |
913 val c = Const (cname, map fastype_of l_args ---> T) |
913 val c = Const (cname, map fastype_of l_args ---> T) |
914 in |
914 in |
915 Goal.prove_global thy8 [] [] |
915 Goal.prove_global thy8 [] [] |
916 (augment_sort thy8 |
916 (augment_sort thy8 |
917 (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom)) |
917 (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom)) |
956 val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts) |
956 val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts) |
957 in |
957 in |
958 (j + length dts + 1, |
958 (j + length dts + 1, |
959 xs @ (x :: args1), ys @ (y :: args2), |
959 xs @ (x :: args1), ys @ (y :: args2), |
960 HOLogic.mk_eq |
960 HOLogic.mk_eq |
961 (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs) |
961 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs) |
962 end; |
962 end; |
963 |
963 |
964 val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts; |
964 val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts; |
965 val Ts = map fastype_of args1; |
965 val Ts = map fastype_of args1; |
966 val c = Const (cname, Ts ---> T) |
966 val c = Const (cname, Ts ---> T) |
967 in |
967 in |
968 Goal.prove_global thy8 [] [] |
968 Goal.prove_global thy8 [] [] |
969 (augment_sort thy8 pt_cp_sort |
969 (augment_sort thy8 pt_cp_sort |
995 val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1); |
995 val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1); |
996 val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; |
996 val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; |
997 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts) |
997 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts) |
998 in |
998 in |
999 (j + length dts + 1, |
999 (j + length dts + 1, |
1000 xs @ (x :: args1), foldr mk_abs_fun x xs :: args2) |
1000 xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2) |
1001 end; |
1001 end; |
1002 |
1002 |
1003 val (_, args1, args2) = foldr process_constr (1, [], []) dts; |
1003 val (_, args1, args2) = List.foldr process_constr (1, [], []) dts; |
1004 val Ts = map fastype_of args1; |
1004 val Ts = map fastype_of args1; |
1005 val c = list_comb (Const (cname, Ts ---> T), args1); |
1005 val c = list_comb (Const (cname, Ts ---> T), args1); |
1006 fun supp t = |
1006 fun supp t = |
1007 Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t; |
1007 Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t; |
1008 fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t; |
1008 fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t; |
1411 |
1411 |
1412 (**** recursion combinator ****) |
1412 (**** recursion combinator ****) |
1413 |
1413 |
1414 val _ = warning "defining recursion combinator ..."; |
1414 val _ = warning "defining recursion combinator ..."; |
1415 |
1415 |
1416 val used = foldr OldTerm.add_typ_tfree_names [] recTs; |
1416 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; |
1417 |
1417 |
1418 val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used; |
1418 val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used; |
1419 |
1419 |
1420 val rec_sort = if null dt_atomTs then HOLogic.typeS else |
1420 val rec_sort = if null dt_atomTs then HOLogic.typeS else |
1421 Sign.certify_sort thy10 pt_cp_sort; |
1421 Sign.certify_sort thy10 pt_cp_sort; |