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