1 theory Equivp

     2 imports "Abs" "Perm" "Tacs" "Rsp"

     3 begin

     4 

     5 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"

     6 by auto

     7 

     8 ML {*

     9 fun supports_tac perm =

    10   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (

    11     REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'

    12     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]

    13       swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh

    14       supp_fset_to_set supp_fmap_atom}))

    15 *}

    16 

    17 ML {*

    18 fun mk_supp ty x =

    19   Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x

    20 *}

    21 

    22 ML {*

    23 fun mk_supports_eq thy cnstr =

    24 let

    25   val (tys, ty) = (strip_type o fastype_of) cnstr

    26   val names = Datatype_Prop.make_tnames tys

    27   val frees = map Free (names ~~ tys)

    28   val rhs = list_comb (cnstr, frees)

    29 

    30   fun mk_supp_arg (x, ty) =

    31     if is_atom thy ty then mk_supp @{typ atom} (mk_atom_ty ty x) else

    32     if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else

    33     if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)

    34     else mk_supp ty x

    35   val lhss = map mk_supp_arg (frees ~~ tys)

    36   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})

    37   val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs)

    38 in

    39   (names, eq)

    40 end

    41 *}

    42 

    43 ML {*

    44 fun prove_supports ctxt perms cnst =

    45 let

    46   val (names, eq) = mk_supports_eq ctxt cnst

    47 in

    48   Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)

    49 end

    50 *}

    51 

    52 ML {*

    53 fun mk_fs tys =

    54 let

    55   val names = Datatype_Prop.make_tnames tys

    56   val frees = map Free (names ~~ tys)

    57   val supps = map2 mk_supp tys frees

    58   val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps

    59 in

    60   (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))

    61 end

    62 *}

    63 

    64 ML {*

    65 fun fs_tac induct supports = rtac induct THEN_ALL_NEW (

    66   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW

    67   asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set

    68     supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})

    69 *}

    70 

    71 ML {*

    72 fun prove_fs ctxt induct supports tys =

    73 let

    74   val (names, eq) = mk_fs tys

    75 in

    76   Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)

    77 end

    78 *}

    79 

    80 ML {*

    81 fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;

    82 

    83 fun mk_supp_neq arg (fv, alpha) =

    84 let

    85   val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});

    86   val ty = fastype_of arg;

    87   val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);

    88   val finite = @{term "finite :: atom set \<Rightarrow> bool"}

    89   val rhs = collect $ Abs ("a", @{typ atom},

    90     HOLogic.mk_not (finite $

    91       (collect $ Abs ("b", @{typ atom},

    92         HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))

    93 in

    94   HOLogic.mk_eq (fv $ arg, rhs)

    95 end;

    96 

    97 fun supp_eq fv_alphas_lst =

    98 let

    99   val (fvs_alphas, ls) = split_list fv_alphas_lst;

   100   val (fv_ts, _) = split_list fvs_alphas;

   101   val tys = map (domain_type o fastype_of) fv_ts;

   102   val names = Datatype_Prop.make_tnames tys;

   103   val args = map Free (names ~~ tys);

   104   fun supp_eq_arg ((fv, arg), l) =

   105     mk_conjl

   106       ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::

   107        (map (mk_supp_neq arg) l))

   108   val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))

   109 in

   110   (names, HOLogic.mk_Trueprop eqs)

   111 end

   112 *}

   113 

   114 ML {*

   115 fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =

   116 if length fv_ts_bn < length alpha_ts_bn then

   117   (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])

   118 else let

   119   val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);

   120   fun filter_fn i (x, j) = if j = i then SOME x else NONE;

   121   val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;

   122   val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;

   123 in

   124   (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all

   125 end

   126 *}

   127 

   128 (* TODO: this is a hack, it assumes that only one type of Abs's is present

   129    in the type and chooses this supp_abs. Additionally single atoms are

   130    treated properly. *)

   131 ML {*

   132 fun choose_alpha_abs eqiff =

   133 let

   134   fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true;

   135   val terms = map prop_of eqiff;

   136   fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms

   137   val no =

   138     if check @{const_name alpha_lst} then 2 else

   139     if check @{const_name alpha_res} then 1 else

   140     if check @{const_name alpha_gen} then 0 else

   141     error "Failure choosing supp_abs"

   142 in

   143   nth @{thms supp_abs[symmetric]} no

   144 end

   145 *}

   146 lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"

   147 by (rule supp_abs(1))

   148 

   149 lemma supp_abs_sum:

   150   "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"

   151   "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"

   152   "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"

   153   apply (simp_all add: supp_abs supp_Pair)

   154   apply blast+

   155   done

   156 

   157 

   158 ML {*

   159 fun supp_eq_tac ind fv perm eqiff ctxt =

   160   rtac ind THEN_ALL_NEW

   161   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW

   162   asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW

   163   asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW

   164   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW

   165   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW

   166   simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW

   167   simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW

   168   simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW

   169   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW

   170   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW

   171   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW

   172   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW

   173   simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW

   174   simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW

   175   simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW

   176   simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW

   177   simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW

   178   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})

   179 *}

   180 

   181 

   182 

   183 

   184 

   185 end