122 FIXME: could insert all constant set expressions, e.g. nat->nat.*) |
122 FIXME: could insert all constant set expressions, e.g. nat->nat.*) |
123 fun data_domain co (rec_tms, con_ty_lists) = |
123 fun data_domain co (rec_tms, con_ty_lists) = |
124 let val rec_hds = map head_of rec_tms |
124 let val rec_hds = map head_of rec_tms |
125 val dummy = assert_all is_Const rec_hds |
125 val dummy = assert_all is_Const rec_hds |
126 (fn t => "Datatype set not previously declared as constant: " ^ |
126 (fn t => "Datatype set not previously declared as constant: " ^ |
127 Sign.string_of_term (sign_of IFOL.thy) t); |
127 Sign.string_of_term IFOL.thy t); |
128 val rec_names = (*nat doesn't have to be added*) |
128 val rec_names = (*nat doesn't have to be added*) |
129 "Nat.nat" :: map (#1 o dest_Const) rec_hds |
129 "Nat.nat" :: map (#1 o dest_Const) rec_hds |
130 val u = if co then quniv else univ |
130 val u = if co then quniv else univ |
131 fun is_OK (Const(a,T)) = not (a mem_string rec_names) |
131 val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) |
132 | is_OK _ = false |
132 (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t |
133 val add_term_consts_2 = |
133 | _ => I)) con_ty_lists []; |
134 foldl_aterms (fn (cs, Const c) => Const c ins cs | (cs, _) => cs); |
|
135 fun fourth (_, name, args, prems) = prems |
|
136 fun add_consts_in_cts cts = |
|
137 Library.foldl (Library.foldl add_term_consts_2) ([], map fourth (List.concat cts)); |
|
138 val cs = List.filter is_OK (add_consts_in_cts con_ty_lists) |
|
139 in u $ union_params (hd rec_tms, cs) end; |
134 in u $ union_params (hd rec_tms, cs) end; |
140 |
135 |
141 |
136 |
142 (*Could go to FOL, but it's hardly general*) |
137 (*Could go to FOL, but it's hardly general*) |
143 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b" |
138 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b" |