42 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
42 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
43 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
43 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
44 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
44 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
45 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
45 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
46 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
46 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
47 |
47 *} |
48 fun fold_union_env tys trms = fold_rev (curry (mk_union_env tys)) trms @{term "{}::atom set"} |
48 |
49 |
49 ML {* |
50 *} |
50 fun fold_left f [] z = z |
|
51 | fold_left f [x] z = x |
|
52 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
|
53 *} |
|
54 |
|
55 ML {* |
|
56 fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} |
|
57 *} |
|
58 |
|
59 ML {* |
|
60 fold_union_env [] [@{term "t1::atom set"}, @{term "t2::atom set"}, @{term "t3::atom set"}] |
|
61 |> Syntax.string_of_term @{context} |
|
62 |> writeln |
|
63 *} |
|
64 |
|
65 |
51 |
66 |
52 |
67 |
53 ML {* |
68 ML {* |
54 fun process_ecase lthy c (params, prems, concl) bclauses = |
69 fun process_ecase lthy c (params, prems, concl) bclauses = |
55 let |
70 let |