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

termination (eqvt)
  by (lexicographic_order)

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
  subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>"  [100,60] 120)
where
  "\<theta><[]> = []"
| "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"

lemma redundant1:
  fixes \<theta>1::"Subst"
  and   \<theta>2::"Subst"
  shows "\<theta>1 \<circ> \<theta>2 = (\<theta>1<\<theta>2>)@\<theta>1"
by (induct \<theta>2) (auto)

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

lemma dom_compose:
  shows "dom (\<theta>1 \<circ> \<theta>2) = dom \<theta>1 |\<union>| dom \<theta>2"
apply(induct rule: dom.induct)
apply(simp)
apply(simp)
by (metis sup_commute union_insert_fset)

lemma redundant3:
  fixes \<theta>1::"Subst"
  and   \<theta>2::"Subst"
  shows "dom (\<theta>2<\<theta>1>) = (dom \<theta>1)"
by (induct \<theta>1) (auto)

lemma dom_pi:
  shows "(p \<bullet> (dom \<theta>)) = dom (map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>)"
apply(induct \<theta>)
apply(auto)
done

lemma dom_fresh_lookup:
  fixes \<theta>::"Subst"
  assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
  shows "lookup \<theta> name = Var name"
using assms
apply(induct \<theta>)
apply(auto simp add: fresh_at_base)
done 

lemma dom_fresh_ty:
  fixes \<theta>::"Subst"
  and   T::"ty"
  assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> T"
  shows "\<theta><T> = T"
using assms
apply(induct T rule: ty.induct)
apply(auto simp add: ty.fresh dom_fresh_lookup)
done 

lemma dom_fresh_subst:
  fixes \<theta> \<theta>'::"Subst"
  assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> \<theta>'"
  shows "\<theta><\<theta>'> = \<theta>'"
using assms
apply(induct \<theta>')
apply(auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
done 


abbreviation
  "sub_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
where
  "xs\<^isub>1 \<subseteq> xs\<^isub>2 \<equiv> \<forall>x. x \<in> set xs\<^isub>1 \<longrightarrow> x \<in> set xs\<^isub>2"


definition
  generalises3 :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec>\<prec>\<prec> _")
where
  " T \<prec>\<prec>\<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"


lemma lookup_fresh:
  fixes X::"name"
  assumes a: "atom X \<sharp> \<theta>"
  shows "lookup \<theta> X = Var X"
  using a
  apply (induct \<theta>)
  apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
  done

lemma lookup_dom:
  fixes X::"name"
  assumes a: "X |\<notin>| dom \<theta>"
  shows "lookup \<theta> X = Var X"
  using a
  apply (induct \<theta>)
  apply(auto)
  done

lemma w1: 
  "\<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'> = map (\<lambda>(X, y). (p \<bullet> X, y)) (\<theta><\<theta>'>)"
apply(induct \<theta>')
apply(auto)
done

lemma w2:
  assumes "name |\<in>| dom \<theta>'" 
  shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
using assms
apply(induct \<theta>')
apply(auto)
by (metis notin_empty_fset)

lemma w3:
  assumes "name |\<in>| dom \<theta>" 
  shows "lookup \<theta> name = lookup (map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>) (p \<bullet> name)"
using assms
apply(induct \<theta>)
apply(auto)
by (metis notin_empty_fset)

lemma fresh_lookup:
  fixes X Y::"name"
  and   \<theta>::"Subst"
  assumes asms: "atom X \<sharp> Y" "atom X \<sharp> \<theta>"
  shows "atom X \<sharp> (lookup \<theta> Y)"
  using assms
  apply (induct \<theta>)
  apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
done

lemma test:
  fixes \<theta> \<theta>'::"Subst"
  and T::"ty"
  assumes "(p \<bullet> atom ` fset (dom \<theta>')) \<sharp>* \<theta>" "supp All [dom \<theta>'].T \<sharp>* p"
  shows "\<theta><\<theta>'<T>> = \<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'><\<theta><p \<bullet> T>>"
using assms
apply(induct T rule: ty.induct)
defer
apply(auto simp add: tys.supp ty.supp fresh_star_def)[1]
apply(auto simp add: tys.supp ty.supp fresh_star_def supp_at_base)[1]
apply(case_tac "name |\<in>| dom \<theta>'")
apply(subgoal_tac "atom (p \<bullet> name) \<sharp> \<theta>")
apply(subst (2) lookup_fresh)
apply(perm_simp)
apply(auto simp add: fresh_star_def)[1]
apply(simp)
apply(simp add: w1)
apply(simp add: w2)
apply(subst w3[symmetric])
apply(simp add:redundant3)
apply(simp)
apply(perm_simp)
apply(rotate_tac 2)
apply(drule_tac p="p" in permute_boolI)
apply(perm_simp)
apply(auto simp add: fresh_star_def)[1]
apply(metis notin_fset)
apply(simp add: lookup_dom)
apply(perm_simp)
apply(subst dom_fresh_ty)
apply(auto)[1]
apply(rule fresh_lookup)
apply(simp add: redundant3)
apply(simp add: dom_pi[symmetric])
apply(perm_simp)
apply(rotate_tac 2)
apply(drule_tac p="p" in permute_boolI)
apply(perm_simp)
apply(simp add: fresh_at_base)
apply (metis in_fset)
apply(simp add: redundant3)
apply(simp add: dom_pi[symmetric])
apply(perm_simp)
apply metis
apply(subst supp_perm_eq)
apply(simp add: supp_at_base fresh_star_def)
apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)
apply(simp)
done

lemma
  shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
unfolding generalises3_def
apply(erule exE)+
apply(erule conjE)+
apply(rule_tac t="S" and s="All [Xs].T'" in subst)
apply(simp)
using at_set_avoiding3
apply -
apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)
apply(drule_tac x="\<theta>" in meta_spec)
apply(drule_tac x="All [Xs].T'" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(drule meta_mp)
apply(simp add: finite_supp)
apply(drule meta_mp)
apply(simp add: finite_supp)
apply(drule meta_mp)
apply(simp add: tys.fresh fresh_star_def)
apply(erule exE)
apply(erule conjE)+
apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)
apply(rule supp_perm_eq)
apply(assumption)
apply(perm_simp)
apply(subst substs.simps)
apply(perm_simp)
apply(simp)
apply(rule_tac x="\<theta><map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>'>" in exI)
apply(rule_tac x="p \<bullet> Xs" in exI)
apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)
apply(rule conjI)
apply(simp)
apply(rule conjI)
defer
apply(simp add: redundant3)
apply(simp add: dom_pi[symmetric])
apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)
apply(simp)
apply(rule test)
apply(perm_simp)
apply(rotate_tac 2)
apply(drule_tac p="p" in permute_boolI)
apply(perm_simp)
apply(auto simp add: fresh_star_def)
done


end