# HG changeset patch # User Cezary Kaliszyk # Date 1306912422 -32400 # Node ID 5ecb857e9de72b0357b445f7237507fa5d2ae4c2 # Parent 6e518b436740b8c24eaa2ad1c1b8ebdf330a05de proved subst for All constructor in type schemes. diff -r 6e518b436740 -r 5ecb857e9de7 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Jun 01 13:41:30 2011 +0900 +++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 01 16:13:42 2011 +0900 @@ -78,13 +78,6 @@ "subst \ (Var X) = lookup \ X" | "subst \ (Fun T1 T2) = Fun (subst \ T1) (subst \ T2)" | "fset (map_fset atom xs) \* \ \ substs \ (All xs T) = All xs (subst \ T)" - -term subst_substs_sumC -thm subst_substs_sumC_def -term Inl -thm subst_substs_graph.induct -thm subst_substs_graph.intros -thm Projl.simps apply(subgoal_tac "\p x r. subst_substs_graph x r \ subst_substs_graph (p \ x) (p \ r)") apply(simp add: eqvt_def) apply(rule allI) @@ -192,7 +185,6 @@ apply (auto)[5] --"LAST GOAL" apply(simp del: ty_tys.eq_iff) -thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff] apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) apply (subgoal_tac "eqvt_at (\(l, r). subst l r) (\', T)") apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\', T))") @@ -343,45 +335,22 @@ lemma lookup2_eqvt[eqvt]: shows "(p \ lookup2 Ts T) = lookup2 (p \ Ts) (p \ T)" -apply(induct Ts T rule: lookup2.induct) -apply(simp_all) -done + by (induct Ts T rule: lookup2.induct) simp_all nominal_primrec subst :: "(name \ ty2) list \ ty2 \ ty2" where "subst \ (Var2 X) = lookup2 \ X" | "subst \ (Fun2 T1 T2) = Fun2 (subst \ T1) (subst \ T2)" -defer -apply(case_tac x) -apply(simp) -apply(rule_tac y="b" in ty2.exhaust) -apply(blast) -apply(blast) -apply(simp_all add: ty2.distinct) -apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ r)") -apply(simp add: eqvt_def) -apply(rule allI) -apply(simp add: permute_fun_def permute_bool_def) -apply(rule ext) -apply(rule ext) -apply(rule iffI) -apply(drule_tac x="p" in meta_spec) -apply(drule_tac x="- p \ x" in meta_spec) -apply(drule_tac x="- p \ xa" in meta_spec) -apply(simp) -apply(drule_tac x="-p" in meta_spec) -apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="xa" in meta_spec) -apply(simp) -apply(erule subst_graph.induct) -apply(perm_simp) -apply(rule subst_graph.intros) -apply(perm_simp) -apply(rule subst_graph.intros) -apply(assumption) -apply(assumption) -done + unfolding eqvt_def subst_graph_def + apply (rule, perm_simp, rule) + apply(case_tac x) + apply(simp) + apply(rule_tac y="b" in ty2.exhaust) + apply(blast) + apply(blast) + apply(simp_all add: ty2.distinct) + done termination apply(relation "measure (size o snd)") @@ -394,40 +363,87 @@ apply(simp_all add: lookup2_eqvt) done -lemma j: - assumes "a \ Ts" " a \ X" - shows "a \ lookup2 Ts X" -using assms -apply(induct Ts X rule: lookup2.induct) -apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair) -done - -lemma i: - assumes "a \ t" " a \ \" - shows "a \ subst \ t" -using assms -apply(induct \ t rule: subst.induct) -apply(auto simp add: ty2.fresh j) -done - -lemma k: - assumes "as \* t" " as \* \" - shows "as \* subst \ t" -using assms -by (simp add: fresh_star_def i) - -lemma h: - assumes "as \ bs \ cs" - and " cs \* x" - shows "(as - bs) \* x" -using assms -by (auto simp add: fresh_star_def) - +lemma supp_fun_app2_eqvt: + assumes e: "eqvt f" + shows "supp (f a b) \ supp a \ supp b" + using supp_fun_app_eqvt[OF e] supp_fun_app + by blast + +lemma supp_subst: + "supp (subst \ t) \ supp \ \ supp t" + apply (rule supp_fun_app2_eqvt) + unfolding eqvt_def by (simp add: eqvts_raw) + +lemma fresh_star_inter1: + "xs \* z \ (xs \ ys) \* z" + unfolding fresh_star_def by blast + nominal_primrec substs :: "(name \ ty2) list \ tys2 \ tys2" where "fset (map_fset atom xs) \* \ \ substs \ (All2 xs t) = All2 xs (subst \ t)" -oops + unfolding eqvt_def substs_graph_def + apply (rule, perm_simp, rule) + apply auto[1] + apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) + apply auto + apply (subst (asm) Abs_eq_res_set) + apply (subst (asm) Abs_eq_iff2) + apply (clarify) + apply (simp add: alphas) + 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 (rule finite_Diff) + apply (rule finite_supp) + apply (subgoal_tac "(atom ` fset xs \ supp t \ atom ` fset xsa \ supp (p \ t)) \* ([atom ` fset xs]res. subst \' t)") + apply (metis Un_absorb2 fresh_star_Un) + apply (subst fresh_star_Un) + apply (rule conjI) + apply (simp (no_asm) add: fresh_star_def) + apply (rule) + apply (simp add: Abs_fresh_iff) + apply (simp add: fresh_star_def) + apply (rule) + apply (simp (no_asm) add: Abs_fresh_iff) + apply auto[1] + apply (simp add: fresh_def supp_Abs) + apply (rule contra_subsetD) + apply (rule supp_subst) + apply auto[1] + apply simp + apply (subst Abs_eq_iff) + apply (rule_tac x="0::perm" in exI) + apply (subgoal_tac "p \ subst \' t = subst \' (p \ t)") + prefer 2 + apply (subgoal_tac "\' = p \ \'") + apply (simp add: subst_eqvt) + apply (rule sym) + apply (rule perm_supp_eq) + apply (subgoal_tac "(atom ` fset xs \ supp t \ atom ` fset xsa \ supp (p \ t)) \* \'") + apply (metis Diff_partition fresh_star_Un) + apply (simp add: fresh_star_Un fresh_star_inter1) + apply (simp add: alphas fresh_star_zero) + apply auto[1] + apply (subgoal_tac "atom xa \ supp(p \ t)") + apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD) + apply (drule subsetD[OF supp_subst]) + apply auto[1] + apply (simp add: fresh_star_def fresh_def) + apply (subgoal_tac "x \ supp(p \ t)") + apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt) + apply (rotate_tac 6) + apply (drule sym) + apply (simp add: subst_eqvt) + apply (drule subsetD[OF supp_subst]) + apply auto[1] + apply (rotate_tac 2) + apply (subst (asm) fresh_star_permute_iff[symmetric]) + apply (simp add: fresh_star_def fresh_def) + apply blast + done text {* Some Tests about Alpha-Equality *}