# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267103680 -3600
# Node ID 393aced4801dee6aba2873c5f9cc80f0da5279cf
# Parent  8c3cf9f4f5f2cc1873255035ff530d2829e5bcb9
Forgot to add one file.

diff -r 8c3cf9f4f5f2 -r 393aced4801d Nominal/TySch.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/TySch.thy	Thu Feb 25 14:14:40 2010 +0100
@@ -0,0 +1,82 @@
+theory TySch
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+text {* type schemes *}
+datatype ty =
+  Var "name"
+| Fun "ty" "ty"
+
+setup {* snd o define_raw_perms ["ty"] ["TySch.ty"] *}
+print_theorems
+
+datatype tyS =
+  All "name set" "ty"
+
+setup {* snd o define_raw_perms ["tyS"] ["TySch.tyS"] *}
+print_theorems
+
+local_setup {* snd o define_fv_alpha "TySch.ty" [[[[]], [[], []]]] *}
+print_theorems
+
+(*
+Doesnot work yet since we do not refer to fv_ty
+local_setup {* define_raw_fv "TySch.tyS" [[[[], []]]] *}
+print_theorems
+*)
+
+primrec
+  fv_tyS
+where
+  "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
+
+inductive
+  alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
+where
+  a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2))
+        \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
+
+lemma
+  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
+  apply(rule a1)
+  apply(simp add: alpha_gen)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: fresh_star_def)
+  done
+
+lemma
+  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
+  apply(rule a1)
+  apply(simp add: alpha_gen)
+  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+  apply(simp add: fresh_star_def)
+  done
+
+lemma
+  shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
+  apply(rule a1)
+  apply(simp add: alpha_gen)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: fresh_star_def)
+  done
+
+lemma
+  assumes a: "a \<noteq> b"
+  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
+  using a
+  apply(clarify)
+  apply(erule alpha_tyS.cases)
+  apply(simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(erule exE)
+  apply(erule conjE)+
+  apply(clarify)
+  apply(simp)
+  apply(simp add: fresh_star_def)
+  apply(auto)
+  done
+
+
+end