130 ML {*

   130 inductive

   131 val inductive_atomize = @{thms induct_atomize};

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

   132 

   132 where

   133 val atomize_conv = 

   133     t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T"

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

   134   | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2"

   135     (HOL_basic_ss addsimps inductive_atomize);

   135   | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2"

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

   136 

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

   137 inductive

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

   138   typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60) 

   139 *}

   139 where

   140 

   140     t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T"

   141 ML {*

   141   | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2"

   142 fun map_term f t = 

   142   | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2"

   143   (case f t of

   143 

   144      NONE => map_term' f t 

   144 inductive

   145    | x => x)

   145   typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60)

   146 and map_term' f (t $ u) = 

   146 and  valid' :: "(name\<times>ty) list \<Rightarrow> bool"

   147     (case (map_term f t, map_term f u) of

   147 where

   148         (NONE, NONE) => NONE

   148     v1[intro]: "valid' []"

   149       | (SOME t'', NONE) => SOME (t'' $ u)

   149   | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)"

   150       | (NONE, SOME u'') => SOME (t $ u'')

   150   | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T"

   151       | (SOME t'', SOME u'') => SOME (t'' $ u''))

   151   | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"

   152   | map_term' f (Abs (s, T, t)) = 

   152   | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2"

   153       (case map_term f t of

   153 

   154         NONE => NONE

   154 use "../../Nominal-General/nominal_eqvt.ML"

   155       | SOME t'' => SOME (Abs (s, T, t'')))

   156   | map_term' _ _  = NONE;

   157 

   158 fun map_thm_tac ctxt tac thm =

   159 let

   160   val monos = Inductive.get_monos ctxt

   161 in

   162   EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,

   163     REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),

   164     REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]

   165 end

   166 

   167 (* 

   168  proves F[f t] from F[t] where F[t] is the given theorem  

   169   

   170   - F needs to be monotone

   171   - f returns either SOME for a term it fires 

   172     and NONE elsewhere 

   173 *)

   174 fun map_thm ctxt f tac thm =

   175 let

   176   val opt_goal_trm = map_term f (prop_of thm)

   177   fun prove goal = 

   178     Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)

   179 in

   180   case opt_goal_trm of

   181     NONE => thm

   182   | SOME goal => prove goal

   183 end

   184 

   185 fun transform_prem ctxt names thm =

   186 let

   187   fun split_conj names (Const ("op &", _) $ p $ q) = 

   188       (case head_of p of

   189          Const (name, _) => if name mem names then SOME q else NONE

   190        | _ => NONE)

   191   | split_conj _ _ = NONE;

   192 in

   193   map_thm ctxt (split_conj names) (etac conjunct2 1) thm

   194 end

   195 *}

   196 

   197 ML {*

   198 open Nominal_Permeq

   199 open Nominal_ThmDecls

   200 *}

   201 

   202 ML {*

   203 fun mk_perm p trm =

   204 let

   205   val ty = fastype_of trm

   206 in

   207   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm

   208 end

   209 

   210 fun mk_minus p = 

   211  Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p   

   212 *}

   213 

   214 ML {* 

   215 fun single_case_tac ctxt pred_names pi intro  = 

   216 let

   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}

   220 in

   221   eqvt_strict_tac ctxt [] [] THEN' 

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

   223     let

   224       val prems' = map (transform_prem ctxt pred_names) prems

   225       val side_cond_tac = EVERY' 

   226         [ rtac rule, 

   227           eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],

   228           resolve_tac prems' ]

   229     in

   230       HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 

   231     end) ctxt

   232 end

   233 *}

   234 

   235 ML {*

   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 = 

   270 let

   271   val thy = ProofContext.theory_of ctxt

   272   val ({names, ...}, {raw_induct, intrs, ...}) =

   273     Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)

   274   val raw_induct = atomize_induct ctxt raw_induct;

   275   val intros = map atomize_intr intrs;

   276   val params_no = length (Inductive.params_of raw_induct)

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

   278     ctxt |> Variable.import_terms false [concl_of raw_induct] 

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

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

   281   val preds = map (fst o HOLogic.dest_imp)

   282     (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));

   283   val goal = HOLogic.mk_Trueprop 

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

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

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

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

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

   289 in

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

   291         |> snd

   292 end

   293 *}

   294 

   295 

   296 ML {*

   297 local structure P = OuterParse and K = OuterKeyword in

   298 

   299 val _ =

   300   OuterSyntax.local_theory "equivariance"

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

   302     (P.xname >> eqvt_rel_tac);

   303 

   304 end;

   305 *}