src/HOL/Nominal/Examples/Pattern.thy
author wenzelm
Mon Aug 31 21:01:21 2015 +0200 (2015-08-31)
changeset 61069 aefe89038dd2
parent 60580 7e741e22d7fc
child 61166 5976fe402824
permissions -rw-r--r--
prefer symbols;
wenzelm@58889
     1
section {* Simply-typed lambda-calculus with let and tuple patterns *}
berghofe@33189
     2
berghofe@33189
     3
theory Pattern
haftmann@44687
     4
imports "../Nominal"
berghofe@33189
     5
begin
berghofe@33189
     6
berghofe@33189
     7
no_syntax
wenzelm@61069
     8
  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
berghofe@33189
     9
berghofe@33189
    10
atom_decl name
berghofe@33189
    11
berghofe@33189
    12
nominal_datatype ty =
berghofe@33189
    13
    Atom nat
berghofe@33189
    14
  | Arrow ty ty  (infixr "\<rightarrow>" 200)
berghofe@33189
    15
  | TupleT ty ty  (infixr "\<otimes>" 210)
berghofe@33189
    16
berghofe@33189
    17
lemma fresh_type [simp]: "(a::name) \<sharp> (T::ty)"
berghofe@33189
    18
  by (induct T rule: ty.induct) (simp_all add: fresh_nat)
berghofe@33189
    19
berghofe@33189
    20
lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)"
berghofe@33189
    21
  by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat)
berghofe@33189
    22
berghofe@33189
    23
lemma perm_type: "(pi::name prm) \<bullet> (T::ty) = T"
berghofe@33189
    24
  by (induct T rule: ty.induct) (simp_all add: perm_nat_def)
berghofe@33189
    25
berghofe@33189
    26
nominal_datatype trm =
berghofe@33189
    27
    Var name
berghofe@33189
    28
  | Tuple trm trm  ("(1'\<langle>_,/ _'\<rangle>)")
berghofe@33189
    29
  | Abs ty "\<guillemotleft>name\<guillemotright>trm"
berghofe@33189
    30
  | App trm trm  (infixl "\<cdot>" 200)
berghofe@33189
    31
  | Let ty trm btrm
berghofe@33189
    32
and btrm =
berghofe@33189
    33
    Base trm
berghofe@33189
    34
  | Bind ty "\<guillemotleft>name\<guillemotright>btrm"
berghofe@33189
    35
berghofe@33189
    36
abbreviation
berghofe@33189
    37
  Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"  ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 
berghofe@33189
    38
where
berghofe@33189
    39
  "\<lambda>x:T. t \<equiv> Abs T x t"
berghofe@33189
    40
blanchet@58310
    41
datatype pat =
berghofe@33189
    42
    PVar name ty
berghofe@33189
    43
  | PTuple pat pat  ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
berghofe@33189
    44
berghofe@33189
    45
(* FIXME: The following should be done automatically by the nominal package *)
berghofe@33189
    46
overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked)
berghofe@33189
    47
begin
berghofe@33189
    48
berghofe@33189
    49
primrec pat_perm
berghofe@33189
    50
where
berghofe@33189
    51
  "pat_perm pi (PVar x ty) = PVar (pi \<bullet> x) (pi \<bullet> ty)"
berghofe@33189
    52
| "pat_perm pi \<langle>\<langle>p, q\<rangle>\<rangle> = \<langle>\<langle>pat_perm pi p, pat_perm pi q\<rangle>\<rangle>"
berghofe@33189
    53
berghofe@33189
    54
end
berghofe@33189
    55
berghofe@33189
    56
declare pat_perm.simps [eqvt]
berghofe@33189
    57
berghofe@33189
    58
lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x"
berghofe@33189
    59
  by (simp add: supp_def perm_fresh_fresh)
berghofe@33189
    60
berghofe@33189
    61
lemma supp_PTuple [simp]: "((supp \<langle>\<langle>p, q\<rangle>\<rangle>)::name set) = supp p \<union> supp q"
berghofe@33189
    62
  by (simp add: supp_def Collect_disj_eq del: disj_not1)
berghofe@33189
    63
berghofe@33189
    64
instance pat :: pt_name
wenzelm@60580
    65
proof (default, goals)
wenzelm@60580
    66
  case (1 x)
berghofe@33189
    67
  show ?case by (induct x) simp_all
berghofe@33189
    68
next
wenzelm@60580
    69
  case (2 _ _ x)
berghofe@33189
    70
  show ?case by (induct x) (simp_all add: pt_name2)
berghofe@33189
    71
next
wenzelm@60580
    72
  case (3 _ _ x)
berghofe@33189
    73
  then show ?case by (induct x) (simp_all add: pt_name3)
berghofe@33189
    74
qed
berghofe@33189
    75
berghofe@33189
    76
instance pat :: fs_name
wenzelm@60580
    77
proof (default, goals)
wenzelm@60580
    78
  case (1 x)
berghofe@33189
    79
  show ?case by (induct x) (simp_all add: fin_supp)
berghofe@33189
    80
qed
berghofe@33189
    81
berghofe@33189
    82
(* the following function cannot be defined using nominal_primrec, *)
berghofe@33189
    83
(* since variable parameters are currently not allowed.            *)
berghofe@33189
    84
primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" ("(3\<lambda>[_]./ _)" [0, 10] 10)
berghofe@33189
    85
where
berghofe@33189
    86
  "(\<lambda>[PVar x T]. t) = Bind T x t"
berghofe@33189
    87
| "(\<lambda>[\<langle>\<langle>p, q\<rangle>\<rangle>]. t) = (\<lambda>[p]. \<lambda>[q]. t)"
berghofe@33189
    88
berghofe@33189
    89
lemma abs_pat_eqvt [eqvt]:
berghofe@33189
    90
  "(pi :: name prm) \<bullet> (\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. (pi \<bullet> t))"
berghofe@33189
    91
  by (induct p arbitrary: t) simp_all
berghofe@33189
    92
berghofe@33189
    93
lemma abs_pat_fresh [simp]:
berghofe@33189
    94
  "(x::name) \<sharp> (\<lambda>[p]. t) = (x \<in> supp p \<or> x \<sharp> t)"
berghofe@33189
    95
  by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm)
berghofe@33189
    96
berghofe@33189
    97
lemma abs_pat_alpha:
berghofe@33189
    98
  assumes fresh: "((pi::name prm) \<bullet> supp p::name set) \<sharp>* t"
berghofe@33189
    99
  and pi: "set pi \<subseteq> supp p \<times> pi \<bullet> supp p"
berghofe@33189
   100
  shows "(\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. pi \<bullet> t)"
berghofe@33189
   101
proof -
berghofe@33189
   102
  note pt_name_inst at_name_inst pi
berghofe@33189
   103
  moreover have "(supp p::name set) \<sharp>* (\<lambda>[p]. t)"
berghofe@33189
   104
    by (simp add: fresh_star_def)
berghofe@33189
   105
  moreover from fresh
berghofe@33189
   106
  have "(pi \<bullet> supp p::name set) \<sharp>* (\<lambda>[p]. t)"
berghofe@33189
   107
    by (simp add: fresh_star_def)
berghofe@33189
   108
  ultimately have "pi \<bullet> (\<lambda>[p]. t) = (\<lambda>[p]. t)"
berghofe@33189
   109
    by (rule pt_freshs_freshs)
berghofe@33189
   110
  then show ?thesis by (simp add: eqvts)
berghofe@33189
   111
qed
berghofe@33189
   112
berghofe@33189
   113
primrec pat_vars :: "pat \<Rightarrow> name list"
berghofe@33189
   114
where
berghofe@33189
   115
  "pat_vars (PVar x T) = [x]"
berghofe@33189
   116
| "pat_vars \<langle>\<langle>p, q\<rangle>\<rangle> = pat_vars q @ pat_vars p"
berghofe@33189
   117
berghofe@33189
   118
lemma pat_vars_eqvt [eqvt]:
berghofe@33189
   119
  "(pi :: name prm) \<bullet> (pat_vars p) = pat_vars (pi \<bullet> p)"
berghofe@33189
   120
  by (induct p rule: pat.induct) (simp_all add: eqvts)
berghofe@33189
   121
berghofe@33189
   122
lemma set_pat_vars_supp: "set (pat_vars p) = supp p"
berghofe@33189
   123
  by (induct p) (auto simp add: supp_atm)
berghofe@33189
   124
berghofe@33189
   125
lemma distinct_eqvt [eqvt]:
berghofe@33189
   126
  "(pi :: name prm) \<bullet> (distinct (xs::name list)) = distinct (pi \<bullet> xs)"
berghofe@33189
   127
  by (induct xs) (simp_all add: eqvts)
berghofe@33189
   128
berghofe@33189
   129
primrec pat_type :: "pat \<Rightarrow> ty"
berghofe@33189
   130
where
berghofe@33189
   131
  "pat_type (PVar x T) = T"
berghofe@33189
   132
| "pat_type \<langle>\<langle>p, q\<rangle>\<rangle> = pat_type p \<otimes> pat_type q"
berghofe@33189
   133
berghofe@33189
   134
lemma pat_type_eqvt [eqvt]:
berghofe@33189
   135
  "(pi :: name prm) \<bullet> (pat_type p) = pat_type (pi \<bullet> p)"
berghofe@33189
   136
  by (induct p) simp_all
berghofe@33189
   137
berghofe@33189
   138
lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p"
berghofe@33189
   139
  by (induct p) (simp_all add: perm_type)
berghofe@33189
   140
wenzelm@41798
   141
type_synonym ctx = "(name \<times> ty) list"
berghofe@33189
   142
berghofe@33189
   143
inductive
berghofe@33189
   144
  ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool"  ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60)
berghofe@33189
   145
where
berghofe@33189
   146
  PVar: "\<turnstile> PVar x T : T \<Rightarrow> [(x, T)]"
wenzelm@53015
   147
| PTuple: "\<turnstile> p : T \<Rightarrow> \<Delta>\<^sub>1 \<Longrightarrow> \<turnstile> q : U \<Rightarrow> \<Delta>\<^sub>2 \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> : T \<otimes> U \<Rightarrow> \<Delta>\<^sub>2 @ \<Delta>\<^sub>1"
berghofe@33189
   148
berghofe@33189
   149
lemma pat_vars_ptyping:
berghofe@33189
   150
  assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
berghofe@33189
   151
  shows "pat_vars p = map fst \<Delta>" using assms
berghofe@33189
   152
  by induct simp_all
berghofe@33189
   153
berghofe@33189
   154
inductive
berghofe@33189
   155
  valid :: "ctx \<Rightarrow> bool"
berghofe@33189
   156
where
berghofe@33189
   157
  Nil [intro!]: "valid []"
berghofe@33189
   158
| Cons [intro!]: "valid \<Gamma> \<Longrightarrow> x \<sharp> \<Gamma> \<Longrightarrow> valid ((x, T) # \<Gamma>)"
berghofe@33189
   159
berghofe@33189
   160
inductive_cases validE[elim!]: "valid ((x, T) # \<Gamma>)"
berghofe@33189
   161
berghofe@33189
   162
lemma fresh_ctxt_set_eq: "((x::name) \<sharp> (\<Gamma>::ctx)) = (x \<notin> fst ` set \<Gamma>)"
berghofe@33189
   163
  by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm)
berghofe@33189
   164
berghofe@33189
   165
lemma valid_distinct: "valid \<Gamma> = distinct (map fst \<Gamma>)"
berghofe@33189
   166
  by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric])
berghofe@33189
   167
berghofe@33189
   168
abbreviation
berghofe@33189
   169
  "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _") 
berghofe@33189
   170
where
wenzelm@53015
   171
  "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^sub>1 \<longrightarrow> x \<in> set \<Gamma>\<^sub>2"
berghofe@33189
   172
berghofe@33189
   173
abbreviation
berghofe@33189
   174
  Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"  ("(LET (_ =/ _)/ IN (_))" 10)
berghofe@33189
   175
where
berghofe@33189
   176
  "LET p = t IN u \<equiv> Let (pat_type p) t (\<lambda>[p]. Base u)"
berghofe@33189
   177
berghofe@33189
   178
inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60)
berghofe@33189
   179
where
berghofe@33189
   180
  Var [intro]: "valid \<Gamma> \<Longrightarrow> (x, T) \<in> set \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
berghofe@33189
   181
| Tuple [intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> u : U \<Longrightarrow> \<Gamma> \<turnstile> \<langle>t, u\<rangle> : T \<otimes> U"
berghofe@33189
   182
| Abs [intro]: "(x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T. t) : T \<rightarrow> U"
berghofe@33189
   183
| App [intro]: "\<Gamma> \<turnstile> t : T \<rightarrow> U \<Longrightarrow> \<Gamma> \<turnstile> u : T \<Longrightarrow> \<Gamma> \<turnstile> t \<cdot> u : U"
berghofe@33189
   184
| Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow>
berghofe@33189
   185
    \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow>
berghofe@33189
   186
    \<Gamma> \<turnstile> (LET p = t IN u) : U"
berghofe@33189
   187
berghofe@33189
   188
equivariance ptyping
berghofe@33189
   189
berghofe@33189
   190
equivariance valid
berghofe@33189
   191
berghofe@33189
   192
equivariance typing
berghofe@33189
   193
berghofe@33189
   194
lemma valid_typing:
berghofe@33189
   195
  assumes "\<Gamma> \<turnstile> t : T"
berghofe@33189
   196
  shows "valid \<Gamma>" using assms
berghofe@33189
   197
  by induct auto
berghofe@33189
   198
berghofe@33189
   199
lemma pat_var:
berghofe@33189
   200
  assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
berghofe@33189
   201
  shows "(supp p::name set) = supp \<Delta>" using assms
berghofe@33189
   202
  by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append)
berghofe@33189
   203
berghofe@33189
   204
lemma valid_app_fresh:
berghofe@33189
   205
  assumes "valid (\<Delta> @ \<Gamma>)" and "(x::name) \<in> supp \<Delta>"
berghofe@33189
   206
  shows "x \<sharp> \<Gamma>" using assms
berghofe@33189
   207
  by (induct \<Delta>)
berghofe@33189
   208
    (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append)
berghofe@33189
   209
berghofe@33189
   210
lemma pat_freshs:
berghofe@33189
   211
  assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
berghofe@33189
   212
  shows "(supp p::name set) \<sharp>* c = (supp \<Delta>::name set) \<sharp>* c" using assms
berghofe@33189
   213
  by (auto simp add: fresh_star_def pat_var)
berghofe@33189
   214
berghofe@33189
   215
lemma valid_app_mono:
wenzelm@53015
   216
  assumes "valid (\<Delta> @ \<Gamma>\<^sub>1)" and "(supp \<Delta>::name set) \<sharp>* \<Gamma>\<^sub>2" and "valid \<Gamma>\<^sub>2" and "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2"
wenzelm@53015
   217
  shows "valid (\<Delta> @ \<Gamma>\<^sub>2)" using assms
berghofe@33189
   218
  by (induct \<Delta>)
berghofe@33189
   219
    (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod
berghofe@33189
   220
       fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim)
berghofe@33189
   221
berghofe@33189
   222
nominal_inductive2 typing
berghofe@33189
   223
avoids
berghofe@33189
   224
  Abs: "{x}"
berghofe@33189
   225
| Let: "(supp p)::name set"
berghofe@33189
   226
  by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var
berghofe@33189
   227
    dest!: valid_typing valid_app_fresh)
berghofe@33189
   228
berghofe@33189
   229
lemma better_T_Let [intro]:
berghofe@33189
   230
  assumes t: "\<Gamma> \<turnstile> t : T" and p: "\<turnstile> p : T \<Rightarrow> \<Delta>" and u: "\<Delta> @ \<Gamma> \<turnstile> u : U"
berghofe@33189
   231
  shows "\<Gamma> \<turnstile> (LET p = t IN u) : U"
berghofe@33189
   232
proof -
berghofe@33189
   233
  obtain pi::"name prm" where pi: "(pi \<bullet> (supp p::name set)) \<sharp>* (t, Base u, \<Gamma>)"
berghofe@33189
   234
    and pi': "set pi \<subseteq> supp p \<times> (pi \<bullet> supp p)"
berghofe@33189
   235
    by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp])
berghofe@33189
   236
  from p u have p_fresh: "(supp p::name set) \<sharp>* \<Gamma>"
berghofe@33189
   237
    by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh)
berghofe@33189
   238
  from pi have p_fresh': "(pi \<bullet> (supp p::name set)) \<sharp>* \<Gamma>"
