theory TypeSchemes
imports "../Nominal2"
begin

section {*** Type Schemes ***}


atom_decl name 

(* defined as a single nominal datatype *)

nominal_datatype ty =
  Var "name"
| Fun "ty" "ty"
and tys =
  All xs::"name fset" ty::"ty" bind (set+) xs in ty

thm ty_tys.distinct
thm ty_tys.induct
thm ty_tys.inducts
thm ty_tys.exhaust ty_tys.strong_exhaust
thm ty_tys.fv_defs
thm ty_tys.bn_defs
thm ty_tys.perm_simps
thm ty_tys.eq_iff
thm ty_tys.fv_bn_eqvt
thm ty_tys.size_eqvt
thm ty_tys.supports
thm ty_tys.supp
thm ty_tys.fresh

fun
  lookup :: "(name \<times> ty) list \<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

lemma test:
  assumes a: "f x = Inl y"
  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
using a 
apply(frule_tac p="p" in permute_boolI)
apply(simp (no_asm_use) only: eqvts)
apply(subst (asm) permute_fun_app_eq)
back
apply(simp)
done

lemma test2:
  assumes a: "f x = Inl y"
  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
using a 
apply(frule_tac p="p" in permute_boolI)
apply(simp (no_asm_use) only: eqvts)
apply(subst (asm) permute_fun_app_eq)
back
apply(simp)
done

lemma helper:
  assumes "A - C = A - D"
  and "B - C = B - D"
  and "E \<subseteq> A \<union> B"
  shows "E - C = E - D"
using assms
by blast

nominal_primrec
    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
where
  "subst \<theta> (Var X) = lookup \<theta> X"
| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
apply(simp add: eqvt_def)
apply(rule allI)
apply(simp add: permute_fun_def permute_bool_def)
apply(rule ext)
apply(rule ext)
apply(rule iffI)
apply(drule_tac x="p" in meta_spec)
apply(drule_tac x="- p \<bullet> x" in meta_spec)
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
apply(simp)
apply(drule_tac x="-p" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(simp)
--"Eqvt One way"
thm subst_substs_graph.induct
thm subst_substs_graph.intros
thm Projl.simps
apply(erule subst_substs_graph.induct)
apply(perm_simp)
apply(rule subst_substs_graph.intros)
thm subst_substs_graph.cases
apply(erule subst_substs_graph.cases)
apply(simp (no_asm_use) only: eqvts)
apply(subst test)
back
apply(assumption)
apply(rotate_tac 1)
apply(erule subst_substs_graph.cases)
apply(subst test)
back
apply(assumption)
apply(perm_simp)
apply(rule subst_substs_graph.intros)
apply(assumption)
apply(assumption)
apply(subst test)
back
apply(assumption)
apply(perm_simp)
apply(rule subst_substs_graph.intros)
apply(assumption)
apply(assumption)
apply(simp)
--"A"
apply(simp (no_asm_use) only: eqvts)
apply(subst test)
back
apply(assumption)
apply(rotate_tac 1)
apply(erule subst_substs_graph.cases)
apply(subst test)
back
apply(assumption)
apply(perm_simp)
apply(rule subst_substs_graph.intros)
apply(assumption)
apply(assumption)
apply(subst test)
back
apply(assumption)
apply(perm_simp)
apply(rule subst_substs_graph.intros)
apply(assumption)
apply(assumption)
apply(simp)
--"A"
apply(simp)
apply(erule subst_substs_graph.cases)
apply(simp (no_asm_use) only: eqvts)
apply(subst test)
back
back
apply(assumption)
apply(rule subst_substs_graph.intros)
apply (simp add: eqvts)
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
apply (simp add: image_eqvt eqvts_raw eqvts)
apply (simp add: fresh_star_permute_iff)
apply(perm_simp)
apply(assumption)
apply(simp (no_asm_use) only: eqvts)
apply(subst test)
back
back
apply(assumption)
apply(rule subst_substs_graph.intros)
apply (simp add: eqvts)
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
apply (simp add: image_eqvt eqvts_raw eqvts)
apply (simp add: fresh_star_permute_iff)
apply(perm_simp)
apply(assumption)
apply(simp)
--"Eqvt done"
apply (case_tac x)
apply simp apply clarify 
apply (rule_tac y="b" in ty_tys.exhaust(1))
apply (auto)[1]
apply (auto)[1]
apply simp apply clarify 
apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
apply (auto)[1]
apply (auto)[5]
--"LAST GOAL"
apply(simp del: ty_tys.eq_iff)
apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
defer
apply (simp add: eqvt_at_def subst_def)
apply rule
apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)")
apply (subst test2)
apply (drule_tac x="(\<theta>', T)" in meta_spec)
apply assumption
apply simp
--"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following"
 apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)")
