# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265203345 -3600
# Node ID 277301dc5c4c7336ebff7332b4da9d9ef6d24d91
# Parent  e8bb5f85e510328b4de724c7387e4e6c65ecea57# Parent  a83ee7ecb1cbdeda53f792486bb7d21e5a8f87cc
merge

diff -r e8bb5f85e510 -r 277301dc5c4c Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 14:19:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 14:22:25 2010 +0100
@@ -38,7 +38,6 @@
 | "rfv_bp (BUnit) = {}"
 | "rfv_bp (BVr x) = {atom x}"
 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"
-print_theorems
 
 (* needs to be stated by the package *)
 instantiation 
@@ -896,4 +895,135 @@
 sorry
 
 
+text {* type schemes *} 
+datatype ty = 
+  Var "name" 
+| Fun "ty" "ty"
+
+instantiation
+  ty :: pt
+begin
+
+primrec
+  permute_ty 
+where
+  "permute_ty pi (Var a) = Var (pi \<bullet> a)"
+| "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"
+
+lemma pt_ty_zero:
+  fixes T::ty
+  shows "0 \<bullet> T = T"
+apply(induct T rule: ty.inducts)
+apply(simp_all)
+done
+
+lemma pt_ty_plus:
+  fixes T::ty
+  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
+apply(induct T rule: ty.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_ty_zero pt_ty_plus)
+done
+
 end
+
+datatype tyS = 
+  All "name set" "ty" 
+
+instantiation
+  tyS :: pt
+begin
+
+primrec
+  permute_tyS 
+where
+  "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"
+
+lemma pt_tyS_zero:
+  fixes T::tyS
+  shows "0 \<bullet> T = T"
+apply(induct T rule: tyS.inducts)
+apply(simp_all)
+done
+
+lemma pt_tyS_plus:
+  fixes T::tyS
+  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
+apply(induct T rule: tyS.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_tyS_zero pt_tyS_plus)
+done
+
+end
+
+
+abbreviation
+  "atoms xs \<equiv> {atom x| x. x \<in> xs}"
+
+primrec
+  rfv_ty
+where
+  "rfv_ty (Var n) = {atom n}"
+| "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"
+
+primrec
+  rfv_tyS
+where 
+  "rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"
+
+inductive
+  alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
+where
+  a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms 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