# HG changeset patch # User Christian Urban # Date 1281998367 -28800 # Node ID 66ae73fd66c0b68e947ef820a8256dc13eb348ce # Parent a92d2c915004da190d1b96043ecc2a9dec84e2d2 added rsp-lemmas for alpha_bns diff -r a92d2c915004 -r 66ae73fd66c0 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Mon Aug 16 19:57:41 2010 +0800 +++ b/Nominal/Ex/CoreHaskell.thy Tue Aug 17 06:39:27 2010 +0800 @@ -88,6 +88,7 @@ (* can lift *) thm distinct thm fv_defs +thm alpha_bn_imps alpha_equivp thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts thm perm_simps @@ -128,7 +129,11 @@ val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws} *} - +ML {* + val thms_e = map (lift_thm qtys @{context}) + @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps + prod.cases]} +*} lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) diff -r a92d2c915004 -r 66ae73fd66c0 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Mon Aug 16 19:57:41 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Tue Aug 17 06:39:27 2010 +0800 @@ -62,11 +62,6 @@ section {* NOT *} -lemma [quot_respect]: - "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" -sorry - - ML {* val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps diff -r a92d2c915004 -r 66ae73fd66c0 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Mon Aug 16 19:57:41 2010 +0800 +++ b/Nominal/NewParser.thy Tue Aug 17 06:39:27 2010 +0800 @@ -423,9 +423,10 @@ alpha_intros alpha_induct alpha_cases lthy6 else raise TEST lthy6 - val alpha_equivp_thms = + val (alpha_equivp_thms, alpha_bn_equivp_thms) = if get_STEPS lthy > 13 - then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6 + then raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms + alpha_trans_thms lthy6 else raise TEST lthy6 (* proving alpha implies alpha_bn *) @@ -450,11 +451,13 @@ val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt + val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms + (* noting the quot_respects lemmas *) val (_, lthy6a) = if get_STEPS lthy > 15 then Local_Theory.note ((Binding.empty, [rsp_attrib]), - raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6 + raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 else raise TEST lthy6 (* defining the quotient type *) @@ -534,6 +537,7 @@ ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) + ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) val _ = if get_STEPS lthy > 20 diff -r a92d2c915004 -r 66ae73fd66c0 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Aug 16 19:57:41 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Tue Aug 17 06:39:27 2010 +0800 @@ -23,12 +23,14 @@ val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list - val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list + val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> + Proof.context -> thm list * thm list val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> term list -> thm -> thm list -> Proof.context -> thm list val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list + val raw_alpha_bn_rsp: thm list -> thm list -> thm list val mk_funs_rsp: thm -> thm val mk_alpha_permute_rsp: thm -> thm @@ -563,7 +565,7 @@ @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" by (rule eq_reflection, auto simp add: transp_def)} -fun raw_prove_equivp alphas refl symm trans ctxt = +fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = let val refl' = map (fold_rule @{thms reflp_def} o atomize) refl val symm' = map (fold_rule @{thms symp_def} o atomize) symm @@ -572,9 +574,10 @@ fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in - Goal.prove_multi ctxt [] [] (map prep_goal alphas) + Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns)) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) + |> chop (length alphas) end @@ -691,6 +694,21 @@ end +(* rsp lemmas for alpha_bn relations *) + +val rsp_equivp = + @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q" + by (simp only: fun_rel_def equivp_def, metis)} + +fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps = +let + fun mk_thm thm1 thm2 = + (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) +in + map2 mk_thm alpha_bn_equivp alpha_bn_imps +end + + (* transformation of the natural rsp-lemmas into standard form *) val fun_rsp = @{lemma @@ -715,5 +733,6 @@ + end (* structure *)