130 

   130 inductive

   131 ML {*

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

   132 fun map_term f t = 

   132 where

   133   (case f t of

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

   134      NONE => map_term' f t 

   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    | x => x)

   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 and map_term' f (t $ u) = 

   136 

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

   137 inductive

   138         (NONE, NONE) => NONE

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

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

   139 where

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

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

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

   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   | map_term' f (Abs (s, T, 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 map_term f t of

   143 

   144         NONE => NONE

   144 inductive

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

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

   146   | map_term' _ _  = NONE;

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

   147 

   147 where

   148 fun map_thm_tac ctxt tac thm =

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

   149 let

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

   150   val monos = Inductive.get_monos ctxt

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

   151 in

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

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

   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     REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),

   153 

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

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

   155 end

   155 

   156 

   156 equivariance valid

   157 (* 

   157 equivariance typing

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

   158 

   159   

   159 thm valid.eqvt

   160   - F needs to be monotone

   160 thm typing.eqvt

   161   - f returns either SOME for a term it fires 

   162     and NONE elsewhere 

   163 *)

   164 fun map_thm ctxt f tac thm =

   165 let

   166   val opt_goal_trm = map_term f (prop_of thm)

   167   fun prove goal = 

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

   169 in

   170   case opt_goal_trm of

   171     NONE => thm

   172   | SOME goal => prove goal

   173 end

   174 

   175 fun transform_prem ctxt names thm =

   176 let

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

   178       (case head_of p of

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

   180        | _ => NONE)

   181   | split_conj _ _ = NONE;

   182 in

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

   184 end

   185 *}

   186 

   187 ML {*

   188 open Nominal_Permeq

   189 *}

   190 

   191 ML {* 

   192 fun single_case_tac ctxt pred_names pi intro  = 

   193 let

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

   195 in

   196   eqvt_strict_tac ctxt [] [] THEN' 

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

   198     let

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

   200       val side_cond_tac = EVERY' 

   201         [ rtac rule, 

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

   203           resolve_tac prems' ]

   204     in

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

   206     end) ctxt

   207 end

   208 *}

   209 

   210 ML {*

   211 fun eqvt_rel_tac pred_name = 

   212 let

   213   val thy = ProofContext.theory_of ctxt

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

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

   216   val param_no = length (Inductive.params_of raw_induct)

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

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

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

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

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

   222 in

   223 

   224 end

   225 *}

   226 

   227 

   228 

   229 lemma [eqvt]:

   230   assumes a: "valid Gamma" 

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

   232 using a

   233 apply(induct)

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

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

   236 done

   237 

   238 lemma 

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

   240 ML_prf {*

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

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

   243 *}

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

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

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

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

   248 done

   249 

   250 lemma uu[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 

   322 declare permute_lam_raw.simps[eqvt]

   164 equivariance typing'

   323 thm alpha_gen_real_eqvt

   165 equivariance typing2' 

   324 (*declare alpha_gen_real_eqvt[eqvt]*)

   166 equivariance typing''

   325 

   167 

   326 lemma

   168 ML {*

   327   assumes a: "alpha_lam_raw t1 t2"

   169 fun mk_minus p = 

   328   shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)"

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

   329 using a

   171 *}

   330 apply(induct)

   172 

   331 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})

   173 inductive

   332 oops

   174   tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"  

   333 

   175   for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"

   334 thm alpha_lam_raw.intros[no_vars]

   176 where

   177     aa: "tt r a a"

   178   | bb: "tt r a b ==> tt r a c"

   179 

   180 (* PROBLEM: derived eqvt-theorem does not conform with [eqvt]

   181 equivariance tt

   182 *)

   183