# HG changeset patch # User Christian Urban # Date 1303962661 -28800 # Node ID d29a8a6f3138a3f1d7c2cc6e63de6b95b3c41943 # Parent c3ff26204d2ac3a8a14a28f1f1a46f127011f0f2# Parent fc21ba07e51e665a4828a32597cdfa20929d881f merged diff -r c3ff26204d2a -r d29a8a6f3138 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Apr 28 11:44:36 2011 +0800 +++ b/Nominal/Ex/Lambda.thy Thu Apr 28 11:51:01 2011 +0800 @@ -16,10 +16,40 @@ Var: "triv (Var x) n" equivariance triv -nominal_inductive triv avoids Var : "{}::name set" -apply(auto simp add: fresh_star_def) -done +nominal_inductive triv avoids Var: "{}::name set" +apply(auto simp add: fresh_star_def) +done + +inductive + triv2 :: "lam \ nat \ bool" +where + Var1: "triv2 (Var x) 0" +| Var2: "triv2 (Var x) (n + n)" +| Var3: "triv2 (Var x) n" + +equivariance triv2 +nominal_inductive triv2 . +lemma Abs1_eq_fdest: + fixes x y :: "'a :: at_base" + and S T :: "'b :: fs" + assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" + and "x \ y \ atom y \ T \ atom x \ f x T" + and "x \ y \ atom y \ T \ atom y \ f x T" + and "x \ y \ atom y \ T \ (atom x \ atom y) \ T = S \ (atom x \ atom y) \ (f x T) = f y S" + and "sort_of (atom x) = sort_of (atom y)" + shows "f x T = f y S" +using assms apply - +apply (subst (asm) Abs1_eq_iff') +apply simp_all +apply (elim conjE disjE) +apply simp +apply(rule trans) +apply (rule_tac p="(atom x \ atom y)" in supp_perm_eq[symmetric]) +apply(rule fresh_star_supp_conv) +apply(simp add: supp_swap fresh_star_def) +apply(simp add: swap_commute) +done text {* height function *} @@ -32,11 +62,8 @@ defer apply(rule_tac y="x" in lam.exhaust) apply(auto simp add: lam.distinct lam.eq_iff) -apply(simp add: Abs_eq_iff alphas) -apply(clarify) -apply(subst (4) supp_perm_eq[where p="p", symmetric]) -apply(simp add: pure_supp fresh_star_def) -apply(simp add: eqvt_at_def) +apply (erule Abs1_eq_fdest) +apply(simp_all add: fresh_def pure_supp eqvt_at_def) apply(subgoal_tac "\p x r. height_graph x r \ height_graph (p \ x) (p \ r)") unfolding eqvt_def apply(rule allI) @@ -82,23 +109,12 @@ defer apply(rule_tac y="x" in lam.exhaust) apply(simp_all)[3] -apply(simp_all only: lam.distinct) -apply(simp add: lam.eq_iff) -apply(simp add: lam.eq_iff) -apply(simp add: lam.eq_iff) -apply(simp add: Abs_eq_iff) -apply(erule exE) -apply(simp add: alphas) -apply(simp add: atom_eqvt) -apply(clarify) -apply(rule trans) -apply(rule_tac p="p" in supp_perm_eq[symmetric]) -apply(simp (no_asm) add: supp_removeAll) +apply(simp_all add: lam.distinct lam.eq_iff) +apply (erule Abs1_eq_fdest) +apply(simp add: supp_removeAll fresh_def) apply(drule supp_eqvt_at) apply(simp add: finite_supp) -apply(auto simp add: fresh_star_def)[1] -unfolding eqvt_at_def -apply(simp only: removeAll_eqvt atom_eqvt) +apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) apply(subgoal_tac "\p x r. frees_lst_graph x r \ frees_lst_graph (p \ x) (p \ r)") unfolding eqvt_def apply(rule allI) @@ -151,36 +167,15 @@ apply(auto simp add: lam.distinct lam.eq_iff) apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) apply(blast)+ -apply(simp add: fresh_star_def) -apply(subgoal_tac "atom xa \ [[atom x]]lst. t") -apply(subst (asm) Abs_eq_iff2) -apply(simp add: alphas atom_eqvt) -apply(clarify) -apply(rule trans) -apply(rule_tac p="p" in supp_perm_eq[symmetric]) -apply(rule fresh_star_supp_conv) -apply(drule fresh_star_perm_set_conv) -apply(simp add: finite_supp) -apply(subgoal_tac "{atom (p \ x), atom x} \* ([[atom x]]lst. subst_sumC (t, ya, sa))") -apply(auto simp add: fresh_star_def)[1] -apply(simp (no_asm) add: fresh_star_def) -apply(rule conjI) -apply(simp (no_asm) add: Abs_fresh_iff) -apply(clarify) -apply(drule_tac a="atom (p \ x)" in fresh_eqvt_at) -apply(simp add: finite_supp) -apply(simp (no_asm_use) add: fresh_Pair) -apply(simp add: Abs_fresh_iff) -apply(simp) -apply(simp add: Abs_fresh_iff) -apply(subgoal_tac "p \ ya = ya") -apply(subgoal_tac "p \ sa = sa") -apply(simp add: atom_eqvt eqvt_at_def) -apply(rule perm_supp_eq) -apply(auto simp add: fresh_star_def fresh_Pair)[1] -apply(rule perm_supp_eq) -apply(auto simp add: fresh_star_def fresh_Pair)[1] -apply(simp add: Abs_fresh_iff) +apply(simp_all add: fresh_star_def fresh_Pair_elim) +apply (erule Abs1_eq_fdest) +apply(simp_all add: Abs_fresh_iff) +apply(drule_tac a="atom (xa)" in fresh_eqvt_at) +apply(simp_all add: finite_supp fresh_Pair) +apply(subgoal_tac "(atom x \ atom xa) \ sa = sa") +apply(subgoal_tac "(atom x \ atom xa) \ ya = ya") +apply(simp add: eqvt_at_def) +apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ r)") unfolding eqvt_def apply(rule allI) @@ -256,6 +251,28 @@ apply (auto simp add: lam.fresh fresh_at_base) done +lemma height_ge_one: + shows "1 \ (height e)" +by (induct e rule: lam.induct) (simp_all) + +theorem height_subst: + shows "height (e[x::=e']) \ ((height e) - 1) + (height e')" +proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) + case (Var y) + have "1 \ height e'" by (rule height_ge_one) + then show "height (Var y[x::=e']) \ height (Var y) - 1 + height e'" by simp +next + case (Lam y e1) + hence ih: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" by simp + moreover + have vc: "atom y\x" "atom y\e'" by fact+ (* usual variable convention *) + ultimately show "height ((Lam [y]. e1)[x::=e']) \ height (Lam [y]. e1) - 1 + height e'" by simp +next + case (App e1 e2) + hence ih1: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" + and ih2: "height (e2[x::=e']) \ ((height e2) - 1) + (height e')" by simp_all + then show "height ((App e1 e2)[x::=e']) \ height (App e1 e2) - 1 + height e'" by simp +qed subsection {* single-step beta-reduction *} @@ -332,9 +349,7 @@ lemma [eqvt]: shows "(p \ lookup xs n x) = lookup (p \ xs) (p \ n) (p \ x)" - apply(induct xs arbitrary: n) - apply(simp_all add: permute_pure) - done + by (induct xs arbitrary: n) (simp_all add: permute_pure) nominal_primrec trans :: "lam \ name list \ ln" @@ -349,50 +364,18 @@ apply(simp_all add: fresh_star_def)[3] apply(blast) apply(blast) -apply(simp_all add: lam.distinct) -apply(simp add: lam.eq_iff) -apply(simp add: lam.eq_iff) -apply(simp add: lam.eq_iff) -apply(erule conjE) -apply(subgoal_tac "atom xa \ [[atom x]]lst. t") +apply(simp_all add: lam.distinct lam.eq_iff) +apply(elim conjE) +apply clarify +apply (erule Abs1_eq_fdest) +apply (simp_all add: ln.fresh) prefer 2 -apply(simp add: Abs_fresh_iff) -apply(subst (asm) Abs_eq_iff2) -apply(auto) -apply(simp add: alphas) -apply(simp add: atom_eqvt) -apply(clarify) -apply(rule trans) -apply(rule_tac p="p" in supp_perm_eq[symmetric]) +apply(drule supp_eqvt_at) +apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] prefer 2 -apply (subgoal_tac "p \ xsa = xsa") +apply (subgoal_tac "(atom x \ atom xa) \ xsa = xsa") apply (simp add: eqvt_at_def) -apply (rule supp_perm_eq) -apply (rule fresh_star_supp_conv) -apply (subgoal_tac "{atom (p \ x), atom x} \* xsa") -apply (simp add: fresh_star_def fresh_def) -apply blast -apply (simp add: fresh_star_def fresh_def) -apply (simp add: ln.supp) -apply(rule fresh_star_supp_conv) -apply (subst (asm) supp_perm_pair) -apply (elim disjE) -apply (simp add: fresh_star_def supp_zero_perm) -apply (simp add: flip_def[symmetric]) -apply(subgoal_tac "supp (x \ p \ x) \* trans_sumC (t, x # xsa)") -apply simp -apply (subst flip_def) -apply (simp add: supp_swap) -apply (simp add: fresh_star_def) -apply (rule) -apply rule -prefer 2 -apply(drule_tac a="atom (p \ x)" in fresh_eqvt_at) -apply(simp add: finite_supp) -apply(simp (no_asm_use) add: fresh_Pair) -apply(simp add: Abs_fresh_iff fresh_Cons)[1] -apply (metis Rep_name_inverse atom_name_def fresh_at_base) -apply assumption +apply (metis atom_name_def swap_fresh_fresh) oops (* lemma helpr: "atom x \ ta \ Lam [xa]. ta = Lam [x]. ((xa \ x) \ ta)" diff -r c3ff26204d2a -r d29a8a6f3138 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Thu Apr 28 11:44:36 2011 +0800 +++ b/Nominal/Nominal2.thy Thu Apr 28 11:51:01 2011 +0800 @@ -323,19 +323,19 @@ val _ = trace_msg (K "Defining the quotient constants...") val qconstrs_descrs = - (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs + (map2 o map2) (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) (get_cnstrs dts) raw_constrs val qbns_descr = - map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns + map2 (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) bn_funs raw_bns val qfvs_descr = map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs val qfv_bns_descr = - map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns + map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.name b, t, NoSyn)) bn_funs raw_fv_bns val qalpha_bns_descr = - map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms + map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.name b, t, NoSyn)) bn_funs alpha_bn_trms val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs @@ -344,7 +344,7 @@ map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms val qperm_bn_descr = - map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns + map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.name b, t, NoSyn)) bn_funs raw_perm_bns val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8) = @@ -646,7 +646,7 @@ val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = tmp_thy - |> Sign.add_types pre_typs + |> Sign.add_types_global pre_typs |> prepare_dts dt_strs ||>> prepare_bn_funs bn_fun_strs bn_eq_strs ||>> prepare_bclauses dt_strs diff -r c3ff26204d2a -r d29a8a6f3138 Nominal/nominal_inductive.ML --- a/Nominal/nominal_inductive.ML Thu Apr 28 11:44:36 2011 +0800 +++ b/Nominal/nominal_inductive.ML Thu Apr 28 11:51:01 2011 +0800 @@ -139,10 +139,10 @@ in (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) -val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel} +val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig -fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig +fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig end @@ -175,7 +175,9 @@ val prm_tys = map (fastype_of o term_of) prms val cperms = map (cterm_of thy o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms - val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem + val prem' = prem + |> cterm_instantiate (intr_cvars ~~ p_prms) + |> eqvt_srule ctxt (* for inductive-premises*) fun tac1 prm = helper_tac true prm p context @@ -189,7 +191,9 @@ fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in - EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ] + EVERY1 [ eqvt_stac context, + rtac prem', + RANGE (map (SUBGOAL o select) prems) ] end) ctxt fun fresh_thm ctxt user_thm p c concl_args avoid_trm = @@ -244,7 +248,9 @@ val cperms = map (cterm_of thy o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms - val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem + val prem' = prem + |> cterm_instantiate (intr_cvars ~~ qp_prms) + |> eqvt_srule ctxt val fprop' = eqvt_srule ctxt' fprop val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) @@ -277,7 +283,8 @@ val tac1 = non_binder_tac prem intr_cvars Ps ctxt val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt in - EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ] + EVERY' [ rtac @{thm allI}, rtac @{thm allI}, + if null avoid then tac1 else tac2 ] end fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args