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+
−