berghofe@33189
   239
    by (simp add: fresh_star_prod_elim)
berghofe@33189
   240
  from pi have p_fresh'': "(pi \<bullet> (supp p::name set)) \<sharp>* Base u"
berghofe@33189
   241
    by (simp add: fresh_star_prod_elim)
berghofe@33189
   242
  from pi have "(supp (pi \<bullet> p)::name set) \<sharp>* t"
berghofe@33189
   243
    by (simp add: fresh_star_prod_elim eqvts)
berghofe@33189
   244
  moreover note t
berghofe@33189
   245
  moreover from p have "pi \<bullet> (\<turnstile> p : T \<Rightarrow> \<Delta>)" by (rule perm_boolI)
berghofe@33189
   246
  then have "\<turnstile> (pi \<bullet> p) : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: eqvts perm_type)
berghofe@33189
   247
  moreover from u have "pi \<bullet> (\<Delta> @ \<Gamma> \<turnstile> u : U)" by (rule perm_boolI)
berghofe@33189
   248
  with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh']
berghofe@33189
   249
  have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> (pi \<bullet> u) : U" by (simp add: eqvts perm_type)
berghofe@33189
   250
  ultimately have "\<Gamma> \<turnstile> (LET (pi \<bullet> p) = t IN (pi \<bullet> u)) : U"
berghofe@33189
   251
    by (rule Let)
berghofe@33189
   252
  then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq)
berghofe@33189
   253
qed
berghofe@33189
   254
berghofe@33189
   255
lemma weakening: 
wenzelm@53015
   256
  assumes "\<Gamma>\<^sub>1 \<turnstile> t : T" and "valid \<Gamma>\<^sub>2" and "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2"
wenzelm@53015
   257
  shows "\<Gamma>\<^sub>2 \<turnstile> t : T" using assms
wenzelm@53015
   258
  apply (nominal_induct \<Gamma>\<^sub>1 t T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
berghofe@33189
   259
  apply auto
wenzelm@53015
   260
  apply (drule_tac x="(x, T) # \<Gamma>\<^sub>2" in meta_spec)
berghofe@33189
   261
  apply (auto intro: valid_typing)
wenzelm@53015
   262
  apply (drule_tac x="\<Gamma>\<^sub>2" in meta_spec)
wenzelm@53015
   263
  apply (drule_tac x="\<Delta> @ \<Gamma>\<^sub>2" in meta_spec)
berghofe@33189
   264
  apply (auto intro: valid_typing)
berghofe@33189
   265
  apply (rule typing.Let)
berghofe@33189
   266
  apply assumption+
berghofe@33189
   267
  apply (drule meta_mp)
berghofe@33189
   268
  apply (rule valid_app_mono)
berghofe@33189
   269
  apply (rule valid_typing)
berghofe@33189
   270
  apply assumption
berghofe@33189
   271
  apply (auto simp add: pat_freshs)
berghofe@33189
   272
  done
berghofe@33189
   273
berghofe@33189
   274
inductive
berghofe@33189
   275
  match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool"  ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50)
berghofe@33189
   276
where
berghofe@33189
   277
  PVar: "\<turnstile> PVar x T \<rhd> t \<Rightarrow> [(x, t)]"
berghofe@33189
   278
| PProd: "\<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> \<turnstile> q \<rhd> u \<Rightarrow> \<theta>' \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> \<langle>t, u\<rangle> \<Rightarrow> \<theta> @ \<theta>'"
berghofe@33189
   279
berghofe@33189
   280
fun
berghofe@33189
   281
  lookup :: "(name \<times> trm) list \<Rightarrow> name \<Rightarrow> trm"   
berghofe@33189
   282
where
berghofe@33189
   283
  "lookup [] x = Var x"
berghofe@33189
   284
| "lookup ((y, e) # \<theta>) x = (if x = y then e else lookup \<theta> x)"
berghofe@33189
   285
berghofe@33189
   286
lemma lookup_eqvt[eqvt]:
berghofe@33189
   287
  fixes pi :: "name prm"
berghofe@33189
   288
  and   \<theta> :: "(name \<times> trm) list"
berghofe@33189
   289
  and   X :: "name"
berghofe@33189
   290
  shows "pi \<bullet> (lookup \<theta> X) = lookup (pi \<bullet> \<theta>) (pi \<bullet> X)"
berghofe@33189
   291
  by (induct \<theta>) (auto simp add: eqvts)
berghofe@33189
   292
 
berghofe@33189
   293
nominal_primrec
berghofe@33189
   294
  psubst :: "(name \<times> trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_\<lparr>_\<rparr>" [95,0] 210)
berghofe@33189
   295
  and psubstb :: "(name \<times> trm) list \<Rightarrow> btrm \<Rightarrow> btrm"  ("_\<lparr>_\<rparr>\<^sub>b" [95,0] 210)
berghofe@33189
   296
where
berghofe@33189
   297
  "\<theta>\<lparr>Var x\<rparr> = (lookup \<theta> x)"
berghofe@33189
   298
| "\<theta>\<lparr>t \<cdot> u\<rparr> = \<theta>\<lparr>t\<rparr> \<cdot> \<theta>\<lparr>u\<rparr>"
berghofe@33189
   299
| "\<theta>\<lparr>\<langle>t, u\<rangle>\<rparr> = \<langle>\<theta>\<lparr>t\<rparr>, \<theta>\<lparr>u\<rparr>\<rangle>"
berghofe@33189
   300
| "\<theta>\<lparr>Let T t u\<rparr> = Let T (\<theta>\<lparr>t\<rparr>) (\<theta>\<lparr>u\<rparr>\<^sub>b)"
berghofe@33189
   301
| "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>x:T. t\<rparr> = (\<lambda>x:T. \<theta>\<lparr>t\<rparr>)"
berghofe@33189
   302
| "\<theta>\<lparr>Base t\<rparr>\<^sub>b = Base (\<theta>\<lparr>t\<rparr>)"
berghofe@33189
   303
| "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>Bind T x t\<rparr>\<^sub>b = Bind T x (\<theta>\<lparr>t\<rparr>\<^sub>b)"
berghofe@33189
   304
  apply finite_guess+
berghofe@33189
   305
  apply (simp add: abs_fresh | fresh_guess)+
berghofe@33189
   306
  done
berghofe@33189
   307
berghofe@33189
   308
lemma lookup_fresh:
berghofe@33189
   309
  "x = y \<longrightarrow> x \<in> set (map fst \<theta>) \<Longrightarrow> \<forall>(y, t)\<in>set \<theta>. x \<sharp> t \<Longrightarrow> x \<sharp> lookup \<theta> y"
berghofe@33189
   310
  apply (induct \<theta>)
berghofe@33189
   311
  apply (simp_all add: split_paired_all fresh_atm)
berghofe@33189
   312
  apply (case_tac "x = y")
berghofe@33189
   313
  apply (auto simp add: fresh_atm)
berghofe@33189
   314
  done
berghofe@33189
   315
berghofe@33189
   316
lemma psubst_fresh:
berghofe@33189
   317
  assumes "x \<in> set (map fst \<theta>)" and "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t"
berghofe@33189
   318
  shows "x \<sharp> \<theta>\<lparr>t\<rparr>" and "x \<sharp> \<theta>\<lparr>t'\<rparr>\<^sub>b" using assms
berghofe@33189
   319
  apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
berghofe@33189
   320
  apply simp
berghofe@33189
   321
  apply (rule lookup_fresh)
berghofe@33189
   322
  apply (rule impI)
berghofe@33189
   323
  apply (simp_all add: abs_fresh)
berghofe@33189
   324
  done
berghofe@33189
   325
berghofe@33189
   326
lemma psubst_eqvt[eqvt]:
berghofe@33189
   327
  fixes pi :: "name prm" 
berghofe@33189
   328
  shows "pi \<bullet> (\<theta>\<lparr>t\<rparr>) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t\<rparr>"
berghofe@33189
   329
  and "pi \<bullet> (\<theta>\<lparr>t'\<rparr>\<^sub>b) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t'\<rparr>\<^sub>b"
berghofe@33189
   330
  by (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
berghofe@33189
   331
    (simp_all add: eqvts fresh_bij)
berghofe@33189
   332
berghofe@33189
   333
abbreviation 
berghofe@33189
   334
  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_\<mapsto>_]" [100,0,0] 100)
