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

lemma

  shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"

  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(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)

  apply(simp add: alpha_gen fresh_star_def eqvts)

  apply auto

  done

lemma

  shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"

  apply(rule_tac x="0::perm" in exI)

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(clarify)

  apply auto

  done

end