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 (Datatype.the_info @{theory} "TySch.ty") 1 *}
print_theorems

datatype tyS =
  All "name set" "ty"

setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *}
print_theorems

local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty")
 [[[[]], [[], []]]] *}
print_theorems

(*
Doesnot work yet since we do not refer to fv_ty
local_setup {* define_raw_fv (Datatype.the_info @{theory} "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