1 theory TypeSchemes

     2 imports "../Nominal2"

     3 begin

     4 

     5 section {*** Type Schemes ***}

     6 

     7 atom_decl name 

     8 

     9 (* defined as a single nominal datatype *)

    10 

    11 nominal_datatype ty =

    12   Var "name"

    13 | Fun "ty" "ty"

    14 and tys =

    15   All xs::"name fset" ty::"ty" binds (set+) xs in ty

    16 

    17 ML {*

    18 get_all_info @{context}

    19 *}

    20 

    21 ML {*

    22 get_info @{context} "TypeSchemes.ty"

    23 *}

    24 

    25 ML {*

    26 #strong_exhaust (the_info @{context} "TypeSchemes.tys")

    27 *}

    28 

    29 thm ty_tys.distinct

    30 thm ty_tys.induct

    31 thm ty_tys.inducts

    32 thm ty_tys.exhaust 

    33 thm ty_tys.strong_exhaust

    34 thm ty_tys.fv_defs

    35 thm ty_tys.bn_defs

    36 thm ty_tys.perm_simps

    37 thm ty_tys.eq_iff

    38 thm ty_tys.fv_bn_eqvt

    39 thm ty_tys.size_eqvt

    40 thm ty_tys.supports

    41 thm ty_tys.supp

    42 thm ty_tys.fresh

    43 

    44 fun

    45   lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"

    46 where

    47   "lookup [] Y = Var Y"

    48 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"

    49 

    50 lemma lookup_eqvt[eqvt]:

    51   shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"

    52 apply(induct Ts T rule: lookup.induct)

    53 apply(simp_all)

    54 done

    55 

    56 lemma TEST1:

    57   assumes "x = Inl y"

    58   shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"

    59 using assms by simp

    60 

    61 lemma TEST2:

    62   assumes "x = Inr y"

    63   shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"

    64 using assms by simp

    65 

    66 lemma test:

    67   assumes a: "\<exists>y. f x = Inl y"

    68   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"

    69 using a

    70 apply clarify

    71 apply(frule_tac p="p" in permute_boolI)

    72 apply(simp (no_asm_use) only: eqvts)

    73 apply(subst (asm) permute_fun_app_eq)

    74 back

    75 apply(simp)

    76 done

    77 

    78 lemma test2:

    79   assumes a: "\<exists>y. f x = Inl y"

    80   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"

    81 using a

    82 apply clarify

    83 apply(frule_tac p="p" in permute_boolI)

    84 apply(simp (no_asm_use) only: eqvts)

    85 apply(subst (asm) permute_fun_app_eq)

    86 back

    87 apply(simp)

    88 done

    89 

    90 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")

    91     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"

    92 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"

    93 where

    94   "subst \<theta> (Var X) = lookup \<theta> X"

    95 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"

    96 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"

    97 (*unfolding subst_substs_graph_def eqvt_def

    98 apply rule

    99 apply perm_simp

   100 apply (subst test3)

   101 defer

   102 apply (subst test3)

   103 defer

   104 apply (subst test3)

   105 defer

   106 apply rule*)

   107 thm subst_substs_graph.intros

   108 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")

   109 apply(simp add: eqvt_def)

   110 apply(rule allI)

   111 apply(simp add: permute_fun_def permute_bool_def)

   112 apply(rule ext)

   113 apply(rule ext)

   114 apply(rule iffI)

   115 apply(drule_tac x="p" in meta_spec)

   116 apply(drule_tac x="- p \<bullet> x" in meta_spec)

   117 apply(drule_tac x="- p \<bullet> xa" in meta_spec)

   118 apply(simp)

   119 apply(drule_tac x="-p" in meta_spec)

   120 apply(drule_tac x="x" in meta_spec)

   121 apply(drule_tac x="xa" in meta_spec)

   122 apply(simp)

   123 --"Eqvt One way"

   124 apply(erule subst_substs_graph.induct)

   125 apply(perm_simp)

   126 apply(rule subst_substs_graph.intros)

   127 apply(erule subst_substs_graph.cases)

   128 apply(simp (no_asm_use) only: eqvts)

   129 apply(subst test)

   130 back

   131 apply (rule exI)

   132 apply(assumption)

   133 apply(rotate_tac 1)

   134 apply(erule subst_substs_graph.cases)

   135 apply(subst test)

   136 back

   137 apply (rule exI)

   138 apply(assumption)

   139 apply(perm_simp)

   140 apply(rule subst_substs_graph.intros)

   141 apply(assumption)

   142 apply(assumption)

   143 apply(subst test)

   144 back

   145 apply (rule exI)

   146 apply(assumption)

   147 apply(perm_simp)

   148 apply(rule subst_substs_graph.intros)

   149 apply(assumption)

   150 apply(assumption)

   151 apply(simp)

   152 --"A"

   153 apply(simp (no_asm_use) only: eqvts)

   154 apply(subst test)

   155 back

   156 apply (rule exI)

   157 apply(assumption)

   158 apply(rotate_tac 1)

   159 apply(erule subst_substs_graph.cases)

   160 apply(subst test)

   161 back

   162 apply (rule exI)

   163 apply(assumption)

   164 apply(perm_simp)

   165 apply(rule subst_substs_graph.intros)

   166 apply(assumption)

   167 apply(assumption)

   168 apply(subst test)

   169 back

   170 apply (rule exI)

   171 apply(assumption)

   172 apply(perm_simp)

   173 apply(rule subst_substs_graph.intros)

   174 apply(assumption)

   175 apply(assumption)

   176 apply(simp)

   177 --"A"

   178 apply(simp)

   179 apply(erule subst_substs_graph.cases)

   180 apply(simp (no_asm_use) only: eqvts)

   181 apply(subst test)

   182 back

   183 back

   184 apply (rule exI)

   185 apply(assumption)

   186 apply(rule subst_substs_graph.intros)

   187 apply (simp add: eqvts)

   188 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")

   189 apply (simp add: image_eqvt eqvts_raw eqvts)

   190 apply (simp add: fresh_star_permute_iff)

   191 apply(perm_simp)

   192 apply(assumption)

   193 apply(simp (no_asm_use) only: eqvts)

   194 apply(subst test)

   195 back

   196 back

   197 apply (rule exI)

   198 apply(assumption)

   199 apply(rule subst_substs_graph.intros)

   200 apply (simp add: eqvts)

   201 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")

   202 apply (simp add: image_eqvt eqvts_raw eqvts)

   203 apply (simp add: fresh_star_permute_iff)

   204 apply(perm_simp)

   205 apply(assumption)

   206 apply(simp)

   207 --"Eqvt done"

   208 apply(rule TrueI)

   209 apply (case_tac x)

   210 apply simp apply clarify 

   211 apply (rule_tac y="b" in ty_tys.exhaust(1))

   212 apply (auto)[1]

   213 apply (auto)[1]

   214 apply simp apply clarify 

   215 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))

   216 apply (auto)[1]

   217 apply (auto)[5]

   218 --"LAST GOAL"

   219 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])

   220 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")

   221 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")

   222 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))")

   223 prefer 2

   224 apply (simp add: eqvt_at_def subst_def)

   225 apply rule

   226 apply (subst test2)

   227 apply (simp add: subst_substs_sumC_def)

   228 apply (simp add: THE_default_def)

   229 apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))")

   230 prefer 2

   231 apply simp

   232 apply (simp add: the1_equality)

   233 apply auto[1]

   234 apply (erule_tac x="x" in allE)

   235 apply simp

   236 apply(cases rule: subst_substs_graph.cases)

   237 apply assumption

   238 apply (rule_tac x="lookup \<theta> X" in exI)

   239 apply clarify

   240 apply (rule the1_equality)

   241 apply blast apply assumption

   242 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))

   243                   (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)

   244 apply clarify

   245 apply (rule the1_equality)

   246 apply blast apply assumption

   247 apply clarify

   248 apply simp

   249 --"-"

   250 apply clarify

   251   apply (frule supp_eqvt_at)

   252   apply (simp add: finite_supp)

   253   apply (erule Abs_res_fcb)

   254   apply (simp add: Abs_fresh_iff)

   255   apply (simp add: Abs_fresh_iff)

   256   apply auto[1]

   257   apply (simp add: fresh_def fresh_star_def)

   258   apply (erule contra_subsetD)

   259   apply (simp add: supp_Pair)

   260   apply blast

   261   apply clarify

   262   apply (simp)

   263   apply (simp add: eqvt_at_def)

   264   apply (subst Abs_eq_iff)

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

   266   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")

   267   apply (simp add: alphas fresh_star_zero)

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

   269   apply blast

   270   apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")

   271   apply (simp add: supp_Pair eqvts eqvts_raw)

   272   apply auto[1]

   273   apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")

   274   apply (simp add: fresh_star_def fresh_def)

   275   apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])

   276   apply (simp add: eqvts eqvts_raw)

   277   apply (simp add: fresh_star_def fresh_def)

   278   apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])

   279   apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")

   280   apply (erule subsetD)

   281   apply (simp add: supp_eqvt)

   282   apply (metis le_eqvt permute_boolI)

   283   apply (rule perm_supp_eq)

   284   apply (simp add: fresh_def fresh_star_def)

   285   apply blast

   286   done

   287 

   288 

   289 termination (eqvt) by lexicographic_order

   290 

   291 

   292 section {* defined as two separate nominal datatypes *}

   293 

   294 nominal_datatype ty2 =

   295   Var2 "name"

   296 | Fun2 "ty2" "ty2"

   297 

   298 nominal_datatype tys2 =

   299   All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty

   300 

   301 thm tys2.distinct

   302 thm tys2.induct tys2.strong_induct

   303 thm tys2.exhaust tys2.strong_exhaust

   304 thm tys2.fv_defs

   305 thm tys2.bn_defs

   306 thm tys2.perm_simps

   307 thm tys2.eq_iff

   308 thm tys2.fv_bn_eqvt

   309 thm tys2.size_eqvt

   310 thm tys2.supports

   311 thm tys2.supp

   312 thm tys2.fresh

   313 

   314 fun

   315   lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"

   316 where

   317   "lookup2 [] Y = Var2 Y"

   318 | "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"

   319 

   320 lemma lookup2_eqvt[eqvt]:

   321   shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"

   322   by (induct Ts T rule: lookup2.induct) simp_all

   323 

   324 nominal_primrec

   325   subst2  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"

   326 where

   327   "subst2 \<theta> (Var2 X) = lookup2 \<theta> X"

   328 | "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)"

   329   unfolding eqvt_def subst2_graph_def

   330   apply (rule, perm_simp, rule)

   331   apply(rule TrueI)

   332   apply(case_tac x)

   333   apply(rule_tac y="b" in ty2.exhaust)

   334   apply(blast)

   335   apply(blast)

   336   apply(simp_all add: ty2.distinct)

   337   done

   338 

   339 termination (eqvt)

   340   by lexicographic_order

   341 

   342 

   343 lemma supp_fun_app2_eqvt:

   344   assumes e: "eqvt f"

   345   shows "supp (f a b) \<subseteq> supp a \<union> supp b"

   346   using supp_fun_app_eqvt[OF e] supp_fun_app

   347   by blast

   348  

   349 lemma supp_subst:

   350   "supp (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t"

   351   apply (rule supp_fun_app2_eqvt)

   352   unfolding eqvt_def by (simp add: eqvts_raw)

   353  

   354 lemma fresh_star_inter1:

   355   "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"

   356   unfolding fresh_star_def by blast

   357 

   358 nominal_primrec

   359   substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"

   360 where

   361   "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)"

   362   unfolding eqvt_def substs2_graph_def

   363   apply (rule, perm_simp, rule)

   364   apply auto[2]

   365   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)

   366   apply auto[1]

   367   apply(simp)

   368   apply(erule conjE)

   369   apply (erule Abs_res_fcb)

   370   apply (simp add: Abs_fresh_iff)

   371   apply(simp add: fresh_def)

   372   apply(simp add: supp_Abs)

   373   apply(rule impI)

   374   apply(subgoal_tac "x \<notin> supp \<theta>")

   375   prefer 2

   376   apply(auto simp add: fresh_star_def fresh_def)[1]

   377   apply(subgoal_tac "x \<in> supp t")

   378   using supp_subst

   379   apply(blast)

   380   using supp_subst

   381   apply(blast)

   382   apply clarify

   383   apply (simp add: subst2.eqvt)

   384   apply (subst Abs_eq_iff)

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

   386   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")

   387   apply (simp add: alphas fresh_star_zero)

   388   apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")

   389   apply blast

   390   apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")

   391   apply (simp add: supp_Pair eqvts eqvts_raw)

   392   apply auto[1]

   393   apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")

   394   apply (simp add: fresh_star_def fresh_def)

   395   apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])

   396   apply (simp add: eqvts eqvts_raw)

   397   apply (simp add: fresh_star_def fresh_def)

   398   apply (drule subsetD[OF supp_subst])

   399   apply (simp add: supp_Pair)

   400   apply (rule perm_supp_eq)

   401   apply (simp add: fresh_def fresh_star_def)

   402   apply blast

   403   done

   404 

   405 text {* Some Tests about Alpha-Equality *}

   406 

   407 lemma

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

   409   apply(simp add: ty_tys.eq_iff Abs_eq_iff)

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

   411   apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)

   412   done

   413 

   414 lemma

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

   416   apply(simp add: ty_tys.eq_iff Abs_eq_iff)

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

   418   apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)

   419   done

   420 

   421 lemma

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

   423   apply(simp add: ty_tys.eq_iff Abs_eq_iff)

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

   425   apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)

   426 done

   427 

   428 lemma

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

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

   431   using a

   432   apply(simp add: ty_tys.eq_iff Abs_eq_iff)

   433   apply(clarify)

   434   apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)

   435   apply auto

   436   done

   437 

   438 

   439 

   440 

   441 end