theory TySch
imports "Parser" "../Attic/Prove" "FSet"
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 fset" 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.inducts
thm t_tyS.distinct
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}

lemma finite_fv_t_tyS:
  shows "finite (fv_t t)" "finite (fv_tyS ts)"
  by (induct rule: t_tyS.inducts) (simp_all)

lemma supp_fv_t_tyS:
  shows "fv_t t = supp t" "fv_tyS ts = supp ts"
  apply(induct rule: t_tyS.inducts)
  apply(simp_all only: t_tyS.fv)
  prefer 3
  apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
  prefer 2
  apply(subst finite_supp_Abs)
  apply(drule sym)
  apply(simp add: finite_fv_t_tyS(1))
  apply(simp)
  apply(simp_all (no_asm) only: supp_def)
  apply(simp_all only: t_tyS.perm)
  apply(simp_all only: permute_ABS)
  apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
  apply(simp_all only: alpha_gen)
  apply(simp_all only: eqvts[symmetric])
  apply(simp_all only: eqvts eqvts_raw)
  apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
  apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
  apply(simp_all only: de_Morgan_conj[symmetric])
  done

instance t and tyS :: fs
  apply default
  apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
  done

lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]

lemma induct:
  assumes a1: "\<And>name b. P b (Var name)"
  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
  and     a3: "\<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
  shows "P a t"
proof -
  have "\<And>p. P a (p \<bullet> t)"
    apply (induct t rule: t_tyS.inducts(1))
    apply (simp add: a1)
    apply (simp_all)
    apply (rule_tac ?t1.0="p \<bullet> t1" and ?t2.0="p \<bullet> t2" in a2)
    sorry
  then have "P a (0 \<bullet> t)" by blast
  then show "P a t" by simp
qed

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 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(simp add: t_tyS.eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alpha_gen fresh_star_def 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 fresh_star_def eqvts t_tyS.eq_iff)
  apply auto
  done

end