author | haftmann |
Wed, 11 Nov 2009 10:06:30 +0100 | |
changeset 33611 | 168b928d5024 |
parent 33099 | b8cdd3d73022 |
child 33855 | cd8acf137c9c |
permissions | -rw-r--r-- |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/fundef_lib.ML |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
4 |
A package for general recursive function definitions. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
Some fairly general functions that should probably go somewhere else... |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
7 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
8 |
structure Function_Lib = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
9 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
10 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
11 |
fun map_option f NONE = NONE |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
12 |
| map_option f (SOME x) = SOME (f x); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
13 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
14 |
fun fold_option f NONE y = y |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
15 |
| fold_option f (SOME x) y = f x y; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
16 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
17 |
fun fold_map_option f NONE y = (NONE, y) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
18 |
| fold_map_option f (SOME x) y = apfst SOME (f x y); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
19 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
20 |
(* Ex: "The variable" ^ plural " is" "s are" vs *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
21 |
fun plural sg pl [x] = sg |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
22 |
| plural sg pl _ = pl |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
23 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
24 |
(* lambda-abstracts over an arbitrarily nested tuple |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
25 |
==> hologic.ML? *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
26 |
fun tupled_lambda vars t = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
27 |
case vars of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
28 |
(Free v) => lambda (Free v) t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
29 |
| (Var v) => lambda (Var v) t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
30 |
| (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs => |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
31 |
(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
32 |
| _ => raise Match |
33611 | 33 |
|
34 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
35 |
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
36 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
37 |
val (n, body) = Term.dest_abs a |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
38 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
39 |
(Free (n, T), body) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
40 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
41 |
| dest_all _ = raise Match |
33611 | 42 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
(* Removes all quantifiers from a term, replacing bound variables by frees. *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
fun dest_all_all (t as (Const ("all",_) $ _)) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
46 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
47 |
val (v,b) = dest_all t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
48 |
val (vs, b') = dest_all_all b |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
50 |
(v :: vs, b') |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
51 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
52 |
| dest_all_all t = ([],t) |
33611 | 53 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
55 |
(* FIXME: similar to Variable.focus *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
56 |
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
57 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
58 |
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
59 |
val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
60 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
61 |
val (n'', body) = Term.dest_abs (n', T, b) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
62 |
val _ = (n' = n'') orelse error "dest_all_ctx" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
63 |
(* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
64 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
val (ctx'', vs, bd) = dest_all_all_ctx ctx' body |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
66 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
(ctx'', (n', T) :: vs, bd) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
68 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
69 |
| dest_all_all_ctx ctx t = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
70 |
(ctx, [], t) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
71 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
72 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
73 |
fun map3 _ [] [] [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
74 |
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
75 |
| map3 _ _ _ _ = raise Library.UnequalLengths; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
76 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
77 |
fun map4 _ [] [] [] [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
78 |
| map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
79 |
| map4 _ _ _ _ _ = raise Library.UnequalLengths; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
fun map6 _ [] [] [] [] [] [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
82 |
| map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
83 |
| map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
84 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
85 |
fun map7 _ [] [] [] [] [] [] [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
86 |
| map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
87 |
| map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
88 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
89 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
90 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
91 |
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
92 |
(* ==> library *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
93 |
fun unordered_pairs [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
94 |
| unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
95 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
96 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
97 |
(* Replaces Frees by name. Works with loose Bounds. *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
98 |
fun replace_frees assoc = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
99 |
map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
100 |
| t => t) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
101 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
102 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
103 |
fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
104 |
| rename_bound n _ = raise Match |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
105 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
106 |
fun mk_forall_rename (n, v) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
107 |
rename_bound n o Logic.all v |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
108 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
109 |
fun forall_intr_rename (n, cv) thm = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
110 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
111 |
val allthm = forall_intr cv thm |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
112 |
val (_ $ abs) = prop_of allthm |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
113 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
114 |
Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
115 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
116 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
117 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
118 |
(* Returns the frees in a term in canonical order, excluding the fixes from the context *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
119 |
fun frees_in_term ctxt t = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
120 |
Term.add_frees t [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
121 |
|> filter_out (Variable.is_fixed ctxt o fst) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
|> rev |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
123 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
124 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
125 |
datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
127 |
fun try_proof cgoal tac = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
128 |
case SINGLE tac (Goal.init cgoal) of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
NONE => Fail |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
| SOME st => |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
131 |
if Thm.no_prems st |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
132 |
then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
133 |
else Stuck st |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
134 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
135 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
136 |
fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
137 |
if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
138 |
| dest_binop_list _ t = [ t ] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
139 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
140 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
141 |
(* separate two parts in a +-expression: |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
142 |
"a + b + c + d + e" --> "(a + b + d) + (c + e)" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
143 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
144 |
Here, + can be any binary operation that is AC. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
145 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
146 |
cn - The name of the binop-constructor (e.g. @{const_name Un}) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
147 |
ac - the AC rewrite rules for cn |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
148 |
is - the list of indices of the expressions that should become the first part |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
149 |
(e.g. [0,1,3] in the above example) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
150 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
151 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
152 |
fun regroup_conv neu cn ac is ct = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
153 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
154 |
val mk = HOLogic.mk_binop cn |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
155 |
val t = term_of ct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
156 |
val xs = dest_binop_list cn t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
157 |
val js = subtract (op =) is (0 upto (length xs) - 1) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
158 |
val ty = fastype_of t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
159 |
val thy = theory_of_cterm ct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
160 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
161 |
Goal.prove_internal [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
162 |
(cterm_of thy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
163 |
(Logic.mk_equals (t, |
33611 | 164 |
if null is |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
165 |
then mk (Const (neu, ty), foldr1 mk (map (nth xs) js)) |
33611 | 166 |
else if null js |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
167 |
then mk (foldr1 mk (map (nth xs) is), Const (neu, ty)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
168 |
else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js))))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
169 |
(K (rewrite_goals_tac ac |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
170 |
THEN rtac Drule.reflexive_thm 1)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
171 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
172 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
173 |
(* instance for unions *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
174 |
fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup} |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
175 |
(map (fn t => t RS eq_reflection) (@{thms Un_ac} @ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
176 |
@{thms Un_empty_right} @ |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
177 |
@{thms Un_empty_left})) t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
178 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
179 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
180 |
end |