# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295749762 -3600
# Node ID de3e4b121c22d580550214f414469b8b0546655a
# Parent  7b2691911fbcd4afeabf853ae285986fe6576ea3
added Tutorial6

diff -r 7b2691911fbc -r de3e4b121c22 Tutorial/Tutorial6.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial6.thy	Sun Jan 23 03:29:22 2011 +0100
@@ -0,0 +1,49 @@
+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
\ No newline at end of file