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)))) |
881 in |
889 in |
882 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
890 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
883 end |
891 end |
884 *} |
892 *} |
885 |
893 |
886 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
894 (* TODO: this is a hack, it assumes that only one type of Abs's is present |
887 apply (simp add: supp_abs supp_Pair) |
895 in the type and chooses this supp_abs. Additionally single atoms are |
888 apply blast |
896 treated properly. *) |
|
897 ML {* |
|
898 fun choose_alpha_abs eqiff = |
|
899 let |
|
900 fun exists_subterms f ts = true mem (map (exists_subterm f) ts); |
|
901 val terms = map prop_of eqiff; |
|
902 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
|
903 val no = |
|
904 if check @{const_name alpha_lst} then 2 else |
|
905 if check @{const_name alpha_res} then 1 else |
|
906 if check @{const_name alpha_gen} then 0 else |
|
907 error "Failure choosing supp_abs" |
|
908 in |
|
909 nth @{thms supp_abs[symmetric]} no |
|
910 end |
|
911 *} |
|
912 lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" |
|
913 by (rule supp_abs(1)) |
|
914 |
|
915 lemma supp_abs_sum: |
|
916 "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
|
917 "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" |
|
918 "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" |
|
919 apply (simp_all add: supp_abs supp_Pair) |
|
920 apply blast+ |
889 done |
921 done |
|
922 |
890 |
923 |
891 ML {* |
924 ML {* |
892 fun supp_eq_tac ind fv perm eqiff ctxt = |
925 fun supp_eq_tac ind fv perm eqiff ctxt = |
893 rel_indtac ind THEN_ALL_NEW |
926 rel_indtac ind THEN_ALL_NEW |
894 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
927 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
895 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW |
928 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW |
|
929 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
896 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
930 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
897 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
931 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
898 simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW |
932 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
899 simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW |
933 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
900 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
934 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
901 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
935 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
902 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
936 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
903 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
937 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
904 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
938 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
916 fun build_eqvt_gl pi frees fnctn ctxt = |
950 fun build_eqvt_gl pi frees fnctn ctxt = |
917 let |
951 let |
918 val typ = domain_type (fastype_of fnctn); |
952 val typ = domain_type (fastype_of fnctn); |
919 val arg = the (AList.lookup (op=) frees typ); |
953 val arg = the (AList.lookup (op=) frees typ); |
920 in |
954 in |
921 ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
955 ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
922 end |
956 end |
923 *} |
957 *} |
924 |
958 |
925 ML {* |
959 ML {* |
926 fun prove_eqvt tys ind simps funs ctxt = |
960 fun prove_eqvt tys ind simps funs ctxt = |
927 let |
961 let |
928 val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
962 val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
929 val pi = Free (pi, @{typ perm}); |
963 val pi = Free (pi, @{typ perm}); |
930 val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt')) |
964 val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt')) |
931 val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
965 val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
932 val ths = Variable.export ctxt' ctxt ths_loc |
966 val ths = Variable.export ctxt' ctxt ths_loc |
933 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
967 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
934 in |
968 in |
935 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
969 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |