194   val rule = Drule.instantiate' [] [SOME pi] @{thm permute_boolE}

   217   val thy = ProofContext.theory_of ctxt

   218   val cpi = Thm.cterm_of thy (mk_minus pi)

   219   val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE}

   211 fun eqvt_rel_tac pred_name = 

   236 fun prepare_pred params_no pi pred =

   237 let

   238   val (c, xs) = strip_comb pred;

   239   val (xs1, xs2) = chop params_no xs

   240 in

   241   HOLogic.mk_imp 

   242     (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))

   243 end

   244 *}

   245 

   246 ML {*

   247 fun transp ([] :: _) = []

   248   | transp xs = map hd xs :: transp (map tl xs);

   249 *}

   250 

   251 ML {* 

   252   Local_Theory.note;

   253   Local_Theory.notes;

   254   fold_map

   255 *}

   256 

   257 ML {*

   258 fun note_named_thm (name, thm) ctxt = 

   259 let

   260   val thm_name = Binding.qualified_name 

   261     (Long_Name.qualify (Long_Name.base_name name) "eqvt")

   262   val attr = Attrib.internal (K eqvt_add)

   263 in

   264   Local_Theory.note ((thm_name, [attr]), [thm]) ctxt

   265 end

   266 *}

   267 

   268 ML {*

   269 fun eqvt_rel_tac pred_name ctxt = 

   216   val param_no = length (Inductive.params_of raw_induct)

   274   val raw_induct = atomize_induct ctxt raw_induct;

   217   val (([raw_concl], [pi]), ctxt') = 

   275   val intros = map atomize_intr intrs;

   276   val params_no = length (Inductive.params_of raw_induct)

   277   val (([raw_concl], [raw_pi]), ctxt') = 

   219          ||>> Variable.variant_fixes ["pi"];

   279          ||>> Variable.variant_fixes ["pi"]

   280   val pi = Free (raw_pi, @{typ perm})

   222 in

   283   val goal = HOLogic.mk_Trueprop 

   223 

   284     (foldr1 HOLogic.mk_conj (map (prepare_pred params_no pi) preds))

   224 end

   285   val thm = Goal.prove ctxt' [] [] goal (fn {context,...} => 

   225 *}

   286     HEADGOAL (EVERY' (rtac raw_induct :: map (single_case_tac context names pi) intros)))

   226 

   287     |> singleton (ProofContext.export ctxt' ctxt)

   227 

   288   val thms = map (fn th => zero_var_indexes (th RS mp)) (Datatype_Aux.split_conj_thm thm)

   228 

   289 in

   229 lemma [eqvt]:

   290    ctxt |> fold_map note_named_thm (names ~~ thms)

   230   assumes a: "valid Gamma" 

   291         |> snd

   231   shows "valid (p \<bullet> Gamma)"

   292 end

   232 using a

   293 *}

   233 apply(induct)

   294 

   234 apply(tactic {* my_tac @{context} ["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(1)} 1 *})

   295 

   235 apply(tactic {* my_tac @{context }["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(2)} 1 *})

   296 ML {*

   236 done

   297 local structure P = OuterParse and K = OuterKeyword in

   237 

   298 

   238 lemma 

   299 val _ =

   239   shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"

   300   OuterSyntax.local_theory "equivariance"

   240 ML_prf {*

   301     "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl

   241 val ({names, ...}, {raw_induct, ...}) =

   302     (P.xname >> eqvt_rel_tac);

   242       Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")

   303 

   243 *}

   304 end;

   244 apply(tactic {* rtac raw_induct 1 *})

   305 *}

   245 apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(1)} 1 *})

   306 

   246 apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(2)} 1 *})

   307 equivariance valid

   247 apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(3)} 1 *})

   308 equivariance typing

   248 done

   309 

   249 

   310 thm valid.eqvt

   250 lemma uu[eqvt]:

   311 thm typing.eqvt

   251   assumes a: "Gamma \<turnstile> t : T" 

   252   shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"

   253 using a

   254 apply(induct)

   255 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})

   256 apply(perm_strict_simp)

   257 apply(rule typing.intros)

   258 apply(rule conj_mono[THEN mp])

   259 prefer 3

   260 apply(assumption)

   261 apply(rule impI)

   262 prefer 2

   263 apply(rule impI)

   264 apply(simp)

   265 apply(auto)[1]

   266 apply(simp)

   267 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})

   268 done

   269 

   270 (*

   271 inductive

   272   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 

   273 where

   274     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

   275   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"

   276   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"

   277 

   278 lemma uu[eqvt]:

   279   assumes a: "Gamma \<turnstile> t : T" 

   280   shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"

   281 using a

   282 apply(induct)

   283 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})

   284 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})

   285 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})

   286 done

   287 *)

   288 

   289 ML {*

   290 val inductive_atomize = @{thms induct_atomize};

   291 

   292 val atomize_conv =

   293   MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))

   294     (HOL_basic_ss addsimps inductive_atomize);

   295 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);

   296 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1

   297   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));

   298 *}

   299 

   300 ML {*

   301 val ({names, ...}, {raw_induct, intrs, elims, ...}) =

   302       Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")

   303 *}

   304 

   305 ML {* val ind_params = Inductive.params_of raw_induct *}

   306 ML {* val raw_induct = atomize_induct @{context} raw_induct; *}

   307 ML {* val elims = map (atomize_induct @{context}) elims; *}

   308 ML {* val monos = Inductive.get_monos @{context}; *}

   309 

   310 lemma 

   311   shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"

   312 apply(tactic {* rtac raw_induct 1 *})

   313 apply(tactic {* my_tac @{context} intrs 1 *})

   314 apply(perm_strict_simp)

   315 apply(rule typing.intros)

   316 oops

   317 

   318