diff -r 01ae96fa4bf9 -r 4135198bbb8a Nominal-General/Nominal2_Eqvt.thy --- 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 \ (map f xs) = map (p \ f) (p \ 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