theory TypeSchemes1
imports "../Nominal2"
begin

section {*** Type Schemes defined as two separate nominal datatypes ***}

atom_decl name 

nominal_datatype ty =
  Var "name"
| Fun "ty" "ty" ("_ \<rightarrow> _")

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

thm tys.distinct
thm tys.induct tys.strong_induct
thm tys.exhaust tys.strong_exhaust
thm tys.fv_defs
thm tys.bn_defs
thm tys.perm_simps
thm tys.eq_iff
thm tys.fv_bn_eqvt
thm tys.size_eqvt
thm tys.supports
thm tys.supp
thm tys.fresh

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

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

fun
  lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"
where
  "lookup [] Y = Var Y"
| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"

lemma lookup_eqvt[eqvt]:
  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
apply(induct Ts T rule: lookup.induct)
apply(simp_all)
done


nominal_primrec
  subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
where
  "\<theta><Var X> = lookup \<theta> X"
| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
  unfolding eqvt_def subst_graph_def
  apply (rule, perm_simp, rule)
  apply(rule TrueI)
  apply(case_tac x)
  apply(rule_tac y="b" in ty.exhaust)
  apply(blast)
  apply(blast)
  apply(simp_all)
  done

termination (eqvt)
  by lexicographic_order

lemma supp_fun_app_eqvt:
  assumes e: "eqvt f"
  shows "supp (f a b) \<subseteq> supp a \<union> supp b"
  using supp_fun_app_eqvt[OF e] supp_fun_app
  by blast
 
lemma supp_subst:
  "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
  apply (rule supp_fun_app_eqvt)
  unfolding eqvt_def 
  by (simp add: permute_fun_def subst.eqvt)
 
nominal_primrec
  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
where
  "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
  unfolding eqvt_def substs_graph_def
  apply (rule, perm_simp, rule)
  apply auto[2]
  apply (rule_tac y="b" and c="a" in tys.strong_exhaust)
  apply auto[1]
  apply(simp)
  apply(erule conjE)
  apply (erule Abs_res_fcb)
  apply (simp add: Abs_fresh_iff)
  apply(simp add: fresh_def)
  apply(simp add: supp_Abs)
  apply(rule impI)
  apply(subgoal_tac "x \<notin> supp \<theta>")
  prefer 2
  apply(auto simp add: fresh_star_def fresh_def)[1]
  apply(subgoal_tac "x \<in> supp T")
  using supp_subst
  apply(blast)
  using supp_subst
  apply(blast)
  apply clarify
  apply (simp add: subst.eqvt)
  apply (subst Abs_eq_iff)
  apply (rule_tac x="0::perm" in exI)
  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
  apply (simp add: alphas fresh_star_zero)
  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 blast
  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
  apply (simp add: supp_Pair eqvts eqvts_raw)
  apply auto[1]
  apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'")
  apply (simp add: fresh_star_def fresh_def)
  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
  apply (simp add: eqvts eqvts_raw)
  apply (simp add: fresh_star_def fresh_def)
  apply (drule subsetD[OF supp_subst])
  apply (simp add: supp_Pair)
  apply (rule perm_supp_eq)
  apply (simp add: fresh_def fresh_star_def)
  apply blast
  done

text {* Some Tests about Alpha-Equality *}

lemma
  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
  apply(simp add: Abs_eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
  done

lemma
  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
  apply(simp add: Abs_eq_iff)
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
  apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
  done

lemma
  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
  apply(simp add: Abs_eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
done

lemma
  assumes a: "a \<noteq> b"
  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
  using a
  apply(simp add: Abs_eq_iff)
  apply(clarify)
  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
  apply auto
  done


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






end