214 end |
216 end |
215 |
217 |
216 val unordered = AList.group (op=) (map aux eqs) |
218 val unordered = AList.group (op=) (map aux eqs) |
217 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
219 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
218 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
220 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
219 in |
221 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
220 ordered |
222 in |
|
223 ordered' |
221 end |
224 end |
222 *} |
225 *} |
223 |
226 |
224 ML {* |
227 ML {* |
225 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
228 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
387 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
390 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
388 else raise TEST lthy1 |
391 else raise TEST lthy1 |
389 |
392 |
390 (* definition of raw fv_functions *) |
393 (* definition of raw fv_functions *) |
391 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
394 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
392 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
395 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
393 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
396 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; |
394 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
397 |
395 |
|
396 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
398 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
397 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
399 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
398 val thy = Local_Theory.exit_global lthy2a; |
400 val thy = Local_Theory.exit_global lthy2a; |
399 val thy_name = Context.theory_name thy |
401 val thy_name = Context.theory_name thy |
400 |
402 |
401 val lthy3 = Theory_Target.init NONE thy; |
403 val lthy3 = Theory_Target.init NONE thy; |
402 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
404 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
403 |
405 |
404 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
406 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
405 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp) |
|
406 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
407 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
407 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
408 |
408 |
|
409 val ((fv, fvbn), fv_def, lthy3a) = |
409 val ((fv, fvbn), fv_def, lthy3a) = |
410 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
410 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
411 else raise TEST lthy3 |
411 else raise TEST lthy3 |
412 |
412 |
413 |
413 |