| changeset 20876 | bc2669d5744d |
| parent 20851 | bf80cb83f8be |
| child 21051 | c49467a9c1e1 |
| 20875:95d24e8d117e | 20876:bc2669d5744d |
|---|---|
63 |
63 |
64 (* unfold *) |
64 (* unfold *) |
65 fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x) |
65 fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x) |
66 |
66 |
67 val dest_implies_list = |
67 val dest_implies_list = |
68 split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single) |
68 split_last o (unfold (can Logic.dest_implies) (fst o Logic.dest_implies) (snd o Logic.dest_implies) single) |
69 |
69 |
70 fun implies_elim_swp a b = implies_elim b a |
70 fun implies_elim_swp a b = implies_elim b a |
71 |
71 |
72 fun map3 _ [] [] [] = [] |
72 fun map3 _ [] [] [] = [] |
73 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
73 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
88 |
88 |
89 |
89 |
90 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
90 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
91 fun unordered_pairs [] = [] |
91 fun unordered_pairs [] = [] |
92 | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
92 | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
93 |
|
94 |
|
95 fun the_single [x] = x |
|
96 | the_single _ = sys_error "the_single" |
|
97 |
93 |
98 |
94 |
99 (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *) |
95 (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *) |
100 fun replace_frees assoc = |
96 fun replace_frees assoc = |
101 map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of |
97 map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of |