557 fun dest_n_tuple 1 t = [t] |
557 fun dest_n_tuple 1 t = [t] |
558 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op :: |
558 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op :: |
559 |
559 |
560 type typedef_info = |
560 type typedef_info = |
561 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, |
561 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, |
562 set_def: thm option, prop_of_Rep: thm, set_name: string, |
562 prop_of_Rep: thm, set_name: string, Abs_inverse: thm option, Rep_inverse: thm option} |
563 Abs_inverse: thm option, Rep_inverse: thm option} |
|
564 |
563 |
565 fun typedef_info ctxt s = |
564 fun typedef_info ctxt s = |
566 if is_frac_type ctxt (Type (s, [])) then |
565 if is_frac_type ctxt (Type (s, [])) then |
567 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, |
566 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, |
568 Abs_name = @{const_name Nitpick.Abs_Frac}, |
567 Abs_name = @{const_name Nitpick.Abs_Frac}, |
569 Rep_name = @{const_name Nitpick.Rep_Frac}, |
568 Rep_name = @{const_name Nitpick.Rep_Frac}, |
570 set_def = NONE, |
|
571 prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"} |
569 prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"} |
572 |> Logic.varify_global, |
570 |> Logic.varify_global, |
573 set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE, |
571 set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE, |
574 Rep_inverse = NONE} |
572 Rep_inverse = NONE} |
575 else case Typedef.get_info ctxt s of |
573 else case Typedef.get_info ctxt s of |
577 we take (according to Florian Haftmann). *) |
575 we take (according to Florian Haftmann). *) |
578 (* The "Logic.varifyT_global" calls are a temporary hack because these |
576 (* The "Logic.varifyT_global" calls are a temporary hack because these |
579 types's type variables sometimes clash with locally fixed type variables. |
577 types's type variables sometimes clash with locally fixed type variables. |
580 Remove these calls once "Typedef" is fully localized. *) |
578 Remove these calls once "Typedef" is fully localized. *) |
581 ({abs_type, rep_type, Abs_name, Rep_name, ...}, |
579 ({abs_type, rep_type, Abs_name, Rep_name, ...}, |
582 {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ => |
580 {Rep, Abs_inverse, Rep_inverse, ...}) :: _ => |
583 SOME {abs_type = Logic.varifyT_global abs_type, |
581 SOME {abs_type = Logic.varifyT_global abs_type, |
584 rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name, |
582 rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name, |
585 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, |
583 Rep_name = Rep_name, prop_of_Rep = prop_of Rep, |
586 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, |
584 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, |
587 Rep_inverse = SOME Rep_inverse} |
585 Rep_inverse = SOME Rep_inverse} |
588 | _ => NONE |
586 | _ => NONE |
589 |
587 |
590 val is_typedef = is_some oo typedef_info |
588 val is_typedef = is_some oo typedef_info |
681 is_integer_like_type T)) |
679 is_integer_like_type T)) |
682 end |
680 end |
683 | is_pure_typedef _ _ = false |
681 | is_pure_typedef _ _ = false |
684 fun is_univ_typedef ctxt (Type (s, _)) = |
682 fun is_univ_typedef ctxt (Type (s, _)) = |
685 (case typedef_info ctxt s of |
683 (case typedef_info ctxt s of |
686 SOME {set_def, prop_of_Rep, ...} => |
684 SOME {prop_of_Rep, ...} => |
687 let |
685 let |
688 val t_opt = |
686 val t_opt = |
689 case set_def of |
687 try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep |
690 SOME thm => try (snd o Logic.dest_equals o prop_of) thm |
|
691 | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) |
|
692 prop_of_Rep |
|
693 in |
688 in |
694 case t_opt of |
689 case t_opt of |
695 SOME (Const (@{const_name top}, _)) => true |
690 SOME (Const (@{const_name top}, _)) => true |
696 (* "Multiset.multiset" *) |
691 (* "Multiset.multiset" *) |
697 | SOME (Const (@{const_name Collect}, _) |
692 | SOME (Const (@{const_name Collect}, _) |