# HG changeset patch # User Christian Urban # Date 1271244071 -7200 # Node ID 16653e702d89bbe306c247f897981568520ccf84 # Parent ac8cb569a17bcaf70cff48f8ee7a362c42df13d0 first working version of the automatic equivariance procedure diff -r ac8cb569a17b -r 16653e702d89 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Apr 14 10:29:56 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Wed Apr 14 13:21:11 2010 +0200 @@ -127,6 +127,16 @@ | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" +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)); +*} ML {* fun map_term f t = @@ -186,12 +196,27 @@ ML {* open Nominal_Permeq +open Nominal_ThmDecls +*} + +ML {* +fun mk_perm p trm = +let + val ty = fastype_of trm +in + Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm +end + +fun mk_minus p = + Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p *} ML {* fun single_case_tac ctxt pred_names pi intro = let - val rule = Drule.instantiate' [] [SOME pi] @{thm permute_boolE} + val thy = ProofContext.theory_of ctxt + val cpi = Thm.cterm_of thy (mk_minus pi) + val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE} in eqvt_strict_tac ctxt [] [] THEN' SUBPROOF (fn {prems, context as ctxt, ...} => @@ -208,130 +233,85 @@ *} ML {* -fun eqvt_rel_tac pred_name = +fun prepare_pred params_no pi pred = +let + val (c, xs) = strip_comb pred; + val (xs1, xs2) = chop params_no xs +in + HOLogic.mk_imp + (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2)) +end +*} + +ML {* +fun transp ([] :: _) = [] + | transp xs = map hd xs :: transp (map tl xs); +*} + +ML {* + Local_Theory.note; + Local_Theory.notes; + fold_map +*} + +ML {* +fun note_named_thm (name, thm) ctxt = +let + val thm_name = Binding.qualified_name + (Long_Name.qualify (Long_Name.base_name name) "eqvt") + val attr = Attrib.internal (K eqvt_add) +in + Local_Theory.note ((thm_name, [attr]), [thm]) ctxt +end +*} + +ML {* +fun eqvt_rel_tac pred_name ctxt = let val thy = ProofContext.theory_of ctxt val ({names, ...}, {raw_induct, intrs, ...}) = Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) - val param_no = length (Inductive.params_of raw_induct) - val (([raw_concl], [pi]), ctxt') = + val raw_induct = atomize_induct ctxt raw_induct; + val intros = map atomize_intr intrs; + val params_no = length (Inductive.params_of raw_induct) + val (([raw_concl], [raw_pi]), ctxt') = ctxt |> Variable.import_terms false [concl_of raw_induct] - ||>> Variable.variant_fixes ["pi"]; + ||>> Variable.variant_fixes ["pi"] + val pi = Free (raw_pi, @{typ perm}) val preds = map (fst o HOLogic.dest_imp) (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map (prepare_pred params_no pi) preds)) + val thm = Goal.prove ctxt' [] [] goal (fn {context,...} => + HEADGOAL (EVERY' (rtac raw_induct :: map (single_case_tac context names pi) intros))) + |> singleton (ProofContext.export ctxt' ctxt) + val thms = map (fn th => zero_var_indexes (th RS mp)) (Datatype_Aux.split_conj_thm thm) in - + ctxt |> fold_map note_named_thm (names ~~ thms) + |> snd end *} - -lemma [eqvt]: - assumes a: "valid Gamma" - shows "valid (p \ Gamma)" -using a -apply(induct) -apply(tactic {* my_tac @{context} ["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(1)} 1 *}) -apply(tactic {* my_tac @{context }["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(2)} 1 *}) -done - -lemma - shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" -ML_prf {* -val ({names, ...}, {raw_induct, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") -*} -apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(1)} 1 *}) -apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(2)} 1 *}) -apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(3)} 1 *}) -done +ML {* +local structure P = OuterParse and K = OuterKeyword in -lemma uu[eqvt]: - assumes a: "Gamma \ t : T" - shows "(p \ Gamma) \ (p \ t) : (p \ T)" -using a -apply(induct) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(perm_strict_simp) -apply(rule typing.intros) -apply(rule conj_mono[THEN mp]) -prefer 3 -apply(assumption) -apply(rule impI) -prefer 2 -apply(rule impI) -apply(simp) -apply(auto)[1] -apply(simp) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -done +val _ = + OuterSyntax.local_theory "equivariance" + "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl + (P.xname >> eqvt_rel_tac); -(* -inductive - typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) -where - t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" - | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" - | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" - -lemma uu[eqvt]: - assumes a: "Gamma \ t : T" - shows "(p \ Gamma) \ (p \ t) : (p \ T)" -using a -apply(induct) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -done -*) - -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)); +end; *} -ML {* -val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") -*} - -ML {* val ind_params = Inductive.params_of raw_induct *} -ML {* val raw_induct = atomize_induct @{context} raw_induct; *} -ML {* val elims = map (atomize_induct @{context}) elims; *} -ML {* val monos = Inductive.get_monos @{context}; *} +equivariance valid +equivariance typing -lemma - shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" -apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} intrs 1 *}) -apply(perm_strict_simp) -apply(rule typing.intros) -oops - - +thm valid.eqvt +thm typing.eqvt thm eqvts thm eqvts_raw -declare permute_lam_raw.simps[eqvt] -thm alpha_gen_real_eqvt -(*declare alpha_gen_real_eqvt[eqvt]*) - -lemma - assumes a: "alpha_lam_raw t1 t2" - shows "alpha_lam_raw (p \ t1) (p \ t2)" -using a -apply(induct) -apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *}) -oops - -thm alpha_lam_raw.intros[no_vars] inductive alpha_lam_raw' @@ -342,18 +322,15 @@ | "\pi. ({atom name}, lam_raw) \gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \ alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" +declare permute_lam_raw.simps[eqvt] +(*declare alpha_gen_real_eqvt[eqvt]*) +(*equivariance alpha_lam_raw'*) + lemma assumes a: "alpha_lam_raw' t1 t2" shows "alpha_lam_raw' (p \ t1) (p \ t2)" using a apply(induct) -apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *}) -apply(perm_strict_simp) -apply(rule alpha_lam_raw'.intros) -apply(simp add: alphas) -apply(rule_tac p="- p" in permute_boolE) -apply(perm_simp permute_minus_cancel(2)) oops