150 nominal_datatype path = Left | Right | In

   150 nominal_datatype path = Left | Right | In

   151 

   151 

   152 section {* Paths to a free variables *} 

   152 section {* Paths to a free variables *} 

   153 

   153 

   154 instance path :: pure

   154 instance path :: pure

   156 apply(induct_tac "x::path" rule: path.induct)

   156 apply(induct_tac "x::path" rule: path.induct)

   157 apply(simp_all)

   157 apply(simp_all)

   158 done

   158 done

   159 

   159 

   160 nominal_function 

   160 nominal_function 

   613   DBVar nat

   613   DBVar nat

   614 | DBApp db db

   614 | DBApp db db

   615 | DBLam db

   615 | DBLam db

   616 

   616 

   617 instance db :: pure

   617 instance db :: pure

   619   apply (induct_tac x rule: db.induct)

   619   apply (induct_tac x rule: db.induct)

   620   apply (simp_all add: permute_pure)

   620   apply (simp_all add: permute_pure)

   621   done

   621   done

   622 

   622 

   623 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"

   623 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"

   928 lemma abs_same_binder:

   928 lemma abs_same_binder:

   929   fixes t ta s sa :: "_ :: fs"

   929   fixes t ta s sa :: "_ :: fs"

   930   and x y::"'a::at"

   930   and x y::"'a::at"

   931   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa

   931   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa

   932      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"

   932      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"

   934 

   934 

   935 nominal_function

   935 nominal_function

   936   aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"

   936   aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"

   937 where

   937 where

   938   "aux2 (Var x) (Var y) = (x = y)"

   938   "aux2 (Var x) (Var y) = (x = y)"