theory TySch
imports "Parser" "../Attic/Prove"
begin

atom_decl name

ML {* val _ = cheat_fv_rsp := false *}
ML {* val _ = cheat_const_rsp := false *}
ML {* val _ = cheat_equivp := false *}
ML {* val _ = cheat_fv_eqvt := false *}
ML {* val _ = cheat_alpha_eqvt := false *}

nominal_datatype t =
  Var "name"
| Fun "t" "t"
and tyS =
  All xs::"name set" ty::"t" bind xs in ty

thm t_tyS_fv
thm t_tyS_eq_iff
thm t_tyS_bn
thm t_tyS_perm
thm t_tyS_induct
thm t_tyS_distinct

lemma
  shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
  apply(simp add: t_tyS_eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alpha_gen)
  apply(auto)
  apply(simp add: fresh_star_def fresh_zero_perm)
  done

lemma
  shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
  apply(simp add: t_tyS_eq_iff)
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts)
  apply auto
  done

lemma
  shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
  apply(simp add: t_tyS_eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
oops

lemma
  assumes a: "a \<noteq> b"
  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
  using a
  apply(simp add: t_tyS_eq_iff)
  apply(clarify)
  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
  apply auto
  done

end