11 declare [[STEPS = 9]]

    11 declare [[STEPS = 10]]

    88 

    88 lemma alpha_gen_sym_test:

    89   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 

    90   and     b: "p \<bullet> R = R"

    91   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"

    92   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"

    93   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"

    94   unfolding alphas fresh_star_def

    95   apply(auto simp add:  fresh_minus_perm)

    96   apply(rule_tac p="p" in permute_boolE)

    97   apply(perm_simp add: permute_minus_cancel b)

    98   apply(simp add: a)

    99   apply(rule_tac p="p" in permute_boolE)

   100   apply(perm_simp add: permute_minus_cancel b)

   101   apply(simp add: a)

   102   apply(rule_tac p="p" in permute_boolE)

   103   apply(perm_simp add: permute_minus_cancel b)

   104   apply(simp add: a)

   105   done  

   106 

   107 ML {*

   108 (* for equalities *)

   109 val tac1 = rtac @{thm sym} THEN' atac 

   110 

   111 (* for "unbound" premises *)

   112 val tac2 = atac

   113 

   114 fun trans_prem_tac pred_names ctxt = 

   115   SUBPROOF (fn {prems, context as ctxt, ...} =>

   116     let

   117       val prems' = map (transform_prem1 ctxt pred_names) prems

   118       val _ = tracing ("prems'\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) prems'))

   119     in

   120       print_tac "goal" THEN resolve_tac prems' 1

   121     end) ctxt

   122 

   123 (* for "bound" premises *) 

   124 fun tac3 pred_names ctxt = 

   125   EVERY' [etac @{thm exi_neg},

   126           resolve_tac @{thms alpha_gen_sym_test},

   127           asm_full_simp_tac (HOL_ss addsimps @{thms split_conv permute_prod.simps 

   128                 prod_alpha_def prod_rel.simps alphas}),

   129           Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},

   130           trans_prem_tac pred_names ctxt] 

   131 

   132 fun tac intro pred_names ctxt = 

   133   resolve_tac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3 pred_names ctxt]

   134 *}

   135 

   136 lemma [eqvt]:

   137 shows "p \<bullet> alpha_tkind_raw = alpha_tkind_raw" 

   138 and   "p \<bullet> alpha_ckind_raw = alpha_ckind_raw" 

   139 and   "p \<bullet> alpha_ty_raw = alpha_ty_raw" 

   140 and   "p \<bullet> alpha_ty_lst_raw = alpha_ty_lst_raw" 

   141 and   "p \<bullet> alpha_co_raw = alpha_co_raw" 

   142 and   "p \<bullet> alpha_co_lst_raw = alpha_co_lst_raw"

   143 and   "p \<bullet> alpha_trm_raw = alpha_trm_raw"

   144 and   "p \<bullet> alpha_assoc_lst_raw = alpha_assoc_lst_raw"

   145 and   "p \<bullet> alpha_pat_raw = alpha_pat_raw"

   146 and   "p \<bullet> alpha_vars_raw = alpha_vars_raw"

   147 and   "p \<bullet> alpha_tvars_raw = alpha_tvars_raw"

   148 and   "p \<bullet> alpha_cvars_raw = alpha_cvars_raw"

   149 and   "p \<bullet> alpha_bv_raw = alpha_bv_raw"

   150 and   "p \<bullet> alpha_bv_vs_raw = alpha_bv_vs_raw"

   151 and   "p \<bullet> alpha_bv_tvs_raw = alpha_bv_tvs_raw"

   152 and   "p \<bullet> alpha_bv_cvs_raw = alpha_bv_cvs_raw"

   153 sorry

   154 

   155 lemmas ii = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts

   156 

   157 lemmas ij = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros

   158 

   159 ML {*

   160 val pp = ["CoreHaskel.alpha_tkind_raw", "CoreHaskell.alpha_ckind_raw", "CoreHaskell.alpha_ty_raw", "CoreHaskell.alpha_ty_lst_raw", "CoreHaskell.alpha_co_raw", "CoreHaskell.alpha_co_lst_raw", "CoreHaskell.alpha_trm_raw", "CoreHaskell.alpha_assoc_lst_raw", "CoreHaskell.alpha_pat_raw", "CoreHaskell.alpha_vars_raw", "CoreHaskell.alpha_tvars_raw", "CoreHaskell.alpha_cvars_raw", "CoreHaskell.alpha_bv_raw", "CoreHaskell.alpha_bv_vs_raw", "CoreHaskell.alpha_bv_tvs_raw", "CoreHaskell.alpha_bv_cvs_raw"]

   161 *}

   162 

   163 lemma

   164 shows "alpha_tkind_raw x1 y1 ==> alpha_tkind_raw y1 x1" 

   165 and   "alpha_ckind_raw x2 y2 ==> alpha_ckind_raw y2 x2" 

   166 and   "alpha_ty_raw x3 y3 ==> alpha_ty_raw y3 x3" 

   167 and   "alpha_ty_lst_raw x4 y4 ==> alpha_ty_lst_raw y4 x4" 

   168 and   "alpha_co_raw x5 y5 ==> alpha_co_raw y5 x5" 

   169 and   "alpha_co_lst_raw x6 y6 ==> alpha_co_lst_raw y6 x6"

   170 and   "alpha_trm_raw x7 y7 ==> alpha_trm_raw y7 x7"

   171 and   "alpha_assoc_lst_raw x8 y8 ==> alpha_assoc_lst_raw y8 x8"

   172 and   "alpha_pat_raw x9 y9 ==> alpha_pat_raw y9 x9"

   173 and   "alpha_vars_raw xa ya ==> alpha_vars_raw ya xa"

   174 and   "alpha_tvars_raw xb yb ==> alpha_tvars_raw yb xb"

   175 and   "alpha_cvars_raw xc yc ==> alpha_cvars_raw yc xc"

   176 and   "alpha_bv_raw xd yd ==> alpha_bv_raw yd xd"

   177 and   "alpha_bv_vs_raw xe ye ==> alpha_bv_vs_raw ye xe"

   178 and   "alpha_bv_tvs_raw xf yf ==> alpha_bv_tvs_raw yf xf"

   179 and   "alpha_bv_cvs_raw xg yg ==> alpha_bv_cvs_raw yg xg"

   180 apply(induct rule: ii)

   181 apply(tactic {* tac @{thms ij} pp @{context} 1 *})+

   182 done

   183 

   184 

   185 lemma

   186 alpha_tkind_raw, alpha_ckind_raw, alpha_ty_raw, alpha_ty_lst_raw, alpha_co_raw, alpha_co_lst_raw, alpha_trm_raw, alpha_assoc_lst_raw, alpha_pat_raw, alpha_vars_raw, alpha_tvars_raw, alpha_cvars_raw, alpha_bv_raw, alpha_bv_vs_raw, alpha_bv_tvs_raw, alpha_bv_cvs_raw