44 | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2 |
44 | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2 |
45 | aux def (t1 $ t2) = aux def t1 andalso aux def t2 |
45 | aux def (t1 $ t2) = aux def t1 andalso aux def t2 |
46 | aux def (t as Const (s, _)) = |
46 | aux def (t as Const (s, _)) = |
47 (not def orelse t <> @{const Suc}) andalso |
47 (not def orelse t <> @{const Suc}) andalso |
48 not (member (op =) |
48 not (member (op =) |
49 [@{const_name Nitpick.Abs_Frac}, @{const_name Nitpick.Rep_Frac}, |
49 [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
50 @{const_name Nitpick.nat_gcd}, @{const_name Nitpick.nat_lcm}, |
50 @{const_name nat_gcd}, @{const_name nat_lcm}, |
51 @{const_name Nitpick.Frac}, @{const_name Nitpick.norm_frac}] s) |
51 @{const_name Frac}, @{const_name norm_frac}] s) |
52 | aux def (Abs (_, _, t')) = aux def t' |
52 | aux def (Abs (_, _, t')) = aux def t' |
53 | aux _ _ = true |
53 | aux _ _ = true |
54 in aux end |
54 in aux end |
55 val should_use_binary_ints = |
55 val should_use_binary_ints = |
56 let |
56 let |
1053 |
1053 |
1054 (** Simplification of constructor/selector terms **) |
1054 (** Simplification of constructor/selector terms **) |
1055 |
1055 |
1056 fun simplify_constrs_and_sels ctxt t = |
1056 fun simplify_constrs_and_sels ctxt t = |
1057 let |
1057 let |
1058 fun is_nth_sel_on t' n (Const (s, _) $ t) = |
1058 fun is_nth_sel_on constr_s t' n (Const (s, _) $ t) = |
1059 (t = t' andalso is_sel_like_and_no_discr s andalso |
1059 (t = t' andalso is_sel_like_and_no_discr s andalso |
1060 sel_no_from_name s = n) |
1060 constr_name_for_sel_like s = constr_s andalso sel_no_from_name s = n) |
1061 | is_nth_sel_on _ _ _ = false |
1061 | is_nth_sel_on _ _ _ _ = false |
1062 fun do_term (Const (@{const_name Nitpick.Rep_Frac}, _) |
1062 fun do_term (Const (@{const_name Rep_Frac}, _) |
1063 $ (Const (@{const_name Nitpick.Abs_Frac}, _) $ t1)) [] = |
1063 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = |
1064 do_term t1 [] |
1064 do_term t1 [] |
1065 | do_term (Const (@{const_name Nitpick.Abs_Frac}, _) |
1065 | do_term (Const (@{const_name Abs_Frac}, _) |
1066 $ (Const (@{const_name Nitpick.Rep_Frac}, _) $ t1)) [] = |
1066 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = |
1067 do_term t1 [] |
1067 do_term t1 [] |
1068 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) |
1068 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) |
1069 | do_term (t as Const (x as (s, T))) (args as _ :: _) = |
1069 | do_term (t as Const (x as (s, T))) (args as _ :: _) = |
1070 ((if is_nonfree_constr ctxt x then |
1070 ((if is_nonfree_constr ctxt x then |
1071 if length args = num_binder_types T then |
1071 if length args = num_binder_types T then |
1072 case hd args of |
1072 case hd args of |
1073 Const (_, T') $ t' => |
1073 Const (_, T') $ t' => |
1074 if domain_type T' = body_type T andalso |
1074 if domain_type T' = body_type T andalso |
1075 forall (uncurry (is_nth_sel_on t')) |
1075 forall (uncurry (is_nth_sel_on s t')) |
1076 (index_seq 0 (length args) ~~ args) then |
1076 (index_seq 0 (length args) ~~ args) then |
1077 t' |
1077 t' |
1078 else |
1078 else |
1079 raise SAME () |
1079 raise SAME () |
1080 | _ => raise SAME () |
1080 | _ => raise SAME () |