898 text {* type schemes *} 

   899 datatype ty = 

   900   Var "name" 

   901 | Fun "ty" "ty"

   902 

   903 instantiation

   904   ty :: pt

   905 begin

   906 

   907 primrec

   908   permute_ty 

   909 where

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

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

   912 

   913 lemma pt_ty_zero:

   914   fixes T::ty

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

   916 apply(induct T rule: ty.inducts)

   917 apply(simp_all)

   918 done

   919 

   920 lemma pt_ty_plus:

   921   fixes T::ty

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

   923 apply(induct T rule: ty.inducts)

   924 apply(simp_all)

   925 done

   926 

   927 instance

   928 apply default

   929 apply(simp_all add: pt_ty_zero pt_ty_plus)

   930 done

   931 

   933 

   934 datatype tyS = 

   935   All "name set" "ty" 

   936 

   937 instantiation

   938   tyS :: pt

   939 begin

   940 

   941 primrec

   942   permute_tyS 

   943 where

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

   945 

   946 lemma pt_tyS_zero:

   947   fixes T::tyS

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

   949 apply(induct T rule: tyS.inducts)

   950 apply(simp_all)

   951 done

   952 

   953 lemma pt_tyS_plus:

   954   fixes T::tyS

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

   956 apply(induct T rule: tyS.inducts)

   957 apply(simp_all)

   958 done

   959 

   960 instance

   961 apply default

   962 apply(simp_all add: pt_tyS_zero pt_tyS_plus)

   963 done

   964 

   965 end

   966 

   967 

   968 abbreviation

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

   970 

   971 primrec

   972   rfv_ty

   973 where

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

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

   976 

   977 primrec

   978   rfv_tyS

   979 where 

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

   981 

   982 inductive

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

   984 where

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

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

   987 

   988 lemma

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

   990   apply(rule a1)

   991   apply(simp add: alpha_gen)

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

   993   apply(simp add: fresh_star_def)

   994   done

   995 

   996 lemma

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

   998   apply(rule a1)

   999   apply(simp add: alpha_gen)

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

  1001   apply(simp add: fresh_star_def)

  1002   done

  1003 

  1004 lemma

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

  1006   apply(rule a1)

  1007   apply(simp add: alpha_gen)

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

  1009   apply(simp add: fresh_star_def)

  1010   done

  1011 

  1012 lemma

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

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

  1015   using a

  1016   apply(clarify)

  1017   apply(erule alpha_tyS.cases)

  1018   apply(simp add: alpha_gen)

  1019   apply(erule conjE)+

  1020   apply(erule exE)

  1021   apply(erule conjE)+

  1022   apply(clarify)

  1023   apply(simp)

  1024   apply(simp add: fresh_star_def)

  1025   apply(auto)

  1026   done

  1027 

  1028 

  1029 end