# HG changeset patch # User Cezary Kaliszyk # Date 1269268021 -3600 # Node ID 2c37f5a8c747e9c8213ee80c324c9e67d8ddb7f3 # Parent 69c9d53fb8173a8ad5ba7d7c809eaa87bbc8f0ac alpha_bn_rsp_pre automatized. diff -r 69c9d53fb817 -r 2c37f5a8c747 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Mon Mar 22 14:07:35 2010 +0100 +++ b/Nominal/Rsp.thy Mon Mar 22 15:27:01 2010 +0100 @@ -259,5 +259,47 @@ end *} +lemma equivp_rspl: + "equivp r \ r a b \ r a c = r b c" + unfolding equivp_reflp_symp_transp symp_def transp_def + by blast + +lemma equivp_rspr: + "equivp r \ r a b \ r c a = r c b" + unfolding equivp_reflp_symp_transp symp_def transp_def + by blast + +ML {* +fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) = +let + val alpha = nth alphas n; + val ty = domain_type (fastype_of alpha); + val names = Datatype_Prop.make_tnames [ty, ty]; + val [l, r] = map (fn x => (Free (x, ty))) names; + val g1 = + Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r), + HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty, + HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)))) + val g2 = + Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r), + HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty, + HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r)))) + fun tac {context, ...} = ( + etac (nth inducts n) THEN_ALL_NEW + (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW + InductTacs.case_tac context "a" THEN_ALL_NEW split_conjs THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW + REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) THEN_ALL_NEW + TRY o eresolve_tac (map (fn x => @{thm equivp_rspl} OF [x]) equivps) THEN_ALL_NEW + TRY o eresolve_tac (map (fn x => @{thm equivp_rspr} OF [x]) equivps) THEN_ALL_NEW + TRY o rtac refl + ) 1; + val t1 = Goal.prove ctxt names [] g1 tac; + val t2 = Goal.prove ctxt names [] g2 tac; +in + [t1, t2] +end +*} + end diff -r 69c9d53fb817 -r 2c37f5a8c747 Nominal/Term5.thy --- a/Nominal/Term5.thy Mon Mar 22 14:07:35 2010 +0100 +++ b/Nominal/Term5.thy Mon Mar 22 15:27:01 2010 +0100 @@ -183,32 +183,8 @@ local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} print_theorems - -lemma alpha_rbv_rsp_pre: - "x \l y \ \z. alpha_rbv5 x z = alpha_rbv5 y z" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done - -lemma alpha_rbv_rsp_pre2: - "x \l y \ \z. alpha_rbv5 z x = alpha_rbv5 z y" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp lemma [quot_respect]: "(alpha_rlts ===> op =) fv_rlts fv_rlts" @@ -221,13 +197,10 @@ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) - apply clarify - apply (simp add: alpha_rbv_rsp_pre2) - apply (simp add: alpha_rbv_rsp_pre) done lemma diff -r 69c9d53fb817 -r 2c37f5a8c747 Nominal/Term5n.thy --- a/Nominal/Term5n.thy Mon Mar 22 14:07:35 2010 +0100 +++ b/Nominal/Term5n.thy Mon Mar 22 15:27:01 2010 +0100 @@ -123,31 +123,9 @@ local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} print_theorems -lemma alpha_rbv_rsp_pre: - "x \l y \ \z. alpha_rbv5 x z = alpha_rbv5 y z" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done +local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} +thm alpha_bn_rsp -lemma alpha_rbv_rsp_pre2: - "x \l y \ \z. alpha_rbv5 z x = alpha_rbv5 z y" - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply (case_tac [!] z) - apply (simp_all add: alpha_dis alpha5_inj) - apply clarify - apply auto - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done lemma [quot_respect]: "(alpha_rlts ===> op =) fv_rlts fv_rlts" @@ -161,7 +139,7 @@ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp) + apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp) apply (clarify) apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) done