theory TypeSchemes
imports "../NewParser"
begin

section {*** Type Schemes ***}

atom_decl name

declare [[STEPS = 15]]

nominal_datatype ty =
  Var "name"
| Fun "ty" "ty"
and tys =
  All xs::"name fset" ty::"ty" bind_res xs in ty

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

instance ty2 :: pt sorry

nominal_datatype tys2 =
  All2 xs::"name fset" ty::"ty2" bind_res xs in ty


lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]



(* below we define manually the function for size *)

lemma size_eqvt_raw:
  "size (pi \<bullet> t  :: ty_raw)  = size t"
  "size (pi \<bullet> ts :: tys_raw) = size ts"
  apply (induct rule: ty_raw_tys_raw.inducts)
  apply simp_all
  done

instantiation ty and tys :: size 
begin

quotient_definition
  "size_ty :: ty \<Rightarrow> nat"
is
  "size :: ty_raw \<Rightarrow> nat"

quotient_definition
  "size_tys :: tys \<Rightarrow> nat"
is
  "size :: tys_raw \<Rightarrow> nat"

lemma size_rsp:
  "alpha_ty_raw x y \<Longrightarrow> size x = size y"
  "alpha_tys_raw a b \<Longrightarrow> size a = size b"
  apply (induct rule: alpha_ty_raw_alpha_tys_raw.inducts)
  apply (simp_all only: ty_raw_tys_raw.size)
  apply (simp_all only: alphas)
  apply clarify
  apply (simp_all only: size_eqvt_raw)
  done

lemma [quot_respect]:
  "(alpha_ty_raw ===> op =) size size"
  "(alpha_tys_raw ===> op =) size size"
  by (simp_all add: size_rsp)

lemma [quot_preserve]:
  "(rep_ty ---> id) size = size"
  "(rep_tys ---> id) size = size"
  by (simp_all add: size_ty_def size_tys_def)

instance
  by default

end

thm ty_raw_tys_raw.size(4)[quot_lifted]
thm ty_raw_tys_raw.size(5)[quot_lifted]
thm ty_raw_tys_raw.size(6)[quot_lifted]


thm ty_tys.fv
thm ty_tys.eq_iff
thm ty_tys.bn
thm ty_tys.perm
thm ty_tys.inducts
thm ty_tys.distinct

ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}

lemma strong_induct:
  assumes a1: "\<And>name b. P b (Var name)"
  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
proof -
  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
    apply (rule ty_tys.induct)
    apply (simp add: a1)
    apply (simp)
    apply (rule allI)+
    apply (rule a2)
    apply simp
    apply simp
    apply (rule allI)
    apply (rule allI)
    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)")
    apply clarify
    apply(rule_tac t="p \<bullet> All fset ty" and 
                   s="pa \<bullet> (p \<bullet> All fset ty)" in subst)
    apply (rule supp_perm_eq)
    apply assumption
    apply (simp only: ty_tys.perm)
    apply (rule a3)
    apply(erule_tac x="(pa + p)" in allE)
    apply simp
    apply (simp add: eqvts eqvts_raw)
    apply (rule at_set_avoiding2)
    apply (simp add: fin_fset_to_set)
    apply (simp add: finite_supp)
    apply (simp add: eqvts finite_supp)
    apply (rule_tac p=" -p" in permute_boolE)
    apply(simp add: eqvts)
    apply(simp add: permute_fun_def atom_eqvt)
    apply (simp add: fresh_star_def)
    apply clarify
    apply (simp add: fresh_def)
    apply (simp add: ty_tys_supp)
    done
  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
  then show ?thesis by simp
qed

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)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alphas)
  apply(simp add: fresh_star_def fresh_zero_perm 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)
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
  apply(simp add: alphas fresh_star_def eqvts supp_at_base)
  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)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff 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)
  apply(clarify)
  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
  apply auto
  done

fun
  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
where
  "lookup [] n = Var n"
| "lookup ((p, s) # t) n = (if p = n then s else lookup t n)"

locale subst_loc =
fixes
    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
assumes
    s1: "subst \<theta> (Var n) = lookup \<theta> n"
and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"
and s3: "fset_to_set (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
begin

lemma subst_ty:
  assumes x: "atom x \<sharp> t"
  shows "subst [(x, S)] t = t"
  using x
  apply (induct t rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
  by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base)

lemma subst_tyS:
  shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"
  apply (rule strong_induct[of
    "\<lambda>a t. True" "\<lambda>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified])
  apply clarify
  apply (subst s3)
  apply (simp add: fresh_star_def fresh_Cons fresh_Nil)
  apply (subst subst_ty)
  apply (simp_all add: fresh_star_prod_elim)
  apply (drule fresh_star_atom)
  apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
  apply (subgoal_tac "atom a \<notin> fset_to_set (fmap atom fset)")
  apply blast
  apply (metis supp_finite_atom_set finite_fset)
  done

lemma subst_lemma_pre:
  "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)"
  apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
  apply (simp add: s1)
  apply (auto simp add: fresh_Pair)
  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3]
  apply (simp add: s2)
  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
  done

lemma substs_lemma_pre:
  "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)"
  apply (rule strong_induct[of
    "\<lambda>a t. True" "\<lambda>(z, y, L) N. (atom z \<sharp> (N, L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N))" _ _ "(z, y, L)", simplified])
  apply clarify
  apply (subst s3)
  apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair)
  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
  apply clarify
  apply (drule fresh_star_atom)
  apply (drule fresh_star_atom)
  apply (simp add: fresh_def)
  apply (simp only: ty_tys.fv[simplified ty_tys.supp])
  apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)")
  apply blast
  apply (subgoal_tac "atom a \<notin> supp t")
  apply (fold fresh_def)[1]
  apply (rule mp[OF subst_lemma_pre])
  apply (simp add: fresh_Pair)
  apply (subgoal_tac "atom a \<notin> (fset_to_set (fmap atom fset))")
  apply blast
  apply (metis supp_finite_atom_set finite_fset)
  done

lemma subst_lemma:
  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
    subst [(y, L)] (subst [(x, N)] M) =
    subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)"
  apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
  apply (simp_all add: s1 s2)
  apply clarify
  apply (subst (2) subst_ty)
  apply simp_all
  done

lemma substs_lemma:
  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
    substs [(y, L)] (substs [(x, N)] M) =
    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)"
  apply (rule strong_induct[of
    "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
    substs [(y, L)] (substs [(x, N)] M) =
    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified])
  apply clarify
  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
  apply (subst s3)
  apply (unfold fresh_star_def)[1]
  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
  apply (subst s3)
  apply (unfold fresh_star_def)[1]
  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
  apply (subst s3)
  apply (unfold fresh_star_def)[1]
  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
  apply (subst s3)
  apply (unfold fresh_star_def)[1]
  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
  apply (rule ballI)
  apply (rule mp[OF subst_lemma_pre])
  apply (simp add: fresh_Pair)
  apply (subst subst_lemma)
  apply simp_all
  done

end

(* PROBLEM:
Type schemes with separate datatypes

nominal_datatype T =
  TVar "name"
| TFun "T" "T"
nominal_datatype TyS =
  TAll xs::"name list" ty::"T" bind xs in ty

*** exception Datatype raised
*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
*** At command "nominal_datatype".
*)


end