26 val mk_atom_fset: term -> term |
26 val mk_atom_fset: term -> term |
27 |
27 |
28 val setify: Proof.context -> term -> term |
28 val setify: Proof.context -> term -> term |
29 val listify: Proof.context -> term -> term |
29 val listify: Proof.context -> term -> term |
30 |
30 |
31 (* FIXME: should be here - currently in Nominal2.thy |
|
32 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
31 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
33 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
32 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
34 (term list * thm list * bn_info list * thm list * local_theory) |
33 (term list * thm list * bn_info list * thm list * local_theory) |
35 *) |
34 |
36 |
35 |
37 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> |
36 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> |
38 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
37 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
39 |
38 |
40 val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> |
39 val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> |
53 (* string list - type variables of a datatype |
52 (* string list - type variables of a datatype |
54 binding - name of the datatype |
53 binding - name of the datatype |
55 mixfix - its mixfix |
54 mixfix - its mixfix |
56 (binding * typ list * mixfix) list - datatype constructors of the type |
55 (binding * typ list * mixfix) list - datatype constructors of the type |
57 *) |
56 *) |
58 type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list |
57 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
59 |
58 |
60 |
59 |
61 (* term - is constant of the bn-function |
60 (* term - is constant of the bn-function |
62 int - is datatype number over which the bn-function is defined |
61 int - is datatype number over which the bn-function is defined |
63 int * term option - is number of the corresponding argument with possibly |
62 int * term option - is number of the corresponding argument with possibly |
145 then HOLogic.mk_list @{typ atom} [mk_atom t] |
144 then HOLogic.mk_list @{typ atom} [mk_atom t] |
146 else if is_atom_list ctxt ty |
145 else if is_atom_list ctxt ty |
147 then mk_atom_list t |
146 then mk_atom_list t |
148 else raise TERM ("listify", [t]) |
147 else raise TERM ("listify", [t]) |
149 end |
148 end |
|
149 |
|
150 |
|
151 (** functions that define the raw binding functions **) |
|
152 |
|
153 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or |
|
154 appends of elements; in case of recursive calls it returns also the applied |
|
155 bn function *) |
|
156 fun strip_bn_fun lthy args t = |
|
157 let |
|
158 fun aux t = |
|
159 case t of |
|
160 Const (@{const_name sup}, _) $ l $ r => aux l @ aux r |
|
161 | Const (@{const_name append}, _) $ l $ r => aux l @ aux r |
|
162 | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => |
|
163 (find_index (equal x) args, NONE) :: aux y |
|
164 | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => |
|
165 (find_index (equal x) args, NONE) :: aux y |
|
166 | Const (@{const_name bot}, _) => [] |
|
167 | Const (@{const_name Nil}, _) => [] |
|
168 | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] |
|
169 | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) |
|
170 in |
|
171 aux t |
|
172 end |
|
173 |
|
174 (** definition of the raw binding functions **) |
|
175 |
|
176 fun prep_bn_info lthy dt_names dts bn_funs eqs = |
|
177 let |
|
178 fun process_eq eq = |
|
179 let |
|
180 val (lhs, rhs) = eq |
|
181 |> HOLogic.dest_Trueprop |
|
182 |> HOLogic.dest_eq |
|
183 val (bn_fun, [cnstr]) = strip_comb lhs |
|
184 val (_, ty) = dest_Const bn_fun |
|
185 val (ty_name, _) = dest_Type (domain_type ty) |
|
186 val dt_index = find_index (fn x => x = ty_name) dt_names |
|
187 val (cnstr_head, cnstr_args) = strip_comb cnstr |
|
188 val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) |
|
189 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
|
190 in |
|
191 ((bn_fun, dt_index), (cnstr_name, rhs_elements)) |
|
192 end |
|
193 |
|
194 (* order according to constructor names *) |
|
195 fun cntrs_order ((bn, dt_index), data) = |
|
196 let |
|
197 val dt = nth dts dt_index |
|
198 val cts = (fn (_, _, _, x) => x) dt |
|
199 val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts |
|
200 in |
|
201 (bn, (bn, dt_index, order (op=) ct_names data)) |
|
202 end |
|
203 in |
|
204 eqs |
|
205 |> map process_eq |
|
206 |> AList.group (op=) (* eqs grouped according to bn_functions *) |
|
207 |> map cntrs_order (* inner data ordered according to constructors *) |
|
208 |> order (op=) bn_funs (* ordered according to bn_functions *) |
|
209 end |
|
210 |
|
211 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = |
|
212 if null raw_bn_funs |
|
213 then ([], [], [], [], lthy) |
|
214 else |
|
215 let |
|
216 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
|
217 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
|
218 |
|
219 val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) |
|
220 val {fs, simps, inducts, ...} = info |
|
221 |
|
222 val raw_bn_induct = (the inducts) |
|
223 val raw_bn_eqs = the simps |
|
224 |
|
225 val raw_bn_info = |
|
226 prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs) |
|
227 in |
|
228 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
|
229 end |
|
230 |
150 |
231 |
151 |
232 |
152 (** functions that construct the equations for fv and fv_bn **) |
233 (** functions that construct the equations for fv and fv_bn **) |
153 |
234 |
154 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |
235 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |