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)

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)

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