berghofe@33189
   335
where 
berghofe@33189
   336
  "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>"
berghofe@33189
   337
berghofe@33189
   338
abbreviation 
berghofe@33189
   339
  substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" ("_[_\<mapsto>_]\<^sub>b" [100,0,0] 100)
berghofe@33189
   340
where 
berghofe@33189
   341
  "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b"
berghofe@33189
   342
berghofe@33189
   343
lemma lookup_forget:
berghofe@33189
   344
  "(supp (map fst \<theta>)::name set) \<sharp>* x \<Longrightarrow> lookup \<theta> x = Var x"
berghofe@33189
   345
  by (induct \<theta>) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm)
berghofe@33189
   346
berghofe@33189
   347
lemma supp_fst: "(x::name) \<in> supp (map fst (\<theta>::(name \<times> trm) list)) \<Longrightarrow> x \<in> supp \<theta>"
berghofe@33189
   348
  by (induct \<theta>) (auto simp add: supp_list_nil supp_list_cons supp_prod)
berghofe@33189
   349
berghofe@33189
   350
lemma psubst_forget:
berghofe@33189
   351
  "(supp (map fst \<theta>)::name set) \<sharp>* t \<Longrightarrow> \<theta>\<lparr>t\<rparr> = t"
berghofe@33189
   352
  "(supp (map fst \<theta>)::name set) \<sharp>* t' \<Longrightarrow> \<theta>\<lparr>t'\<rparr>\<^sub>b = t'"
berghofe@33189
   353
  apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
berghofe@33189
   354
  apply (auto simp add: fresh_star_def lookup_forget abs_fresh)
berghofe@33189
   355
  apply (drule_tac x=\<theta> in meta_spec)
berghofe@33189
   356
  apply (drule meta_mp)
berghofe@33189
   357
  apply (rule ballI)
berghofe@33189
   358
  apply (drule_tac x=x in bspec)
berghofe@33189
   359
  apply assumption
berghofe@33189
   360
  apply (drule supp_fst)
berghofe@33189
   361
  apply (auto simp add: fresh_def)
berghofe@33189
   362
  apply (drule_tac x=\<theta> in meta_spec)
berghofe@33189
   363
  apply (drule meta_mp)
berghofe@33189
   364
  apply (rule ballI)
berghofe@33189
   365
  apply (drule_tac x=x in bspec)
berghofe@33189
   366
  apply assumption
berghofe@33189
   367
  apply (drule supp_fst)
berghofe@33189
   368
  apply (auto simp add: fresh_def)
berghofe@33189
   369
  done
berghofe@33189
   370
berghofe@33189
   371
lemma psubst_nil: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'"
berghofe@33189
   372
  by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)
berghofe@33189
   373
berghofe@33189
   374
lemma psubst_cons:
berghofe@33189
   375
  assumes "(supp (map fst \<theta>)::name set) \<sharp>* u"
berghofe@33189
   376
  shows "((x, u) # \<theta>)\<lparr>t\<rparr> = \<theta>\<lparr>t[x\<mapsto>u]\<rparr>" and "((x, u) # \<theta>)\<lparr>t'\<rparr>\<^sub>b = \<theta>\<lparr>t'[x\<mapsto>u]\<^sub>b\<rparr>\<^sub>b"
berghofe@33189
   377
  using assms
berghofe@33189
   378
  by (nominal_induct t and t' avoiding: x u \<theta> rule: trm_btrm.strong_inducts)
berghofe@33189
   379
    (simp_all add: fresh_list_nil fresh_list_cons psubst_forget)
berghofe@33189
   380
berghofe@33189
   381
lemma psubst_append:
wenzelm@53015
   382
  "(supp (map fst (\<theta>\<^sub>1 @ \<theta>\<^sub>2))::name set) \<sharp>* map snd (\<theta>\<^sub>1 @ \<theta>\<^sub>2) \<Longrightarrow> (\<theta>\<^sub>1 @ \<theta>\<^sub>2)\<lparr>t\<rparr> = \<theta>\<^sub>2\<lparr>\<theta>\<^sub>1\<lparr>t\<rparr>\<rparr>"
wenzelm@53015
   383
  by (induct \<theta>\<^sub>1 arbitrary: t)
berghofe@33189
   384
    (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def
berghofe@33189
   385
      fresh_list_cons fresh_list_append supp_list_append)
berghofe@33189
   386
berghofe@33189
   387
lemma abs_pat_psubst [simp]:
berghofe@33189
   388
  "(supp p::name set) \<sharp>* \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>[p]. t\<rparr>\<^sub>b = (\<lambda>[p]. \<theta>\<lparr>t\<rparr>\<^sub>b)"
berghofe@33189
   389
  by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm)
berghofe@33189
   390
berghofe@33189
   391
lemma valid_insert:
berghofe@33189
   392
  assumes "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
berghofe@33189
   393
  shows "valid (\<Delta> @ \<Gamma>)" using assms
berghofe@33189
   394
  by (induct \<Delta>)
berghofe@33189
   395
    (auto simp add: fresh_list_append fresh_list_cons)
berghofe@33189
   396
berghofe@33189
   397
lemma fresh_set: 
berghofe@33189
   398
  shows "y \<sharp> xs = (\<forall>x\<in>set xs. y \<sharp> x)"
berghofe@33189
   399
  by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)
berghofe@33189
   400
berghofe@33189
   401
lemma context_unique:
berghofe@33189
   402
  assumes "valid \<Gamma>"
berghofe@33189
   403
  and "(x, T) \<in> set \<Gamma>"
berghofe@33189
   404
  and "(x, U) \<in> set \<Gamma>"
berghofe@33189
   405
  shows "T = U" using assms
berghofe@33189
   406
  by induct (auto simp add: fresh_set fresh_prod fresh_atm)
berghofe@33189
   407
berghofe@33189
   408
lemma subst_type_aux:
berghofe@33189
   409
  assumes a: "\<Delta> @ [(x, U)] @ \<Gamma> \<turnstile> t : T"
berghofe@33189
   410
  and b: "\<Gamma> \<turnstile> u : U"
berghofe@33189
   411
  shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
berghofe@33189
   412
proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
berghofe@34915
   413
  case (Var y T x u \<Delta>)
berghofe@34915
   414
  from `valid (\<Delta> @ [(x, U)] @ \<Gamma>)`
berghofe@34915
   415
  have valid: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
berghofe@33189
   416
  show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
berghofe@33189
   417
  proof cases
berghofe@33189
   418
    assume eq: "x = y"
berghofe@34915
   419
    from Var eq have "T = U" by (auto intro: context_unique)
berghofe@34915
   420
    with Var eq valid show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" by (auto intro: weakening)
berghofe@33189
   421
  next
berghofe@33189
   422
    assume ineq: "x \<noteq> y"
berghofe@34915
   423
    from Var ineq have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" by simp
berghofe@34915
   424
    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq valid by auto
berghofe@33189
   425
  qed
berghofe@33189
   426
next
wenzelm@53015
   427
  case (Tuple t\<^sub>1 T\<^sub>1 t\<^sub>2 T\<^sub>2)
berghofe@34915
   428
  from refl `\<Gamma> \<turnstile> u : U`
wenzelm@53015
   429
  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T\<^sub>1" by (rule Tuple)
berghofe@34915
   430
  moreover from refl `\<Gamma> \<turnstile> u : U`
wenzelm@53015
   431
  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<mapsto>u] : T\<^sub>2" by (rule Tuple)
wenzelm@53015
   432
  ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^sub>1[x\<mapsto>u], t\<^sub>2[x\<mapsto>u]\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" ..
berghofe@33189
   433
  then show ?case by simp
berghofe@33189
   434
next
berghofe@34915
   435
  case (Let p t T \<Delta>' s S)
berghofe@34915
   436
  from refl `\<Gamma> \<turnstile> u : U`
berghofe@33189
   437
  have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
berghofe@33189
   438
  moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'`
berghofe@34915
   439
  moreover have "\<Delta>' @ (\<Delta> @ [(x, U)] @ \<Gamma>) = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
berghofe@34915
   440
  then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Let)
berghofe@33189
   441
  then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
berghofe@33189
   442
  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S"
berghofe@33189
   443
    by (rule better_T_Let)
berghofe@33189
   444
  moreover from Let have "(supp p::name set) \<sharp>* [(x, u)]"
