1438 (t0 as Const (@{const_name Int.number_class.number_of}, |
1438 (t0 as Const (@{const_name Int.number_class.number_of}, |
1439 Type ("fun", [_, ran_T]))) $ t1 => |
1439 Type ("fun", [_, ran_T]))) $ t1 => |
1440 ((if is_number_type thy ran_T then |
1440 ((if is_number_type thy ran_T then |
1441 let |
1441 let |
1442 val j = t1 |> HOLogic.dest_numeral |
1442 val j = t1 |> HOLogic.dest_numeral |
1443 |> ran_T <> int_T ? curry Int.max 0 |
1443 |> ran_T = nat_T ? Integer.max 0 |
1444 val s = numeral_prefix ^ signed_string_of_int j |
1444 val s = numeral_prefix ^ signed_string_of_int j |
1445 in |
1445 in |
1446 if is_integer_type ran_T then |
1446 if is_integer_type ran_T then |
1447 Const (s, ran_T) |
1447 Const (s, ran_T) |
1448 else |
1448 else |
1654 [] => true |
1654 [] => true |
1655 | triples => |
1655 | triples => |
1656 let |
1656 let |
1657 val binders_T = HOLogic.mk_tupleT (binder_types T) |
1657 val binders_T = HOLogic.mk_tupleT (binder_types T) |
1658 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T |
1658 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T |
1659 val j = List.foldl Int.max 0 (map maxidx_of_term intro_ts) + 1 |
1659 val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1 |
1660 val rel = (("R", j), rel_T) |
1660 val rel = (("R", j), rel_T) |
1661 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel :: |
1661 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel :: |
1662 map (wf_constraint_for_triple rel) triples |
1662 map (wf_constraint_for_triple rel) triples |
1663 |> foldr1 s_conj |> HOLogic.mk_Trueprop |
1663 |> foldr1 s_conj |> HOLogic.mk_Trueprop |
1664 val _ = if debug then |
1664 val _ = if debug then |
2920 (* styp -> special -> special -> term *) |
2920 (* styp -> special -> special -> term *) |
2921 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) = |
2921 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) = |
2922 let |
2922 let |
2923 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) |
2923 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) |
2924 val Ts = binder_types T |
2924 val Ts = binder_types T |
2925 val max_j = fold (fold (curry Int.max)) [js1, js2] ~1 |
2925 val max_j = fold (fold Integer.max) [js1, js2] ~1 |
2926 val (eqs, (args1, args2)) = |
2926 val (eqs, (args1, args2)) = |
2927 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) |
2927 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) |
2928 (js1 ~~ ts1, js2 ~~ ts2) of |
2928 (js1 ~~ ts1, js2 ~~ ts2) of |
2929 (SOME t1, SOME t2) => apfst (cons (t1, t2)) |
2929 (SOME t1, SOME t2) => apfst (cons (t1, t2)) |
2930 | (SOME t1, NONE) => apsnd (apsnd (cons t1)) |
2930 | (SOME t1, NONE) => apsnd (apsnd (cons t1)) |