# HG changeset patch # User Cezary Kaliszyk # Date 1267626505 -3600 # Node ID c6e521a2a0b1b228a94cc35527385cd4af7d953b # Parent 0f329449e3044451fb07ff948521345cc92fa3fe reflp for multiple quantifiers. diff -r 0f329449e304 -r c6e521a2a0b1 Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Mar 03 14:22:58 2010 +0100 +++ b/Nominal/Fv.thy Wed Mar 03 15:28:25 2010 +0100 @@ -1,5 +1,5 @@ theory Fv -imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *) +imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" (* For testing *) begin (* Bindings are given as a list which has a length being equal @@ -312,15 +312,16 @@ *} ML {* -fun reflp_tac induct inj = +fun reflp_tac induct inj ctxt = rtac induct THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW -(* TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*) - (rtac @{thm exI[of _ "0 :: perm"]} THEN' - asm_full_simp_tac (HOL_ss addsimps - @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) + simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW + split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} + THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps + @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv + add_0_left supp_zero_perm Int_empty_left}) *} + lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" apply (erule exE) apply (rule_tac x="-pi" in exI) @@ -400,7 +401,7 @@ let val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) - fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; + fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';