314 else (Datatab.empty, Theory.check_thy theory) |
314 else (Datatab.empty, Theory.check_thy theory) |
315 | NONE => (Datatab.empty, Theory.check_thy theory) |
315 | NONE => (Datatab.empty, Theory.check_thy theory) |
316 val data = case Datatab.lookup datatab kind |
316 val data = case Datatab.lookup datatab kind |
317 of SOME data => data |
317 of SOME data => data |
318 | NONE => invoke_init kind; |
318 | NONE => invoke_init kind; |
319 val result as (x, data') = f (dest data); |
319 val result as (_, data') = f (dest data); |
320 val _ = Synchronized.change dataref |
320 val _ = Synchronized.change dataref |
321 ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); |
321 ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); |
322 in result end; |
322 in result end; |
323 |
323 |
324 end; (*local*) |
324 end; (*local*) |
358 of SOME ty => ty |
358 of SOME ty => ty |
359 | NONE => (Type.strip_sorts o Sign.the_const_type thy) c; |
359 | NONE => (Type.strip_sorts o Sign.the_const_type thy) c; |
360 |
360 |
361 fun subst_signature thy c ty = |
361 fun subst_signature thy c ty = |
362 let |
362 let |
363 fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) = |
363 fun mk_subst (Type (_, tys1)) (Type (_, tys2)) = |
364 fold2 mk_subst tys1 tys2 |
364 fold2 mk_subst tys1 tys2 |
365 | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty)) |
365 | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty)) |
366 in case lookup_typ thy c |
366 in case lookup_typ thy c |
367 of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty' |
367 of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty' |
368 | NONE => ty |
368 | NONE => ty |
369 end; |
369 end; |
370 |
370 |
405 fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = |
405 fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = |
406 let |
406 let |
407 val _ = if (tyco' : string) <> tyco |
407 val _ = if (tyco' : string) <> tyco |
408 then error "Different type constructors in constructor set" |
408 then error "Different type constructors in constructor set" |
409 else (); |
409 else (); |
410 val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts |
410 val sorts'' = |
411 in ((tyco, sorts), c :: cs) end; |
411 map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts |
|
412 in ((tyco, sorts''), c :: cs) end; |
412 fun inst vs' (c, (vs, ty)) = |
413 fun inst vs' (c, (vs, ty)) = |
413 let |
414 let |
414 val the_v = the o AList.lookup (op =) (vs ~~ vs'); |
415 val the_v = the o AList.lookup (op =) (vs ~~ vs'); |
415 val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty; |
416 val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty; |
416 val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty')); |
417 val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty')); |
437 of SOME (vs, Abstractor spec) => (vs, spec) |
438 of SOME (vs, Abstractor spec) => (vs, spec) |
438 | _ => error ("Not an abstract type: " ^ tyco); |
439 | _ => error ("Not an abstract type: " ^ tyco); |
439 |
440 |
440 fun get_type_of_constr_or_abstr thy c = |
441 fun get_type_of_constr_or_abstr thy c = |
441 case (snd o strip_type o const_typ thy) c |
442 case (snd o strip_type o const_typ thy) c |
442 of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco |
443 of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco |
443 in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end |
444 in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end |
444 | _ => NONE; |
445 | _ => NONE; |
445 |
446 |
446 fun is_constr thy c = case get_type_of_constr_or_abstr thy c |
447 fun is_constr thy c = case get_type_of_constr_or_abstr thy c |
447 of SOME (_, false) => true |
448 of SOME (_, false) => true |
639 in map_filter (fn (((v, i), x), v') => |
640 in map_filter (fn (((v, i), x), v') => |
640 if v = v' andalso i = 0 then NONE |
641 if v = v' andalso i = 0 then NONE |
641 else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) |
642 else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) |
642 end; |
643 end; |
643 |
644 |
644 fun desymbolize_tvars thy thms = |
645 fun desymbolize_tvars thms = |
645 let |
646 let |
646 val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; |
647 val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; |
647 val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs; |
648 val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs; |
648 in map (Thm.certify_instantiate (tvar_subst, [])) thms end; |
649 in map (Thm.certify_instantiate (tvar_subst, [])) thms end; |
649 |
650 |
650 fun desymbolize_vars thy thm = |
651 fun desymbolize_vars thm = |
651 let |
652 let |
652 val vs = Term.add_vars (Thm.prop_of thm) []; |
653 val vs = Term.add_vars (Thm.prop_of thm) []; |
653 val var_subst = mk_desymbolization I I Var vs; |
654 val var_subst = mk_desymbolization I I Var vs; |
654 in Thm.certify_instantiate ([], var_subst) thm end; |
655 in Thm.certify_instantiate ([], var_subst) thm end; |
655 |
656 |
656 fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); |
657 fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars; |
657 |
658 |
658 |
659 |
659 (* abstype certificates *) |
660 (* abstype certificates *) |
660 |
661 |
661 fun check_abstype_cert thy proto_thm = |
662 fun check_abstype_cert thy proto_thm = |
670 handle TERM _ => bad "Not an abstype certificate"; |
671 handle TERM _ => bad "Not an abstype certificate"; |
671 val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c |
672 val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c |
672 then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); |
673 then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); |
673 val _ = check_decl_ty thy (abs, raw_ty); |
674 val _ = check_decl_ty thy (abs, raw_ty); |
674 val _ = check_decl_ty thy (rep, rep_ty); |
675 val _ = check_decl_ty thy (rep, rep_ty); |
675 val var = (fst o dest_Var) param |
676 val _ = (fst o dest_Var) param |
676 handle TERM _ => bad "Not an abstype certificate"; |
677 handle TERM _ => bad "Not an abstype certificate"; |
677 val _ = if param = rhs then () else bad "Not an abstype certificate"; |
678 val _ = if param = rhs then () else bad "Not an abstype certificate"; |
678 val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty); |
679 val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty); |
679 val ty = domain_type ty'; |
680 val ty = domain_type ty'; |
680 val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty')); |
681 val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty')); |
681 val ty_abs = range_type ty'; |
|
682 in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; |
682 in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; |
683 |
683 |
684 |
684 |
685 (* code equation certificates *) |
685 (* code equation certificates *) |
686 |
686 |
714 |> pair subst |
714 |> pair subst |
715 end; |
715 end; |
716 |
716 |
717 fun concretify_abs thy tyco abs_thm = |
717 fun concretify_abs thy tyco abs_thm = |
718 let |
718 let |
719 val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco; |
719 val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco; |
720 val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm |
720 val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm |
721 val ty = fastype_of lhs; |
721 val ty = fastype_of lhs; |
722 val ty_abs = (fastype_of o snd o dest_comb) lhs; |
722 val ty_abs = (fastype_of o snd o dest_comb) lhs; |
723 val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs)); |
723 val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs)); |
724 val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm]; |
724 val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm]; |
744 let |
744 let |
745 val raw_ty = const_typ thy c; |
745 val raw_ty = const_typ thy c; |
746 val tvars = Term.add_tvar_namesT raw_ty []; |
746 val tvars = Term.add_tvar_namesT raw_ty []; |
747 val tvars' = case AxClass.class_of_param thy c |
747 val tvars' = case AxClass.class_of_param thy c |
748 of SOME class => [TFree (Name.aT, [class])] |
748 of SOME class => [TFree (Name.aT, [class])] |
749 | NONE => Name.invent_list [] Name.aT (length tvars) |
749 | NONE => (case get_type_of_constr_or_abstr thy c |
750 |> map (fn v => TFree (v, [])); |
750 of SOME (tyco, _) => map TFree ((fst o the) |
|
751 (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c)) |
|
752 | NONE => Name.invent_list [] Name.aT (length tvars) |
|
753 |> map (fn v => TFree (v, []))); |
751 val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty; |
754 val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty; |
752 val chead = build_head thy (c, ty); |
755 val chead = build_head thy (c, ty); |
753 in Equations (Thm.weaken chead Drule.dummy_thm, []) end; |
756 in Equations (Thm.weaken chead Drule.dummy_thm, []) end; |
754 |
757 |
755 fun cert_of_eqns thy c [] = empty_cert thy c |
758 fun cert_of_eqns thy c [] = empty_cert thy c |
765 val vss = map (tvars_of o snd o head_eqn) thms; |
768 val vss = map (tvars_of o snd o head_eqn) thms; |
766 fun inter_sorts vs = |
769 fun inter_sorts vs = |
767 fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; |
770 fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; |
768 val sorts = map_transpose inter_sorts vss; |
771 val sorts = map_transpose inter_sorts vss; |
769 val vts = Name.names Name.context Name.aT sorts; |
772 val vts = Name.names Name.context Name.aT sorts; |
770 val thms as thm :: _ = |
773 val thms' = |
771 map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms; |
774 map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms; |
772 val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms)))); |
775 val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); |
773 fun head_conv ct = if can Thm.dest_comb ct |
776 fun head_conv ct = if can Thm.dest_comb ct |
774 then Conv.fun_conv head_conv ct |
777 then Conv.fun_conv head_conv ct |
775 else Conv.rewr_conv head_thm ct; |
778 else Conv.rewr_conv head_thm ct; |
776 val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv); |
779 val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv); |
777 val cert_thm = Conjunction.intr_balanced (map rewrite_head thms); |
780 val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); |
778 in Equations (cert_thm, propers) end; |
781 in Equations (cert_thm, propers) end; |
779 |
782 |
780 fun cert_of_proj thy c tyco = |
783 fun cert_of_proj thy c tyco = |
781 let |
784 let |
782 val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco; |
785 val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco; |
783 val _ = if c = rep then () else |
786 val _ = if c = rep then () else |
784 error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep); |
787 error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep); |
785 in Projection (mk_proj tyco vs ty abs rep, tyco) end; |
788 in Projection (mk_proj tyco vs ty abs rep, tyco) end; |
786 |
789 |
787 fun cert_of_abs thy tyco c raw_abs_thm = |
790 fun cert_of_abs thy tyco c raw_abs_thm = |
822 val vs = (fst o fst) (get_head thy cert_thm); |
825 val vs = (fst o fst) (get_head thy cert_thm); |
823 val equations = if null propers then [] else |
826 val equations = if null propers then [] else |
824 Thm.prop_of cert_thm |
827 Thm.prop_of cert_thm |
825 |> Logic.dest_conjunction_balanced (length propers); |
828 |> Logic.dest_conjunction_balanced (length propers); |
826 in (vs, fold (add_rhss_of_eqn thy) equations []) end |
829 in (vs, fold (add_rhss_of_eqn thy) equations []) end |
827 | typargs_deps_of_cert thy (Projection (t, tyco)) = |
830 | typargs_deps_of_cert thy (Projection (t, _)) = |
828 (fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) |
831 (fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) |
829 | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = |
832 | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = |
830 let |
833 let |
831 val vs = fst (typscheme_abs thy abs_thm); |
834 val vs = fst (typscheme_abs thy abs_thm); |
832 val (_, concrete_thm) = concretify_abs thy tyco abs_thm; |
835 val (_, concrete_thm) = concretify_abs thy tyco abs_thm; |
862 fun pretty_cert thy (cert as Equations _) = |
865 fun pretty_cert thy (cert as Equations _) = |
863 (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd) |
866 (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd) |
864 o snd o equations_of_cert thy) cert |
867 o snd o equations_of_cert thy) cert |
865 | pretty_cert thy (Projection (t, _)) = |
868 | pretty_cert thy (Projection (t, _)) = |
866 [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)] |
869 [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)] |
867 | pretty_cert thy (Abstract (abs_thm, tyco)) = |
870 | pretty_cert thy (Abstract (abs_thm, _)) = |
868 [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; |
871 [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; |
869 |
872 |
870 fun bare_thms_of_cert thy (cert as Equations _) = |
873 fun bare_thms_of_cert thy (cert as Equations _) = |
871 (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
874 (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
872 o snd o equations_of_cert thy) cert |
875 o snd o equations_of_cert thy) cert |
1116 val c = const_abs_eqn thy abs_thm; |
1119 val c = const_abs_eqn thy abs_thm; |
1117 in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end; |
1120 in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end; |
1118 |
1121 |
1119 fun del_eqn thm thy = case mk_eqn_liberal thy thm |
1122 fun del_eqn thm thy = case mk_eqn_liberal thy thm |
1120 of SOME (thm, _) => let |
1123 of SOME (thm, _) => let |
1121 fun del_eqn' (Default eqns) = empty_fun_spec |
1124 fun del_eqn' (Default _) = empty_fun_spec |
1122 | del_eqn' (Eqns eqns) = |
1125 | del_eqn' (Eqns eqns) = |
1123 Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns) |
1126 Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns) |
1124 | del_eqn' spec = spec |
1127 | del_eqn' spec = spec |
1125 in change_fun_spec true (const_eqn thy thm) del_eqn' thy end |
1128 in change_fun_spec true (const_eqn thy thm) del_eqn' thy end |
1126 | NONE => thy; |
1129 | NONE => thy; |
1128 fun del_eqns c = change_fun_spec true c (K empty_fun_spec); |
1131 fun del_eqns c = change_fun_spec true c (K empty_fun_spec); |
1129 |
1132 |
1130 |
1133 |
1131 (* cases *) |
1134 (* cases *) |
1132 |
1135 |
1133 fun case_cong thy case_const (num_args, (pos, constrs)) = |
1136 fun case_cong thy case_const (num_args, (pos, _)) = |
1134 let |
1137 let |
1135 val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context; |
1138 val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context; |
1136 val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt; |
1139 val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt; |
1137 val (ws, vs) = chop pos zs; |
1140 val (ws, vs) = chop pos zs; |
1138 val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const); |
1141 val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const); |