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

lemma permute_rsp_fset[quot_respect]:
  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
  apply (simp add: eqvts[symmetric])
  apply clarify
  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
  apply (subst mem_eqvt[symmetric])
  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
  apply (subst mem_eqvt[symmetric])
  apply (erule_tac x="- x \<bullet> xb" in allE)
  apply simp
  done

instantiation FSet.fset :: (pt) pt
begin

term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"

quotient_definition
  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
is
  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"

lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
by (rule permute_zero)

lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
by (lifting permute_list_zero)

lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
by (rule permute_plus)

lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
by (lifting permute_list_plus)

instance
apply default
apply (rule permute_fset_zero)
apply (rule permute_fset_plus)
done

end

lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
by (lifting set_eqvt)

thm list_induct2'[no_vars]

lemma fset_induct2:
    "Pa {||} {||} \<Longrightarrow>
    (\<forall>x xs. Pa (finsert x xs) {||}) \<Longrightarrow>
    (\<forall>y ys. Pa {||} (finsert y ys)) \<Longrightarrow>
    (\<forall>x xs y ys. Pa xs ys \<longrightarrow> Pa (finsert x xs) (finsert y ys)) \<Longrightarrow>
    Pa xsa ysa"
by (lifting list_induct2')

lemma set_cong: "(set x = set y) = (x \<approx> y)"
  apply rule
  apply simp_all
  apply (induct x y rule: list_induct2')
  apply simp_all
  apply auto
  done

lemma fset_cong:
  "(fset_to_set x = fset_to_set y) = (x = y)"
  by (lifting set_cong)

lemma supp_fset_to_set:
  "supp (fset_to_set x) = supp x"
  apply (simp add: supp_def)
  apply (simp add: eqvts)
  apply (simp add: fset_cong)
  done

lemma inj_map_eq_iff:
  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
  by (simp add: Set.expand_set_eq[symmetric] inj_image_eq_iff)

lemma inj_fmap_eq_iff:
  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
  by (lifting inj_map_eq_iff)

lemma atom_fmap_cong:
  shows "(fmap atom x = fmap atom y) = (x = y)"
  apply(rule inj_fmap_eq_iff)
  apply(simp add: inj_on_def)
  done

lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
apply (induct l)
apply (simp_all)
apply (simp only: eqvt_apply)
done

lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
by (lifting map_eqvt)

lemma supp_fmap_atom:
  "supp (fmap atom x) = supp x"
  apply (simp add: supp_def)
  apply (simp add: eqvts eqvts_raw atom_fmap_cong)
  done

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

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

lemma infinite_Un:
  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
  by simp

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



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