761 text {* type schemes *} 

   762 datatype ty = 

   763   Var "name" 

   764 | Fun "ty" "ty"

   765 

   766 instantiation

   767   ty :: pt

   768 begin

   769 

   770 primrec

   771   permute_ty 

   772 where

   773   "permute_ty pi (Var a) = Var (pi \<bullet> a)"

   774 | "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"

   775 

   776 lemma pt_ty_zero:

   777   fixes T::ty

   778   shows "0 \<bullet> T = T"

   779 apply(induct T rule: ty.inducts)

   780 apply(simp_all)

   781 done

   782 

   783 lemma pt_ty_plus:

   784   fixes T::ty

   785   shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"

   786 apply(induct T rule: ty.inducts)

   787 apply(simp_all)

   788 done

   789 

   790 instance

   791 apply default

   792 apply(simp_all add: pt_ty_zero pt_ty_plus)

   793 done

   796 

   797 datatype tyS = 

   798   All "name set" "ty" 

   799 

   800 instantiation

   801   tyS :: pt

   802 begin

   803 

   804 primrec

   805   permute_tyS 

   806 where

   807   "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"

   808 

   809 lemma pt_tyS_zero:

   810   fixes T::tyS

   811   shows "0 \<bullet> T = T"

   812 apply(induct T rule: tyS.inducts)

   813 apply(simp_all)

   814 done

   815 

   816 lemma pt_tyS_plus:

   817   fixes T::tyS

   818   shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"

   819 apply(induct T rule: tyS.inducts)

   820 apply(simp_all)

   821 done

   822 

   823 instance

   824 apply default

   825 apply(simp_all add: pt_tyS_zero pt_tyS_plus)

   826 done

   827 

   828 end

   829 

   830 

   831 abbreviation

   832   "atoms xs \<equiv> {atom x| x. x \<in> xs}"

   833 

   834 primrec

   835   rfv_ty

   836 where

   837   "rfv_ty (Var n) = {atom n}"

   838 | "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"

   839 

   840 primrec

   841   rfv_tyS

   842 where 

   843   "rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"

   844 

   845 inductive

   846   alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)

   847 where

   848   a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms xs2, T2)) 

   849         \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"

   850 

   851 lemma

   852   shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"

   853   apply(rule a1)

   854   apply(simp add: alpha_gen)

   855   apply(rule_tac x="0::perm" in exI)

   856   apply(simp add: fresh_star_def)

   857   done

   858 

   859 lemma

   860   shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"

   861   apply(rule a1)

   862   apply(simp add: alpha_gen)

   863   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)

   864   apply(simp add: fresh_star_def)

   865   done

   866 

   867 lemma

   868   shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"

   869   apply(rule a1)

   870   apply(simp add: alpha_gen)

   871   apply(rule_tac x="0::perm" in exI)

   872   apply(simp add: fresh_star_def)

   873   done

   874 

   875 lemma

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

   877   shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"

   878   using a

   879   apply(clarify)

   880   apply(erule alpha_tyS.cases)

   881   apply(simp add: alpha_gen)

   882   apply(erule conjE)+

   883   apply(erule exE)

   884   apply(erule conjE)+

   885   apply(clarify)

   886   apply(simp)

   887   apply(simp add: fresh_star_def)

   888   apply(auto)

   889   done

   890   

   891 

   892 end