233 | string_for_op2 Subset = "Subset" |
231 | string_for_op2 Subset = "Subset" |
234 | string_for_op2 DefEq = "DefEq" |
232 | string_for_op2 DefEq = "DefEq" |
235 | string_for_op2 Eq = "Eq" |
233 | string_for_op2 Eq = "Eq" |
236 | string_for_op2 Triad = "Triad" |
234 | string_for_op2 Triad = "Triad" |
237 | string_for_op2 Composition = "Composition" |
235 | string_for_op2 Composition = "Composition" |
238 | string_for_op2 Product = "Product" |
|
239 | string_for_op2 Image = "Image" |
236 | string_for_op2 Image = "Image" |
240 | string_for_op2 Apply = "Apply" |
237 | string_for_op2 Apply = "Apply" |
241 | string_for_op2 Lambda = "Lambda" |
238 | string_for_op2 Lambda = "Lambda" |
242 |
239 |
243 fun string_for_op3 Let = "Let" |
240 fun string_for_op3 Let = "Let" |
526 Op1 (Converse, range_type T, Any, sub t1) |
523 Op1 (Converse, range_type T, Any, sub t1) |
527 | (Const (@{const_name trancl}, T), [t1]) => |
524 | (Const (@{const_name trancl}, T), [t1]) => |
528 Op1 (Closure, range_type T, Any, sub t1) |
525 Op1 (Closure, range_type T, Any, sub t1) |
529 | (Const (@{const_name rel_comp}, T), [t1, t2]) => |
526 | (Const (@{const_name rel_comp}, T), [t1, t2]) => |
530 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) |
527 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) |
531 | (Const (@{const_name prod}, T), [t1, t2]) => |
|
532 Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2) |
|
533 | (Const (@{const_name image}, T), [t1, t2]) => |
528 | (Const (@{const_name image}, T), [t1, t2]) => |
534 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) |
529 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) |
535 | (Const (x as (s as @{const_name Suc}, T)), []) => |
530 | (Const (x as (s as @{const_name Suc}, T)), []) => |
536 if is_built_in_const thy stds x then Cst (Suc, T, Any) |
531 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 [] |
532 else if is_constr ctxt stds x then do_construct x [] |