407 ML {* |
407 ML {* |
408 fun bns_same l = |
408 fun bns_same l = |
409 length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1 |
409 length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1 |
410 *} |
410 *} |
411 |
411 |
|
412 ML {* |
|
413 fun setify x = |
|
414 if fastype_of x = @{typ "atom list"} then |
|
415 Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x |
|
416 *} |
|
417 |
412 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
418 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
413 ML {* |
419 ML {* |
414 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
420 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
415 let |
421 let |
416 val thy = ProofContext.theory_of lthy; |
422 val thy = ProofContext.theory_of lthy; |
437 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
443 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
438 val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = |
444 val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = |
439 alpha_bns dt_info alpha_frees bns bns_rec |
445 alpha_bns dt_info alpha_frees bns bns_rec |
440 val alpha_bn_frees = map snd bn_alpha_bns; |
446 val alpha_bn_frees = map snd bn_alpha_bns; |
441 val alpha_bn_types = map fastype_of alpha_bn_frees; |
447 val alpha_bn_types = map fastype_of alpha_bn_frees; |
|
448 |
442 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
449 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
443 let |
450 let |
444 val Ts = map (typ_of_dtyp descr sorts) dts; |
451 val Ts = map (typ_of_dtyp descr sorts) dts; |
445 val bindslen = length bindcs |
452 val bindslen = length bindcs |
446 val pi_strs_same = replicate bindslen "pi" |
453 val pi_strs_same = replicate bindslen "pi" |
462 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
469 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
463 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else |
470 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else |
464 if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else |
471 if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else |
465 (* TODO we do not know what to do with non-atomizable things *) |
472 (* TODO we do not know what to do with non-atomizable things *) |
466 @{term "{} :: atom set"} |
473 @{term "{} :: atom set"} |
467 | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i); |
474 | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) |
468 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
475 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
|
476 fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant) |
469 fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE |
477 fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE |
470 | find_nonrec_binder _ _ = NONE |
478 | find_nonrec_binder _ _ = NONE |
471 fun fv_arg ((dt, x), arg_no) = |
479 fun fv_arg ((dt, x), arg_no) = |
472 case get_first (find_nonrec_binder arg_no) bindcs of |
480 case get_first (find_nonrec_binder arg_no) bindcs of |
473 SOME f => |
481 SOME f => |
483 if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else |
491 if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else |
484 (* TODO we do not know what to do with non-atomizable things *) |
492 (* TODO we do not know what to do with non-atomizable things *) |
485 @{term "{} :: atom set"}; |
493 @{term "{} :: atom set"}; |
486 (* If i = j then we generate it only once *) |
494 (* If i = j then we generate it only once *) |
487 val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
495 val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
488 val sub = fv_binds args relevant |
496 val sub = fv_binds_as_set args relevant |
489 in |
497 in |
490 mk_diff arg sub |
498 mk_diff arg sub |
491 end; |
499 end; |
492 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
500 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
493 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
501 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |