374 atom_decl var

   375 

   376 ML {*

   377 val inductive_atomize = @{thms induct_atomize};

   378 

   379 val atomize_conv =

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

   381     (HOL_basic_ss addsimps inductive_atomize);

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

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

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

   385 

   386 fun map_term f t u = (case f t u of

   387       NONE => map_term' f t u | x => x)

   388 and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of

   389       (NONE, NONE) => NONE

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

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

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

   393   | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of

   394       NONE => NONE

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

   396   | map_term' _ _ _ = NONE;

   397 

   398 

   399 fun map_thm ctxt f tac monos opt th =

   400   let

   401     val prop = prop_of th;

   402     fun prove t =

   403       Goal.prove ctxt [] [] t (fn _ =>

   404         EVERY [cut_facts_tac [th] 1, etac rev_mp 1,

   405           REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),

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

   407   in Option.map prove (map_term f prop (the_default prop opt)) end;

   408 

   409 fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of

   410       Const (name, _) =>

   411         if name mem names then SOME (f p q) else NONE

   412     | _ => NONE)

   413   | split_conj _ _ _ _ = NONE;

   414 *}

   415 

   416 ML {*

   417 val perm_bool = @{thm "permute_bool_def"};

   418 val perm_boolI = @{thm "permute_boolI"};

   419 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb

   420   (Drule.strip_imp_concl (cprop_of perm_boolI))));

   421 

   422 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate

   423   [(perm_boolI_pi, pi)] perm_boolI;

   424 

   425 *}

   426 

   427 ML {*

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

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

   430 

   431 fun prove_eqvt s xatoms ctxt =

   432   let

   433     val thy = ProofContext.theory_of ctxt;

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

   435       Inductive.the_inductive ctxt (Sign.intern_const thy s);

   436     val raw_induct = atomize_induct ctxt raw_induct;

   437     val elims = map (atomize_induct ctxt) elims;

   438     val intrs = map atomize_intr intrs;

   439     val monos = Inductive.get_monos ctxt;

   440     val intrs' = Inductive.unpartition_rules intrs

   441       (map (fn (((s, ths), (_, k)), th) =>

   442            (s, ths ~~ Inductive.infer_intro_vars th k ths))

   443          (Inductive.partition_rules raw_induct intrs ~~

   444           Inductive.arities_of raw_induct ~~ elims));

   445     val k = length (Inductive.params_of raw_induct);

   446     val atoms' = ["var"];

   447     val atoms =

   448       if null xatoms then atoms' else

   449       let val atoms = map (Sign.intern_type thy) xatoms

   450       in

   451         (case duplicates op = atoms of

   452              [] => ()

   453            | xs => error ("Duplicate atoms: " ^ commas xs);

   454          case subtract (op =) atoms' atoms of

   455              [] => ()

   456            | xs => error ("No such atoms: " ^ commas xs);

   457          atoms)

   458       end;

   459     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";

   460     val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps

   461       (Nominal_ThmDecls.get_eqvts_thms ctxt @ perm_pi_simp);

   462     val (([t], [pi]), ctxt') = ctxt |>

   463       Variable.import_terms false [concl_of raw_induct] ||>>

   464       Variable.variant_fixes ["pi"];

   465     val ps = map (fst o HOLogic.dest_imp)

   466       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));

   467     fun eqvt_tac ctxt'' pi (intr, vs) st =

   468       let

   469         fun eqvt_err s =

   470           let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt

   471           in error ("Could not prove equivariance for introduction rule\n" ^

   472             Syntax.string_of_term ctxt''' t ^ "\n" ^ s)

   473           end;

   474         val res = SUBPROOF (fn {prems, params, ...} =>

   475           let

   476             val prems' = map (fn th => the_default th (map_thm ctxt'

   477               (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;

   478             val prems'' = map (fn th => Simplifier.simplify eqvt_ss

   479               (mk_perm_bool (cterm_of thy pi) th)) prems';

   480             val intr' = intr 

   481           in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1

   482           end) ctxt' 1 st

   483       in

   484         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of

   485           NONE => eqvt_err ("Rule does not match goal\n" ^

   486             Syntax.string_of_term ctxt'' (hd (prems_of st)))

   487         | SOME (th, _) => Seq.single th

   488       end;

   489     val thss = map (fn atom =>

   490       let val pi' = Free (pi, @{typ perm})

   491       in map (fn th => zero_var_indexes (th RS mp))

   492         (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []

   493           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>

   494             let

   495               val (h, ts) = strip_comb p;

   496               val (ts1, ts2) = chop k ts

   497             in

   498               HOLogic.mk_imp (p, list_comb (h, ts1))

   499             end) ps)))

   500           (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>

   501               full_simp_tac eqvt_ss 1 THEN

   502               eqvt_tac context pi' intr_vs) intrs')) |>

   503           singleton (ProofContext.export ctxt' ctxt)))

   504       end) atoms

   505   in

   506     ctxt |>

   507     Local_Theory.notes (map (fn (name, ths) =>

   508         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),

   509           [Attrib.internal (K Nominal_ThmDecls.eqvt_add)]), [(ths, [])]))

   510       (names ~~ transp thss)) |> snd

   511   end;

   512 *}

   513