1 theory ExCoreHaskell

     2 imports "../NewParser"

     3 begin

     4 

     5 (* core haskell *)

     6 

     7 atom_decl var

     8 atom_decl cvar

     9 atom_decl tvar

    10 

    11 (* there are types, coercion types and regular types list-data-structure *)

    12 

    13 nominal_datatype tkind =

    14   KStar

    15 | KFun "tkind" "tkind"

    16 and ckind =

    17   CKEq "ty" "ty"

    18 and ty =

    19   TVar "tvar"

    20 | TC "string"

    21 | TApp "ty" "ty"

    22 | TFun "string" "ty_lst"

    23 | TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T

    24 | TEq "ckind" "ty"

    25 and ty_lst =

    26   TsNil

    27 | TsCons "ty" "ty_lst"

    28 and co =

    29   CVar "cvar"

    30 | CConst "string"

    31 | CApp "co" "co"

    32 | CFun "string" "co_lst"

    33 | CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C

    34 | CEq "ckind" "co"

    35 | CRefl "ty"

    36 | CSym "co"

    37 | CCir "co" "co"

    38 | CAt "co" "ty"

    39 | CLeft "co"

    40 | CRight "co"

    41 | CSim "co" "co"

    42 | CRightc "co"

    43 | CLeftc "co"

    44 | CCoe "co" "co"

    45 and co_lst =

    46   CsNil

    47 | CsCons "co" "co_lst"

    48 and trm =

    49   Var "var"

    50 | K "string"

    51 | LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t

    52 | LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t

    53 | AppT "trm" "ty"

    54 | AppC "trm" "co"

    55 | Lam v::"var" "ty" t::"trm"       bind_set v in t

    56 | App "trm" "trm"

    57 | Let x::"var" "ty" "trm" t::"trm" bind_set x in t

    58 | Case "trm" "assoc_lst"

    59 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"

    60 and assoc_lst =

    61   ANil

    62 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t

    63 and pat =

    64   Kpat "string" "tvars" "cvars" "vars"

    65 and vars =

    66   VsNil

    67 | VsCons "var" "ty" "vars"

    68 and tvars =

    69   TvsNil

    70 | TvsCons "tvar" "tkind" "tvars"

    71 and cvars =

    72   CvsNil

    73 | CvsCons "cvar" "ckind" "cvars"

    74 binder

    75     bv :: "pat \<Rightarrow> atom list"

    76 and bv_vs :: "vars \<Rightarrow> atom list"

    77 and bv_tvs :: "tvars \<Rightarrow> atom list"

    78 and bv_cvs :: "cvars \<Rightarrow> atom list"

    79 where

    80   "bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"

    81 | "bv_vs VsNil = []"

    82 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t"

    83 | "bv_tvs TvsNil = []"

    84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"

    85 | "bv_cvs CvsNil = []"

    86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"

    87 

    88 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)

    89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]

    90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

    91 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff

    92 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts

    93 

    94 lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts

    95 lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros

    96 

    97 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"

    98   unfolding fresh_star_def Ball_def

    99   by auto (simp_all add: fresh_minus_perm)

   100 

   101 primrec permute_bv_vs_raw

   102 where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"

   103 |     "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"

   104 primrec permute_bv_cvs_raw

   105 where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"

   106 |     "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"

   107 primrec permute_bv_tvs_raw

   108 where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"

   109 |     "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"

   110 primrec permute_bv_raw

   111 where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =

   112      Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"

   113 

   114 quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"

   115 is "permute_bv_vs_raw"

   116 quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"

   117 is "permute_bv_cvs_raw"

   118 quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"

   119 is "permute_bv_tvs_raw"

   120 quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"

   121 is "permute_bv_raw"

   122 

   123 lemma rsp_pre:

   124  "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"

   125  "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"

   126  "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"

   127  apply (erule_tac [!] alpha_inducts)

   128  apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)

   129  done

   130 

   131 lemma [quot_respect]:

   132  "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"

   133  "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"

   134  "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"

   135  "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"

   136  apply (simp_all add: rsp_pre)

   137  apply clarify

   138  apply (erule_tac alpha_inducts)

   139  apply (simp_all)

   140  apply (rule alpha_intros)

   141  apply (simp_all add: rsp_pre)

   142  done

   143 

   144 thm permute_bv_raw.simps[no_vars]

   145  permute_bv_vs_raw.simps[quot_lifted]

   146  permute_bv_cvs_raw.simps[quot_lifted]

   147  permute_bv_tvs_raw.simps[quot_lifted]

   148 

   149 lemma permute_bv_pre:

   150   "permute_bv p (Kpat c l1 l2 l3) =

   151    Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"

   152   by (lifting permute_bv_raw.simps)

   153 

   154 lemmas permute_bv[simp] =

   155  permute_bv_pre

   156  permute_bv_vs_raw.simps[quot_lifted]

   157  permute_bv_cvs_raw.simps[quot_lifted]

   158  permute_bv_tvs_raw.simps[quot_lifted]

   159 

   160 lemma perm_bv1:

   161   "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"

   162   "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"

   163   "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"

   164   apply(induct b rule: inducts(12))

   165   apply(simp_all add:permute_bv eqvts)

   166   apply(induct c rule: inducts(11))

   167   apply(simp_all add:permute_bv eqvts)

   168   apply(induct d rule: inducts(10))

   169   apply(simp_all add:permute_bv eqvts)

   170   done

   171 

   172 lemma perm_bv2:

   173   "p \<bullet> bv l = bv (permute_bv p l)"

   174   apply(induct l rule: inducts(9))

   175   apply(simp_all add:permute_bv)

   176   apply(simp add: perm_bv1[symmetric])

   177   apply(simp add: eqvts)

   178   done

   179 

   180 lemma alpha_perm_bn1:

   181  "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"

   182  "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"

   183  "alpha_bv_vs vars (permute_bv_vs q vars)"

   184   apply(induct tvars rule: inducts(11))

   185   apply(simp_all add:permute_bv eqvts eq_iff)

   186   apply(induct cvars rule: inducts(12))

   187   apply(simp_all add:permute_bv eqvts eq_iff)

   188   apply(induct vars rule: inducts(10))

   189   apply(simp_all add:permute_bv eqvts eq_iff)

   190   done

   191 

   192 lemma alpha_perm_bn:

   193   "alpha_bv pat (permute_bv q pat)"

   194   apply(induct pat rule: inducts(9))

   195   apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)

   196   done

   197 

   198 lemma ACons_subst:

   199   "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"

   200   apply (simp only: eq_iff)

   201   apply (simp add: alpha_perm_bn)

   202   apply (rule_tac x="q" in exI)

   203   apply (simp add: alphas)

   204   apply (simp add: perm_bv2[symmetric])

   205   apply (simp add: eqvts[symmetric])

   206   apply (simp add: supp_abs)

   207   apply (simp add: fv_supp)

   208   apply (rule supp_perm_eq[symmetric])

   209   apply (subst supp_finite_atom_set)

   210   apply (rule finite_Diff)

   211   apply (simp add: finite_supp)

   212   apply (assumption)

   213   done

   214 

   215 lemma permute_bv_zero1:

   216   "permute_bv_cvs 0 b = b"

   217   "permute_bv_tvs 0 c = c"

   218   "permute_bv_vs 0 d = d"

   219   apply(induct b rule: inducts(12))

   220   apply(simp_all add:permute_bv eqvts)

   221   apply(induct c rule: inducts(11))

   222   apply(simp_all add:permute_bv eqvts)

   223   apply(induct d rule: inducts(10))

   224   apply(simp_all add:permute_bv eqvts)

   225   done

   226 

   227 lemma permute_bv_zero2:

   228   "permute_bv 0 a = a"

   229   apply(induct a rule: inducts(9))

   230   apply(simp_all add:permute_bv eqvts permute_bv_zero1)

   231   done

   232 

   233 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"

   234   apply (induct x rule: inducts(11))

   235   apply (simp_all add: eq_iff fresh_star_union)

   236   done

   237 

   238 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"

   239 apply (induct x rule: inducts(12))

   240 apply (rule TrueI)+

   241 apply (simp_all add: eq_iff fresh_star_union)

   242 apply (subst supp_perm_eq)

   243 apply (simp_all add: fv_supp)

   244 done

   245 

   246 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"

   247 apply (induct x rule: inducts(10))

   248 apply (rule TrueI)+

   249 apply (simp_all add: fresh_star_union eq_iff)

   250 apply (subst supp_perm_eq)

   251 apply (simp_all add: fv_supp)

   252 done

   253 

   254 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"

   255 apply (induct x rule: inducts(9))

   256 apply (rule TrueI)+

   257 apply (simp_all add: eq_iff fresh_star_union)

   258 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)

   259 apply (subst supp_perm_eq)

   260 apply (simp_all add: fv_supp)

   261 done

   262 

   263 lemma fin1: "finite (fv_bv_tvs x)"

   264 apply (induct x rule: inducts(11))

   265 apply (simp_all add: fv_supp finite_supp)

   266 done

   267 

   268 lemma fin2: "finite (fv_bv_cvs x)"

   269 apply (induct x rule: inducts(12))

   270 apply (simp_all add: fv_supp finite_supp)

   271 done

   272 

   273 lemma fin3: "finite (fv_bv_vs x)"

   274 apply (induct x rule: inducts(10))

   275 apply (simp_all add: fv_supp finite_supp)

   276 done

   277 

   278 lemma fin_fv_bv: "finite (fv_bv x)"

   279 apply (induct x rule: inducts(9))

   280 apply (rule TrueI)+

   281 defer

   282 apply (rule TrueI)+

   283 apply (simp add: fin1 fin2 fin3)

   284 apply (rule finite_supp)

   285 done

   286 

   287 lemma finb1: "finite (set (bv_tvs x))"

   288 apply (induct x rule: inducts(11))

   289 apply (simp_all add: fv_supp finite_supp)

   290 done

   291 

   292 lemma finb2: "finite (set (bv_cvs x))"

   293 apply (induct x rule: inducts(12))

   294 apply (simp_all add: fv_supp finite_supp)

   295 done

   296 

   297 lemma finb3: "finite (set (bv_vs x))"

   298 apply (induct x rule: inducts(10))

   299 apply (simp_all add: fv_supp finite_supp)

   300 done

   301 

   302 lemma fin_bv: "finite (set (bv x))"

   303 apply (induct x rule: inducts(9))

   304 apply (simp_all add: finb1 finb2 finb3)

   305 done

   306 

   307 lemma strong_induction_principle:

   308   assumes a01: "\<And>b. P1 b KStar"

   309   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"

   310   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"

   311   and a04: "\<And>tvar b. P3 b (TVar tvar)"

   312   and a05: "\<And>string b. P3 b (TC string)"

   313   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"

   314   and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"

   315   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>

   316     \<Longrightarrow> P3 b (TAll tvar tkind ty)"

   317   and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"

   318   and a10: "\<And>b. P4 b TsNil"

   319   and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"

   320   and a12: "\<And>string b. P5 b (CVar string)"

   321   and a12a:"\<And>str b. P5 b (CConst str)"

   322   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"

   323   and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"

   324   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>

   325     \<Longrightarrow> P5 b (CAll tvar ckind co)"

   326   and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"

   327   and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"

   328   and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"

   329   and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"

   330   and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"

   331   and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"

   332   and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"

   333   and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"

   334   and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"

   335   and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"

   336   and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"

   337   and a25: "\<And>b. P6 b CsNil"

   338   and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"

   339   and a27: "\<And>var b. P7 b (Var var)"

   340   and a28: "\<And>string b. P7 b (K string)"

   341   and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>

   342     \<Longrightarrow> P7 b (LAMT tvar tkind trm)"

   343   and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>

   344     \<Longrightarrow> P7 b (LAMC tvar ckind trm)"

   345   and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)"

   346   and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"

   347   and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"

   348   and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"

   349   and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>

   350     \<Longrightarrow> P7 b (Let var ty trm1 trm2)"

   351   and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"

   352   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"

   353   and a37: "\<And>b. P8 b ANil"

   354   and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>

   355     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"

   356   and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>

   357     \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"

   358   and a40: "\<And>b. P10 b VsNil"

   359   and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)"

   360   and a42: "\<And>b. P11 b TvsNil"

   361   and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk>

   362     \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"

   363   and a44: "\<And>b. P12 b CvsNil"

   364   and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>

   365     \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"

   366   shows "P1 (a :: 'a :: pt) tkind \<and>

   367          P2 (b :: 'b :: pt) ckind \<and>

   368          P3 (c :: 'c :: {pt,fs}) ty \<and>

   369          P4 (d :: 'd :: pt) ty_lst \<and>

   370          P5 (e :: 'e :: {pt,fs}) co \<and>

   371          P6 (f :: 'f :: pt) co_lst \<and>

   372          P7 (g :: 'g :: {pt,fs}) trm \<and>

   373          P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>

   374          P9 (i :: 'i :: pt) pat \<and>

   375          P10 (j :: 'j :: pt) vars \<and>

   376          P11 (k :: 'k :: pt) tvars \<and>

   377          P12 (l :: 'l :: pt) cvars"

   378 proof -

   379   have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"

   380     apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)

   381     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})

   382     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})

   383 

   384 (* GOAL1 *)

   385     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>

   386                        supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")

   387     apply clarify

   388     apply (simp only: perm)

   389     apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"

   390                and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)

   391     apply (simp add: eq_iff)

   392     apply (rule_tac x="-pa" in exI)

   393     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)

   394     apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"

   395                 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)

   396     apply (simp add: eqvts)

   397     apply (simp add: eqvts[symmetric])

   398     apply (rule conjI)

   399     apply (rule supp_perm_eq)

   400     apply (simp add: eqvts)

   401     apply (subst supp_finite_atom_set)

   402     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   403     apply (simp add: eqvts)

   404     apply (simp add: eqvts)

   405     apply (subst supp_perm_eq)

   406     apply (subst supp_finite_atom_set)

   407     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   408     apply (simp add: eqvts)

   409     apply assumption

   410     apply (simp add: fresh_star_minus_perm)

   411     apply (rule a08)

   412     apply simp

   413     apply(rotate_tac 1)

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

   415     apply simp

   416     apply (simp add: eqvts eqvts_raw)

   417     apply (rule at_set_avoiding2_atom)

   418     apply (simp add: finite_supp)

   419     apply (simp add: finite_supp)

   420     apply (simp add: fresh_def)

   421     apply (simp only: supp_abs eqvts)

   422     apply blast

   423 

   424 (* GOAL2 *)

   425     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>

   426                        supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")

   427     apply clarify

   428     apply (simp only: perm)

   429     apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"

   430                and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)

   431     apply (simp add: eq_iff)

   432     apply (rule_tac x="-pa" in exI)

   433     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)

   434     apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"

   435                 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)

   436     apply (simp add: eqvts)

   437     apply (simp add: eqvts[symmetric])

   438     apply (rule conjI)

   439     apply (rule supp_perm_eq)

   440     apply (simp add: eqvts)

   441     apply (subst supp_finite_atom_set)

   442     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   443     apply (simp add: eqvts)

   444     apply (simp add: eqvts)

   445     apply (subst supp_perm_eq)

   446     apply (subst supp_finite_atom_set)

   447     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   448     apply (simp add: eqvts)

   449     apply assumption

   450     apply (simp add: fresh_star_minus_perm)

   451     apply (rule a15)

   452     apply simp

   453     apply(rotate_tac 1)

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

   455     apply simp

   456     apply (simp add: eqvts eqvts_raw)

   457     apply (rule at_set_avoiding2_atom)

   458     apply (simp add: finite_supp)

   459     apply (simp add: finite_supp)

   460     apply (simp add: fresh_def)

   461     apply (simp only: supp_abs eqvts)

   462     apply blast

   463 

   464 

   465 (* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)

   466     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>

   467                        supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")

   468     apply clarify

   469     apply (simp only: perm)

   470     apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"

   471                and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)

   472     apply (simp add: eq_iff)

   473     apply (rule_tac x="-pa" in exI)

   474     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)

   475     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"

   476                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)

   477     apply (simp add: eqvts)

   478     apply (simp add: eqvts[symmetric])

   479     apply (rule conjI)

   480     apply (rule supp_perm_eq)

   481     apply (simp add: eqvts)

   482     apply (subst supp_finite_atom_set)

   483     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   484     apply (simp add: eqvts)

   485     apply (simp add: eqvts)

   486     apply (subst supp_perm_eq)

   487     apply (subst supp_finite_atom_set)

   488     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   489     apply (simp add: eqvts)

   490     apply assumption

   491     apply (simp add: fresh_star_minus_perm)

   492     apply (rule a29)

   493     apply simp

   494     apply(rotate_tac 1)

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

   496     apply simp

   497     apply (simp add: eqvts eqvts_raw)

   498     apply (rule at_set_avoiding2_atom)

   499     apply (simp add: finite_supp)

   500     apply (simp add: finite_supp)

   501     apply (simp add: fresh_def)

   502     apply (simp only: supp_abs eqvts)

   503     apply blast

   504 

   505 (* GOAL4 a copy-and-paste *)

   506     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>

   507                        supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")

   508     apply clarify

   509     apply (simp only: perm)

   510     apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"

   511                and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)

   512     apply (simp add: eq_iff)

   513     apply (rule_tac x="-pa" in exI)

   514     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)

   515     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"

   516                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)

   517     apply (simp add: eqvts)

   518     apply (simp add: eqvts[symmetric])

   519     apply (rule conjI)

   520     apply (rule supp_perm_eq)

   521     apply (simp add: eqvts)

   522     apply (subst supp_finite_atom_set)

   523     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   524     apply (simp add: eqvts)

   525     apply (simp add: eqvts)

   526     apply (subst supp_perm_eq)

   527     apply (subst supp_finite_atom_set)

   528     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   529     apply (simp add: eqvts)

   530     apply assumption

   531     apply (simp add: fresh_star_minus_perm)

   532     apply (rule a30)

   533     apply simp

   534     apply(rotate_tac 1)

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

   536     apply simp

   537     apply (simp add: eqvts eqvts_raw)

   538     apply (rule at_set_avoiding2_atom)

   539     apply (simp add: finite_supp)

   540     apply (simp add: finite_supp)

   541     apply (simp add: fresh_def)

   542     apply (simp only: supp_abs eqvts)

   543     apply blast

   544 

   545 

   546 (* GOAL5 a copy-and-paste *)

   547     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>

   548                        supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")

   549     apply clarify

   550     apply (simp only: perm)

   551     apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"

   552                and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)

   553     apply (simp add: eq_iff)

   554     apply (rule_tac x="-pa" in exI)

   555     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)

   556     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"

   557                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)

   558     apply (simp add: eqvts)

   559     apply (simp add: eqvts[symmetric])

   560     apply (rule conjI)

   561     apply (rule supp_perm_eq)

   562     apply (simp add: eqvts)

   563     apply (subst supp_finite_atom_set)

   564     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   565     apply (simp add: eqvts)

   566     apply (simp add: eqvts)

   567     apply (subst supp_perm_eq)

   568     apply (subst supp_finite_atom_set)

   569     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   570     apply (simp add: eqvts)

   571     apply assumption

   572     apply (simp add: fresh_star_minus_perm)

   573     apply (rule a32)

   574     apply simp

   575     apply(rotate_tac 1)

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

   577     apply simp

   578     apply (simp add: eqvts eqvts_raw)

   579     apply (rule at_set_avoiding2_atom)

   580     apply (simp add: finite_supp)

   581     apply (simp add: finite_supp)

   582     apply (simp add: fresh_def)

   583     apply (simp only: supp_abs eqvts)

   584     apply blast

   585 

   586 

   587 (* GOAL6 a copy-and-paste *)

   588     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>

   589                        supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")

   590     apply clarify

   591     apply (simp only: perm)

   592     apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"

   593                and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)

   594     apply (simp add: eq_iff)

   595     apply (rule_tac x="-pa" in exI)

   596     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)

   597     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"

   598                 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)

   599     apply (simp add: eqvts)

   600     apply (simp add: eqvts[symmetric])

   601     apply (rule conjI)

   602     apply (rule supp_perm_eq)

   603     apply (simp add: eqvts)

   604     apply (subst supp_finite_atom_set)

   605     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   606     apply (simp add: eqvts)

   607     apply (simp add: eqvts)

   608     apply (subst supp_perm_eq)

   609     apply (subst supp_finite_atom_set)

   610     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)

   611     apply (simp add: eqvts)

   612     apply assumption

   613     apply (simp add: fresh_star_minus_perm)

   614     apply (rule a34)

   615     apply simp

   616     apply simp

   617     apply(rotate_tac 2)

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

   619     apply simp

   620     apply (simp add: eqvts eqvts_raw)

   621     apply (rule at_set_avoiding2_atom)

   622     apply (simp add: finite_supp)

   623     apply (simp add: finite_supp)

   624     apply (simp add: fresh_def)

   625     apply (simp only: supp_abs eqvts)

   626     apply blast

   627 

   628 (* MAIN ACons Goal *)

   629     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>

   630                        supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")

   631     apply clarify

   632     apply (simp only: perm eqvts)

   633     apply (subst ACons_subst)

   634     apply assumption

   635     apply (rule a38)

   636     apply simp

   637     apply(rotate_tac 1)

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

   639     apply simp

   640     apply simp

   641     apply (simp add: perm_bv2[symmetric])

   642     apply (simp add: eqvts eqvts_raw)

   643     apply (rule at_set_avoiding2)

   644     apply (simp add: fin_bv)

   645     apply (simp add: finite_supp)

   646     apply (simp add: supp_abs)

   647     apply (simp add: finite_supp)

   648     apply (simp add: fresh_star_def fresh_def supp_abs eqvts)

   649     done

   650   then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)

   651   moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)

   652   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)

   653 qed

   654 

   655 section {* test about equivariance for alpha *}

   656 

   657 (* this should not be an equivariance rule *)

   658 (* for the moment, we force it to be       *)

   659 

   660 (*declare permute_pure[eqvt]*)

   661 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *)

   662 

   663 thm eqvts

   664 thm eqvts_raw

   665 

   666 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]

   667 declare alpha_gen_eqvt[eqvt]

   668 

   669 equivariance alpha_tkind_raw

   670 

   671 thm eqvts

   672 thm eqvts_raw

   673 

   674 end

   675