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