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 *}

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 b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"

  shows "P (a :: 'a :: pt) t \<and> P' d ts "

proof -

  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"

    apply (rule t_tyS.induct)

    apply (simp add: a1)

    apply (simp)

    apply (rule allI)+

    apply (rule a2)

    apply simp

    apply simp

    apply (rule allI)

    apply (rule allI)

    apply(subgoal_tac "\<exists>new::name fset. fset_to_set (fmap atom new) \<sharp>* (d, All (p \<bullet> fset) (p \<bullet> t))

                                      \<and> fcard new = fcard fset")

    apply clarify

    (*apply(rule_tac t="p \<bullet> All fset t" and 

                   s="(((p \<bullet> fset) \<leftrightarrow> new) + p) \<bullet> All fset t" in subst)

    apply (rule a3)

    apply simp_all*)

    sorry

  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast

  then show ?thesis 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