824 (ZAppp (proof lev p, Same.commit (proof lev) q) |
824 (ZAppp (proof lev p, Same.commit (proof lev) q) |
825 handle Same.SAME => ZAppp (p, proof lev q)) |
825 handle Same.SAME => ZAppp (p, proof lev q)) |
826 | proof _ _ = raise Same.SAME; |
826 | proof _ _ = raise Same.SAME; |
827 in ZAbsps prems (Same.commit (proof 0) prf) end; |
827 in ZAbsps prems (Same.commit (proof 0) prf) end; |
828 |
828 |
829 fun box_proof zproof_name thy hyps concl prf = |
829 fun box_proof {unconstrain} zproof_name thy hyps concl prf = |
830 let |
830 let |
831 val {zterm, ...} = zterm_cache thy; |
831 val {zterm, ...} = zterm_cache thy; |
832 |
832 |
833 val present_set = Types.build (fold Types.add_atyps hyps #> Types.add_atyps concl); |
833 val present_set = Types.build (fold Types.add_atyps hyps #> Types.add_atyps concl); |
834 val ucontext = Logic.unconstrain_context [] present_set; |
834 val ucontext as {constraints, outer_constraints, ...} = |
835 |
835 Logic.unconstrain_context [] present_set; |
836 val outer_constraints = map (apfst ztyp_of) (#outer_constraints ucontext); |
|
837 val constraints = map (zterm o #2) (#constraints ucontext); |
|
838 |
836 |
839 val typ_operation = #typ_operation ucontext {strip_sorts = true}; |
837 val typ_operation = #typ_operation ucontext {strip_sorts = true}; |
840 val unconstrain_typ = Same.commit typ_operation; |
838 val unconstrain_typ = Same.commit typ_operation; |
841 val unconstrain_ztyp = |
839 val unconstrain_ztyp = |
842 ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)); |
840 ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)); |
843 val unconstrain_zterm = zterm o Term.map_types typ_operation; |
841 val unconstrain_zterm = zterm o Term.map_types typ_operation; |
844 val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp); |
842 val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp); |
845 |
843 |
846 val constrain_instT = |
844 val constrain_instT = |
847 ZTVars.build (present_set |> Types.fold (fn (T, _) => |
845 if unconstrain then ZTVars.empty |
848 let |
846 else |
849 val ZTVar v = ztyp_of (unconstrain_typ T) and U = ztyp_of T; |
847 ZTVars.build (present_set |> Types.fold (fn (T, _) => |
850 val equal = (case U of ZTVar u => u = v | _ => false); |
848 let |
851 in not equal ? ZTVars.add (v, U) end)); |
849 val ZTVar v = ztyp_of (unconstrain_typ T) and U = ztyp_of T; |
|
850 val equal = (case U of ZTVar u => u = v | _ => false); |
|
851 in not equal ? ZTVars.add (v, U) end)); |
852 val constrain_proof = |
852 val constrain_proof = |
853 if ZTVars.is_empty constrain_instT then I |
853 if ZTVars.is_empty constrain_instT then I |
854 else |
854 else |
855 map_proof_types {hyps = true} |
855 map_proof_types {hyps = true} |
856 (subst_type_same (Same.function (ZTVars.lookup constrain_instT))); |
856 (subst_type_same (Same.function (ZTVars.lookup constrain_instT))); |
857 |
857 |
858 val args = map ZClassp outer_constraints @ map (ZHyp o zterm) hyps; |
858 val hyps' = map unconstrain_zterm hyps; |
859 val prems = constraints @ map unconstrain_zterm hyps; |
859 val prems = map (zterm o #2) constraints @ hyps'; |
860 val prop' = beta_norm_term (close_prop prems (unconstrain_zterm concl)); |
860 val prop' = beta_norm_term (close_prop prems (unconstrain_zterm concl)); |
861 val prf' = beta_norm_prooft (close_proof prems (unconstrain_proof prf)); |
861 val prf' = beta_norm_prooft (close_proof prems (unconstrain_proof prf)); |
862 |
862 |
863 val i = serial (); |
863 val i = serial (); |
864 val zbox: zbox = (i, (prop', prf')); |
864 val zbox: zbox = (i, (prop', prf')); |
|
865 |
865 val const = constrain_proof (ZConstp (zproof_const (zproof_name i) prop')); |
866 val const = constrain_proof (ZConstp (zproof_const (zproof_name i) prop')); |
866 in (zbox, ZAppps (const, args)) end; |
867 val args1 = |
|
868 outer_constraints |> map (fn (T, c) => |
|
869 ZClassp (ztyp_of (if unconstrain then unconstrain_typ T else T), c)); |
|
870 val args2 = if unconstrain then map ZHyp hyps' else map (ZHyp o zterm) hyps; |
|
871 in (zbox, ZAppps (ZAppps (const, args1), args2)) end; |
867 |
872 |
868 in |
873 in |
869 |
874 |
870 fun thm_proof thy thm_name = |
875 fun thm_proof thy thm_name = |
871 let |
876 let |
872 val thy_name = Context.theory_long_name thy; |
877 val thy_name = Context.theory_long_name thy; |
873 fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i}; |
878 fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i}; |
874 in box_proof zproof_name thy end; |
879 in box_proof {unconstrain = false} zproof_name thy end; |
875 |
880 |
876 fun add_box_proof {unconstrain} thy hyps concl prf zboxes = |
881 fun add_box_proof unconstrain thy hyps concl prf zboxes = |
877 let |
882 let |
878 (* FIXME unconstrain *) |
883 val (zbox, prf') = box_proof unconstrain ZBox thy hyps concl prf; |
879 val (zbox, prf') = box_proof ZBox thy hyps concl prf; |
|
880 val zboxes' = add_zboxes zbox zboxes; |
884 val zboxes' = add_zboxes zbox zboxes; |
881 in (prf', zboxes') end; |
885 in (prf', zboxes') end; |
882 |
886 |
883 end; |
887 end; |
884 |
888 |