# HG changeset patch # User Cezary Kaliszyk # Date 1267635107 -3600 # Node ID 6ab8c46b3b4bf1caed4259192da9c74a7ccc9d18 # Parent c3dfd4193b422c13607194abe0677875b07dc4be# Parent 103eb390f1b1a82fbe42e2584ee6769dd5bdeb90 merge diff -r 103eb390f1b1 -r 6ab8c46b3b4b Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Mar 03 14:46:14 2010 +0100 +++ b/Nominal/Fv.thy Wed Mar 03 17:51:47 2010 +0100 @@ -1,5 +1,5 @@ theory Fv -imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *) +imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" begin (* Bindings are given as a list which has a length being equal @@ -312,29 +312,34 @@ *} 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) by auto ML {* -fun symp_tac induct inj eqvt = - (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW - (REPEAT o etac conjE THEN' etac @{thm exi_neg} 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_sym} THEN' - (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) +fun symp_tac induct inj eqvt ctxt = + ind_tac induct THEN_ALL_NEW + simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs + THEN_ALL_NEW + REPEAT o etac @{thm exi_neg} + THEN_ALL_NEW + split_conjs THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW + (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [ + (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})), + (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) + ]) *} ML {* @@ -400,8 +405,8 @@ 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 symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; + fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; + fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 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'; val symt = Goal.prove ctxt' [] [] symg symp_tac'; diff -r 103eb390f1b1 -r 6ab8c46b3b4b Nominal/Rsp.thy --- a/Nominal/Rsp.thy Wed Mar 03 14:46:14 2010 +0100 +++ b/Nominal/Rsp.thy Wed Mar 03 17:51:47 2010 +0100 @@ -146,7 +146,9 @@ by auto ML {* - fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct +fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct +*} +ML {* 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) @@ -161,7 +163,7 @@ ML {* fun alpha_eqvt_tac induct simps ctxt = - indtac induct THEN_ALL_NEW + ind_tac 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 diff -r 103eb390f1b1 -r 6ab8c46b3b4b Nominal/Test.thy --- a/Nominal/Test.thy Wed Mar 03 14:46:14 2010 +0100 +++ b/Nominal/Test.thy Wed Mar 03 17:51:47 2010 +0100 @@ -1,5 +1,5 @@ theory Test -imports "Parser" +imports "Parser" "../Attic/Prove" begin text {* weirdo example from Peter Sewell's bestiary *} @@ -14,6 +14,66 @@ thm alpha_weird_raw.intros[no_vars] thm fv_weird_raw.simps[no_vars] +thm eqvts + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *} +thm weird_inj + +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []), +build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \ weird_raw \ weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *} + +ML {* +fun is_ex (Const ("Ex", _) $ Abs _) = true + | is_ex _ = false; +*} + +ML {* +fun eetac rule = Subgoal.FOCUS_PARAMS + (fn (focus) => + let + val concl = #concl focus + val prems = Logic.strip_imp_prems (term_of concl) + val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems + val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs + val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs + in + (etac rule THEN' RANGE[ + atac, + eresolve_tac thins + ]) 1 + end + ) +*} + + +prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *} +ML_prf {* +fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = + ind_tac induct THEN_ALL_NEW + (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW + asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW + split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) + THEN_ALL_NEW split_conjs +*} + +apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj} @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *}) +apply (simp_all) +apply (erule alpha_gen_compose_trans) +apply assumption +apply (simp add: alpha_eqvt) +defer defer +apply (erule alpha_gen_compose_trans) +apply assumption +apply (simp add: alpha_eqvt) +apply (subgoal_tac "pia + pb + (pib + pa) = (pia + pib) + (pb + pa)") +apply simp +apply (erule alpha_gen_compose_trans) +apply assumption +apply (simp add: alpha_eqvt) +sorry + + abbreviation "WBind \ WBind_raw" abbreviation "WP \ WP_raw"