1 theory Tutorial6

     2 imports "../Nominal/Nominal2"

     3 begin

     4 

     5 

     6 section {* Type Schemes *}

     7 

     8 text {*

     9   Nominal2 can deal also with more complicated binding

    10   structures; for example the finite set of binders found

    11   in type schemes.

    12 *}

    13 

    14 atom_decl name

    15 

    16 nominal_datatype ty =

    17   Var "name"

    18 | Fun "ty" "ty" (infixr "\<rightarrow>" 100)

    19 and tys =

    20   All as::"name fset" ty::"ty" binds (set+) as in ty ("All _. _" [100, 100] 100)

    21 

    22 

    23 text {* Some alpha-equivalences *}

    24 

    25 lemma

    26   shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) = All {|b, a|}. (Var a) \<rightarrow> (Var b)"

    27   unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def

    28   by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero)

    29   

    30 lemma

    31   shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) = All {|a, b|}. (Var b) \<rightarrow> (Var a)"

    32   unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def

    33   by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def swap_atom)

    34      (metis permute_flip_at)

    35   

    36 lemma

    37   shows "All {|a, b, c|}. (Var a) \<rightarrow> (Var b) = All {|a, b|}. (Var a) \<rightarrow> (Var b)"

    38   unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def

    39   by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero)

    40   

    41 lemma

    42   assumes a: "a \<noteq> b"

    43   shows "All {|a, b|}. (Var a) \<rightarrow> (Var b) \<noteq> All {|c|}. (Var c) \<rightarrow> (Var c)"

    44   using a

    45   unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def

    46   by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def)

    47 

    48 

    49 end