# HG changeset patch # User Cezary Kaliszyk # Date 1308103608 -32400 # Node ID 1af453d560839dd3b4488116a3cb0208ec025f59 # Parent 7661c4d7ca315a0320198f52b4b45a3c3fbd86d9# Parent b577f06e0804b466a13a8c25836cff9d87e613dd merge diff -r 7661c4d7ca31 -r 1af453d56083 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Wed Jun 15 09:51:26 2011 +0900 +++ b/Nominal/Ex/Let.thy Wed Jun 15 11:06:48 2011 +0900 @@ -90,6 +90,69 @@ lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] +lemma Abs_lst_fcb: + fixes xs ys :: "'a :: fs" + and S T :: "'b :: fs" + assumes e: "(Abs_lst (ba xs) T) = (Abs_lst (ba ys) S)" + and f1: "\x. x \ set (ba xs) \ x \ f xs T" + and f2: "\x. supp T - set (ba xs) = supp S - set (ba ys) \ x \ set (ba ys) \ x \ f xs T" + and eqv: "\p. p \ T = S \ p \ ba xs = ba ys \ supp p \ set (ba xs) \ set (ba ys) \ p \ (f xs T) = f ys S" + shows "f xs T = f ys S" + using e apply - + apply(subst (asm) Abs_eq_iff2) + apply(simp add: alphas) + apply(elim exE conjE) + 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 "(set (ba xs) \ set (ba ys)) \* f xs T") + apply(metis Un_absorb2 fresh_star_Un) + apply(subst fresh_star_Un) + apply(rule conjI) + apply(simp add: fresh_star_def f1) + apply(simp add: fresh_star_def f2) + apply(simp add: eqv) + done + +lemma max_eqvt[eqvt]: "p \ (max (a :: _ :: pure) b) = max (p \ a) (p \ b)" + by (simp add: permute_pure) + +(* TODO: should be provided by nominal *) +lemma [eqvt]: "p \ bn a = bn (p \ a)" + by descending (rule eqvts) + +(* PROBLEM: the proof needs induction on alpha_bn inside which is not possible... *) +nominal_primrec + height_trm :: "trm \ nat" +and height_assn :: "assn \ nat" +where + "height_trm (Var x) = 1" +| "height_trm (App l r) = max (height_trm l) (height_trm r)" +| "height_trm (Lam v b) = 1 + (height_trm b)" +| "height_trm (Let as b) = max (height_assn as) (height_trm b)" +| "height_assn ANil = 0" +| "height_assn (ACons v t as) = max (height_trm t) (height_assn as)" + apply (simp only: eqvt_def height_trm_height_assn_graph_def) + apply (rule, perm_simp, rule, rule TrueI) + apply (case_tac x) + apply (case_tac a rule: trm_assn.exhaust(1)) + apply (auto)[4] + apply (drule_tac x="assn" in meta_spec) + apply (drule_tac x="trm" in meta_spec) + apply (simp add: alpha_bn_refl) + apply (case_tac b rule: trm_assn.exhaust(2)) + apply (auto) + apply (erule Abs_lst1_fcb) + apply (simp_all add: pure_fresh) + apply (simp add: eqvt_at_def) + apply (erule Abs_lst_fcb) + apply (simp_all add: pure_fresh) + apply (simp_all add: eqvt_at_def eqvts) + oops + nominal_primrec subst :: "name \ trm \ trm \ trm" and substa :: "name \ trm \ assn \ assn" @@ -118,6 +181,7 @@ apply auto apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff]) + (*apply (erule Abs_lst1_fcb)*) prefer 3 apply (erule alpha_bn_inducts) apply (simp add: alpha_bn_refl)