526 Op1 (Converse, range_type T, Any, sub t1) |
526 Op1 (Converse, range_type T, Any, sub t1) |
527 | (Const (@{const_name trancl}, T), [t1]) => |
527 | (Const (@{const_name trancl}, T), [t1]) => |
528 Op1 (Closure, range_type T, Any, sub t1) |
528 Op1 (Closure, range_type T, Any, sub t1) |
529 | (Const (@{const_name rel_comp}, T), [t1, t2]) => |
529 | (Const (@{const_name rel_comp}, T), [t1, t2]) => |
530 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) |
530 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) |
531 | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) => |
531 | (Const (@{const_name prod}, T), [t1, t2]) => |
532 Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2') |
532 Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2) |
533 | (Const (@{const_name image}, T), [t1, t2]) => |
533 | (Const (@{const_name image}, T), [t1, t2]) => |
534 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) |
534 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) |
535 | (Const (x as (s as @{const_name Suc}, T)), []) => |
535 | (Const (x as (s as @{const_name Suc}, T)), []) => |
536 if is_built_in_const thy stds x then Cst (Suc, T, Any) |
536 if is_built_in_const thy stds x then Cst (Suc, T, Any) |
537 else if is_constr ctxt stds x then do_construct x [] |
537 else if is_constr ctxt stds x then do_construct x [] |