prefer 2
apply (simp add: THE_default_def)
apply (case_tac "Ex1 (subst_substs_graph (Inl y))")
prefer 2
apply simp
apply (simp add: the1_equality)
apply auto[1]
apply (erule_tac x="x" in allE)
apply simp
apply(cases rule: subst_substs_graph.cases)
apply assumption
apply (rule_tac x="lookup \<theta> X" in exI)
apply clarify
apply (rule the1_equality)
apply metis apply assumption
apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
                  (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
apply clarify
apply (rule the1_equality)
apply metis apply assumption
apply clarify
--"This is exactly the assumption for the properly defined function"
defer
apply (simp only: Abs_eq_res_set)
apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
apply (subst (asm) Abs_eq_iff2)
apply (clarify)
apply (simp add: alphas)
apply (clarify)
apply (rule trans)
apply(rule_tac p="p" in supp_perm_eq[symmetric])
apply(rule fresh_star_supp_conv)
thm fresh_star_perm_set_conv
apply(drule fresh_star_perm_set_conv)
apply (rule finite_Diff)
apply (rule finite_supp)
apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. subst \<theta>' T)")
apply (metis Un_absorb2 fresh_star_Un)
apply (simp add: fresh_star_Un)
apply (rule conjI)
apply (simp (no_asm) add: fresh_star_def)

apply rule
apply(simp (no_asm) only: Abs_fresh_iff)
apply(clarify)
apply auto[1]
apply (simp add: fresh_star_def fresh_def)

apply (simp (no_asm) add: fresh_star_def)
apply rule
apply auto[1]
apply(simp (no_asm) only: Abs_fresh_iff)
apply(clarify)
apply auto[1]
apply(drule_tac a="atom x" in fresh_eqvt_at)
apply (simp add: supp_Pair finite_supp)
apply (simp add: fresh_Pair)
apply(auto simp add: Abs_fresh_iff fresh_star_def)[2]
apply (simp add: fresh_def)
apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
prefer 2
apply (rule perm_supp_eq)
apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'")
apply (auto simp add: fresh_star_def)[1]
apply (simp add: fresh_star_Un fresh_star_def)
apply blast
apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
apply (simp only: Abs_eq_res_set[symmetric])
apply (simp add: Abs_eq_iff alphas)
apply rule
prefer 2
apply (rule_tac x="0 :: perm" in exI)
apply (simp add: fresh_star_zero)
apply (rule helper)
prefer 3
apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)")
apply simp
apply (subst supp_Pair[symmetric])
apply (rule supp_eqvt_at)
apply (simp add: eqvt_at_def)
apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)")
apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)")
apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)")
apply (thin_tac "(atom ` fset xsa \<inter> supp (p \<bullet> T) - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'")
apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'")
apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p")
apply (rule)
apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)")
apply (erule_tac x="p" in allE)
apply (erule_tac x="pa + p" in allE)
apply (metis permute_plus)
apply assumption
apply (simp add: supp_Pair finite_supp)
prefer 2 apply blast
prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI)
apply (rule_tac s="supp \<theta>'" in trans)
apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'")
apply (auto simp add: fresh_star_def fresh_def)[1]
apply (subgoal_tac "supp p \<sharp>* \<theta>'")
apply (metis fresh_star_permute_iff)
apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'")
apply (auto simp add: fresh_star_def)[1]
apply (simp add: fresh_star_Un)
apply (auto simp add: fresh_star_def fresh_def)[1]
oops

