Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/ExCoreHaskell.thy
changeset 1700 b5141d1ab24f
parent 1699 2dca07aca287
child 1701 58abc09d6f9c
equal deleted inserted replaced
1699:2dca07aca287 1700:b5141d1ab24f 
    62 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 
    62 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 
    63 and assoc_lst =
 
    63 and assoc_lst =
 
    64   ANil
 
    64   ANil
 
    65 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 
    65 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 
    66 and pat =
 
    66 and pat =
 
    67   Kpat "string" "tvtk_lst" "tvck_lst" "vt_lst"
 
    67   Kpat "string" "tvars" "cvars" "vars"
 
    68 and vt_lst =
 
    68 and vars =
 
    69   VTNil
 
    69   VsNil
 
    70 | VTCons "var" "ty" "vt_lst"
 
    70 | VsCons "var" "ty" "vars"
 
    71 and tvtk_lst =
 
    71 and tvars =
 
    72   TVTKNil
 
    72   TvsNil
 
    73 | TVTKCons "tvar" "tkind" "tvtk_lst"
 
    73 | TvsCons "tvar" "tkind" "tvars"
 
    74 and tvck_lst =
 
    74 and cvars =
 
    75   TVCKNil
 
    75   CvsNil
 
    76 | TVCKCons "cvar" "ckind" "tvck_lst"
 
    76 | CvsCons "cvar" "ckind" "cvars"
 
    77 binder
 
    77 binder
 
    78     bv :: "pat \<Rightarrow> atom list"
 
    78     bv :: "pat \<Rightarrow> atom list"
 
    79 and bv_vt :: "vt_lst \<Rightarrow> atom list"
 
    79 and bv_vs :: "vars \<Rightarrow> atom list"
 
    80 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom list"
 
    80 and bv_tvs :: "tvars \<Rightarrow> atom list"
 
    81 and bv_tvck :: "tvck_lst \<Rightarrow> atom list"
 
    81 and bv_cvs :: "cvars \<Rightarrow> atom list"
 
    82 where
 
    82 where
 
    83   "bv (K s tvts tvcs vs) = append (bv_tvtk tvts) (append (bv_tvck tvcs) (bv_vt vs))"
 
    83   "bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
 
    84 | "bv_vt VTNil = []"
 
    84 | "bv_vs VsNil = []"
 
    85 | "bv_vt (VTCons v k t) = (atom v) # bv_vt t"
 
    85 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
 
    86 | "bv_tvtk TVTKNil = []"
 
    86 | "bv_tvs TvsNil = []"
 
    87 | "bv_tvtk (TVTKCons v k t) = (atom v) # bv_tvtk t"
 
    87 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
 
    88 | "bv_tvck TVCKNil = []"
 
    88 | "bv_cvs CvsNil = []"
 
    89 | "bv_tvck (TVCKCons v k t) = (atom v) # bv_tvck t"
 
    89 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
    90 
    90 
    91 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15)
 
    91 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 
    92 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
 
    92 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 
    93 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm
 
    93 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
 
    94 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff
 
    94 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
 
    95 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts
 
    95 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts
 
    96 
    96 
    97 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_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.inducts
 
    97 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
 
    98 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_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.intros
 
    98 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
 
    99 
    99 
   100 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
 
   100 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
 
   101   unfolding fresh_star_def Ball_def
 
   101   unfolding fresh_star_def Ball_def
 
   102   by auto (simp_all add: fresh_minus_perm)
 
   102   by auto (simp_all add: fresh_minus_perm)
 
   103 
   103 
   104 primrec permute_bv_vt_raw
 
   104 primrec permute_bv_vs_raw
 
   105 where "permute_bv_vt_raw p VTNil_raw = VTNil_raw"
 
   105 where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
 
   106 |     "permute_bv_vt_raw p (VTCons_raw v t l) = VTCons_raw (p \<bullet> v) t (permute_bv_vt_raw p l)"
 
   106 |     "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
 
   107 primrec permute_bv_tvck_raw
 
   107 primrec permute_bv_cvs_raw
 
   108 where "permute_bv_tvck_raw p TVCKNil_raw = TVCKNil_raw"
 
   108 where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
 
   109 |     "permute_bv_tvck_raw p (TVCKCons_raw v t l) = TVCKCons_raw (p \<bullet> v) t (permute_bv_tvck_raw p l)"
 
   109 |     "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
 
   110 primrec permute_bv_tvtk_raw
 
   110 primrec permute_bv_tvs_raw
 
   111 where "permute_bv_tvtk_raw p TVTKNil_raw = TVTKNil_raw"
 
   111 where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
 
   112 |     "permute_bv_tvtk_raw p (TVTKCons_raw v t l) = TVTKCons_raw (p \<bullet> v) t (permute_bv_tvtk_raw p l)"
 
   112 |     "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
 
   113 primrec permute_bv_raw
 
   113 primrec permute_bv_raw
 
   114 where "permute_bv_raw p (K_raw c l1 l2 l3) =
 
   114 where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
 
   115      K_raw c (permute_bv_tvtk_raw p l1) (permute_bv_tvck_raw p l2) (permute_bv_vt_raw p l3)"
 
   115      Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
 
   116 
   116 
   117 quotient_definition "permute_bv_vt :: perm \<Rightarrow> vt_lst \<Rightarrow> vt_lst"
 
   117 quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
 
   118 is "permute_bv_vt_raw"
 
   118 is "permute_bv_vs_raw"
 
   119 quotient_definition "permute_bv_tvck :: perm \<Rightarrow> tvck_lst \<Rightarrow> tvck_lst"
 
   119 quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
 
   120 is "permute_bv_tvck_raw"
 
   120 is "permute_bv_cvs_raw"
 
   121 quotient_definition "permute_bv_tvtk :: perm \<Rightarrow> tvtk_lst \<Rightarrow> tvtk_lst"
 
   121 quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
 
   122 is "permute_bv_tvtk_raw"
 
   122 is "permute_bv_tvs_raw"
 
   123 quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
 
   123 quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
 
   124 is "permute_bv_raw"
 
   124 is "permute_bv_raw"
 
   125 
   125 
   126 lemma rsp_pre:
 
   126 lemma rsp_pre:
 
   127  "alpha_tvtk_lst_raw d a \<Longrightarrow> alpha_tvtk_lst_raw (permute_bv_tvtk_raw x d) (permute_bv_tvtk_raw x a)"
 
   127  "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
 
   128  "alpha_tvck_lst_raw e b \<Longrightarrow> alpha_tvck_lst_raw (permute_bv_tvck_raw x e) (permute_bv_tvck_raw x b)"
 
   128  "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
 
   129  "alpha_vt_lst_raw f c \<Longrightarrow> alpha_vt_lst_raw (permute_bv_vt_raw x f) (permute_bv_vt_raw x c)"
 
   129  "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
 
   130  apply (erule_tac [!] alpha_inducts)
 
   130  apply (erule_tac [!] alpha_inducts)
 
   131  apply simp_all
 
   131  apply simp_all
 
   132  apply (rule_tac [!] alpha_intros)
 
   132  apply (rule_tac [!] alpha_intros)
 
   133  apply simp_all
 
   133  apply simp_all
 
   134  done
 
   134  done
 
   135 
   135 
   136 lemma [quot_respect]:
 
   136 lemma [quot_respect]:
 
   137  "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
 
   137  "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
 
   138  "(op = ===> alpha_tvtk_lst_raw ===> alpha_tvtk_lst_raw) permute_bv_tvtk_raw permute_bv_tvtk_raw"
 
   138  "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
 
   139  "(op = ===> alpha_tvck_lst_raw ===> alpha_tvck_lst_raw) permute_bv_tvck_raw permute_bv_tvck_raw"
 
   139  "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
 
   140  "(op = ===> alpha_vt_lst_raw ===> alpha_vt_lst_raw) permute_bv_vt_raw permute_bv_vt_raw"
 
   140  "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
 
   141  apply (simp_all add: rsp_pre)
 
   141  apply (simp_all add: rsp_pre)
 
   142  apply clarify
 
   142  apply clarify
 
   143  apply (erule_tac alpha_inducts)
 
   143  apply (erule_tac alpha_inducts)
 
   144  apply (simp_all)
 
   144  apply (simp_all)
 
   145  apply (rule alpha_intros)
 
   145  apply (rule alpha_intros)
 
   146  apply (simp_all add: rsp_pre)
 
   146  apply (simp_all add: rsp_pre)
 
   147  done
 
   147  done
 
   148 
   148 
   149 thm permute_bv_raw.simps[no_vars]
 
   149 thm permute_bv_raw.simps[no_vars]
 
   150  permute_bv_vt_raw.simps[quot_lifted]
 
   150  permute_bv_vs_raw.simps[quot_lifted]
 
   151  permute_bv_tvck_raw.simps[quot_lifted]
 
   151  permute_bv_cvs_raw.simps[quot_lifted]
 
   152  permute_bv_tvtk_raw.simps[quot_lifted]
 
   152  permute_bv_tvs_raw.simps[quot_lifted]
 
   153 
   153 
   154 lemma permute_bv_pre:
 
   154 lemma permute_bv_pre:
 
   155   "permute_bv p (K c l1 l2 l3) =
 
   155   "permute_bv p (Kpat c l1 l2 l3) =
 
   156    K c (permute_bv_tvtk p l1) (permute_bv_tvck p l2) (permute_bv_vt p l3)"
 
   156    Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
 
   157   by (lifting permute_bv_raw.simps)
 
   157   by (lifting permute_bv_raw.simps)
 
   158 
   158 
   159 lemmas permute_bv[simp] =
 
   159 lemmas permute_bv[simp] =
 
   160  permute_bv_pre
 
   160  permute_bv_pre
 
   161  permute_bv_vt_raw.simps[quot_lifted]
 
   161  permute_bv_vs_raw.simps[quot_lifted]
 
   162  permute_bv_tvck_raw.simps[quot_lifted]
 
   162  permute_bv_cvs_raw.simps[quot_lifted]
 
   163  permute_bv_tvtk_raw.simps[quot_lifted]
 
   163  permute_bv_tvs_raw.simps[quot_lifted]
 
   164 
   164 
   165 lemma perm_bv1:
 
   165 lemma perm_bv1:
 
   166   "p \<bullet> bv_tvck b = bv_tvck (permute_bv_tvck p b)"
 
   166   "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
 
   167   "p \<bullet> bv_tvtk c = bv_tvtk (permute_bv_tvtk p c)"
 
   167   "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
 
   168   "p \<bullet> bv_vt d = bv_vt (permute_bv_vt p d)"
 
   168   "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
 
   169   apply(induct b rule: inducts(12))
 
   169   apply(induct b rule: inducts(12))
 
   170   apply(rule TrueI)
 
   170   apply(rule TrueI)
 
   171   apply(simp_all add:permute_bv eqvts)
 
   171   apply(simp_all add:permute_bv eqvts)
 
   172   apply(induct c rule: inducts(11))
 
   172   apply(induct c rule: inducts(11))
 
   173   apply(rule TrueI)
 
   173   apply(rule TrueI)
 
   185   apply(simp add: perm_bv1[symmetric])
 
   185   apply(simp add: perm_bv1[symmetric])
 
   186   apply(simp add: eqvts)
 
   186   apply(simp add: eqvts)
 
   187   done
 
   187   done
 
   188 
   188 
   189 lemma alpha_perm_bn1:
 
   189 lemma alpha_perm_bn1:
 
   190  " alpha_bv_tvtk tvtk_lst (permute_bv_tvtk q tvtk_lst)"
 
   190  " alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
 
   191  "alpha_bv_tvck tvck_lst (permute_bv_tvck q tvck_lst)"
 
   191  "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
 
   192  "alpha_bv_vt vt_lst (permute_bv_vt q vt_lst)"
 
   192  "alpha_bv_vs vars (permute_bv_vs q vars)"
 
   193   apply(induct tvtk_lst rule: inducts(11))
 
   193   apply(induct tvars rule: inducts(11))
 
   194   apply(simp_all add:permute_bv eqvts eq_iff)
 
   194   apply(simp_all add:permute_bv eqvts eq_iff)
 
   195   apply(induct tvck_lst rule: inducts(12))
 
   195   apply(induct cvars rule: inducts(12))
 
   196   apply(simp_all add:permute_bv eqvts eq_iff)
 
   196   apply(simp_all add:permute_bv eqvts eq_iff)
 
   197   apply(induct vt_lst rule: inducts(10))
 
   197   apply(induct vars rule: inducts(10))
 
   198   apply(simp_all add:permute_bv eqvts eq_iff)
 
   198   apply(simp_all add:permute_bv eqvts eq_iff)
 
   199   done
 
   199   done
 
   200 
   200 
   201 lemma alpha_perm_bn:
 
   201 lemma alpha_perm_bn:
 
   202   "alpha_bv pat (permute_bv q pat)"
 
   202   "alpha_bv pat (permute_bv q pat)"
 
   220   apply (simp add: finite_supp)
 
   220   apply (simp add: finite_supp)
 
   221   apply (assumption)
 
   221   apply (assumption)
 
   222   done
 
   222   done
 
   223 
   223 
   224 lemma permute_bv_zero1:
 
   224 lemma permute_bv_zero1:
 
   225   "permute_bv_tvck 0 b = b"
 
   225   "permute_bv_cvs 0 b = b"
 
   226   "permute_bv_tvtk 0 c = c"
 
   226   "permute_bv_tvs 0 c = c"
 
   227   "permute_bv_vt 0 d = d"
 
   227   "permute_bv_vs 0 d = d"
 
   228   apply(induct b rule: inducts(12))
 
   228   apply(induct b rule: inducts(12))
 
   229   apply(rule TrueI)
 
   229   apply(rule TrueI)
 
   230   apply(simp_all add:permute_bv eqvts)
 
   230   apply(simp_all add:permute_bv eqvts)
 
   231   apply(induct c rule: inducts(11))
 
   231   apply(induct c rule: inducts(11))
 
   232   apply(rule TrueI)
 
   232   apply(rule TrueI)
 
   241   apply(induct a rule: inducts(9))
 
   241   apply(induct a rule: inducts(9))
 
   242   apply(rule TrueI)
 
   242   apply(rule TrueI)
 
   243   apply(simp_all add:permute_bv eqvts permute_bv_zero1)
 
   243   apply(simp_all add:permute_bv eqvts permute_bv_zero1)
 
   244   done
 
   244   done
 
   245 
   245 
   246 lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x"
 
   246 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
 
   247 apply (induct x rule: inducts(11))
 
   247 apply (induct x rule: inducts(11))
 
   248 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   248 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   249 apply (simp_all add: eq_iff fresh_star_union)
 
   249 apply (simp_all add: eq_iff fresh_star_union)
 
   250 apply (subst supp_perm_eq)
 
   250 apply (subst supp_perm_eq)
 
   251 apply (simp_all add: fv_supp)
 
   251 apply (simp_all add: fv_supp)
 
   252 done
 
   252 done
 
   253 
   253 
   254 lemma fv_alpha2: "fv_bv_tvck x \<sharp>* pa \<Longrightarrow> alpha_bv_tvck (pa \<bullet> x) x"
 
   254 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
 
   255 apply (induct x rule: inducts(12))
 
   255 apply (induct x rule: inducts(12))
 
   256 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   256 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   257 apply (simp_all add: eq_iff fresh_star_union)
 
   257 apply (simp_all add: eq_iff fresh_star_union)
 
   258 apply (subst supp_perm_eq)
 
   258 apply (subst supp_perm_eq)
 
   259 apply (simp_all add: fv_supp)
 
   259 apply (simp_all add: fv_supp)
 
   260 done
 
   260 done
 
   261 
   261 
   262 lemma fv_alpha3: "fv_bv_vt x \<sharp>* pa \<Longrightarrow> alpha_bv_vt (pa \<bullet> x) x"
 
   262 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
 
   263 apply (induct x rule: inducts(10))
 
   263 apply (induct x rule: inducts(10))
 
   264 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   264 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   265 apply (simp_all add: eq_iff fresh_star_union)
 
   265 apply (simp_all add: eq_iff fresh_star_union)
 
   266 apply (subst supp_perm_eq)
 
   266 apply (subst supp_perm_eq)
 
   267 apply (simp_all add: fv_supp)
 
   267 apply (simp_all add: fv_supp)
 
   273 apply (simp_all add: eq_iff fresh_star_union)
 
   273 apply (simp_all add: eq_iff fresh_star_union)
 
   274 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
 
   274 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
 
   275 apply (simp add: eqvts)
 
   275 apply (simp add: eqvts)
 
   276 done
 
   276 done
 
   277 
   277 
   278 lemma fin1: "finite (fv_bv_tvtk x)"
 
   278 lemma fin1: "finite (fv_bv_tvs x)"
 
   279 apply (induct x rule: inducts(11))
 
   279 apply (induct x rule: inducts(11))
 
   280 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   280 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   281 apply (simp_all add: fv_supp finite_supp)
 
   281 apply (simp_all add: fv_supp finite_supp)
 
   282 done
 
   282 done
 
   283 
   283 
   284 lemma fin2: "finite (fv_bv_tvck x)"
 
   284 lemma fin2: "finite (fv_bv_cvs x)"
 
   285 apply (induct x rule: inducts(12))
 
   285 apply (induct x rule: inducts(12))
 
   286 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   286 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   287 apply (simp_all add: fv_supp finite_supp)
 
   287 apply (simp_all add: fv_supp finite_supp)
 
   288 done
 
   288 done
 
   289 
   289 
   290 lemma fin3: "finite (fv_bv_vt x)"
 
   290 lemma fin3: "finite (fv_bv_vs x)"
 
   291 apply (induct x rule: inducts(10))
 
   291 apply (induct x rule: inducts(10))
 
   292 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   292 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   293 apply (simp_all add: fv_supp finite_supp)
 
   293 apply (simp_all add: fv_supp finite_supp)
 
   294 done
 
   294 done
 
   295 
   295 
   297 apply (induct x rule: inducts(9))
 
   297 apply (induct x rule: inducts(9))
 
   298 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   298 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   299 apply (simp add: fin1 fin2 fin3)
 
   299 apply (simp add: fin1 fin2 fin3)
 
   300 done
 
   300 done
 
   301 
   301 
   302 lemma finb1: "finite (set (bv_tvtk x))"
 
   302 lemma finb1: "finite (set (bv_tvs x))"
 
   303 apply (induct x rule: inducts(11))
 
   303 apply (induct x rule: inducts(11))
 
   304 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   304 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   305 apply (simp_all add: fv_supp finite_supp)
 
   305 apply (simp_all add: fv_supp finite_supp)
 
   306 done
 
   306 done
 
   307 
   307 
   308 lemma finb2: "finite (set (bv_tvck x))"
 
   308 lemma finb2: "finite (set (bv_cvs x))"
 
   309 apply (induct x rule: inducts(12))
 
   309 apply (induct x rule: inducts(12))
 
   310 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   310 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   311 apply (simp_all add: fv_supp finite_supp)
 
   311 apply (simp_all add: fv_supp finite_supp)
 
   312 done
 
   312 done
 
   313 
   313 
   314 lemma finb3: "finite (set (bv_vt x))"
 
   314 lemma finb3: "finite (set (bv_vs x))"
 
   315 apply (induct x rule: inducts(10))
 
   315 apply (induct x rule: inducts(10))
 
   316 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   316 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   317 apply (simp_all add: fv_supp finite_supp)
 
   317 apply (simp_all add: fv_supp finite_supp)
 
   318 done
 
   318 done
 
   319 
   319 
   332   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
   332   and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
 
   333   and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
 
   333   and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
 
   334   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
 
   334   and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
 
   335     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
 
   335     \<Longrightarrow> P3 b (TAll tvar tkind ty)"
 
   336   and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)"
 
   336   and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)"
 
   337   and a10: "\<And>b. P4 b TsNil"
 
   337   and a10: "\<And>b. P4 b TvsNil"
 
   338   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)"
 
   338   and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TvsCons ty ty_lst)"
 
   339   and a12: "\<And>string b. P5 b (CC string)"
 
   339   and a12: "\<And>string b. P5 b (CC string)"
 
   340   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   340   and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
 
   341   and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
 
   341   and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
 
   342   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
 
   342   and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
 
   343     \<Longrightarrow> P5 b (CAll tvar ckind co)"
 
   343     \<Longrightarrow> P5 b (CAll tvar ckind co)"
 
   366   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)"
 
   366   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)"
 
   367   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   367   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
 
   368   and a37: "\<And>b. P8 b ANil"
 
   368   and a37: "\<And>b. P8 b ANil"
 
   369   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>
 
   369   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>
 
   370     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   370     \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
 
   371   and a39: "\<And>string tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk>
 
   371   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>
 
   372     \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)"
 
   372     \<Longrightarrow> P9 b (K string tvars cvars vars)"
 
   373   and a40: "\<And>b. P10 b VTNil"
 
   373   and a40: "\<And>b. P10 b VsNil"
 
   374   and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)"
 
   374   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)"
 
   375   and a42: "\<And>b. P11 b TVTKNil"
 
   375   and a42: "\<And>b. P11 b TvsNil"
 
   376   and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk>
 
   376   and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk>
 
   377     \<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)"
 
   377     \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"
 
   378   and a44: "\<And>b. P12 b TVCKNil"
 
   378   and a44: "\<And>b. P12 b CvsNil"
 
   379   and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk>
 
   379   and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>
 
   380     \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)"
 
   380     \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"
 
   381   shows "P1 (a :: 'a :: pt) tkind \<and>
 
   381   shows "P1 (a :: 'a :: pt) tkind \<and>
 
   382          P2 (b :: 'b :: pt) ckind \<and>
 
   382          P2 (b :: 'b :: pt) ckind \<and>
 
   383          P3 (c :: 'c :: {pt,fs}) ty \<and>
 
   383          P3 (c :: 'c :: {pt,fs}) ty \<and>
 
   384          P4 (d :: 'd :: pt) ty_lst \<and>
 
   384          P4 (d :: 'd :: pt) ty_lst \<and>
 
   385          P5 (e :: 'e :: {pt,fs}) co \<and>
 
   385          P5 (e :: 'e :: {pt,fs}) co \<and>
 
   386          P6 (f :: 'f :: pt) co_lst \<and>
 
   386          P6 (f :: 'f :: pt) co_lst \<and>
 
   387          P7 (g :: 'g :: {pt,fs}) trm \<and>
 
   387          P7 (g :: 'g :: {pt,fs}) trm \<and>
 
   388          P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
 
   388          P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
 
   389          P9 (i :: 'i :: pt) pat \<and>
 
   389          P9 (i :: 'i :: pt) pat \<and>
 
   390          P10 (j :: 'j :: pt) vt_lst \<and>
 
   390          P10 (j :: 'j :: pt) vars \<and>
 
   391          P11 (k :: 'k :: pt) tvtk_lst \<and>
 
   391          P11 (k :: 'k :: pt) tvars \<and>
 
   392          P12 (l :: 'l :: pt) tvck_lst"
 
   392          P12 (l :: 'l :: pt) cvars"
 
   393 proof -
 
   393 proof -
 
   394   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_vt q (p \<bullet> vt_lst)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvtk q (p \<bullet> tvtk_lst)))" and a4:"(\<forall>p q l. P12 l (permute_bv_tvck q (p \<bullet> tvck_lst)))"
 
   394   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)))"
 
   395     apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts)
 
   395     apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
 
   396     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
 
   396     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
 
   397     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
 
   397     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
 
   398 
   398 
   399 (* GOAL1 *)
 
   399 (* GOAL1 *)
 
   400     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
 
   400     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
 
   661     apply (simp add: supp_abs)
 
   661     apply (simp add: supp_abs)
 
   662     apply (simp add: finite_supp)
 
   662     apply (simp add: finite_supp)
 
   663     apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
 
   663     apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
 
   664     done
 
   664     done
 
   665   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+)
 
   665   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+)
 
   666   moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+)
 
   666   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+)
 
   667   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 
   667   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 
   668 qed
 
   668 qed
 
   669 
   669 
   670 end
 
   670 end
 
   671 
   671
nominal2