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

atom_decl name

ML {* val _ = cheat_fv_rsp := false *}
ML {* val _ = cheat_alpha_bn_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

lemma size_eqvt: "size (pi \<bullet> x) = size x"
sorry (* Can this be shown? *)

instantiation t and tyS :: size begin

quotient_definition
  "size_t :: t \<Rightarrow> nat"
is
  "size :: t_raw \<Rightarrow> nat"

quotient_definition
  "size_tyS :: tyS \<Rightarrow> nat"
is
  "size :: tyS_raw \<Rightarrow> nat"

lemma size_rsp:
  "alpha_t_raw x y \<Longrightarrow> size x = size y"
  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
  apply (simp_all only: t_raw_tyS_raw.size)
  apply (simp_all only: alpha_gen)
  apply clarify
  apply (simp_all only: size_eqvt)
  done

lemma [quot_respect]:
  "(alpha_t_raw ===> op =) size size"
  "(alpha_tyS_raw ===> op =) size size"
  by (simp_all add: size_rsp)

lemma [quot_preserve]:
  "(rep_t ---> id) size = size"
  "(rep_tyS ---> id) size = size"
  by (simp_all add: size_t_def size_tyS_def)

instance
  by default

end

thm t_raw_tyS_raw.size(4)[quot_lifted]
thm t_raw_tyS_raw.size(5)[quot_lifted]
thm t_raw_tyS_raw.size(6)[quot_lifted]


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

lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]

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