berghofe@33189
   445
    by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
berghofe@33189
   446
  ultimately show ?case by simp
berghofe@33189
   447
next
berghofe@34915
   448
  case (Abs y T t S)
berghofe@34915
   449
  have "(y, T) # \<Delta> @ [(x, U)] @ \<Gamma> = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
berghofe@33189
   450
    by simp
berghofe@34915
   451
  then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Abs)
berghofe@33189
   452
  then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
berghofe@33189
   453
  then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S"
berghofe@33189
   454
    by (rule typing.Abs)
berghofe@33189
   455
  moreover from Abs have "y \<sharp> [(x, u)]"
berghofe@33189
   456
    by (simp add: fresh_list_nil fresh_list_cons)
berghofe@33189
   457
  ultimately show ?case by simp
berghofe@33189
   458
next
wenzelm@53015
   459
  case (App t\<^sub>1 T S t\<^sub>2)
berghofe@34915
   460
  from refl `\<Gamma> \<turnstile> u : U`
wenzelm@53015
   461
  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
berghofe@34915
   462
  moreover from refl `\<Gamma> \<turnstile> u : U`
wenzelm@53015
   463
  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<mapsto>u] : T" by (rule App)
wenzelm@53015
   464
  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^sub>1[x\<mapsto>u]) \<cdot> (t\<^sub>2[x\<mapsto>u]) : S"
berghofe@33189
   465
    by (rule typing.App)
berghofe@33189
   466
  then show ?case by simp
berghofe@33189
   467
qed
berghofe@33189
   468
berghofe@33189
   469
lemmas subst_type = subst_type_aux [of "[]", simplified]
berghofe@33189
   470
berghofe@33189
   471
lemma match_supp_fst:
berghofe@33189
   472
  assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map fst \<theta>)::name set) = supp p" using assms
berghofe@33189
   473
  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append)
berghofe@33189
   474
berghofe@33189
   475
lemma match_supp_snd:
berghofe@33189
   476
  assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map snd \<theta>)::name set) = supp u" using assms
berghofe@33189
   477
  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp)
berghofe@33189
   478
berghofe@33189
   479
lemma match_fresh: "\<turnstile> p \<rhd> u \<Rightarrow> \<theta> \<Longrightarrow> (supp p::name set) \<sharp>* u \<Longrightarrow>
berghofe@33189
   480
  (supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
berghofe@33189
   481
  by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd)
berghofe@33189
   482
berghofe@33189
   483
lemma match_type_aux:
berghofe@33189
   484
  assumes "\<turnstile> p : U \<Rightarrow> \<Delta>"
wenzelm@53015
   485
  and "\<Gamma>\<^sub>2 \<turnstile> u : U"
wenzelm@53015
   486
  and "\<Gamma>\<^sub>1 @ \<Delta> @ \<Gamma>\<^sub>2 \<turnstile> t : T"
berghofe@33189
   487
  and "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>"
berghofe@33189
   488
  and "(supp p::name set) \<sharp>* u"
wenzelm@53015
   489
  shows "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<lparr>t\<rparr> : T" using assms
wenzelm@53015
   490
proof (induct arbitrary: \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 t u T \<theta>)
berghofe@33189
   491
  case (PVar x U)
wenzelm@53015
   492
  from `\<Gamma>\<^sub>1 @ [(x, U)] @ \<Gamma>\<^sub>2 \<turnstile> t : T` `\<Gamma>\<^sub>2 \<turnstile> u : U`
wenzelm@53015
   493
  have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t[x\<mapsto>u] : T" by (rule subst_type_aux)
berghofe@33189
   494
  moreover from `\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>` have "\<theta> = [(x, u)]"
berghofe@33189
   495
    by cases simp_all
berghofe@33189
   496
  ultimately show ?case by simp
berghofe@33189
   497
next
wenzelm@53015
   498
  case (PTuple p S \<Delta>\<^sub>1 q U \<Delta>\<^sub>2)
wenzelm@53015
   499
  from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` obtain u\<^sub>1 u\<^sub>2 \<theta>\<^sub>1 \<theta>\<^sub>2
wenzelm@53015
   500
    where u: "u = \<langle>u\<^sub>1, u\<^sub>2\<rangle>" and \<theta>: "\<theta> = \<theta>\<^sub>1 @ \<theta>\<^sub>2"
wenzelm@53015
   501
    and p: "\<turnstile> p \<rhd> u\<^sub>1 \<Rightarrow> \<theta>\<^sub>1" and q: "\<turnstile> q \<rhd> u\<^sub>2 \<Rightarrow> \<theta>\<^sub>2"
berghofe@33189
   502
    by cases simp_all
wenzelm@53015
   503
  with PTuple have "\<Gamma>\<^sub>2 \<turnstile> \<langle>u\<^sub>1, u\<^sub>2\<rangle> : S \<otimes> U" by simp
wenzelm@53015
   504
  then obtain u\<^sub>1: "\<Gamma>\<^sub>2 \<turnstile> u\<^sub>1 : S" and u\<^sub>2: "\<Gamma>\<^sub>2 \<turnstile> u\<^sub>2 : U"
berghofe@33189
   505
    by cases (simp_all add: ty.inject trm.inject)
wenzelm@53015
   506
  note u\<^sub>1
wenzelm@53015
   507
  moreover from `\<Gamma>\<^sub>1 @ (\<Delta>\<^sub>2 @ \<Delta>\<^sub>1) @ \<Gamma>\<^sub>2 \<turnstile> t : T`
wenzelm@53015
   508
  have "(\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2) @ \<Delta>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t : T" by simp
berghofe@33189
   509
  moreover note p
berghofe@33189
   510
  moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u
wenzelm@53015
   511
  have "(supp p::name set) \<sharp>* u\<^sub>1" by (simp add: fresh_star_def)
wenzelm@53015
   512
  ultimately have \<theta>\<^sub>1: "(\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2) @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>1\<lparr>t\<rparr> : T"
berghofe@33189
   513
    by (rule PTuple)
wenzelm@53015
   514
  note u\<^sub>2
wenzelm@53015
   515
  moreover from \<theta>\<^sub>1
wenzelm@53015
   516
  have "\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2 @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>1\<lparr>t\<rparr> : T" by simp
berghofe@33189
   517
  moreover note q
berghofe@33189
   518
  moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u
wenzelm@53015
   519
  have "(supp q::name set) \<sharp>* u\<^sub>2" by (simp add: fresh_star_def)
wenzelm@53015
   520
  ultimately have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>2\<lparr>\<theta>\<^sub>1\<lparr>t\<rparr>\<rparr> : T"
berghofe@33189
   521
    by (rule PTuple)
berghofe@33189
   522
  moreover from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u`
berghofe@33189
   523
  have "(supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
berghofe@33189
   524
    by (rule match_fresh)
berghofe@33189
   525
  ultimately show ?case using \<theta> by (simp add: psubst_append)
berghofe@33189
   526
qed
berghofe@33189
   527
wenzelm@53015
   528
lemmas match_type = match_type_aux [where \<Gamma>\<^sub>1="[]", simplified]
berghofe@33189
   529
berghofe@33189
   530
inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
berghofe@33189
   531
where
berghofe@33189
   532
  TupleL: "t \<longmapsto> t' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t', u\<rangle>"
berghofe@33189
   533
| TupleR: "u \<longmapsto> u' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t, u'\<rangle>"
berghofe@33189
   534
| Abs: "t \<longmapsto> t' \<Longrightarrow> (\<lambda>x:T. t) \<longmapsto> (\<lambda>x:T. t')"
berghofe@33189
   535
| AppL: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
berghofe@33189
   536
| AppR: "u \<longmapsto> u' \<Longrightarrow> t \<cdot> u \<longmapsto> t \<cdot> u'"
berghofe@33189
   537
| Beta: "x \<sharp> u \<Longrightarrow> (\<lambda>x:T. t) \<cdot> u \<longmapsto> t[x\<mapsto>u]"
berghofe@33189
   538
| Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow> distinct (pat_vars p) \<Longrightarrow>
berghofe@33189
   539
    \<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> (LET p = t IN u) \<longmapsto> \<theta>\<lparr>u\<rparr>"
berghofe@33189
   540
berghofe@33189
   541
equivariance match
berghofe@33189
   542
berghofe@33189
   543
equivariance eval
berghofe@33189
   544
