theory TypeSchemes

imports "../Parser"

begin

section {*** Type Schemes ***}

atom_decl name

ML {* val _ = alpha_type := AlphaRes *}

nominal_datatype ty =

  Var "name"

| Fun "ty" "ty"

and tys =

  All xs::"name fset" ty::"ty" bind 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 (subst atom_eqvt_raw[symmetric])

    apply (subst fmap_eqvt[symmetric])

    apply (subst fset_to_set_eqvt[symmetric])

    apply (simp only: fresh_star_permute_iff)

    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)

  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)

  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)

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)

  apply auto

  done

(* 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