1 theory TypeSchemes1

     2 imports "../Nominal2"

     3 begin

     4 

     5 section {* Type Schemes defined as two separate nominal datatypes *}

     6 

     7 atom_decl name 

     8 

     9 nominal_datatype ty =

    10   Var "name"

    11 | Fun "ty" "ty" ("_ \<rightarrow> _")

    12 

    13 nominal_datatype tys =

    14   All xs::"name fset" ty::"ty" binds (set+) xs in ty ("All [_]._")

    15 

    16 thm tys.distinct

    17 thm tys.induct tys.strong_induct

    18 thm tys.exhaust tys.strong_exhaust

    19 thm tys.fv_defs

    20 thm tys.bn_defs

    21 thm tys.perm_simps

    22 thm tys.eq_iff

    23 thm tys.fv_bn_eqvt

    24 thm tys.size_eqvt

    25 thm tys.supports

    26 thm tys.supp

    27 thm tys.fresh

    28 

    29 subsection {* Some Tests about Alpha-Equality *}

    30 

    31 lemma

    32   shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"

    33   apply(simp add: Abs_eq_iff)

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

    35   apply(simp add: alphas fresh_star_def ty.supp supp_at_base)

    36   done

    37 

    38 lemma

    39   shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"

    40   apply(simp add: Abs_eq_iff)

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

    42   apply(simp add: alphas fresh_star_def supp_at_base ty.supp)

    43   done

    44 

    45 lemma

    46   shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"

    47   apply(simp add: Abs_eq_iff)

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

    49   apply(simp add: alphas fresh_star_def ty.supp supp_at_base)

    50 done

    51 

    52 lemma

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

    54   shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"

    55   using a

    56   apply(simp add: Abs_eq_iff)

    57   apply(clarify)

    58   apply(simp add: alphas fresh_star_def ty.supp supp_at_base)

    59   apply auto

    60   done

    61 

    62 

    63 subsection {* Substitution function for types and type schemes *}

    64 

    65 type_synonym 

    66   Subst = "(name \<times> ty) list"

    67 

    68 fun

    69   lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"

    70 where

    71   "lookup [] Y = Var Y"

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

    73 

    74 lemma lookup_eqvt[eqvt]:

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

    76   by (induct Ts T rule: lookup.induct) (simp_all)

    77 

    78 nominal_primrec

    79   subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)

    80 where

    81   "\<theta><Var X> = lookup \<theta> X"

    82 | "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"

    83   apply(simp add: eqvt_def subst_graph_aux_def)

    84   apply(rule TrueI)

    85   apply(case_tac x)

    86   apply(rule_tac y="b" in ty.exhaust)

    87   apply(blast)

    88   apply(blast)

    89   apply(simp_all)

    90   done

    91 

    92 termination (eqvt)

    93   by lexicographic_order

    94 

    95 lemma subst_id1:

    96   fixes T::"ty"

    97   shows "[]<T> = T"

    98 by (induct T rule: ty.induct) (simp_all)

    99 

   100 lemma subst_id2:

   101   fixes T::"ty"

   102   shows "[(X, Var X)]<T> = T"

   103 by (induct T rule: ty.induct) (simp_all)

   104 

   105 lemma supp_fun_app_eqvt:

   106   assumes e: "eqvt f"

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

   108   using supp_fun_app_eqvt[OF e] supp_fun_app

   109   by blast

   110  

   111 lemma supp_subst:

   112   "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t"

   113   apply (rule supp_fun_app_eqvt)

   114   unfolding eqvt_def 

   115   by (simp add: permute_fun_def subst.eqvt)

   116  

   117 nominal_primrec

   118   substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)

   119 where

   120   "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"

   121   apply(simp add: eqvt_def substs_graph_aux_def)

   122   apply auto[2]

   123   apply (rule_tac y="b" and c="a" in tys.strong_exhaust)

   124   apply auto[1]

   125   apply(simp)

   126   apply(erule conjE)

   127   apply (erule Abs_res_fcb)

   128   apply (simp add: Abs_fresh_iff)

   129   apply(simp add: fresh_def)

   130   apply(simp add: supp_Abs)

   131   apply(rule impI)

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

   133   prefer 2

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

   135   apply(subgoal_tac "x \<in> supp T")

   136   using supp_subst

   137   apply(blast)

   138   using supp_subst

   139   apply(blast)

   140   apply clarify

   141   apply (simp add: subst.eqvt)

   142   apply (subst Abs_eq_iff)

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

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

   145   apply (simp add: alphas fresh_star_zero)

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

   147   apply(simp)

   148   apply blast

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

   150   apply (simp add: supp_Pair eqvts eqvts_raw)

   151   apply auto[1]

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

   153   apply (simp add: fresh_star_def fresh_def)

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

   155   apply (simp add: eqvts eqvts_raw)

   156   apply (simp add: fresh_star_def fresh_def)

   157   apply (drule subsetD[OF supp_subst])

   158   apply (simp add: supp_Pair)

   159   apply (rule perm_supp_eq)

   160   apply (simp add: fresh_def fresh_star_def)

   161   apply blast

   162   done

   163 

   164 termination (eqvt)

   165   by (lexicographic_order)

   166 

   167 

   168 subsection {* Generalisation of types and type-schemes*}

   169 

   170 fun

   171   subst_Dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_|_")

   172 where

   173   "[]|p = []"

   174 | "((X,T)#\<theta>)|p = (p \<bullet> X, T)#(\<theta>|p)" 

   175 

   176 fun

   177   subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>"  [100,60] 120)

   178 where

   179   "\<theta><[]> = []"

   180 | "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"

   181 

   182 fun

   183   Dom :: "Subst \<Rightarrow> name set"

   184 where

   185   "Dom [] = {}"

   186 | "Dom ((X,T)#\<theta>) = {X} \<union> Dom \<theta>"

   187 

   188 lemma Dom_eqvt[eqvt]:

   189   shows "p \<bullet> (Dom \<theta>) = Dom (p \<bullet> \<theta>)"

   190 apply (induct \<theta> rule: Dom.induct) 

   191 apply (simp_all add: permute_set_def)

   192 apply (auto)

   193 done

   194 

   195 lemma Dom_subst:

   196   fixes \<theta>1 \<theta>2::"Subst"

   197   shows "Dom (\<theta>2<\<theta>1>) = (Dom \<theta>1)"

   198 by (induct \<theta>1) (auto)

   199 

   200 lemma Dom_pi:

   201   shows "Dom (\<theta>|p) = Dom (p \<bullet> \<theta>)"

   202 by (induct \<theta>) (auto)

   203 

   204 lemma Dom_fresh_lookup:

   205   fixes \<theta>::"Subst"

   206   assumes "\<forall>Y \<in> Dom \<theta>. atom Y \<sharp> X"

   207   shows "lookup \<theta> X = Var X"

   208 using assms

   209 by (induct \<theta>) (auto simp add: fresh_at_base)

   210 

   211 lemma Dom_fresh_ty:

   212   fixes \<theta>::"Subst"

   213   and   T::"ty"

   214   assumes "\<forall>X \<in> Dom \<theta>. atom X \<sharp> T"

   215   shows "\<theta><T> = T"

   216 using assms

   217 by (induct T rule: ty.induct) (auto simp add: ty.fresh Dom_fresh_lookup)

   218 

   219 lemma Dom_fresh_subst:

   220   fixes \<theta> \<theta>'::"Subst"

   221   assumes "\<forall>X \<in> Dom \<theta>. atom X \<sharp> \<theta>'"

   222   shows "\<theta><\<theta>'> = \<theta>'"

   223 using assms

   224 by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons Dom_fresh_ty)

   225 

   226 lemma s1:

   227   assumes "name \<in> Dom \<theta>"

   228   shows "lookup \<theta> name = lookup \<theta>|p (p \<bullet> name)"

   229 using assms

   230 apply(induct \<theta>)

   231 apply(auto)

   232 done

   233 

   234 lemma lookup_fresh:

   235   fixes X::"name"

   236   assumes a: "atom X \<sharp> \<theta>"

   237   shows "lookup \<theta> X = Var X"

   238   using a

   239   by (induct \<theta>) (auto simp add: fresh_Cons fresh_Pair fresh_at_base)

   240 

   241 lemma lookup_Dom:

   242   fixes X::"name"

   243   assumes "X \<notin> Dom \<theta>"

   244   shows "lookup \<theta> X = Var X"

   245   using assms

   246   by (induct \<theta>) (auto)

   247 

   248 lemma t:

   249   fixes T::"ty"

   250   assumes a: "(supp T - atom ` Dom \<theta>) \<sharp>* p"

   251   shows "\<theta><T> = \<theta>|p<p \<bullet> T>"

   252 using a

   253 apply(induct T rule: ty.induct)

   254 defer

   255 apply(simp add: ty.supp fresh_star_def)

   256 apply(simp)

   257 apply(case_tac "name \<in> Dom \<theta>")

   258 apply(rule s1)

   259 apply(assumption)

   260 apply(subst lookup_Dom)

   261 apply(assumption)

   262 apply(subst lookup_Dom)

   263 apply(simp add: Dom_pi)

   264 apply(rule_tac p="- p" in permute_boolE)

   265 apply(perm_simp add: permute_minus_cancel)

   266 apply(simp)

   267 apply(simp)

   268 apply(simp add: ty.supp supp_at_base)

   269 apply(simp add: fresh_star_def)

   270 apply(drule_tac x="atom name" in bspec)

   271 apply(auto)[1]

   272 apply(simp add: fresh_def supp_perm)

   273 done

   274 

   275 nominal_primrec

   276   generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")

   277 where

   278   "atom ` (fset Xs) \<sharp>* T \<Longrightarrow>  

   279      T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"

   280 apply(simp add: generalises_graph_aux_def eqvt_def)

   281 apply(rule TrueI)

   282 apply(case_tac x)

   283 apply(simp)

   284 apply(rule_tac y="b" and c="a" in tys.strong_exhaust)

   285 apply(simp)

   286 apply(clarify)

   287 apply(simp only: tys.eq_iff map_fset_image)

   288 apply(erule_tac c="Ta" in Abs_res_fcb2)

   289 apply(simp)

   290 apply(simp)

   291 apply(simp add: fresh_star_def pure_fresh)

   292 apply(simp add: fresh_star_def pure_fresh)

   293 apply(simp add: fresh_star_def pure_fresh)

   294 apply(perm_simp)

   295 apply(subst perm_supp_eq)

   296 apply(simp)

   297 apply(simp)

   298 apply(perm_simp)

   299 apply(subst perm_supp_eq)

   300 apply(simp)

   301 apply(simp)

   302 done

   303 

   304 termination (eqvt)

   305   by lexicographic_order

   306   

   307 lemma better:

   308   "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"

   309 using at_set_avoiding3

   310 apply -

   311 apply(drule_tac x="atom ` fset Xs" in meta_spec)

   312 apply(drule_tac x="T" in meta_spec)

   313 apply(drule_tac x="All [Xs].T'" in meta_spec)

   314 apply(drule meta_mp)

   315 apply(simp)

   316 apply(drule meta_mp)

   317 apply(simp add: finite_supp)

   318 apply(drule meta_mp)

   319 apply(simp add: finite_supp)

   320 apply(drule_tac meta_mp)

   321 apply(simp add: fresh_star_def tys.fresh)

   322 apply(clarify)

   323 apply(rule_tac t="All [Xs].T'" and s="p \<bullet> All [Xs].T'" in subst)

   324 apply(rule supp_perm_eq)

   325 apply(assumption)

   326 apply(perm_simp)

   327 apply(subst generalises.simps)

   328 apply(assumption)

   329 apply(rule iffI)

   330 defer

   331 apply(clarify)

   332 apply(rule_tac x="\<theta>|p" in exI)

   333 apply(rule conjI)

   334 apply(rule t)

   335 apply(simp add: tys.supp)

   336 apply (metis Diff_Int_distrib Int_Diff Int_commute inf_sup_absorb)

   337 apply(simp add: Dom_pi)

   338 apply(rotate_tac 3)

   339 apply(drule_tac p="p" in permute_boolI)

   340 apply(perm_simp)

   341 apply(assumption)

   342 apply(clarify)

   343 apply(rule_tac x="\<theta>|- p" in exI)

   344 apply(rule conjI)

   345 apply(subst t[where p="- p"])

   346 apply(simp add: tys.supp)

   347 apply(rotate_tac 1)

   348 apply(drule_tac p="p" in permute_boolI)

   349 apply(perm_simp)

   350 apply(simp add: permute_self)

   351 apply(simp add: fresh_star_def)

   352 apply(simp add: fresh_minus_perm)

   353 apply (metis Diff_Int_distrib Int_Diff Int_commute inf_sup_absorb)

   354 apply(simp)

   355 apply(simp add: Dom_pi)

   356 apply(rule_tac p="p" in permute_boolE)

   357 apply(perm_simp add: permute_minus_cancel)

   358 apply(assumption)

   359 done

   360 

   361 

   362 (* Tests *)

   363 

   364 fun 

   365   compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)

   366 where

   367   "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"

   368 | "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"

   369 

   370 lemma compose_ty:

   371   fixes  \<theta>1 \<theta>2 :: "Subst"

   372   and    T :: "ty"

   373   shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"

   374 proof (induct T rule: ty.induct)

   375   case (Var X) 

   376   have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X" 

   377     by (induct \<theta>2) (auto)

   378   then show ?case by simp

   379 next

   380   case (Fun T1 T2)

   381   then show ?case by simp

   382 qed

   383 

   384 lemma compose_Dom:

   385   shows "Dom (\<theta>1 \<circ> \<theta>2) = Dom \<theta>1 \<union> Dom \<theta>2"

   386 apply(induct \<theta>2)

   387 apply(auto)

   388 done

   389 

   390 lemma t1:

   391   fixes T::"ty"

   392   and Xs::"name fset"

   393   shows "\<exists>\<theta>. atom ` Dom \<theta> = atom ` fset Xs \<and> \<theta><T> = T"

   394 apply(induct Xs)

   395 apply(rule_tac x="[]" in exI)

   396 apply(simp add: subst_id1)

   397 apply(clarify)

   398 apply(rule_tac x="[(x, Var x)] \<circ> \<theta>" in exI)

   399 apply(simp add: compose_ty[symmetric] subst_id2 compose_Dom)

   400 done

   401 

   402 nominal_primrec

   403   ftv  :: "ty \<Rightarrow> name fset"

   404 where

   405   "ftv (Var X) = {|X|}"

   406 | "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"

   407   apply(simp add: eqvt_def ftv_graph_aux_def)

   408   apply(rule TrueI)

   409   apply(rule_tac y="x" in ty.exhaust)

   410   apply(blast)

   411   apply(blast)

   412   apply(simp_all)

   413   done

   414 

   415 termination (eqvt)

   416   by lexicographic_order

   417 

   418 lemma tt:

   419   shows "supp T = atom ` fset (ftv T)"

   420 apply(induct T rule: ty.induct)

   421 apply(simp_all add: ty.supp supp_at_base)

   422 apply(auto)

   423 done

   424 

   425 

   426 lemma t2:

   427   shows "T \<prec>\<prec> All [Xs].T"

   428 unfolding better

   429 using t1

   430 apply -

   431 apply(drule_tac x="Xs |\<inter>| ftv T" in meta_spec)

   432 apply(drule_tac x="T" in meta_spec)

   433 apply(clarify)

   434 apply(rule_tac x="\<theta>" in exI)

   435 apply(simp add: tt)

   436 apply(auto)

   437 done

   438 

   439 (* HERE *)

   440 

   441 lemma w1: 

   442   shows "\<theta><\<theta>'|p> = (\<theta><\<theta>'>)|p"

   443   by (induct \<theta>')(auto)

   444 

   445 (*

   446 lemma w2:

   447   assumes "name |\<in>| Dom \<theta>'" 

   448   shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"

   449 using assms

   450 apply(induct \<theta>')

   451 apply(auto simp add: notin_empty_fset)

   452 done

   453 

   454 lemma w3:

   455   assumes "name |\<in>| Dom \<theta>" 

   456   shows "lookup \<theta> name = lookup (\<theta>|p) (p \<bullet> name)"

   457 using assms

   458 apply(induct \<theta>)

   459 apply(auto simp add: notin_empty_fset)

   460 done

   461 

   462 lemma fresh_lookup:

   463   fixes X Y::"name"

   464   and   \<theta>::"Subst"

   465   assumes asms: "atom X \<sharp> Y" "atom X \<sharp> \<theta>"

   466   shows "atom X \<sharp> (lookup \<theta> Y)"

   467   using assms

   468   apply (induct \<theta>)

   469   apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)

   470   done

   471 

   472 lemma test:

   473   fixes \<theta> \<theta>'::"Subst"

   474   and T::"ty"

   475   assumes "(p \<bullet> atom ` fset (Dom \<theta>')) \<sharp>* \<theta>" "supp All [Dom \<theta>'].T \<sharp>* p"

   476   shows "\<theta><\<theta>'<T>> = \<theta><\<theta>'|p><\<theta><p \<bullet> T>>"

   477 using assms

   478 apply(induct T rule: ty.induct)

   479 defer

   480 apply(auto simp add: tys.supp ty.supp fresh_star_def)[1]

   481 apply(auto simp add: tys.supp ty.supp fresh_star_def supp_at_base)[1]

   482 apply(case_tac "name |\<in>| Dom \<theta>'")

   483 apply(subgoal_tac "atom (p \<bullet> name) \<sharp> \<theta>")

   484 apply(subst (2) lookup_fresh)

   485 apply(perm_simp)

   486 apply(auto simp add: fresh_star_def)[1]

   487 apply(simp)

   488 apply(simp add: w1)

   489 apply(simp add: w2)

   490 apply(subst w3[symmetric])

   491 apply(simp add: Dom_subst)

   492 apply(simp)

   493 apply(perm_simp)

   494 apply(rotate_tac 2)

   495 apply(drule_tac p="p" in permute_boolI)

   496 apply(perm_simp)

   497 apply(auto simp add: fresh_star_def)[1]

   498 apply(metis notin_fset)

   499 apply(simp add: lookup_Dom)

   500 apply(perm_simp)

   501 apply(subst Dom_fresh_ty)

   502 apply(auto)[1]

   503 apply(rule fresh_lookup)

   504 apply(simp add: Dom_subst)

   505 apply(simp add: Dom_pi)

   506 apply(perm_simp)

   507 apply(rotate_tac 2)

   508 apply(drule_tac p="p" in permute_boolI)

   509 apply(perm_simp)

   510 apply(simp add: fresh_at_base)

   511 apply (metis in_fset)

   512 apply(simp add: Dom_subst)

   513 apply(simp add: Dom_pi[symmetric])

   514 apply(perm_simp)

   515 apply(subst supp_perm_eq)

   516 apply(simp add: supp_at_base fresh_star_def)

   517 apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)

   518 apply(simp)

   519 done

   520 

   521 lemma generalises_subst:

   522   shows "T \<prec>\<prec> All [Xs].T' \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><All [Xs].T'>"

   523 using at_set_avoiding3

   524 apply -

   525 apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)

   526 apply(drule_tac x="\<theta>" in meta_spec)

   527 apply(drule_tac x="All [Xs].T'" in meta_spec)

   528 apply(drule meta_mp)

   529 apply(simp)

   530 apply(drule meta_mp)

   531 apply(simp add: finite_supp)

   532 apply(drule meta_mp)

   533 apply(simp add: finite_supp)

   534 apply(drule meta_mp)

   535 apply(simp add: tys.fresh fresh_star_def)

   536 apply(erule exE)

   537 apply(erule conjE)+

   538 apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)

   539 apply(rule supp_perm_eq)

   540 apply(assumption)

   541 apply(perm_simp)

   542 apply(subst substs.simps)

   543 apply(simp)

   544 apply(simp add: better)

   545 apply(erule exE)

   546 apply(simp)

   547 apply(rule_tac x="\<theta><\<theta>'|p>" in exI)

   548 apply(rule conjI)

   549 apply(rule test)

   550 apply(simp)

   551 apply(perm_simp)

   552 apply(simp add: fresh_star_def)

   553 apply(auto)[1]

   554 apply(simp add: tys.supp)

   555 apply(simp add: fresh_star_def)

   556 apply(auto)[1]

   557 oops

   558 

   559 lemma generalises_subst:

   560   shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"

   561 unfolding generalises_def

   562 apply(erule exE)+

   563 apply(erule conjE)+

   564 apply(rule_tac t="S" and s="All [Xs].T'" in subst)

   565 apply(simp)

   566 using at_set_avoiding3

   567 apply -

   568 apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)

   569 apply(drule_tac x="\<theta>" in meta_spec)

   570 apply(drule_tac x="All [Xs].T'" in meta_spec)

   571 apply(drule meta_mp)

   572 apply(simp)

   573 apply(drule meta_mp)

   574 apply(simp add: finite_supp)

   575 apply(drule meta_mp)

   576 apply(simp add: finite_supp)

   577 apply(drule meta_mp)

   578 apply(simp add: tys.fresh fresh_star_def)

   579 apply(erule exE)

   580 apply(erule conjE)+

   581 apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)

   582 apply(rule supp_perm_eq)

   583 apply(assumption)

   584 apply(perm_simp)

   585 apply(subst substs.simps)

   586 apply(perm_simp)

   587 apply(simp)

   588 apply(rule_tac x="\<theta><\<theta>'|p>" in exI)

   589 apply(rule_tac x="p \<bullet> Xs" in exI)

   590 apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)

   591 apply(rule conjI)

   592 apply(simp)

   593 apply(rule conjI)

   594 defer

   595 apply(simp add: Dom_subst)

   596 apply(simp add: Dom_pi Dom_eqvt[symmetric])

   597 apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)

   598 apply(simp)

   599 apply(simp)

   600 apply(rule test)

   601 apply(perm_simp)

   602 apply(rotate_tac 2)

   603 apply(drule_tac p="p" in permute_boolI)

   604 apply(perm_simp)

   605 apply(auto simp add: fresh_star_def)

   606 done

   607 

   608 

   609 lemma r:

   610   "A - (B \<inter> A) = A - B"

   611 by (metis Diff_Int Diff_cancel sup_bot_right)

   612 

   613 

   614 lemma t3:

   615   "T \<prec>\<prec>  All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> Dom \<theta> = Xs)"

   616 apply(auto)

   617 defer

   618 apply(simp add: generalises_def)

   619 apply(auto)[1]

   620 unfolding generalises_def

   621 apply(auto)[1]

   622 apply(simp add:  Abs_eq_res_set)

   623 apply(simp add: Abs_eq_iff2)

   624 apply(simp add: alphas)

   625 apply(perm_simp)

   626 apply(clarify)

   627 apply(simp add: r)

   628 apply(drule sym)

   629 apply(simp)

   630 apply(rule_tac x="\<theta>|p" in exI)

   631 sorry

   632 

   633 definition

   634   generalises_tys :: "tys \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")

   635 where

   636   "S1 \<prec>\<prec> S2 = (\<forall>T::ty. T \<prec>\<prec> S1 \<longrightarrow> T \<prec>\<prec> S2)"

   637 

   638 lemma

   639   "All [Xs1].T1 \<prec>\<prec> All [Xs2].T2 

   640      \<longleftrightarrow> (\<exists>\<theta>. Dom \<theta> = Xs2 \<and> T1 = \<theta><T2> \<and> (\<forall>X \<in> fset Xs1. atom X \<sharp> All [Xs2].T2))"

   641 apply(rule iffI)

   642 apply(simp add: generalises_tys_def)

   643 apply(drule_tac x="T1" in spec)

   644 apply(drule mp)

   645 apply(rule t2)

   646 apply(simp add: t3)

   647 apply(clarify)

   648 apply(rule_tac x="\<theta>" in exI)

   649 apply(simp)

   650 apply(rule ballI)

   651 defer

   652 apply(simp add: generalises_tys_def)

   653 apply(clarify)

   654 apply(simp add: t3)

   655 apply(clarify)

   656 

   657 

   658 

   659 lemma 

   660   "T \<prec>\<prec>  All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> Dom \<theta> = Xs)"

   661 apply(auto)

   662 defer

   663 apply(simp add: generalises_def)

   664 apply(auto)[1]

   665 apply(auto)[1]

   666 apply(drule sym)

   667 apply(simp add: Abs_eq_iff2)

   668 apply(simp add: alphas)

   669 apply(auto)

   670 apply(rule_tac x="map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>" in exI)

   671 apply(auto)

   672 oops

   673 

   674 *)

   675 

   676 end