223 fun string_for_op2 All = "All" |
221 fun string_for_op2 All = "All" |
224 | string_for_op2 Exist = "Exist" |
222 | string_for_op2 Exist = "Exist" |
225 | string_for_op2 Or = "Or" |
223 | string_for_op2 Or = "Or" |
226 | string_for_op2 And = "And" |
224 | string_for_op2 And = "And" |
227 | string_for_op2 Less = "Less" |
225 | string_for_op2 Less = "Less" |
228 | string_for_op2 Subset = "Subset" |
|
229 | string_for_op2 DefEq = "DefEq" |
226 | string_for_op2 DefEq = "DefEq" |
230 | string_for_op2 Eq = "Eq" |
227 | string_for_op2 Eq = "Eq" |
231 | string_for_op2 Triad = "Triad" |
228 | string_for_op2 Triad = "Triad" |
232 | string_for_op2 Composition = "Composition" |
229 | string_for_op2 Composition = "Composition" |
233 | string_for_op2 Apply = "Apply" |
230 | string_for_op2 Apply = "Apply" |
565 Op2 (Less, bool_T, Any, sub t1, sub t2) |
562 Op2 (Less, bool_T, Any, sub t1, sub t2) |
566 else |
563 else |
567 do_apply t0 ts |
564 do_apply t0 ts |
568 | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)), |
565 | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)), |
569 ts as [t1, t2]) => |
566 ts as [t1, t2]) => |
570 if is_set_like_type (domain_type T) then |
567 if is_built_in_const x then |
571 Op2 (Subset, bool_T, Any, sub t1, sub t2) |
|
572 else if is_built_in_const x then |
|
573 (* FIXME: find out if this case is necessary *) |
568 (* FIXME: find out if this case is necessary *) |
574 Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) |
569 Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) |
575 else |
570 else |
576 do_apply t0 ts |
571 do_apply t0 ts |
577 | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any) |
572 | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any) |
912 let |
907 let |
913 val u1 = sub u1 |
908 val u1 = sub u1 |
914 val u2 = sub u2 |
909 val u2 = sub u2 |
915 val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2]) |
910 val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2]) |
916 in s_op2 Less T R u1 u2 end |
911 in s_op2 Less T R u1 u2 end |
917 | Op2 (Subset, T, _, u1, u2) => |
|
918 let |
|
919 val u1 = sub u1 |
|
920 val u2 = sub u2 |
|
921 val opt = exists (is_opt_rep o rep_of) [u1, u2] |
|
922 val R = bool_rep polar opt |
|
923 in |
|
924 if is_opt_rep R then |
|
925 triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2) |
|
926 else if not opt orelse unsound orelse polar = Neg orelse |
|
927 is_concrete_type data_types true (type_of u1) then |
|
928 s_op2 Subset T R u1 u2 |
|
929 else |
|
930 Cst (False, T, Formula Pos) |
|
931 end |
|
932 | Op2 (DefEq, T, _, u1, u2) => |
912 | Op2 (DefEq, T, _, u1, u2) => |
933 s_op2 DefEq T (Formula Neut) (sub u1) (sub u2) |
913 s_op2 DefEq T (Formula Neut) (sub u1) (sub u2) |
934 | Op2 (Eq, T, _, u1, u2) => |
914 | Op2 (Eq, T, _, u1, u2) => |
935 let |
915 let |
936 val u1' = sub u1 |
916 val u1' = sub u1 |