theory Ex2

imports "../NewParser"

begin

text {* example 2 *}

atom_decl name

nominal_datatype trm =

  Var "name"

| App "trm" "trm"

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

| Let p::"pat" "trm" t::"trm"     bind "f p" in t

and pat =

  PN

| PS "name"

| PD "name" "name"

binder

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

where

  "f PN = []"

| "f (PS x) = [atom x]"

| "f (PD x y) = [atom x, atom y]"

thm trm_pat.bn

thm trm_pat.perm

thm trm_pat.induct

thm trm_pat.distinct

thm trm_pat.fv[simplified trm_pat.supp(1-2)]

lemma lets_overlap1:

  "atom a \<noteq> atom b \<Longrightarrow> Let (PD a a) x y \<noteq> Let (PD a b) x y"

  by (simp add: trm_pat.eq_iff alphas)

lemma lets_overlap2:

  "atom a \<notin> supp y \<Longrightarrow> atom b \<notin> supp y \<Longrightarrow> Let (PD a a) x y = Let (PD b b) x y"

  apply (simp add: trm_pat.eq_iff alphas trm_pat.supp)

  apply (rule_tac x="(a\<leftrightarrow>b)" in exI)

  apply (simp add: eqvts)

  apply (rule conjI)

  prefer 2

  apply (rule Nominal2_Supp.supp_perm_eq)

  apply (unfold fresh_star_def)

  apply (unfold fresh_def)

  apply (unfold flip_def)

  apply (simp_all add: supp_swap)

  apply auto

  done

end