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"

lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s"
apply (simp add: supp_def)
apply (simp add: eqvts eqvts_raw)
(* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*)
sorry

lemma atom_image_swap_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at) set); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
apply (simp add: fresh_def)
apply (simp add: support_image)
apply (fold fresh_def)
apply (simp add: swap_fresh_fresh)
done

lemma "\<lbrakk>a \<sharp> atom ` fun; a \<sharp> t; b \<sharp> atom ` fun; b \<sharp> t\<rbrakk> \<Longrightarrow> All ((a \<rightleftharpoons> b) \<bullet> fun) t = All fun t"
apply (simp add: atom_image_swap_fresh)
done

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