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"

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

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


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


nominal_primrec
  subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
where
  "subst \<theta> (Var X) = lookup \<theta> X"
| "subst \<theta> (Fun T1 T) = Fun (subst \<theta> T1) (subst \<theta> T)"
  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)
 
lemma fresh_star_inter1:
  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
  unfolding fresh_star_def by blast

nominal_primrec
  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
where
  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<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|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (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|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (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|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (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|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (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




end