berghofe@33189
   545
lemma match_vars:
berghofe@33189
   546
  assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "x \<in> supp p"
berghofe@33189
   547
  shows "x \<in> set (map fst \<theta>)" using assms
berghofe@33189
   548
  by induct (auto simp add: supp_atm)
berghofe@33189
   549
berghofe@33189
   550
lemma match_fresh_mono:
berghofe@33189
   551
  assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "(x::name) \<sharp> t"
berghofe@33189
   552
  shows "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t" using assms
berghofe@33189
   553
  by induct auto
berghofe@33189
   554
berghofe@33189
   555
nominal_inductive2 eval
berghofe@33189
   556
avoids
berghofe@33189
   557
  Abs: "{x}"
berghofe@33189
   558
| Beta: "{x}"
berghofe@33189
   559
| Let: "(supp p)::name set"
berghofe@33189
   560
  apply (simp_all add: fresh_star_def abs_fresh fin_supp)
berghofe@33189
   561
  apply (rule psubst_fresh)
berghofe@33189
   562
  apply simp
berghofe@33189
   563
  apply simp
berghofe@33189
   564
  apply (rule ballI)
berghofe@33189
   565
  apply (rule psubst_fresh)
berghofe@33189
   566
  apply (rule match_vars)
berghofe@33189
   567
  apply assumption+
berghofe@33189
   568
  apply (rule match_fresh_mono)
berghofe@33189
   569
  apply auto
berghofe@33189
   570
  done
berghofe@33189
   571
berghofe@33189
   572
lemma typing_case_Abs:
berghofe@33189
   573
  assumes ty: "\<Gamma> \<turnstile> (\<lambda>x:T. t) : S"
berghofe@33189
   574
  and fresh: "x \<sharp> \<Gamma>"
berghofe@33189
   575
  and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P"
berghofe@33189
   576
  shows P using ty
berghofe@33189
   577
proof cases
berghofe@34990
   578
  case (Abs x' T' t' U)
berghofe@33189
   579
  obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')"
berghofe@33189
   580
    by (rule exists_fresh) (auto intro: fin_supp)
berghofe@33189
   581
  from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric]
berghofe@33189
   582
  have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
berghofe@33189
   583
  have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
berghofe@34990
   584
  from `(x', T') # \<Gamma> \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>"
berghofe@33189
   585
    by (auto dest: valid_typing)
berghofe@33189
   586
  have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact
berghofe@33189
   587
  also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')"
berghofe@33189
   588
    by (simp only: perm_fresh_fresh fresh_prod)
berghofe@33189
   589
  also have "\<dots> = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')"
berghofe@33189
   590
    by (simp add: swap_simps perm_fresh_fresh)
berghofe@33189
   591
  finally have "(\<lambda>x:T. t) = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')" .
berghofe@33189
   592
  then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t"
berghofe@33189
   593
    by (simp_all add: trm.inject alpha)
berghofe@33189
   594
  from Abs T have "S = T \<rightarrow> U" by simp
berghofe@34990
   595
  moreover from `(x', T') # \<Gamma> \<turnstile> t' : U`
berghofe@34990
   596
  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma> \<turnstile> t' : U)"
berghofe@33189
   597
    by (simp add: perm_bool)
berghofe@34990
   598
  with T t y x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
berghofe@33189
   599
    by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
berghofe@33189
   600
  ultimately show ?thesis by (rule R)
berghofe@33189
   601
qed simp_all
berghofe@33189
   602
berghofe@33189
   603
nominal_primrec ty_size :: "ty \<Rightarrow> nat"
berghofe@33189
   604
where
berghofe@33189
   605
  "ty_size (Atom n) = 0"
berghofe@33189
   606
| "ty_size (T \<rightarrow> U) = ty_size T + ty_size U + 1"
berghofe@33189
   607
| "ty_size (T \<otimes> U) = ty_size T + ty_size U + 1"
berghofe@33189
   608
  by (rule TrueI)+
berghofe@33189
   609
berghofe@33189
   610
lemma bind_tuple_ineq:
berghofe@33189
   611
  "ty_size (pat_type p) < ty_size U \<Longrightarrow> Bind U x t \<noteq> (\<lambda>[p]. u)"
berghofe@33189
   612
  by (induct p arbitrary: U x t u) (auto simp add: btrm.inject)
berghofe@33189
   613
berghofe@33189
   614
lemma valid_appD: assumes "valid (\<Gamma> @ \<Delta>)"
berghofe@33189
   615
  shows "valid \<Gamma>" "valid \<Delta>" using assms
berghofe@33189
   616
  by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
berghofe@33189
   617
    (auto simp add: Cons_eq_append_conv fresh_list_append)
berghofe@33189
   618
berghofe@33189
   619
lemma valid_app_freshs: assumes "valid (\<Gamma> @ \<Delta>)"
berghofe@33189
   620
  shows "(supp \<Gamma>::name set) \<sharp>* \<Delta>" "(supp \<Delta>::name set) \<sharp>* \<Gamma>" using assms
berghofe@33189
   621
  by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
berghofe@33189
   622
    (auto simp add: Cons_eq_append_conv fresh_star_def
berghofe@33189
   623
     fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
berghofe@33189
   624
     supp_prod fresh_prod supp_atm fresh_atm
haftmann@44687
   625
     dest: notE [OF iffD1 [OF fresh_def]])
berghofe@33189
   626
berghofe@33189
   627
lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A"
berghofe@33189
   628
  by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)
berghofe@33189
   629
berghofe@33189
   630
lemma perm_mem_right: "(rev (pi::name prm) \<bullet> (x::name)) \<in> A \<Longrightarrow> x \<in> (pi \<bullet> A)"
berghofe@33189
   631
  by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp)
berghofe@33189
   632
berghofe@33189
   633
lemma perm_cases:
berghofe@33189
   634
  assumes pi: "set pi \<subseteq> A \<times> A"
berghofe@33189
   635
  shows "((pi::name prm) \<bullet> B) \<subseteq> A \<union> B"
berghofe@33189
   636
proof
berghofe@33189
   637
  fix x assume "x \<in> pi \<bullet> B"
berghofe@33189
   638
  then show "x \<in> A \<union> B" using pi
berghofe@33189
   639
    apply (induct pi arbitrary: x B rule: rev_induct)
berghofe@33189
   640
    apply simp
berghofe@33189
   641
    apply (simp add: split_paired_all supp_eqvt)
berghofe@33189
   642
    apply (drule perm_mem_left)
berghofe@33189
   643
    apply (simp add: calc_atm split: split_if_asm)
berghofe@33189
   644
    apply (auto dest: perm_mem_right)
berghofe@33189
   645
    done
berghofe@33189
   646
qed
berghofe@33189
   647
berghofe@33189
   648
lemma abs_pat_alpha':
berghofe@33189
   649
  assumes eq: "(\<lambda>[p]. t) = (\<lambda>[q]. u)"
berghofe@33189
   650
  and ty: "pat_type p = pat_type q"
berghofe@33189
   651
  and pv: "distinct (pat_vars p)"
berghofe@33189
   652
  and qv: "distinct (pat_vars q)"
berghofe@33189
   653
  shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
berghofe@33189
   654
    set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
berghofe@33189
   655
  using assms
wenzelm@45129
   656
proof (induct p arbitrary: q t u)
berghofe@33189
   657
  case (PVar x T)
berghofe@33189
   658
  note PVar' = this
berghofe@33189
   659
  show ?case
berghofe@33189
   660
  proof (cases q)
berghofe@33189
   661
    case (PVar x' T')
berghofe@33189
   662
    with `(\<lambda>[PVar x T]. t) = (\<lambda>[q]. u)`
berghofe@33189
   663
    have "x = x' \<and> t = u \<or> x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
berghofe@33189
   664
      by (simp add: btrm.inject alpha)
berghofe@33189
   665
    then show ?thesis
berghofe@33189
   666
    proof
berghofe@33189
   667
      assume "x = x' \<and> t = u"
berghofe@33189
   668
      with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
wenzelm@33268
   669
        t = ([]::name prm) \<bullet> u \<and>
wenzelm@33268
   670
        set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
berghofe@33189
   671
          (supp (PVar x T) \<union> supp q)" by simp
berghofe@33189
   672
      then show ?thesis ..
berghofe@33189
   673
    next
berghofe@33189
   674
      assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
