# HG changeset patch # User Christian Urban # Date 1280394993 -3600 # Node ID 082d9fd28f89f39d9219f992088e0c22e2256442 # Parent b1b6489338504512171a9cf4347c0392ad4c69e6 helper lemmas for rsp-lemmas diff -r b1b648933850 -r 082d9fd28f89 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Jul 27 23:34:30 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Thu Jul 29 10:16:33 2010 +0100 @@ -24,6 +24,7 @@ thm alpha_bn_imps thm distinct thm eq_iff +thm eq_iff_simps thm fv_defs thm perm_simps thm perm_laws @@ -39,13 +40,13 @@ term alpha_bn - lemma a2: shows "alpha_trm_raw x1 y1 \ fv_trm_raw x1 = fv_trm_raw y1" and "alpha_assg_raw x2 y2 \ fv_assg_raw x2 = fv_assg_raw y2 \ bn_raw x2 = bn_raw y2" and "alpha_bn_raw x3 y3 \ fv_bn_raw x3 = fv_bn_raw y3" apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms) +apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps + alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms) done lemma [quot_respect]: @@ -59,24 +60,17 @@ "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(assumption) +apply(simp only: eq_iff) +apply(simp only: simp_thms) apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(assumption) -apply(assumption) +apply(simp only: eq_iff) +apply(tactic {* asm_full_simp_tac HOL_ss 1*}) apply(simp only: fun_rel_def) +apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2) apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2) -apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) +apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2) +apply(simp add: a2) apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) apply(simp only: fun_rel_def) apply(rule allI | rule impI)+ diff -r b1b648933850 -r 082d9fd28f89 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue Jul 27 23:34:30 2010 +0200 +++ b/Nominal/NewParser.thy Thu Jul 29 10:16:33 2010 +0100 @@ -362,7 +362,7 @@ (* definition of alpha_eq_iff lemmas *) (* they have a funny shape for the simplifier *) val _ = warning "Eq-iff theorems"; - val alpha_eq_iff = + val (alpha_eq_iff_simps, alpha_eq_iff) = if get_STEPS lthy > 5 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases else raise TEST lthy4 @@ -426,7 +426,9 @@ (* auxiliary lemmas for respectfulness proofs *) (* HERE *) - + val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns + alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 + val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test)) (* defining the quotient type *) val _ = warning "Declaring the quotient types" @@ -481,7 +483,8 @@ val (_, lthy8') = lthy8 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) - ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) + ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) + ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) diff -r b1b648933850 -r 082d9fd28f89 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Tue Jul 27 23:34:30 2010 +0200 +++ b/Nominal/nominal_dt_alpha.ML Thu Jul 29 10:16:33 2010 +0100 @@ -14,13 +14,16 @@ val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> term list -> term list -> bn_info -> thm list * thm list - val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list + val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> + thm list -> (thm list * thm list) 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_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 end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = @@ -333,7 +336,7 @@ val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms - |> map mk_simp_rule + |> `(map mk_simp_rule) end @@ -637,5 +640,78 @@ |> filter_out (is_true o concl_of) end + +(* helper lemmas for respectfulness for fv_raw / bn_raw *) + +fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = +let + val arg_tys = + alpha_trms + |> map fastype_of + |> map domain_type + + val fv_bn_tys1 = + (bns @ fvs) + |> map fastype_of + |> map domain_type + + val (arg_names1, (arg_names2, ctxt')) = + ctxt + |> Variable.variant_fixes (replicate (length arg_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_tys) "y") + + val args1 = map Free (arg_names1 ~~ arg_tys) + val args2 = map Free (arg_names2 ~~ arg_tys) + + val fv_bn_args1a = map (lookup (arg_tys ~~ args1)) fv_bn_tys1 + val fv_bn_args1b = map (lookup (arg_tys ~~ args2)) fv_bn_tys1 + val fv_bn_eqs1 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) + (bns @ fvs) (fv_bn_args1a ~~ fv_bn_args1b) + + val arg_bn_tys = + alpha_bn_trms + |> map fastype_of + |> map domain_type + + val fv_bn_tys2 = + fv_bns + |> map fastype_of + |> map domain_type + + val (arg_bn_names1, (arg_bn_names2, ctxt'')) = + ctxt' + |> Variable.variant_fixes (replicate (length arg_bn_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_bn_tys) "y") + + val args_bn1 = map Free (arg_bn_names1 ~~ fv_bn_tys2) + val args_bn2 = map Free (arg_bn_names2 ~~ fv_bn_tys2) + val fv_bn_eqs2 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) + fv_bns (args_bn1 ~~ args_bn2) + + val goal_rhs = + group (fv_bn_tys1 ~~ fv_bn_eqs1) + |> map snd + |> map (foldr1 HOLogic.mk_conj) + + val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) + (alpha_trms @ alpha_bn_trms) ((args1 ~~ args2) @ (args_bn1 ~~ args_bn2)) + + val goal = + map2 (curry HOLogic.mk_imp) goal_lhs (goal_rhs @ fv_bn_eqs2) + |> foldr1 HOLogic.mk_conj + |> HOLogic.mk_Trueprop + + val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} + @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) +in + Goal.prove ctxt'' [] [] goal (fn {context, ...} => + HEADGOAL (DETERM o (rtac alpha_induct) THEN_ALL_NEW (asm_full_simp_tac ss))) + |> singleton (ProofContext.export ctxt'' ctxt) + |> Datatype_Aux.split_conj_thm + |> map (fn th => zero_var_indexes (th RS mp)) + |> map Datatype_Aux.split_conj_thm + |> flat +end + end (* structure *)