theory LetPat

imports "../Nominal2"

begin

atom_decl name

nominal_datatype trm =

  Var "name"

| App "trm" "trm"

| Lam x::"name" t::"trm"       binds x in t

| Let p::"pat" "trm" t::"trm"  binds "bn p" in t

and pat =

  PNil

| PVar "name"

| PTup "pat" "pat"

binder

  bn::"pat \<Rightarrow> atom list"

where

  "bn PNil = []"

| "bn (PVar x) = [atom x]"

| "bn (PTup p1 p2) = bn p1 @ bn p2"

thm trm_pat.eq_iff

thm trm_pat.distinct

thm trm_pat.induct

thm trm_pat.strong_induct[no_vars]

thm trm_pat.exhaust

thm trm_pat.strong_exhaust[no_vars]

thm trm_pat.fv_defs

thm trm_pat.bn_defs

thm trm_pat.perm_simps

thm trm_pat.eq_iff

thm trm_pat.fv_bn_eqvt

thm trm_pat.size

(* Nominal_Abs test *)

lemma alpha_res_alpha_set:

  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> 

  (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"

  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast

lemma

  fixes x::"'a::fs"

  assumes "(supp x - as) \<sharp>* p"

      and "p \<bullet> x = y"

      and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"

  shows "(as, x) \<approx>res (op =) supp p (bs, y)"

  using assms

  unfolding alpha_res_alpha_set

  unfolding alphas

  apply simp

  apply rule

  apply (rule trans)

  apply (rule supp_perm_eq[symmetric, of _ p])

  apply(subst supp_finite_atom_set)

  apply (metis finite_Diff finite_supp)

  apply (simp add: fresh_star_def)

  apply blast

  apply(perm_simp)

  apply(simp)

  done

lemma

  fixes x::"'a::fs"

  assumes "(supp x - as) \<sharp>* p"

      and "p \<bullet> x = y"

      and "p \<bullet> as = bs"

  shows "(as, x) \<approx>set (op =) supp p (bs, y)"

  using assms

  unfolding alphas

  apply simp

  apply (rule trans)

  apply (rule supp_perm_eq[symmetric, of _ p])

  apply(subst supp_finite_atom_set)

  apply (metis finite_Diff finite_supp)

  apply(simp)

  apply(perm_simp)

  apply(simp)

  done

lemma

  fixes x::"'a::fs"

  assumes "(supp x - set as) \<sharp>* p"

      and "p \<bullet> x = y"

      and "p \<bullet> as = bs"

  shows "(as, x) \<approx>lst (op =) supp p (bs, y)"

  using assms

  unfolding alphas

  apply simp

  apply (rule trans)

  apply (rule supp_perm_eq[symmetric, of _ p])

  apply(subst supp_finite_atom_set)

  apply (metis finite_Diff finite_supp)

  apply(simp)

  apply(perm_simp)

  apply(simp)

  done

end