# HG changeset patch # User Cezary Kaliszyk # Date 1267622578 -3600 # Node ID 0f329449e3044451fb07ff948521345cc92fa3fe # Parent 88d2d4beb9e034cd925b283d5d774f3c8be34b71 Fix eqvt for multiple quantifiers. diff -r 88d2d4beb9e0 -r 0f329449e304 Nominal/Nominal2_Eqvt.thy --- a/Nominal/Nominal2_Eqvt.thy Wed Mar 03 12:48:05 2010 +0100 +++ b/Nominal/Nominal2_Eqvt.thy Wed Mar 03 14:22:58 2010 +0100 @@ -251,7 +251,7 @@ empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt - atom_eqvt + atom_eqvt add_perm_eqvt thm eqvts thm eqvts_raw diff -r 88d2d4beb9e0 -r 0f329449e304 Nominal/Parser.thy --- a/Nominal/Parser.thy Wed Mar 03 12:48:05 2010 +0100 +++ b/Nominal/Parser.thy Wed Mar 03 14:22:58 2010 +0100 @@ -245,10 +245,10 @@ val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; -(* val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms + val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; - val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc +(* val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; val qty_names = map (fn (_, b, _, _) => b) dts; diff -r 88d2d4beb9e0 -r 0f329449e304 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Wed Mar 03 12:48:05 2010 +0100 +++ b/Nominal/Rsp.thy Wed Mar 03 14:22:58 2010 +0100 @@ -146,6 +146,34 @@ by auto ML {* + fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct + fun all_eqvts ctxt = + Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt + val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) +*} + +ML {* +fun mk_minimal_ss ctxt = + Simplifier.context ctxt empty_ss + setsubgoaler asm_simp_tac + setmksimps (mksimps []) +*} + +ML {* +fun alpha_eqvt_tac induct simps ctxt = + indtac induct THEN_ALL_NEW + simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW + REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps + @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW + (split_conjs THEN_ALL_NEW TRY o resolve_tac + @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) + THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (@{thms permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt)) +*} + +ML {* fun build_alpha_eqvts funs perms simps induct ctxt = let val pi = Free ("p", @{typ perm}); @@ -158,17 +186,7 @@ HOLogic.mk_imp (alpha $ arg $ arg2, (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) - fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - ( - (asm_full_simp_tac (HOL_ss addsimps - ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))) - THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' - REPEAT o etac conjE THEN' - (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW - (asm_full_simp_tac HOL_ss) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))))) 1 + fun tac _ = alpha_eqvt_tac induct simps ctxt 1 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac in map (fn x => mp OF [x]) (HOLogic.conj_elims thm) diff -r 88d2d4beb9e0 -r 0f329449e304 Nominal/Test.thy --- a/Nominal/Test.thy Wed Mar 03 12:48:05 2010 +0100 +++ b/Nominal/Test.thy Wed Mar 03 14:22:58 2010 +0100 @@ -14,42 +14,6 @@ thm alpha_weird_raw.intros[no_vars] thm fv_weird_raw.simps[no_vars] -lemma "alpha_weird_raw a b \ alpha_weird_raw (p \ a) (p \ b)" -apply (erule alpha_weird_raw.induct) -defer -apply (simp add: alpha_weird_raw.intros) -apply (simp add: alpha_weird_raw.intros) -apply (simp only: permute_weird_raw.simps) -apply (rule alpha_weird_raw.intros) -apply (erule exi[of _ _ "p"]) -apply (erule exi[of _ _ "p"]) -apply (erule exi[of _ _ "p"]) -apply (erule exi[of _ _ "p"]) -apply (erule conjE)+ -apply (rule conjI) -apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"]) -apply (simp add: eqvts) -apply (simp add: eqvts) -apply (rule conjI) -defer -apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"]) -apply (simp add: eqvts) -apply (simp add: eqvts) -apply (rule conjI) -defer -apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt) -apply(simp add: alpha_gen.simps) -apply(erule conjE)+ - apply(rule conjI) - apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1]) -apply (simp add: eqvts) - apply(rule conjI) - apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) -apply (simp add: eqvts add_perm_eqvt) -apply (simp add: permute_eqvt[symmetric]) -done - - (* abbreviation "WBind \ WBind_raw" abbreviation "WP \ WP_raw"