berghofe@33189
   675
      with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
wenzelm@33268
   676
        t = [(x, x')] \<bullet> u \<and>
wenzelm@33268
   677
        set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
berghofe@33189
   678
          (supp (PVar x T) \<union> supp q)"
wenzelm@33268
   679
        by (simp add: perm_swap swap_simps supp_atm perm_type)
berghofe@33189
   680
      then show ?thesis ..
berghofe@33189
   681
    qed
berghofe@33189
   682
  next
wenzelm@53015
   683
    case (PTuple p\<^sub>1 p\<^sub>2)
wenzelm@53015
   684
    with PVar have "ty_size (pat_type p\<^sub>1) < ty_size T" by simp
wenzelm@53015
   685
    then have "Bind T x t \<noteq> (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. u)"
berghofe@33189
   686
      by (rule bind_tuple_ineq)
berghofe@33189
   687
    moreover from PTuple PVar
wenzelm@53015
   688
    have "Bind T x t = (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. u)" by simp
berghofe@33189
   689
    ultimately show ?thesis ..
berghofe@33189
   690
  qed
berghofe@33189
   691
next
wenzelm@53015
   692
  case (PTuple p\<^sub>1 p\<^sub>2)
berghofe@33189
   693
  note PTuple' = this
berghofe@33189
   694
  show ?case
berghofe@33189
   695
  proof (cases q)
berghofe@33189
   696
    case (PVar x T)
wenzelm@53015
   697
    with PTuple have "ty_size (pat_type p\<^sub>1) < ty_size T" by auto
wenzelm@53015
   698
    then have "Bind T x u \<noteq> (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. t)"
berghofe@33189
   699
      by (rule bind_tuple_ineq)
berghofe@33189
   700
    moreover from PTuple PVar
wenzelm@53015
   701
    have "Bind T x u = (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. t)" by simp
berghofe@33189
   702
    ultimately show ?thesis ..
berghofe@33189
   703
  next
wenzelm@53015
   704
    case (PTuple p\<^sub>1' p\<^sub>2')
wenzelm@53015
   705
    with PTuple' have "(\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. t) = (\<lambda>[p\<^sub>1']. \<lambda>[p\<^sub>2']. u)" by simp
wenzelm@53015
   706
    moreover from PTuple PTuple' have "pat_type p\<^sub>1 = pat_type p\<^sub>1'"
berghofe@33189
   707
      by (simp add: ty.inject)
wenzelm@53015
   708
    moreover from PTuple' have "distinct (pat_vars p\<^sub>1)" by simp
wenzelm@53015
   709
    moreover from PTuple PTuple' have "distinct (pat_vars p\<^sub>1')" by simp
wenzelm@53015
   710
    ultimately have "\<exists>pi::name prm. p\<^sub>1 = pi \<bullet> p\<^sub>1' \<and>
wenzelm@53015
   711
      (\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u) \<and>
wenzelm@53015
   712
      set pi \<subseteq> (supp p\<^sub>1 \<union> supp p\<^sub>1') \<times> (supp p\<^sub>1 \<union> supp p\<^sub>1')"
berghofe@33189
   713
      by (rule PTuple')
berghofe@33189
   714
    then obtain pi::"name prm" where
wenzelm@53015
   715
      "p\<^sub>1 = pi \<bullet> p\<^sub>1'" "(\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u)" and
wenzelm@53015
   716
      pi: "set pi \<subseteq> (supp p\<^sub>1 \<union> supp p\<^sub>1') \<times> (supp p\<^sub>1 \<union> supp p\<^sub>1')" by auto
wenzelm@53015
   717
    from `(\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u)`
wenzelm@53015
   718
    have "(\<lambda>[p\<^sub>2]. t) = (\<lambda>[pi \<bullet> p\<^sub>2']. pi \<bullet> u)"
berghofe@33189
   719
      by (simp add: eqvts)
wenzelm@53015
   720
    moreover from PTuple PTuple' have "pat_type p\<^sub>2 = pat_type (pi \<bullet> p\<^sub>2')"
berghofe@33189
   721
      by (simp add: ty.inject pat_type_perm_eq)
wenzelm@53015
   722
    moreover from PTuple' have "distinct (pat_vars p\<^sub>2)" by simp
wenzelm@53015
   723
    moreover from PTuple PTuple' have "distinct (pat_vars (pi \<bullet> p\<^sub>2'))"
berghofe@33189
   724
      by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric])
wenzelm@53015
   725
    ultimately have "\<exists>pi'::name prm. p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2' \<and>
berghofe@33189
   726
      t = pi' \<bullet> pi \<bullet> u \<and>
wenzelm@53015
   727
      set pi' \<subseteq> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2'))"
berghofe@33189
   728
      by (rule PTuple')
berghofe@33189
   729
    then obtain pi'::"name prm" where
wenzelm@53015
   730
      "p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2'" "t = pi' \<bullet> pi \<bullet> u" and
wenzelm@53015
   731
      pi': "set pi' \<subseteq> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2')) \<times>
wenzelm@53015
   732
        (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2'))" by auto
wenzelm@53015
   733
    from PTuple PTuple' have "pi \<bullet> distinct (pat_vars \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>)" by simp
wenzelm@53015
   734
    then have "distinct (pat_vars \<langle>\<langle>pi \<bullet> p\<^sub>1', pi \<bullet> p\<^sub>2'\<rangle>\<rangle>)" by (simp only: eqvts)
wenzelm@53015
   735
    with `p\<^sub>1 = pi \<bullet> p\<^sub>1'` PTuple'
wenzelm@53015
   736
    have fresh: "(supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2') :: name set) \<sharp>* p\<^sub>1"
berghofe@33189
   737
      by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts)
wenzelm@53015
   738
    from `p\<^sub>1 = pi \<bullet> p\<^sub>1'` have "pi' \<bullet> (p\<^sub>1 = pi \<bullet> p\<^sub>1')" by (rule perm_boolI)
berghofe@33189
   739
    with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh]
wenzelm@53015
   740
    have "p\<^sub>1 = pi' \<bullet> pi \<bullet> p\<^sub>1'" by (simp add: eqvts)
wenzelm@53015
   741
    with `p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2'` have "\<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>"
berghofe@33189
   742
      by (simp add: pt_name2)
berghofe@33189
   743
    moreover
wenzelm@53015
   744
    have "((supp p\<^sub>2 \<union> (pi \<bullet> supp p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> (pi \<bullet> supp p\<^sub>2'))::(name \<times> name) set) \<subseteq>
