equal
deleted
inserted
replaced
775 end |
775 end |
776 |
776 |
777 fun check_qty qty = if not (is_Type qty) |
777 fun check_qty qty = if not (is_Type qty) |
778 then error "The abstract type must be a type constructor." |
778 then error "The abstract type must be a type constructor." |
779 else () |
779 else () |
780 val config = { notes = true } |
|
781 |
780 |
782 fun setup_quotient () = |
781 fun setup_quotient () = |
783 let |
782 let |
784 val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm |
783 val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm |
785 val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else () |
784 val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else () |
786 val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm |
785 val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm |
787 val _ = check_qty (snd (quot_thm_rty_qty input_thm)) |
786 val _ = check_qty (snd (quot_thm_rty_qty input_thm)) |
788 in |
787 in |
789 setup_by_quotient config input_thm opt_reflp_thm opt_par_thm lthy |> snd |
788 setup_by_quotient default_config input_thm opt_reflp_thm opt_par_thm lthy |> snd |
790 end |
789 end |
791 |
790 |
792 fun setup_typedef () = |
791 fun setup_typedef () = |
793 let |
792 let |
794 val qty = (range_type o fastype_of o hd o get_args 2) input_term |
793 val qty = (range_type o fastype_of o hd o get_args 2) input_term |
797 case opt_reflp_xthm of |
796 case opt_reflp_xthm of |
798 SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." |
797 SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." |
799 | NONE => ( |
798 | NONE => ( |
800 case opt_par_xthm of |
799 case opt_par_xthm of |
801 SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used." |
800 SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used." |
802 | NONE => setup_by_typedef_thm config input_thm lthy |> snd |
801 | NONE => setup_by_typedef_thm default_config input_thm lthy |> snd |
803 ) |
802 ) |
804 end |
803 end |
805 in |
804 in |
806 case input_term of |
805 case input_term of |
807 (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient () |
806 (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient () |