theory Tutorial6
imports "../Nominal/Nominal2"
begin


section {* 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 name

nominal_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