wenzelm@53015
   745
      (supp p\<^sub>2 \<union> (supp p\<^sub>1 \<union> supp p\<^sub>1' \<union> supp p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> (supp p\<^sub>1 \<union> supp p\<^sub>1' \<union> supp p\<^sub>2'))"
berghofe@33189
   746
      by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+
berghofe@33189
   747
    with pi' have "set pi' \<subseteq> \<dots>" by (simp add: supp_eqvt [symmetric])
wenzelm@53015
   748
    with pi have "set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>) \<times>
wenzelm@53015
   749
      (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>)"
berghofe@33189
   750
      by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast
berghofe@33189
   751
    moreover note `t = pi' \<bullet> pi \<bullet> u`
wenzelm@53015
   752
    ultimately have "\<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> q \<and> t = (pi' @ pi) \<bullet> u \<and>
wenzelm@53015
   753
      set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp q) \<times>
wenzelm@53015
   754
        (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp q)" using PTuple
berghofe@33189
   755
      by (simp add: pt_name2)
berghofe@33189
   756
    then show ?thesis ..
berghofe@33189
   757
  qed
berghofe@33189
   758
qed
berghofe@33189
   759
berghofe@33189
   760
lemma typing_case_Let:
berghofe@33189
   761
  assumes ty: "\<Gamma> \<turnstile> (LET p = t IN u) : U"
berghofe@33189
   762
  and fresh: "(supp p::name set) \<sharp>* \<Gamma>"
berghofe@33189
   763
  and distinct: "distinct (pat_vars p)"
berghofe@33189
   764
  and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P"
berghofe@33189
   765
  shows P using ty
berghofe@33189
   766
proof cases
berghofe@34990
   767
  case (Let p' t' T \<Delta> u')
berghofe@33189
   768
  then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>"
berghofe@33189
   769
    by (auto intro: valid_typing valid_app_freshs)
berghofe@33189
   770
  with Let have "(supp p'::name set) \<sharp>* \<Gamma>"
berghofe@33189
   771
    by (simp add: pat_var)
berghofe@33189
   772
  with fresh have fresh': "(supp p \<union> supp p' :: name set) \<sharp>* \<Gamma>"
berghofe@33189
   773
    by (auto simp add: fresh_star_def)
berghofe@33189
   774
  from Let have "(\<lambda>[p]. Base u) = (\<lambda>[p']. Base u')"
berghofe@33189
   775
    by (simp add: trm.inject)
berghofe@33189
   776
  moreover from Let have "pat_type p = pat_type p'"
berghofe@33189
   777
    by (simp add: trm.inject)
berghofe@33189
   778
  moreover note distinct
berghofe@34990
   779
  moreover from `\<Delta> @ \<Gamma> \<turnstile> u' : U` have "valid (\<Delta> @ \<Gamma>)"
berghofe@33189
   780
    by (rule valid_typing)
berghofe@33189
   781
  then have "valid \<Delta>" by (rule valid_appD)
berghofe@33189
   782
  with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')"
berghofe@33189
   783
    by (simp add: valid_distinct pat_vars_ptyping)
berghofe@33189
   784
  ultimately have "\<exists>pi::name prm. p = pi \<bullet> p' \<and> Base u = pi \<bullet> Base u' \<and>
berghofe@33189
   785
    set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
berghofe@33189
   786
    by (rule abs_pat_alpha')
berghofe@33189
   787
  then obtain pi::"name prm" where pi: "p = pi \<bullet> p'" "u = pi \<bullet> u'"
berghofe@33189
   788
    and pi': "set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
berghofe@33189
   789
    by (auto simp add: btrm.inject)
berghofe@33189
   790
  from Let have "\<Gamma> \<turnstile> t : T" by (simp add: trm.inject)
berghofe@33189
   791
  moreover from `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "\<turnstile> (pi \<bullet> p') : (pi \<bullet> T) \<Rightarrow> (pi \<bullet> \<Delta>)"
berghofe@33189
   792
    by (simp add: ptyping.eqvt)
berghofe@33189
   793
  with pi have "\<turnstile> p : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: perm_type)
berghofe@33189
   794
  moreover from Let
berghofe@33189
   795
  have "(pi \<bullet> \<Delta>) @ (pi \<bullet> \<Gamma>) \<turnstile> (pi \<bullet> u') : (pi \<bullet> U)"
berghofe@33189
   796
    by (simp add: append_eqvt [symmetric] typing.eqvt)
berghofe@33189
   797
  with pi have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> u : U"
berghofe@33189
   798
    by (simp add: perm_type pt_freshs_freshs
berghofe@33189
   799
      [OF pt_name_inst at_name_inst pi' fresh' fresh'])
berghofe@33189
   800
  ultimately show ?thesis by (rule R)
berghofe@33189
   801
qed simp_all
berghofe@33189
   802
berghofe@33189
   803
lemma preservation:
berghofe@33189
   804
  assumes "t \<longmapsto> t'" and "\<Gamma> \<turnstile> t : T"
berghofe@33189
   805
  shows "\<Gamma> \<turnstile> t' : T" using assms
berghofe@33189
   806
proof (nominal_induct avoiding: \<Gamma> T rule: eval.strong_induct)
berghofe@33189
   807
  case (TupleL t t' u)
wenzelm@53015
   808
  from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^sub>1 T\<^sub>2
wenzelm@53015
   809
    where "T = T\<^sub>1 \<otimes> T\<^sub>2" "\<Gamma> \<turnstile> t : T\<^sub>1" "\<Gamma> \<turnstile> u : T\<^sub>2"
berghofe@33189
   810
    by cases (simp_all add: trm.inject)
wenzelm@53015
   811
  from `\<Gamma> \<turnstile> t : T\<^sub>1` have "\<Gamma> \<turnstile> t' : T\<^sub>1" by (rule TupleL)
wenzelm@53015
   812
  then have "\<Gamma> \<turnstile> \<langle>t', u\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" using `\<Gamma> \<turnstile> u : T\<^sub>2`
berghofe@33189
   813
    by (rule Tuple)
wenzelm@53015
   814
  with `T = T\<^sub>1 \<otimes> T\<^sub>2` show ?case by simp
berghofe@33189
   815
next
berghofe@33189
   816
  case (TupleR u u' t)
wenzelm@53015
   817
  from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^sub>1 T\<^sub>2
wenzelm@53015
   818
    where "T = T\<^sub>1 \<otimes> T\<^sub>2" "\<Gamma> \<turnstile> t : T\<^sub>1" "\<Gamma> \<turnstile> u : T\<^sub>2"
berghofe@33189
   819
    by cases (simp_all add: trm.inject)
wenzelm@53015
   820
  from `\<Gamma> \<turnstile> u : T\<^sub>2` have "\<Gamma> \<turnstile> u' : T\<^sub>2" by (rule TupleR)
wenzelm@53015
   821
  with `\<Gamma> \<turnstile> t : T\<^sub>1` have "\<Gamma> \<turnstile> \<langle>t, u'\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2"
berghofe@33189
   822
    by (rule Tuple)
wenzelm@53015
   823
  with `T = T\<^sub>1 \<otimes> T\<^sub>2` show ?case by simp
berghofe@33189
   824
next
berghofe@33189
   825
  case (Abs t t' x S)
berghofe@33189
   826
  from `\<Gamma> \<turnstile> (\<lambda>x:S. t) : T` `x \<sharp> \<Gamma>` obtain U where
berghofe@33189
   827
    T: "T = S \<rightarrow> U" and U: "(x, S) # \<Gamma> \<turnstile> t : U"
berghofe@33189
   828
    by (rule typing_case_Abs)
berghofe@33189
   829
  from U have "(x, S) # \<Gamma> \<turnstile> t' : U" by (rule Abs)
berghofe@33189
   830
  then have "\<Gamma> \<turnstile> (\<lambda>x:S. t') : S \<rightarrow> U"
berghofe@33189
   831
    by (rule typing.Abs)
berghofe@33189
   832
  with T show ?case by simp
berghofe@33189
   833
next
berghofe@33189
   834
  case (Beta x u S t)
berghofe@33189
   835
  from `\<Gamma> \<turnstile> (\<lambda>x:S. t) \<cdot> u : T` `x \<sharp> \<Gamma>`
berghofe@33189
   836
  obtain "(x, S) # \<Gamma> \<turnstile> t : T" and "\<Gamma> \<turnstile> u : S"
berghofe@33189
   837
    by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs)
berghofe@33189
   838
  then show ?case by (rule subst_type)
berghofe@33189
   839
next
berghofe@33189
   840
  case (Let p t \<theta> u)
berghofe@33189
   841
  from `\<Gamma> \<turnstile> (LET p = t IN u) : T` `supp p \<sharp>* \<Gamma>` `distinct (pat_vars p)`
berghofe@33189
   842
  obtain U \<Delta> where "\<turnstile> p : U \<Rightarrow> \<Delta>" "\<Gamma> \<turnstile> t : U" "\<Delta> @ \<Gamma> \<turnstile> u : T"
berghofe@33189
   843
    by (rule typing_case_Let)
berghofe@33189
   844
  then show ?case using `\<turnstile> p \<rhd> t \<Rightarrow> \<theta>` `supp p \<sharp>* t`
berghofe@33189
   845
    by (rule match_type)
berghofe@33189
   846
next
berghofe@33189
   847
  case (AppL t t' u)
berghofe@33189
   848
  from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where
berghofe@33189
   849
    t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U"
berghofe@33189
   850
    by cases (auto simp add: trm.inject)
berghofe@33189
   851
  from t have "\<Gamma> \<turnstile> t' : U \<rightarrow> T" by (rule AppL)
berghofe@33189
   852
  then show ?case using u by (rule typing.App)
berghofe@33189
   853
next
berghofe@33189
   854
  case (AppR u u' t)
berghofe@33189
   855
  from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where
berghofe@33189
   856
    t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U"
berghofe@33189
   857
    by cases (auto simp add: trm.inject)
berghofe@33189
   858
  from u have "\<Gamma> \<turnstile> u' : U" by (rule AppR)
berghofe@33189
   859
  with t show ?case by (rule typing.App)
berghofe@33189
   860
qed
berghofe@33189
   861
berghofe@33189
   862
end