theory Tutorial6imports "../Nominal/Nominal2"beginsection {* Type Schemes *}text {* Nominal2 can deal also with more complicated binding structures; for example the finite set of binders found in type schemes.*}atom_decl namenominal_datatype ty = Var "name"| Fun "ty" "ty" (infixr "\<rightarrow>" 100)and tys = All as::"name fset" ty::"ty" bind (set+) as in ty ("All _. _" [100, 100] 100)text {* Some alpha-equivalences *}lemma shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) = All {|b, a|}. (Var a) \<rightarrow> (Var b)" unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero)lemma shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) = All {|a, b|}. (Var b) \<rightarrow> (Var a)" unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def swap_atom) (metis permute_flip_at)lemma shows "All {|a, b, c|}. (Var a) \<rightarrow> (Var b) = All {|a, b|}. (Var a) \<rightarrow> (Var b)" unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero)lemma assumes a: "a \<noteq> b" shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) \<noteq> All {|c|}. (Var c) \<rightarrow> (Var c)" using a unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def)end