--- a/Nominal-General/Nominal2_Eqvt.thy Mon Apr 12 17:44:26 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Tue Apr 13 00:47:57 2010 +0200
@@ -204,6 +204,9 @@
shows "supp (set xs) = supp xs"
*)
+lemma map_eqvt:
+ shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ by (induct xs) (simp_all, simp only: permute_fun_app_eq)
section {* Product Operations *}
@@ -250,7 +253,7 @@
(* datatypes *)
permute_prod.simps append_eqvt rev_eqvt set_eqvt
- fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
+ map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
(* sets *)
empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
@@ -368,5 +371,144 @@
(* apply(perm_strict_simp) *)
oops
+atom_decl var
+
+ML {*
+val inductive_atomize = @{thms induct_atomize};
+
+val atomize_conv =
+ MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
+ (HOL_basic_ss addsimps inductive_atomize);
+val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
+fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
+ (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+
+fun map_term f t u = (case f t u of
+ NONE => map_term' f t u | x => x)
+and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of
+ (NONE, NONE) => NONE
+ | (SOME t'', NONE) => SOME (t'' $ u)
+ | (NONE, SOME u'') => SOME (t $ u'')
+ | (SOME t'', SOME u'') => SOME (t'' $ u''))
+ | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of
+ NONE => NONE
+ | SOME t'' => SOME (Abs (s, T, t'')))
+ | map_term' _ _ _ = NONE;
+
+
+fun map_thm ctxt f tac monos opt th =
+ let
+ val prop = prop_of th;
+ fun prove t =
+ Goal.prove ctxt [] [] t (fn _ =>
+ EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
+ REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
+ REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
+ in Option.map prove (map_term f prop (the_default prop opt)) end;
+
+fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
+ Const (name, _) =>
+ if name mem names then SOME (f p q) else NONE
+ | _ => NONE)
+ | split_conj _ _ _ _ = NONE;
+*}
+
+ML {*
+val perm_bool = @{thm "permute_bool_def"};
+val perm_boolI = @{thm "permute_boolI"};
+val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
+ (Drule.strip_imp_concl (cprop_of perm_boolI))));
+
+fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
+ [(perm_boolI_pi, pi)] perm_boolI;
+
+*}
+
+ML {*
+fun transp ([] :: _) = []
+ | transp xs = map hd xs :: transp (map tl xs);
+
+fun prove_eqvt s xatoms ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+ Inductive.the_inductive ctxt (Sign.intern_const thy s);
+ val raw_induct = atomize_induct ctxt raw_induct;
+ val elims = map (atomize_induct ctxt) elims;
+ val intrs = map atomize_intr intrs;
+ val monos = Inductive.get_monos ctxt;
+ val intrs' = Inductive.unpartition_rules intrs
+ (map (fn (((s, ths), (_, k)), th) =>
+ (s, ths ~~ Inductive.infer_intro_vars th k ths))
+ (Inductive.partition_rules raw_induct intrs ~~
+ Inductive.arities_of raw_induct ~~ elims));
+ val k = length (Inductive.params_of raw_induct);
+ val atoms' = ["var"];
+ val atoms =
+ if null xatoms then atoms' else
+ let val atoms = map (Sign.intern_type thy) xatoms
+ in
+ (case duplicates op = atoms of
+ [] => ()
+ | xs => error ("Duplicate atoms: " ^ commas xs);
+ case subtract (op =) atoms' atoms of
+ [] => ()
+ | xs => error ("No such atoms: " ^ commas xs);
+ atoms)
+ end;
+ val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
+ val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
+ (Nominal_ThmDecls.get_eqvts_thms ctxt @ perm_pi_simp);
+ val (([t], [pi]), ctxt') = ctxt |>
+ Variable.import_terms false [concl_of raw_induct] ||>>
+ Variable.variant_fixes ["pi"];
+ val ps = map (fst o HOLogic.dest_imp)
+ (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
+ fun eqvt_tac ctxt'' pi (intr, vs) st =
+ let
+ fun eqvt_err s =
+ let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
+ in error ("Could not prove equivariance for introduction rule\n" ^
+ Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
+ end;
+ val res = SUBPROOF (fn {prems, params, ...} =>
+ let
+ val prems' = map (fn th => the_default th (map_thm ctxt'
+ (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
+ val prems'' = map (fn th => Simplifier.simplify eqvt_ss
+ (mk_perm_bool (cterm_of thy pi) th)) prems';
+ val intr' = intr
+ in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
+ end) ctxt' 1 st
+ in
+ case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
+ NONE => eqvt_err ("Rule does not match goal\n" ^
+ Syntax.string_of_term ctxt'' (hd (prems_of st)))
+ | SOME (th, _) => Seq.single th
+ end;
+ val thss = map (fn atom =>
+ let val pi' = Free (pi, @{typ perm})
+ in map (fn th => zero_var_indexes (th RS mp))
+ (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
+ let
+ val (h, ts) = strip_comb p;
+ val (ts1, ts2) = chop k ts
+ in
+ HOLogic.mk_imp (p, list_comb (h, ts1))
+ end) ps)))
+ (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
+ full_simp_tac eqvt_ss 1 THEN
+ eqvt_tac context pi' intr_vs) intrs')) |>
+ singleton (ProofContext.export ctxt' ctxt)))
+ end) atoms
+ in
+ ctxt |>
+ Local_Theory.notes (map (fn (name, ths) =>
+ ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
+ [Attrib.internal (K Nominal_ThmDecls.eqvt_add)]), [(ths, [])]))
+ (names ~~ transp thss)) |> snd
+ end;
+*}
end