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 *}
ML {* val _ = recursive := 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_inject
thm t_tyS_bn
thm t_tyS_perm
thm t_tyS_induct
thm t_tyS_distinct

lemma supports:
  "(supp (atom i)) supports (Var i)"
  "(supp A \<union> supp M) supports (Fun A M)"
apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm)
apply clarify
apply(simp_all add: fresh_atom)
done

lemma fs:
  "finite (supp (x\<Colon>t)) \<and> finite (supp (z\<Colon>tyS))"
apply(induct rule: t_tyS_induct)
apply(rule supports_finite)
apply(rule supports)
apply(simp add: supp_atom)
apply(rule supports_finite)
apply(rule supports)
apply(simp add: supp_atom)
sorry

instance t and tyS :: fs
apply default
apply (simp_all add: fs)
sorry

(* Should be moved to a proper place *)
lemma infinite_Un:
  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
  by simp

lemma supp_fv_t_tyS:
  shows "supp T = fv_t T" 
  and   "supp S = fv_tyS S"
apply(induct T and S rule: t_tyS_inducts)
apply(simp_all add: t_tyS_fv)
(* VarTS case *)
apply(simp only: supp_def)
apply(simp only: t_tyS_perm)
apply(simp only: t_tyS_inject)
apply(simp only: supp_def[symmetric])
apply(simp only: supp_at_base)
(* FunTS case *)
apply(simp only: supp_def)
apply(simp only: t_tyS_perm)
apply(simp only: t_tyS_inject)
apply(simp only: de_Morgan_conj)
apply(simp only: Collect_disj_eq)
apply(simp only: infinite_Un)
apply(simp only: Collect_disj_eq)
(* All case *)
apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
apply(simp (no_asm) only: supp_def)
apply(simp only: t_tyS_perm)
apply(simp only: permute_ABS)
apply(simp only: t_tyS_inject)
apply(simp only: Abs_eq_iff)
apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
apply(simp only: alpha_gen)
apply(simp only: supp_eqvt[symmetric])
apply(simp only: eqvts)
apply(simp only: supp_Abs)
done

lemma
  shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
  apply(simp add: t_tyS_inject)
  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_inject)
  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_inject)
  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_inject)
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_inject)
  apply(clarify)
  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject)
  apply auto
  done


end