# HG changeset patch # User Christian Urban # Date 1310048223 -7200 # Node ID d0f83a35950ef700b156a42cf46effe5015c337c # Parent 01ff621599bcfc3f4a2d7a669aaa1002ac221f63# Parent 7e1c309bf820114d34b031f487451cbdd4c320b9 merged diff -r 01ff621599bc -r d0f83a35950e Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Thu Jul 07 16:16:42 2011 +0200 +++ b/Nominal/Ex/Let.thy Thu Jul 07 16:17:03 2011 +0200 @@ -31,6 +31,7 @@ thm trm_assn.bn_defs thm trm_assn.bn_inducts thm trm_assn.perm_simps +thm trm_assn.permute_bn thm trm_assn.induct thm trm_assn.inducts thm trm_assn.distinct diff -r 01ff621599bc -r d0f83a35950e Nominal/Ex/LetInv.thy --- a/Nominal/Ex/LetInv.thy Thu Jul 07 16:16:42 2011 +0200 +++ b/Nominal/Ex/LetInv.thy Thu Jul 07 16:17:03 2011 +0200 @@ -238,7 +238,12 @@ apply (auto simp add: fresh_star_def)[3] apply (drule_tac x="assn" in meta_spec) apply (simp add: Abs1_eq_iff alpha_bn_refl) - apply auto + apply auto[7] + prefer 2 + apply(simp) + thm subst_sumC_def + thm THE_default_def + thm theI apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) apply (simp add: Abs_fresh_iff) apply (simp add: fresh_star_def) diff -r 01ff621599bc -r d0f83a35950e Nominal/Ex/NBE.thy --- a/Nominal/Ex/NBE.thy Thu Jul 07 16:16:42 2011 +0200 +++ b/Nominal/Ex/NBE.thy Thu Jul 07 16:17:03 2011 +0200 @@ -13,7 +13,7 @@ nominal_datatype sem = - L e::"env" x::"name" l::"lam" binds "bn e" x in l + L e::"env" x::"name" l::"lam" binds x "bn e" in l | N "neu" and neu = V "name" @@ -25,7 +25,8 @@ bn where "bn ENil = []" -| "bn (ECons env x v) = atom x # bn env" +| "bn (ECons env x v) = (atom x) # (bn env)" + nominal_primrec evals :: "env \ lam \ sem" and @@ -121,23 +122,33 @@ done lemma test: + fixes env::"env" shows "supp (evals env t) \ (supp t - set (bn env)) \ (fv_bn env)" - and "supp (evals_aux s t env) \ ((supp s) - set (bn cenv)) \ supp (fn cenv) \ supp (evals env t)" -apply(induct rule: evals_evals_aux.induct) + and "supp (evals_aux s t env) \ (supp s) \ (fv_bn env) \ (supp (t) - set (bn env))" +apply(induct env t and s t env rule: evals_evals_aux.induct) apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs) apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs) apply(rule conjI) apply(auto)[1] apply(rule impI) apply(simp) -apply (metis (no_types) at_base_infinite finite_UNIV) +apply(simp add: supp_at_base) +apply(blast) apply(simp) apply(subst sem_neu_env.supp) apply(simp add: sem_neu_env.supp lam.supp) apply(auto)[1] -apply(simp) -apply(metis) -sorry +apply(simp add: lam.supp sem_neu_env.supp) +apply(blast) +apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs) +prefer 2 +apply(simp add: sem_neu_env.supp) +apply(rule conjI) +apply(blast) +apply(blast) +apply(blast) +done + nominal_primrec reify :: "sem \ lam" and @@ -197,13 +208,13 @@ apply(simp) apply(erule conjE) apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff]) -apply (subgoal_tac "eqvt_at (\t. reify t) (evals (ECons enva y (N (V x))) t)") +apply (subgoal_tac "eqvt_at (\t. reify t) (evals (ECons env y (N (V x))) t)") apply (subgoal_tac "eqvt_at (\t. reify t) (evals (ECons enva ya (N (V xa))) ta)") -apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva y (N (V x))) t))") +apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons env y (N (V x))) t))") apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))") defer apply (simp_all add: eqvt_at_def reify_def)[2] -apply(subgoal_tac "\c::name. atom c \ (x, xa, enva, y, ya, t, ta)") +apply(subgoal_tac "\c::name. atom c \ (x, xa, env, enva, y, ya, t, ta)") prefer 2 apply(rule obtain_fresh) apply(blast) @@ -218,7 +229,7 @@ back apply(assumption) apply(simp add: finite_supp) -apply(rule_tac S="supp (enva, y, x, t)" in supports_fresh) +apply(rule_tac S="supp (env, y, x, t)" in supports_fresh) apply(simp add: supports_def fresh_def[symmetric]) apply(perm_simp) apply(simp add: swap_fresh_fresh fresh_Pair) @@ -250,6 +261,49 @@ apply(perm_simp) apply(simp add: flip_fresh_fresh) apply(simp (no_asm) add: Abs1_eq_iff) +thm at_set_avoiding3 +using at_set_avoiding3 +apply - +apply(drule_tac x="set (atom y # bn env)" in meta_spec) +apply(drule_tac x="(env, enva)" in meta_spec) +apply(drule_tac x="[atom y # bn env]lst. t" in meta_spec) +apply(simp (no_asm_use) add: finite_supp) +apply(drule meta_mp) +apply(rule Abs_fresh_star) +apply(auto)[1] +apply(erule exE) +apply(erule conjE)+ +apply(drule_tac q="(x \ c)" in eqvt_at_perm) +apply(perm_simp) +apply(simp add: flip_fresh_fresh fresh_Pair) +apply(drule_tac q="(xa \ c)" in eqvt_at_perm) +apply(perm_simp) +apply(simp add: flip_fresh_fresh fresh_Pair) +apply(drule sym) +apply(rotate_tac 9) +apply(drule trans) +apply(rule sym) +(* HERE *) + +apply(rule_tac p="p" in supp_perm_eq) +apply(simp) +apply(perm_simp) +apply(simp add: Abs_eq_iff2 alphas) +apply(clarify) +apply(rule trans) +apply(rule sym) +apply(rule_tac p="pa" in perm_supp_eq) +defer +apply(rule sym) +apply(rule trans) +apply(rule sym) +apply(rule_tac p="p" in perm_supp_eq) +defer +apply(simp add: atom_eqvt) +apply(drule_tac q="(x \ c)" in eqvt_at_perm) +apply(perm_simp) +apply(simp add: flip_fresh_fresh fresh_Pair) + apply(rule sym) apply(erule_tac Abs_lst1_fcb2') apply(rule fresh_eqvt_at)