section {* defined as two separate nominal datatypes *}

nominal_datatype ty2 =
  Var2 "name"
| Fun2 "ty2" "ty2"

nominal_datatype tys2 =
  All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty

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

fun
  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
where
  "lookup2 [] Y = Var2 Y"
| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"

lemma lookup2_eqvt[eqvt]:
  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
  by (induct Ts T rule: lookup2.induct) simp_all

nominal_primrec
  subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
where
  "subst \<theta> (Var2 X) = lookup2 \<theta> X"
| "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
  unfolding eqvt_def subst_graph_def
  apply (rule, perm_simp, rule)
  apply(case_tac x)
  apply(simp)
  apply(rule_tac y="b" in ty2.exhaust)
  apply(blast)
  apply(blast)
  apply(simp_all add: ty2.distinct)
  done

termination
  apply(relation "measure (size o snd)")
  apply(simp_all add: ty2.size)
  done

lemma subst_eqvt[eqvt]:
  shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
apply(induct \<theta> T rule: subst.induct)
apply(simp_all add: lookup2_eqvt)
done

lemma supp_fun_app2_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_app2_eqvt)
  unfolding eqvt_def by (simp add: eqvts_raw)
 
lemma fresh_star_inter1:
  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
  unfolding fresh_star_def by blast
 
nominal_primrec
  substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
where
  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
  unfolding eqvt_def substs_graph_def
  apply (rule, perm_simp, rule)
  apply auto[1]
  apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
  apply auto
  apply (subst (asm) Abs_eq_res_set)
  apply (subst (asm) Abs_eq_iff2)
  apply (clarify)
  apply (simp add: alphas)
  apply (clarify)
  apply (rule trans)
  apply(rule_tac p="p" in supp_perm_eq[symmetric])
  apply(rule fresh_star_supp_conv)
  apply(drule fresh_star_perm_set_conv)
  apply (rule finite_Diff)
  apply (rule finite_supp)
  apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* ([atom ` fset xs]res. subst \<theta>' t)")
  apply (metis Un_absorb2 fresh_star_Un)
  apply (subst fresh_star_Un)
  apply (rule conjI)
  apply (simp (no_asm) add: fresh_star_def)
  apply (rule)
  apply (simp add: Abs_fresh_iff)
  apply (simp add: fresh_star_def)
  apply (rule)
  apply (simp (no_asm) add: Abs_fresh_iff)
  apply auto[1]
  apply (simp add: fresh_def supp_Abs)
  apply (rule contra_subsetD)
  apply (rule supp_subst)
  apply auto[1]
  apply simp
  apply (subst Abs_eq_iff)
  apply (rule_tac x="0::perm" in exI)
  apply (subgoal_tac "p \<bullet> subst \<theta>' t = subst \<theta>' (p \<bullet> t)")
  prefer 2
  apply (subgoal_tac "\<theta>' = p \<bullet> \<theta>'")
  apply (simp add: subst_eqvt)
  apply (rule sym)
  apply (rule perm_supp_eq)
  apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'")
  apply (metis Diff_partition fresh_star_Un)
  apply (simp add: fresh_star_Un fresh_star_inter1)
  apply (simp add: alphas fresh_star_zero)
  apply auto[1]
  apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
  apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
  apply (drule subsetD[OF supp_subst])
  apply auto[1]
  apply (simp add: fresh_star_def fresh_def)
  apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
  apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt)
  apply (rotate_tac 6)
  apply (drule sym)
  apply (simp add: subst_eqvt)
  apply (drule subsetD[OF supp_subst])
  apply auto[1]
  apply (rotate_tac 2)
  apply (subst (asm) fresh_star_permute_iff[symmetric])
  apply (simp add: fresh_star_def fresh_def)
  apply blast
  done


text {* Some Tests about Alpha-Equality *}

lemma
  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
  done

lemma
  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
  apply(simp add: ty_tys.eq_iff 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_tys.supp)
  done

lemma
  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
done

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: ty_tys.eq_iff Abs_eq_iff)
  apply(clarify)
  apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
  apply auto
  done




end