1 theory ExTySch

     2 imports "Parser"

     3 begin

     4 

     5 (* Type Schemes *)

     6 atom_decl name

     7 

     8 nominal_datatype t =

     9   Var "name"

    10 | Fun "t" "t"

    11 and tyS =

    12   All xs::"name fset" ty::"t" bind xs in ty

    13 

    14 lemma size_eqvt_raw:

    15   "size (pi \<bullet> t :: t_raw) = size t"

    16   "size (pi \<bullet> ts :: tyS_raw) = size ts"

    17   apply (induct rule: t_raw_tyS_raw.inducts)

    18   apply simp_all

    19   done

    20 

    21 instantiation t and tyS :: size begin

    22 

    23 quotient_definition

    24   "size_t :: t \<Rightarrow> nat"

    25 is

    26   "size :: t_raw \<Rightarrow> nat"

    27 

    28 quotient_definition

    29   "size_tyS :: tyS \<Rightarrow> nat"

    30 is

    31   "size :: tyS_raw \<Rightarrow> nat"

    32 

    33 lemma size_rsp:

    34   "alpha_t_raw x y \<Longrightarrow> size x = size y"

    35   "alpha_tyS_raw a b \<Longrightarrow> size a = size b"

    36   apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)

    37   apply (simp_all only: t_raw_tyS_raw.size)

    38   apply (simp_all only: alpha_gen)

    39   apply clarify

    40   apply (simp_all only: size_eqvt_raw)

    41   done

    42 

    43 lemma [quot_respect]:

    44   "(alpha_t_raw ===> op =) size size"

    45   "(alpha_tyS_raw ===> op =) size size"

    46   by (simp_all add: size_rsp)

    47 

    48 lemma [quot_preserve]:

    49   "(rep_t ---> id) size = size"

    50   "(rep_tyS ---> id) size = size"

    51   by (simp_all add: size_t_def size_tyS_def)

    52 

    53 instance

    54   by default

    55 

    56 end

    57 

    58 thm t_raw_tyS_raw.size(4)[quot_lifted]

    59 thm t_raw_tyS_raw.size(5)[quot_lifted]

    60 thm t_raw_tyS_raw.size(6)[quot_lifted]

    61 

    62 

    63 thm t_tyS.fv

    64 thm t_tyS.eq_iff

    65 thm t_tyS.bn

    66 thm t_tyS.perm

    67 thm t_tyS.inducts

    68 thm t_tyS.distinct

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

    70 

    71 lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]

    72 

    73 lemma induct:

    74   assumes a1: "\<And>name b. P b (Var name)"

    75   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"

    76   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)"

    77   shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "

    78 proof -

    79   have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"

    80     apply (rule t_tyS.induct)

    81     apply (simp add: a1)

    82     apply (simp)

    83     apply (rule allI)+

    84     apply (rule a2)

    85     apply simp

    86     apply simp

    87     apply (rule allI)

    88     apply (rule allI)

    89     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")

    90     apply clarify

    91     apply(rule_tac t="p \<bullet> TySch.All fset t" and 

    92                    s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)

    93     apply (rule supp_perm_eq)

    94     apply assumption

    95     apply (simp only: t_tyS.perm)

    96     apply (rule a3)

    97     apply(erule_tac x="(pa + p)" in allE)

    98     apply simp

    99     apply (simp add: eqvts eqvts_raw)

   100     apply (rule at_set_avoiding2)

   101     apply (simp add: fin_fset_to_set)

   102     apply (simp add: finite_supp)

   103     apply (simp add: eqvts finite_supp)

   104     apply (subst atom_eqvt_raw[symmetric])

   105     apply (subst fmap_eqvt[symmetric])

   106     apply (subst fset_to_set_eqvt[symmetric])

   107     apply (simp only: fresh_star_permute_iff)

   108     apply (simp add: fresh_star_def)

   109     apply clarify

   110     apply (simp add: fresh_def)

   111     apply (simp add: t_tyS_supp)

   112     done

   113   then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast

   114   then show ?thesis by simp

   115 qed

   116 

   117 lemma

   118   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"

   119   apply(simp add: t_tyS.eq_iff)

   120   apply(rule_tac x="0::perm" in exI)

   121   apply(simp add: alpha_gen)

   122   apply(auto)

   123   apply(simp add: fresh_star_def fresh_zero_perm)

   124   done

   125 

   126 lemma

   127   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"

   128   apply(simp add: t_tyS.eq_iff)

   129   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)

   130   apply(simp add: alpha_gen fresh_star_def eqvts)

   131   apply auto

   132   done

   133 

   134 lemma

   135   shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"

   136   apply(simp add: t_tyS.eq_iff)

   137   apply(rule_tac x="0::perm" in exI)

   138   apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)

   139 oops

   140 

   141 lemma

   142   assumes a: "a \<noteq> b"

   143   shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"

   144   using a

   145   apply(simp add: t_tyS.eq_iff)

   146   apply(clarify)

   147   apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)

   148   apply auto

   149   done

   150 

   151 (* PROBLEM:

   152 Type schemes with separate datatypes

   153 

   154 nominal_datatype T =

   155   TVar "name"

   156 | TFun "T" "T"

   157 nominal_datatype TyS =

   158   TAll xs::"name list" ty::"T" bind xs in ty

   159 

   160 *** exception Datatype raised

   161 *** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")

   162 *** At command "nominal_datatype".

   163 *)

   164 

   165 

   166 end