66 fun build_eqvts funs perms simps induct ctxt =

    66 fun build_eqvts bind funs perms simps induct ctxt =

    70   val fv_indnames = Datatype_Prop.make_tnames (map body_type types);

    70   val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));

    71   val args = map Free (fv_indnames ~~ types);

    71   val args = map Free (indnames ~~ types);

    72   val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})

    72   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}

    73   fun eqvtc (fv, (arg, perm)) =

    73   fun eqvtc (fnctn, (arg, perm)) =

    74     HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))

    74     HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))

    76   fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW

    76   fun tac _ = (indtac induct indnames THEN_ALL_NEW

    79   val thm = Goal.prove ctxt ("p" :: fv_indnames) [] gl tac

    79   val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac

    82   Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt

    82   Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt

    87 snd o (build_eqvts [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})

    87 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})

    91 snd o build_eqvts [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}

    91 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}

    92 *}

    92 *}

    93 thm eqvts

    93 

    94 lemma alpha1_eqvt:

    94 ML {*

    95   "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"

    95 fun build_alpha_eqvts funs perms simps induct ctxt =

    96   "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"

    96 let

    97   apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)

    97   val pi = Free ("p", @{typ perm});

    98   apply (simp_all add:eqvts alpha1_inj)

    98   val types = map (domain_type o fastype_of) funs;

    99   apply (tactic {* 

    99   val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));

   100     ALLGOALS (

   100   val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types));

   101       TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   101   val args = map Free (indnames ~~ types);

   102       (etac @{thm alpha_gen_compose_eqvt})

   102   val args2 = map Free (indnames2 ~~ types);

   103     ) *})

   103   fun eqvtc ((alpha, perm), (arg, arg2)) =

   104   apply (simp_all only: eqvts atom_eqvt)

   104     HOLogic.mk_imp (alpha $ arg $ arg2,

   105   done

   105       (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))

   106   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))

   107   fun tac _ = (rtac induct THEN_ALL_NEW

   108     (asm_full_simp_tac (HOL_ss addsimps 

   109       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))

   110     THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   111       (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW

   112     (asm_full_simp_tac (HOL_ss addsimps 

   113       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))

   114 ) 1

   115   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac

   116 in

   117   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)

   118 end

   119 *}

   120 

   121 local_setup {*

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

   123   build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt))

   124 *}

   125 print_theorems

   126 

   127 lemma alpha1_eqvt_proper[eqvt]:

   128   "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"

   129   "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"

   130   apply (simp_all only: eqvts)

   131   apply rule

   132   apply (simp_all add: alpha1_eqvt)

   133   apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"])

   134   apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"])

   135   apply (simp_all only: alpha1_eqvt)

   136   apply rule

   137   apply (simp_all add: alpha1_eqvt)

   138   apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])

   139   apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])

   140   apply (simp_all only: alpha1_eqvt)

   141 done

   147 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]

   183 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted]

   393 

   429 thm alpha_rtrm4_alpha_rtrm4_list.induct

   394 lemma alpha4_eqvt:

   430 

   395   "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)"

   431 local_setup {*

   396   "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"

   432 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}

   397 sorry

   433 *}

   434 print_theorems

   435 

   436 local_setup {*

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

   438   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))

   439 *}

   440 print_theorems