1 theory TySch

     2 imports "Parser" "../Attic/Prove" "FSet"

     3 begin

     4 

     5 atom_decl name

     6 

     7 nominal_datatype t =

     8   Var "name"

     9 | Fun "t" "t"

    10 and tyS =

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

    12 

    13 lemma size_eqvt_raw:

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

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

    16   apply (induct rule: t_raw_tyS_raw.inducts)

    17   apply simp_all

    18   done

    19 

    20 instantiation t and tyS :: size begin

    21 

    22 quotient_definition

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

    24 is

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

    26 

    27 quotient_definition

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

    29 is

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

    31 

    32 lemma size_rsp:

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

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

    35   apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)

    36   apply (simp_all only: t_raw_tyS_raw.size)

    37   apply (simp_all only: alpha_gen)

    38   apply clarify

    39   apply (simp_all only: size_eqvt_raw)

    40   done

    41 

    42 lemma [quot_respect]:

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

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

    45   by (simp_all add: size_rsp)

    46 

    47 lemma [quot_preserve]:

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

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

    50   by (simp_all add: size_t_def size_tyS_def)

    51 

    52 instance

    53   by default

    54 

    55 end

    56 

    57 thm t_raw_tyS_raw.size(4)[quot_lifted]

    58 thm t_raw_tyS_raw.size(5)[quot_lifted]

    59 thm t_raw_tyS_raw.size(6)[quot_lifted]

    60 

    61 

    62 thm t_tyS.fv

    63 thm t_tyS.eq_iff

    64 thm t_tyS.bn

    65 thm t_tyS.perm

    66 thm t_tyS.inducts

    67 thm t_tyS.distinct

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

    69 

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

    71 

    72 lemma induct:

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

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

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

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

    77 proof -

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

    79     apply (rule t_tyS.induct)

    80     apply (simp add: a1)

    81     apply (simp)

    82     apply (rule allI)+

    83     apply (rule a2)

    84     apply simp

    85     apply simp

    86     apply (rule allI)

    87     apply (rule allI)

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

    89     apply clarify

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

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

    92     apply (rule supp_perm_eq)

    93     apply assumption

    94     apply (simp only: t_tyS.perm)

    95     apply (rule a3)

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

    97     apply simp

    98     apply (simp add: eqvts eqvts_raw)

    99     apply (rule at_set_avoiding2)

   100     apply (simp add: fin_fset_to_set)

   101     apply (simp add: finite_supp)

   102     apply (simp add: eqvts finite_supp)

   103     apply (subst atom_eqvt_raw[symmetric])

   104     apply (subst fmap_eqvt[symmetric])

   105     apply (subst fset_to_set_eqvt[symmetric])

   106     apply (simp only: fresh_star_permute_iff)

   107     apply (simp add: fresh_star_def)

   108     apply clarify

   109     apply (simp add: fresh_def)

   110     apply (simp add: t_tyS_supp)

   111     done

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

   113   then show ?thesis by simp

   114 qed

   115 

   116 lemma

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

   118   apply(simp add: t_tyS.eq_iff)

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

   120   apply(simp add: alpha_gen)

   121   apply(auto)

   122   apply(simp add: fresh_star_def fresh_zero_perm)

   123   done

   124 

   125 lemma

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

   127   apply(simp add: t_tyS.eq_iff)

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

   129   apply(simp add: alpha_gen fresh_star_def eqvts)

   130   apply auto

   131   done

   132 

   133 lemma

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

   135   apply(simp add: t_tyS.eq_iff)

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

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

   138 oops

   139 

   140 lemma

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

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

   143   using a

   144   apply(simp add: t_tyS.eq_iff)

   145   apply(clarify)

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

   147   apply auto

   148   done

   149 

   150 (* PROBLEM:

   151 Type schemes with separate datatypes

   152 

   153 nominal_datatype T =

   154   TVar "name"

   155 | TFun "T" "T"

   156 nominal_datatype TyS =

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

   158 

   159 *** exception Datatype raised

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

   161 *** At command "nominal_datatype".

   162 *)

   163 

   164 

   165 end