16 

    17 thm eqvts

    18 

    19 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *}

    20 thm weird_inj

    21 

    22 local_setup {*

    23 (fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []),

    24 build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *}

    25 

    26 ML {*

    27 fun is_ex (Const ("Ex", _) $ Abs _) = true

    28   | is_ex _ = false;

    29 *}

    30 

    31 ML {*

    32 fun eetac rule = Subgoal.FOCUS_PARAMS 

    33   (fn (focus) =>

    34      let

    35        val concl = #concl focus

    36        val prems = Logic.strip_imp_prems (term_of concl)

    37        val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems

    38        val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs

    39        val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs

    40      in

    41      (etac rule THEN' RANGE[

    42         atac,

    43         eresolve_tac thins

    44      ]) 1

    45      end

    46   )

    47 *}

    48 

    49 

    50 prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *}

    51 ML_prf {*

    52 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =

    53   ind_tac induct THEN_ALL_NEW

    54   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW

    55   asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW

    56   split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt)

    57   THEN_ALL_NEW split_conjs

    58 *}

    59 

    60 apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj}  @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *})

    61 apply (simp_all)

    62 apply (erule alpha_gen_compose_trans)

    63 apply assumption

    64 apply (simp add: alpha_eqvt)

    65 defer defer

    66 apply (erule alpha_gen_compose_trans)

    67 apply assumption

    68 apply (simp add: alpha_eqvt)

    69 apply (subgoal_tac "pia + pb + (pib + pa) = (pia + pib) + (pb + pa)")

    70 apply simp

    71 apply (erule alpha_gen_compose_trans)

    72 apply assumption

    73 apply (simp add: alpha_eqvt)

    74 sorry

    75