# HG changeset patch # User Christian Urban # Date 1276174408 -7200 # Node ID 1a14c4171a514cec4ed02acefea6a3fb3f0737f4 # Parent 25d2cdf7d7e4295a47df6ed275ee5df274140cdf premerge diff -r 25d2cdf7d7e4 -r 1a14c4171a51 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Wed Jun 09 15:14:16 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Thu Jun 10 14:53:28 2010 +0200 @@ -85,105 +85,6 @@ | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" -lemma alpha_gen_sym_test: - assumes a: "R (p \ x) y \ R y (p \ x)" - and b: "p \ R = R" - shows "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" - and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" - and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" - unfolding alphas fresh_star_def - apply(auto simp add: fresh_minus_perm) - apply(rule_tac p="p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel b) - apply(simp add: a) - apply(rule_tac p="p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel b) - apply(simp add: a) - apply(rule_tac p="p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel b) - apply(simp add: a) - done - -ML {* -(* for equalities *) -val tac1 = rtac @{thm sym} THEN' atac - -(* for "unbound" premises *) -val tac2 = atac - -fun trans_prem_tac pred_names ctxt = - SUBPROOF (fn {prems, context as ctxt, ...} => - let - val prems' = map (transform_prem1 ctxt pred_names) prems - val _ = tracing ("prems'\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) prems')) - in - print_tac "goal" THEN resolve_tac prems' 1 - end) ctxt - -(* for "bound" premises *) -fun tac3 pred_names ctxt = - EVERY' [etac @{thm exi_neg}, - resolve_tac @{thms alpha_gen_sym_test}, - asm_full_simp_tac (HOL_ss addsimps @{thms split_conv permute_prod.simps - prod_alpha_def prod_rel.simps alphas}), - Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, - trans_prem_tac pred_names ctxt] - -fun tac intro pred_names ctxt = - resolve_tac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3 pred_names ctxt] -*} - -lemma [eqvt]: -shows "p \ alpha_tkind_raw = alpha_tkind_raw" -and "p \ alpha_ckind_raw = alpha_ckind_raw" -and "p \ alpha_ty_raw = alpha_ty_raw" -and "p \ alpha_ty_lst_raw = alpha_ty_lst_raw" -and "p \ alpha_co_raw = alpha_co_raw" -and "p \ alpha_co_lst_raw = alpha_co_lst_raw" -and "p \ alpha_trm_raw = alpha_trm_raw" -and "p \ alpha_assoc_lst_raw = alpha_assoc_lst_raw" -and "p \ alpha_pat_raw = alpha_pat_raw" -and "p \ alpha_vars_raw = alpha_vars_raw" -and "p \ alpha_tvars_raw = alpha_tvars_raw" -and "p \ alpha_cvars_raw = alpha_cvars_raw" -and "p \ alpha_bv_raw = alpha_bv_raw" -and "p \ alpha_bv_vs_raw = alpha_bv_vs_raw" -and "p \ alpha_bv_tvs_raw = alpha_bv_tvs_raw" -and "p \ alpha_bv_cvs_raw = alpha_bv_cvs_raw" -sorry - -lemmas ii = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts - -lemmas ij = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros - -ML {* -val pp = ["CoreHaskel.alpha_tkind_raw", "CoreHaskell.alpha_ckind_raw", "CoreHaskell.alpha_ty_raw", "CoreHaskell.alpha_ty_lst_raw", "CoreHaskell.alpha_co_raw", "CoreHaskell.alpha_co_lst_raw", "CoreHaskell.alpha_trm_raw", "CoreHaskell.alpha_assoc_lst_raw", "CoreHaskell.alpha_pat_raw", "CoreHaskell.alpha_vars_raw", "CoreHaskell.alpha_tvars_raw", "CoreHaskell.alpha_cvars_raw", "CoreHaskell.alpha_bv_raw", "CoreHaskell.alpha_bv_vs_raw", "CoreHaskell.alpha_bv_tvs_raw", "CoreHaskell.alpha_bv_cvs_raw"] -*} - -lemma -shows "alpha_tkind_raw x1 y1 ==> alpha_tkind_raw y1 x1" -and "alpha_ckind_raw x2 y2 ==> alpha_ckind_raw y2 x2" -and "alpha_ty_raw x3 y3 ==> alpha_ty_raw y3 x3" -and "alpha_ty_lst_raw x4 y4 ==> alpha_ty_lst_raw y4 x4" -and "alpha_co_raw x5 y5 ==> alpha_co_raw y5 x5" -and "alpha_co_lst_raw x6 y6 ==> alpha_co_lst_raw y6 x6" -and "alpha_trm_raw x7 y7 ==> alpha_trm_raw y7 x7" -and "alpha_assoc_lst_raw x8 y8 ==> alpha_assoc_lst_raw y8 x8" -and "alpha_pat_raw x9 y9 ==> alpha_pat_raw y9 x9" -and "alpha_vars_raw xa ya ==> alpha_vars_raw ya xa" -and "alpha_tvars_raw xb yb ==> alpha_tvars_raw yb xb" -and "alpha_cvars_raw xc yc ==> alpha_cvars_raw yc xc" -and "alpha_bv_raw xd yd ==> alpha_bv_raw yd xd" -and "alpha_bv_vs_raw xe ye ==> alpha_bv_vs_raw ye xe" -and "alpha_bv_tvs_raw xf yf ==> alpha_bv_tvs_raw yf xf" -and "alpha_bv_cvs_raw xg yg ==> alpha_bv_cvs_raw yg xg" -apply(induct rule: ii) -apply(tactic {* tac @{thms ij} pp @{context} 1 *})+ -done - - -lemma -alpha_tkind_raw, alpha_ckind_raw, alpha_ty_raw, alpha_ty_lst_raw, alpha_co_raw, alpha_co_lst_raw, alpha_trm_raw, alpha_assoc_lst_raw, alpha_pat_raw, alpha_vars_raw, alpha_tvars_raw, alpha_cvars_raw, alpha_bv_raw, alpha_bv_vs_raw, alpha_bv_tvs_raw, alpha_bv_cvs_raw lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm diff -r 25d2cdf7d7e4 -r 1a14c4171a51 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed Jun 09 15:14:16 2010 +0200 +++ b/Nominal/NewParser.thy Thu Jun 10 14:53:28 2010 +0200 @@ -5,6 +5,11 @@ "Perm" "Tacs" "Equivp" "Lift" begin +(* TODO + + we need to also export a cases-rule for nominal datatypes + size function +*) section{* Interface for nominal_datatype *} diff -r 25d2cdf7d7e4 -r 1a14c4171a51 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Wed Jun 09 15:14:16 2010 +0200 +++ b/Nominal/nominal_dt_alpha.ML Thu Jun 10 14:53:28 2010 +0200 @@ -401,6 +401,7 @@ (** transitivity proof for alphas **) +(* applies cases rules and resolves them with the last premise *) fun ecases_tac cases = Subgoal.FOCUS (fn {prems, ...} => HEADGOAL (resolve_tac cases THEN' rtac (List.last prems))) @@ -409,6 +410,7 @@ SUBPROOF (fn {prems, context, ...} => HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems))) +(* instantiates exI with the permutation p + q *) val perm_inst_tac = Subgoal.FOCUS (fn {params, ...} => let @@ -425,7 +427,7 @@ in resolve_tac intros THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' - TRY o EVERY' + TRY o EVERY' (* if binders are present *) [ etac @{thm exE}, etac @{thm exE}, perm_inst_tac ctxt, @@ -447,7 +449,7 @@ ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]) end -xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = +fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = let val lhs = alpha_trm $ arg1 $ arg2 val mid = alpha_trm $ arg2 $ (Bound 0)