231 | string_for_op2 Subset = "Subset" |
229 | string_for_op2 Subset = "Subset" |
232 | string_for_op2 DefEq = "DefEq" |
230 | string_for_op2 DefEq = "DefEq" |
233 | string_for_op2 Eq = "Eq" |
231 | string_for_op2 Eq = "Eq" |
234 | string_for_op2 Triad = "Triad" |
232 | string_for_op2 Triad = "Triad" |
235 | string_for_op2 Composition = "Composition" |
233 | string_for_op2 Composition = "Composition" |
236 | string_for_op2 Image = "Image" |
|
237 | string_for_op2 Apply = "Apply" |
234 | string_for_op2 Apply = "Apply" |
238 | string_for_op2 Lambda = "Lambda" |
235 | string_for_op2 Lambda = "Lambda" |
239 |
236 |
240 fun string_for_op3 Let = "Let" |
237 fun string_for_op3 Let = "Let" |
241 | string_for_op3 If = "If" |
238 | string_for_op3 If = "If" |
523 Op1 (Converse, range_type T, Any, sub t1) |
520 Op1 (Converse, range_type T, Any, sub t1) |
524 | (Const (@{const_name trancl}, T), [t1]) => |
521 | (Const (@{const_name trancl}, T), [t1]) => |
525 Op1 (Closure, range_type T, Any, sub t1) |
522 Op1 (Closure, range_type T, Any, sub t1) |
526 | (Const (@{const_name rel_comp}, T), [t1, t2]) => |
523 | (Const (@{const_name rel_comp}, T), [t1, t2]) => |
527 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) |
524 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) |
528 | (Const (@{const_name image}, T), [t1, t2]) => |
|
529 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) |
|
530 | (Const (x as (s as @{const_name Suc}, T)), []) => |
525 | (Const (x as (s as @{const_name Suc}, T)), []) => |
531 if is_built_in_const thy stds x then Cst (Suc, T, Any) |
526 if is_built_in_const thy stds x then Cst (Suc, T, Any) |
532 else if is_constr ctxt stds x then do_construct x [] |
527 else if is_constr ctxt stds x then do_construct x [] |
533 else ConstName (s, T, Any) |
528 else ConstName (s, T, Any) |
534 | (Const (@{const_name finite}, T), [t1]) => |
529 | (Const (@{const_name finite}, T), [t1]) => |
934 | (false, false) => non_opt_case () |
929 | (false, false) => non_opt_case () |
935 else |
930 else |
936 Cst (False, T, Formula Pos) |
931 Cst (False, T, Formula Pos) |
937 |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u)) |
932 |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u)) |
938 end |
933 end |
939 | Op2 (Image, T, _, u1, u2) => |
|
940 let |
|
941 val u1' = sub u1 |
|
942 val u2' = sub u2 |
|
943 in |
|
944 (case (rep_of u1', rep_of u2') of |
|
945 (Func (R11, R12), Func (R21, Formula Neut)) => |
|
946 if R21 = R11 andalso is_lone_rep R12 then |
|
947 let |
|
948 val R = |
|
949 best_non_opt_set_rep_for_type scope T |
|
950 |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T |
|
951 in s_op2 Image T R u1' u2' end |
|
952 else |
|
953 raise SAME () |
|
954 | _ => raise SAME ()) |
|
955 handle SAME () => |
|
956 let |
|
957 val T1 = type_of u1 |
|
958 val dom_T = domain_type T1 |
|
959 val ran_T = range_type T1 |
|
960 val x_u = BoundName (~1, dom_T, Any, "image.x") |
|
961 val y_u = BoundName (~2, ran_T, Any, "image.y") |
|
962 in |
|
963 Op2 (Lambda, T, Any, y_u, |
|
964 Op2 (Exist, bool_T, Any, x_u, |
|
965 Op2 (And, bool_T, Any, |
|
966 case u2 of |
|
967 Op2 (Lambda, _, _, u21, u22) => |
|
968 if num_occurrences_in_nut u21 u22 = 0 then |
|
969 u22 |
|
970 else |
|
971 Op2 (Apply, bool_T, Any, u2, x_u) |
|
972 | _ => Op2 (Apply, bool_T, Any, u2, x_u), |
|
973 |
|
974 Op2 (Eq, bool_T, Any, y_u, |
|
975 Op2 (Apply, ran_T, Any, u1, x_u))))) |
|
976 |> sub |
|
977 end |
|
978 end |
|
979 | Op2 (Apply, T, _, u1, u2) => |
934 | Op2 (Apply, T, _, u1, u2) => |
980 let |
935 let |
981 val u1 = sub u1 |
936 val u1 = sub u1 |
982 val u2 = sub u2 |
937 val u2 = sub u2 |
983 val T1 = type_of u1 |
938 val T1 = type_of u1 |