| Fun "ty" "ty" ("_ \<rightarrow> _")

  All xs::"name fset" ty::"ty" binds (set+) xs in ty ("All [_]._")

subsection {* Substitution function for types and type schemes *}

type_synonym 

  Subst = "(name \<times> ty) list"

  lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"

  subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)

  "\<theta><Var X> = lookup \<theta> X"

| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"

  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)

  "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"

  apply(subgoal_tac "x \<in> supp T")

  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa")

  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")

  apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'")

  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"

  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"

  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"

  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"

text {* HERE *}

fun 

  compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)

where

  "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"

| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"

lemma compose_eqvt:

  fixes  \<theta>1 \<theta>2::"Subst"

  shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))"

apply(induct \<theta>2) 

apply(auto simp add: subst.eqvt)

done

lemma compose_ty:

  fixes  \<theta>1 :: "Subst"

  and    \<theta>2 :: "Subst"

  and    T :: "ty"

  shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"

proof (induct T rule: ty.induct)

  case (Var X) 

  have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X" 

    by (induct \<theta>2) (auto)

  then show ?case by simp

next

  case (Fun T1 T2)

  then show ?case by simp

qed

fun

  dom :: "Subst \<Rightarrow> name fset"

where

  "dom [] = {||}"

| "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"

lemma dom_eqvt[eqvt]:

  shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"

apply(induct \<theta> rule: dom.induct)

apply(simp_all)

done

nominal_primrec

  ftv  :: "ty \<Rightarrow> name fset"

where

  "ftv (Var X) = {|X|}"

| "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"

  unfolding eqvt_def ftv_graph_def

  apply (rule, perm_simp, rule)

  apply(auto)[2]

  apply(rule_tac y="x" in ty.exhaust)

  apply(blast)

  apply(blast)

  apply(simp_all)

  done

termination (eqvt)

  by lexicographic_order

lemma s1:

  fixes T::"ty"

  shows "(X \<leftrightarrow> Y) \<bullet> T = [(X, Var Y),(Y, Var X)]<T>"

apply(induct T rule: ty.induct)

apply(simp_all)

done

lemma s2:

  fixes T::"ty"

  shows "[]<T> = T"

apply(induct T rule: ty.induct)

apply(simp_all)

done

lemma perm_struct_induct_name[case_names pure zero swap]:

  assumes pure: "supp p \<subseteq> atom ` (UNIV::name set)"

  and     zero: "P 0"

  and     swap: "\<And>p a b::name. \<lbrakk>P p; a \<noteq> b\<rbrakk> \<Longrightarrow> P ((a \<leftrightarrow> b) + p)"

  shows "P p"

apply(rule_tac S="supp p \<inter> atom ` (UNIV::name set)" in perm_struct_induct)

using pure

apply(auto)[1]

apply(rule zero)

apply(auto)

apply(simp add: flip_def[symmetric])

apply(rule swap)

apply(auto)

done

lemma s3:

  fixes T::"ty"

  assumes "supp p \<subseteq> atom ` (UNIV::name set)"

  shows "\<exists>\<theta>. p \<bullet> T = \<theta><T>"

apply(induct p rule: perm_struct_induct_name)

apply(rule assms)

apply(simp)

apply(rule_tac x="[]" in exI)

apply(simp add: s2)

apply(clarify)

apply(simp) 

apply(rule_tac x="[(a, Var b),(b, Var a)] \<circ> \<theta>" in exI)

apply(simp add: compose_ty[symmetric])

apply(simp add: s1)

done

lemma s4:

  fixes x::"'a::fs"

  assumes "supp x \<subseteq> atom ` (UNIV::name set)"

  shows "\<exists>q. p \<bullet> x = q \<bullet> x \<and> supp q \<subseteq> atom ` (UNIV::name set)"

apply(induct p rule: perm_simple_struct_induct)

apply(rule_tac x="0" in exI)

apply(auto)[1]

apply(simp add: supp_zero_perm)

apply(auto)[1]

apply(case_tac "supp (a \<rightleftharpoons> b) \<subseteq> range atom")

apply(rule_tac x="(a \<rightleftharpoons> b) + q" in exI)

apply(simp)

apply(rule subset_trans)

apply(rule supp_plus_perm)

apply(simp)

apply(rule_tac x="q" in exI)

apply(simp)

apply(rule swap_fresh_fresh)

apply(simp add: fresh_permute_left)

apply(subst perm_supp_eq)

apply(simp add: supp_swap)

apply(simp add: supp_minus_perm)

apply(simp add: fresh_star_def fresh_def)

apply(simp add: supp_atom)

apply(auto)[1]

apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))

apply(simp add: supp_swap)

using assms

apply(simp add: fresh_def)

apply(auto)[1]

apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))

apply(simp add: fresh_permute_left)

apply(subst perm_supp_eq)

apply(simp add: supp_swap)

apply(simp add: supp_minus_perm)

apply(simp add: fresh_star_def fresh_def)

apply(simp add: supp_atom)

apply(auto)[1]

apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))

apply(simp add: supp_swap)

using assms

apply(simp add: fresh_def)

apply(auto)[1]

apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))

done

lemma s5:

  fixes T::"ty"

  shows "supp T \<subseteq> atom ` (UNIV::name set)"

apply(induct T rule: ty.induct)

apply(auto simp add: ty.supp supp_at_base)

done

function

  generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")

where

  "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. \<theta><T'> = T)"

  apply auto[1]

  apply (rule_tac y="b" in tys.exhaust)

  apply auto[1]

  apply(simp)

  apply(clarify)

  apply(rule iffI)

  apply(clarify)

  apply(drule sym)

  apply(simp add: Abs_eq_iff2)

  apply(simp add: alphas)

  apply(clarify)

  using s4[OF s5]

  apply -

  apply(drule_tac x="p" in meta_spec)

  apply(drule_tac x="T'a" in meta_spec)

  apply(clarify)

  apply(simp)

  using s3

  apply -

  apply(drule_tac x="q" in meta_spec)

  apply(drule_tac x="T'a" in meta_spec)

  apply(drule meta_mp)

  apply(simp)

  apply(clarify)

  apply(simp)

  apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI)

  apply(simp add: compose_ty)

  apply(auto)

  apply(simp add: Abs_eq_iff2)

  apply(simp add: alphas)

  apply(clarify)

  apply(drule_tac x="p" in meta_spec)

  apply(drule_tac x="T'" in meta_spec)

  apply(clarify)

  apply(simp)

  apply(drule_tac x="q" in meta_spec)

  apply(drule_tac x="T'" in meta_spec)

  apply(drule meta_mp)

  apply(simp)

  apply(clarify)

  apply(simp)

  apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI)

  apply(simp add: compose_ty)

  done