# HG changeset patch # User Christian Urban # Date 1271428151 -7200 # Node ID 6d4e4bf9bce661b00bbb2f6084c1fe7e29576ea5 # Parent b71b838b0a75fd80b8eb2831c201db369dd297cf automatic proofs for equivariance of alphas diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Fri Apr 16 11:09:32 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Fri Apr 16 16:29:11 2010 +0200 @@ -369,6 +369,7 @@ text {* Problem: there is no raw eqvt-rule for The *} lemma "p \ (THE x. P x) = foo" +apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*}) apply(perm_simp) (* apply(perm_strict_simp) *) oops diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Fri Apr 16 11:09:32 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Fri Apr 16 16:29:11 2010 +0200 @@ -86,22 +86,28 @@ (** equivariance tactics **) +val perm_boolE = @{thm permute_boolE} +val perm_cancel = @{thms permute_minus_cancel(2)} +val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def} + fun eqvt_rel_case_tac ctxt pred_names pi intro = let val thy = ProofContext.theory_of ctxt val cpi = Thm.cterm_of thy (mk_minus pi) - val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE} - val permute_cancel = @{thms permute_minus_cancel(2)} + val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE + val simps = HOL_basic_ss addsimps perm_expand_bool in - eqvt_strict_tac ctxt [] [] THEN' - SUBPROOF (fn {prems, context, ...} => + eqvt_strict_tac ctxt [] pred_names THEN' + SUBPROOF (fn {prems, context as ctxt, ...} => let val prems' = map (transform_prem ctxt pred_names) prems - val side_cond_tac = EVERY' - [ rtac rule, eqvt_strict_tac context permute_cancel [], - resolve_tac prems' ] + val tac1 = resolve_tac prems' + val tac2 = EVERY' [ rtac pi_intro_rule, + eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] + val tac3 = EVERY' [ rtac pi_intro_rule, + eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems'] in - (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1 + (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 end) ctxt end diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Fri Apr 16 11:09:32 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Fri Apr 16 16:29:11 2010 +0200 @@ -106,11 +106,16 @@ (* conversion that raises an error or prints a warning message, if a permutation on a constant or application cannot be analysed *) -fun progress_info_conv ctxt strict_flag ctrm = +fun progress_info_conv ctxt strict_flag bad_hds ctrm = let - fun msg trm = - (if strict_flag then error else warning) - ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) + fun msg trm = + let + val hd = head_of trm + in + if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () + else (if strict_flag then error else warning) + ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) + end val _ = case (term_of ctrm) of Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm @@ -136,7 +141,7 @@ eqvt_apply_conv bad_hds, eqvt_lambda_conv, More_Conv.rewrs_conv post_thms, - progress_info_conv ctxt strict_flag + progress_info_conv ctxt strict_flag bad_hds ] ctrm end diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Fri Apr 16 11:09:32 2010 +0200 +++ b/Nominal/Ex/Classical.thy Fri Apr 16 16:29:11 2010 +0200 @@ -63,6 +63,14 @@ alpha (ImpR_raw coname1 name trm_raw coname2) (ImpR_raw coname1a namea trm_rawa coname2a)" +thm alpha.intros + +declare permute_trm_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha +thm eqvts_raw + end diff -r b71b838b0a75 -r 6d4e4bf9bce6 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Fri Apr 16 11:09:32 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Fri Apr 16 16:29:11 2010 +0200 @@ -188,56 +188,28 @@ declare permute_lam_raw.simps[eqvt] declare alpha_gen_eqvt[eqvt] -(*equivariance alpha_lam_raw'*) +equivariance alpha_lam_raw' thm eqvts_raw + + +(* HERE *) + lemma assumes a: "alpha_lam_raw' t1 t2" shows "alpha_lam_raw' (p \ t1) (p \ t2)" using a apply(induct) -apply(perm_simp) -apply(rule a1) -apply(simp) -apply(perm_simp) -apply(rule a2) -apply(simp) -apply(simp) - -apply simp -apply (rule a3) -apply (erule exi[of _ _ "p"]) -apply (simp add: alphas) -apply (erule conjE)+ -apply (rule conjI) -apply (rule permute_eq_iff[of "- p", THEN iffD1]) -apply (simp add: eqvts) -apply (rule conjI) -apply (rule fresh_star_permute_iff[of "- p", THEN iffD1]) -apply (simp add: eqvts) -apply (rule conjI) -apply (simp add: permute_eqvt[symmetric]) -apply (rule permute_eq_iff[of "- p", THEN iffD1]) -apply (subst permute_eqvt) -apply (simp add: eqvts) -done - -lemma - assumes a: "alpha_lam_raw' t1 t2" - shows "alpha_lam_raw' (p \ t1) (p \ t2)" -using a -apply(induct) -ML_prf {* -val ({names, ...}, {raw_induct, intrs, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw") -*} +apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac + @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*}) apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*}) + @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*}) +(* apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*}) + @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*}) +*) oops - section {* size function *} lemma size_eqvt_raw: