184 Pretty.quote (Syntax.pretty_typ ctxt' qty), |
202 Pretty.quote (Syntax.pretty_typ ctxt' qty), |
185 Pretty.brk 1, |
203 Pretty.brk 1, |
186 Pretty.str "is not a type constructor."]] |
204 Pretty.str "is not a type constructor."]] |
187 val errs = extra_rty_tfrees @ not_type_constr |
205 val errs = extra_rty_tfrees @ not_type_constr |
188 in |
206 in |
189 if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] |
207 if null errs then () else raise QUOT_ERROR errs |
190 @ (map Pretty.string_of errs))) |
208 end |
|
209 handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] |
|
210 @ (map (Pretty.string_of o Pretty.item o single) errs))) |
|
211 end |
|
212 |
|
213 fun lifting_bundle qty_full_name qinfo lthy = |
|
214 let |
|
215 fun qualify suffix defname = Binding.qualified true suffix defname |
|
216 val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting" |
|
217 val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding |
|
218 val bundle_name = Name_Space.full_name (Name_Space.naming_of |
|
219 (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding |
|
220 fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo |
|
221 |
|
222 val thy = Proof_Context.theory_of lthy |
|
223 val dummy_thm = Thm.transfer thy Drule.dummy_thm |
|
224 val pointer = Outer_Syntax.scan Position.none bundle_name |
|
225 val restore_lifting_att = |
|
226 ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)]) |
|
227 in |
|
228 lthy |
|
229 |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
230 (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) |
|
231 |> Bundle.bundle ((binding, [restore_lifting_att])) [] |
191 end |
232 end |
192 |
233 |
193 fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy = |
234 fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy = |
194 let |
235 let |
195 val _ = quot_thm_sanity_check lthy quot_thm |
236 val _ = quot_thm_sanity_check lthy quot_thm |
219 |> define_abs_type gen_code quot_thm |
260 |> define_abs_type gen_code quot_thm |
220 in |
261 in |
221 lthy |
262 lthy |
222 |> Local_Theory.declaration {syntax = false, pervasive = true} |
263 |> Local_Theory.declaration {syntax = false, pervasive = true} |
223 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |
264 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |
|
265 |> lifting_bundle qty_full_name quotients |
224 end |
266 end |
225 |
267 |
226 local |
268 local |
227 fun importT_inst_exclude exclude ts ctxt = |
269 fun importT_inst_exclude exclude ts ctxt = |
228 let |
270 let |
229 val tvars = rev (subtract op= exclude (fold Term.add_tvars ts [])); |
271 val tvars = rev (subtract op= exclude (fold Term.add_tvars ts [])) |
230 val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt; |
272 val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt |
231 in (tvars ~~ map TFree tfrees, ctxt') end |
273 in (tvars ~~ map TFree tfrees, ctxt') end |
232 |
274 |
233 fun import_inst_exclude exclude ts ctxt = |
275 fun import_inst_exclude exclude ts ctxt = |
234 let |
276 let |
235 val excludeT = fold (Term.add_tvarsT o snd) exclude [] |
277 val excludeT = fold (Term.add_tvarsT o snd) exclude [] |
236 val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt; |
278 val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt |
237 val vars = map (apsnd (Term_Subst.instantiateT instT)) |
279 val vars = map (apsnd (Term_Subst.instantiateT instT)) |
238 (rev (subtract op= exclude (fold Term.add_vars ts []))); |
280 (rev (subtract op= exclude (fold Term.add_vars ts []))) |
239 val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'; |
281 val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt' |
240 val inst = vars ~~ map Free (xs ~~ map #2 vars); |
282 val inst = vars ~~ map Free (xs ~~ map #2 vars) |
241 in ((instT, inst), ctxt'') end |
283 in ((instT, inst), ctxt'') end |
242 |
284 |
243 fun import_terms_exclude exclude ts ctxt = |
285 fun import_terms_exclude exclude ts ctxt = |
244 let val (inst, ctxt') = import_inst_exclude exclude ts ctxt |
286 let val (inst, ctxt') = import_inst_exclude exclude ts ctxt |
245 in (map (Term_Subst.instantiate inst) ts, ctxt') end |
287 in (map (Term_Subst.instantiate inst) ts, ctxt') end |
732 "setup lifting infrastructure" |
774 "setup lifting infrastructure" |
733 (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm |
775 (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm |
734 -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> |
776 -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> |
735 (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => |
777 (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => |
736 setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm)) |
778 setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm)) |
737 end; |
779 |
|
780 (* restoring lifting infrastructure *) |
|
781 |
|
782 local |
|
783 exception PCR_ERROR of Pretty.T list |
|
784 in |
|
785 |
|
786 fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) = |
|
787 let |
|
788 val quot_thm = (#quot_thm qinfo) |
|
789 val _ = quot_thm_sanity_check ctxt quot_thm |
|
790 val pcr_info_err = |
|
791 (case #pcr_info qinfo of |
|
792 SOME pcr => |
|
793 let |
|
794 val pcrel_def = #pcrel_def pcr |
|
795 val pcr_cr_eq = #pcr_cr_eq pcr |
|
796 val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def) |
|
797 handle TERM _ => raise PCR_ERROR [Pretty.block |
|
798 [Pretty.str "The pcr definiton theorem is not a plain meta equation:", |
|
799 Pretty.brk 1, |
|
800 Display.pretty_thm ctxt pcrel_def]] |
|
801 val pcr_const_def = head_of def_lhs |
|
802 val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq)) |
|
803 handle TERM _ => raise PCR_ERROR [Pretty.block |
|
804 [Pretty.str "The pcr_cr equation theorem is not a plain equation:", |
|
805 Pretty.brk 1, |
|
806 Display.pretty_thm ctxt pcr_cr_eq]] |
|
807 val (pcr_const_eq, eqs) = strip_comb eq_lhs |
|
808 fun is_eq (Const ("HOL.eq", _)) = true |
|
809 | is_eq _ = false |
|
810 fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2) |
|
811 | eq_Const _ _ = false |
|
812 val all_eqs = if not (forall is_eq eqs) then |
|
813 [Pretty.block |
|
814 [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:", |
|
815 Pretty.brk 1, |
|
816 Display.pretty_thm ctxt pcr_cr_eq]] |
|
817 else [] |
|
818 val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then |
|
819 [Pretty.block |
|
820 [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:", |
|
821 Pretty.brk 1, |
|
822 Syntax.pretty_term ctxt pcr_const_def, |
|
823 Pretty.brk 1, |
|
824 Pretty.str "vs.", |
|
825 Pretty.brk 1, |
|
826 Syntax.pretty_term ctxt pcr_const_eq]] |
|
827 else [] |
|
828 val crel = quot_thm_crel quot_thm |
|
829 val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then |
|
830 [Pretty.block |
|
831 [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:", |
|
832 Pretty.brk 1, |
|
833 Syntax.pretty_term ctxt crel, |
|
834 Pretty.brk 1, |
|
835 Pretty.str "vs.", |
|
836 Pretty.brk 1, |
|
837 Syntax.pretty_term ctxt eq_rhs]] |
|
838 else [] |
|
839 in |
|
840 all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal |
|
841 end |
|
842 | NONE => []) |
|
843 val errs = pcr_info_err |
|
844 in |
|
845 if null errs then () else raise PCR_ERROR errs |
|
846 end |
|
847 handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] |
|
848 @ (map (Pretty.string_of o Pretty.item o single) errs))) |
|
849 end |
|
850 |
|
851 fun lifting_restore qinfo ctxt = |
|
852 let |
|
853 val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo |
|
854 val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo) |
|
855 val qty_full_name = (fst o dest_Type) qty |
|
856 val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name |
|
857 in |
|
858 if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo))) |
|
859 then error (Pretty.string_of |
|
860 (Pretty.block |
|
861 [Pretty.str "Lifting is already setup for the type", |
|
862 Pretty.brk 1, |
|
863 Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)])) |
|
864 else Lifting_Info.update_quotients qty_full_name qinfo ctxt |
|
865 end |
|
866 |
|
867 val parse_opt_pcr = |
|
868 Scan.optional (Attrib.thm -- Attrib.thm >> |
|
869 (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE |
|
870 |
|
871 val lifting_restore_attribute_setup = |
|
872 Attrib.setup @{binding lifting_restore} |
|
873 ((Attrib.thm -- parse_opt_pcr) >> |
|
874 (fn (quot_thm, opt_pcr) => |
|
875 let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr} |
|
876 in Thm.declaration_attribute (K (lifting_restore qinfo)) end)) |
|
877 "restoring lifting infrastructure" |
|
878 |
|
879 val _ = Theory.setup lifting_restore_attribute_setup |
|
880 |
|
881 fun lifting_restore_internal bundle_name ctxt = |
|
882 let |
|
883 val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name |
|
884 in |
|
885 case restore_info of |
|
886 SOME restore_info => |
|
887 ctxt |
|
888 |> lifting_restore (#quotient restore_info) |
|
889 |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info)) |
|
890 | NONE => ctxt |
|
891 end |
|
892 |
|
893 val lifting_restore_internal_attribute_setup = |
|
894 Attrib.setup @{binding lifting_restore_internal} |
|
895 (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name)))) |
|
896 "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users" |
|
897 |
|
898 val _ = Theory.setup lifting_restore_internal_attribute_setup |
|
899 |
|
900 (* lifting_forget *) |
|
901 |
|
902 val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total}, |
|
903 @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}] |
|
904 |
|
905 fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel |
|
906 | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $ |
|
907 (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel |
|
908 | fold_transfer_rel f (Const (name, _) $ rel) = |
|
909 if member op= monotonicity_names name then f rel else f @{term undefined} |
|
910 | fold_transfer_rel f _ = f @{term undefined} |
|
911 |
|
912 fun filter_transfer_rules_by_rel transfer_rel transfer_rules = |
|
913 let |
|
914 val transfer_rel_name = transfer_rel |> dest_Const |> fst; |
|
915 fun has_transfer_rel thm = |
|
916 let |
|
917 val concl = thm |> concl_of |> HOLogic.dest_Trueprop |
|
918 in |
|
919 member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name |
|
920 end |
|
921 handle TERM _ => false |
|
922 in |
|
923 filter has_transfer_rel transfer_rules |
|
924 end |
|
925 |
|
926 type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T} |
|
927 |
|
928 fun get_transfer_rel qinfo = |
|
929 let |
|
930 fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of |
|
931 in |
|
932 if is_some (#pcr_info qinfo) |
|
933 then get_pcrel (#pcrel_def (the (#pcr_info qinfo))) |
|
934 else quot_thm_crel (#quot_thm qinfo) |
|
935 end |
|
936 |
|
937 fun pointer_of_bundle_name bundle_name ctxt = |
|
938 let |
|
939 val bundle_name = Bundle.check ctxt bundle_name |
|
940 val bundle = Bundle.the_bundle ctxt bundle_name |
|
941 in |
|
942 case bundle of |
|
943 [(_, [arg_src])] => |
|
944 (let |
|
945 val ((_, tokens), _) = Args.dest_src arg_src |
|
946 in |
|
947 (fst (Args.name tokens)) |
|
948 handle _ => error "The provided bundle is not a lifting bundle." |
|
949 end) |
|
950 | _ => error "The provided bundle is not a lifting bundle." |
|
951 end |
|
952 |
|
953 fun lifting_forget pointer lthy = |
|
954 let |
|
955 fun get_transfer_rules_to_delete qinfo ctxt = |
|
956 let |
|
957 fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of |
|
958 val transfer_rel = if is_some (#pcr_info qinfo) |
|
959 then get_pcrel (#pcrel_def (the (#pcr_info qinfo))) |
|
960 else quot_thm_crel (#quot_thm qinfo) |
|
961 in |
|
962 filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt) |
|
963 end |
|
964 in |
|
965 case Lifting_Info.lookup_restore_data lthy pointer of |
|
966 SOME restore_info => |
|
967 let |
|
968 val qinfo = #quotient restore_info |
|
969 val quot_thm = #quot_thm qinfo |
|
970 val transfer_rules = get_transfer_rules_to_delete qinfo lthy |
|
971 in |
|
972 Local_Theory.declaration {syntax = false, pervasive = true} |
|
973 (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm)) |
|
974 lthy |
|
975 end |
|
976 | NONE => error "The lifting bundle refers to non-existent restore data." |
|
977 end |
|
978 |
|
979 |
|
980 fun lifting_forget_cmd bundle_name lthy = |
|
981 lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy |
|
982 |
|
983 |
|
984 val _ = |
|
985 Outer_Syntax.local_theory @{command_spec "lifting_forget"} |
|
986 "unsetup Lifting and Transfer for the given lifting bundle" |
|
987 (Parse.position Parse.xname >> (lifting_forget_cmd)) |
|
988 |
|
989 (* lifting_update *) |
|
990 |
|
991 fun update_transfer_rules pointer lthy = |
|
992 let |
|
993 fun new_transfer_rules { quotient = qinfo, ... } lthy = |
|
994 let |
|
995 val transfer_rel = get_transfer_rel qinfo |
|
996 val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy) |
|
997 in |
|
998 fn phi => fold_rev |
|
999 (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules |
|
1000 end |
|
1001 in |
|
1002 case Lifting_Info.lookup_restore_data lthy pointer of |
|
1003 SOME refresh_data => |
|
1004 Local_Theory.declaration {syntax = false, pervasive = true} |
|
1005 (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer |
|
1006 (new_transfer_rules refresh_data lthy phi)) lthy |
|
1007 | NONE => error "The lifting bundle refers to non-existent restore data." |
|
1008 end |
|
1009 |
|
1010 fun lifting_update_cmd bundle_name lthy = |
|
1011 update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy |
|
1012 |
|
1013 val _ = |
|
1014 Outer_Syntax.local_theory @{command_spec "lifting_update"} |
|
1015 "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer" |
|
1016 (Parse.position Parse.xname >> lifting_update_cmd) |
|
1017 |
|
1018 end |