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 ["ty"] ["TySch.ty"] *}

print_theorems

datatype tyS =

  All "name set" "ty"

setup {* snd o define_raw_perms ["tyS"] ["TySch.tyS"] *}

print_theorems

local_setup {* snd o define_fv_alpha "TySch.ty" [[[[]], [[], []]]] *}

print_theorems

(*

Doesnot work yet since we do not refer to fv_ty

local_setup {* define_raw_fv "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