383 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
383 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
384 val fv_frees = map Free (fv_names ~~ fv_types); |
384 val fv_frees = map Free (fv_names ~~ fv_types); |
385 val nr_bns = non_rec_binds bindsall; |
385 val nr_bns = non_rec_binds bindsall; |
386 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
386 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
387 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
387 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
|
388 val fvbns = map snd bn_fv_bns; |
388 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
389 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
389 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
390 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
390 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
391 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
391 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
392 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
392 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
393 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
546 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
547 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
547 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
548 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
548 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) |
549 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) |
549 (alpha_types @ alpha_bn_types)) [] |
550 (alpha_types @ alpha_bn_types)) [] |
550 (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') |
551 (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') |
|
552 val ordered_fvs = fv_frees @ fvbns; |
|
553 val exported_fvs = map (Morphism.term (ProofContext.export_morphism lthy''' lthy)) ordered_fvs; |
551 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
554 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
552 in |
555 in |
553 ((all_fvs, alphas), lthy''') |
556 (((all_fvs, ordered_fvs), alphas), lthy''') |
554 end |
557 end |
555 *} |
558 *} |
556 |
559 |
557 (* |
560 (* |
558 atom_decl name |
561 atom_decl name |
918 in |
921 in |
919 Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) |
922 Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) |
920 end |
923 end |
921 *} |
924 *} |
922 |
925 |
923 end |
926 ML {* |
|
927 fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x; |
|
928 |
|
929 fun mk_supp_neq arg (fv, alpha) = |
|
930 let |
|
931 val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"}); |
|
932 val ty = fastype_of arg; |
|
933 val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty); |
|
934 val finite = @{term "finite :: atom set \<Rightarrow> bool"} |
|
935 val rhs = collect $ Abs ("a", @{typ atom}, |
|
936 HOLogic.mk_not (finite $ |
|
937 (collect $ Abs ("b", @{typ atom}, |
|
938 HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg))))) |
|
939 in |
|
940 HOLogic.mk_eq (fv $ arg, rhs) |
|
941 end; |
|
942 |
|
943 fun supp_eq fv_alphas_lst = |
|
944 let |
|
945 val (fvs_alphas, ls) = split_list fv_alphas_lst; |
|
946 val (fv_ts, _) = split_list fvs_alphas; |
|
947 val tys = map (domain_type o fastype_of) fv_ts; |
|
948 val names = Datatype_Prop.make_tnames tys; |
|
949 val args = map Free (names ~~ tys); |
|
950 fun supp_eq_arg ((fv, arg), l) = |
|
951 mk_conjl |
|
952 ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) :: |
|
953 (map (mk_supp_neq arg) l)) |
|
954 val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls)) |
|
955 in |
|
956 (names, HOLogic.mk_Trueprop eqs) |
|
957 end |
|
958 *} |
|
959 |
|
960 ML {* |
|
961 fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos = |
|
962 if length fv_ts_bn < length alpha_ts_bn then |
|
963 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) []) |
|
964 else let |
|
965 val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1); |
|
966 fun filter_fn i (x, j) = if j = i then SOME x else NONE; |
|
967 val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos; |
|
968 val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos; |
|
969 in |
|
970 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
|
971 end |
|
972 *} |
|
973 |
|
974 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
|
975 apply (simp add: supp_Abs supp_Pair) |
|
976 apply blast |
|
977 done |
|
978 |
|
979 ML {* |
|
980 fun supp_eq_tac ind fv perm eqiff ctxt = |
|
981 ind_tac ind THEN_ALL_NEW |
|
982 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
|
983 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW |
|
984 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
|
985 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
|
986 simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW |
|
987 simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW |
|
988 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
|
989 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
|
990 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
|
991 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
|
992 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
|
993 simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
994 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
|
995 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
|
996 *} |
|
997 |
|
998 end |