src/HOL/Nominal/Examples/SN.thy
author urbanc
Wed Mar 08 18:00:00 2006 +0100 (2006-03-08)
changeset 19218 47b05ebe106b
parent 18659 2ff0ae57431d
child 19496 79dbe35c6cba
permissions -rw-r--r--
deleted some proofs "on comment"
urbanc@18263
     1
(* $Id$ *)
urbanc@18106
     2
urbanc@18106
     3
theory sn
urbanc@18106
     4
imports lam_substs  Accessible_Part
urbanc@18106
     5
begin
urbanc@18106
     6
urbanc@18269
     7
text {* Strong Normalisation proof from the Proofs and Types book *}
urbanc@18106
     8
urbanc@18106
     9
section {* Beta Reduction *}
urbanc@18106
    10
urbanc@18106
    11
lemma subst_rename[rule_format]: 
urbanc@18106
    12
  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
urbanc@18659
    13
apply(nominal_induct t1 avoiding: a c t2 rule: lam.induct)
urbanc@18313
    14
apply(auto simp add: calc_atm fresh_atm abs_fresh)
urbanc@18106
    15
done
urbanc@18106
    16
urbanc@18313
    17
lemma forget: 
urbanc@18313
    18
  assumes a: "a\<sharp>t1"
urbanc@18313
    19
  shows "t1[a::=t2] = t1"
urbanc@18313
    20
  using a
urbanc@18659
    21
apply (nominal_induct t1 avoiding: a t2 rule: lam.induct)
urbanc@18313
    22
apply(auto simp add: abs_fresh fresh_atm)
urbanc@18106
    23
done
urbanc@18106
    24
urbanc@18313
    25
lemma fresh_fact: 
urbanc@18313
    26
  fixes a::"name"
urbanc@18313
    27
  assumes a: "a\<sharp>t1"
urbanc@18313
    28
  and     b: "a\<sharp>t2"
urbanc@18313
    29
  shows "a\<sharp>(t1[b::=t2])"
urbanc@18313
    30
using a b
urbanc@18659
    31
apply(nominal_induct t1 avoiding: a b t2 rule: lam.induct)
urbanc@18313
    32
apply(auto simp add: abs_fresh fresh_atm)
urbanc@18106
    33
done
urbanc@18106
    34
urbanc@18383
    35
lemma subst_lemma:  
urbanc@18313
    36
  assumes a: "x\<noteq>y"
urbanc@18313
    37
  and     b: "x\<sharp>L"
urbanc@18313
    38
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
urbanc@18313
    39
using a b
urbanc@18659
    40
by (nominal_induct M avoiding: x y N L rule: lam.induct)
urbanc@18313
    41
   (auto simp add: fresh_fact forget)
urbanc@18106
    42
urbanc@18106
    43
lemma id_subs: "t[x::=Var x] = t"
urbanc@18659
    44
apply(nominal_induct t avoiding: x rule: lam.induct)
urbanc@18106
    45
apply(simp_all add: fresh_atm)
urbanc@18106
    46
done
urbanc@18106
    47
urbanc@18106
    48
consts
urbanc@18106
    49
  Beta :: "(lam\<times>lam) set"
urbanc@18106
    50
syntax 
urbanc@18106
    51
  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
urbanc@18106
    52
  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
urbanc@18106
    53
translations 
urbanc@18106
    54
  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
urbanc@18106
    55
  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
urbanc@18106
    56
inductive Beta
urbanc@18106
    57
  intros
urbanc@18106
    58
  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
urbanc@18106
    59
  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
urbanc@18106
    60
  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
urbanc@18106
    61
  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
urbanc@18106
    62
urbanc@18106
    63
lemma eqvt_beta: 
urbanc@18106
    64
  fixes pi :: "name prm"
urbanc@18106
    65
  and   t  :: "lam"
urbanc@18106
    66
  and   s  :: "lam"
urbanc@18313
    67
  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
urbanc@18313
    68
  shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
urbanc@18313
    69
  using a by (induct, auto)
urbanc@18106
    70
urbanc@18313
    71
lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]:
urbanc@18313
    72
  fixes  P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
urbanc@18106
    73
  and    t :: "lam"
urbanc@18106
    74
  and    s :: "lam"
urbanc@18106
    75
  and    x :: "'a::fs_name"
urbanc@18106
    76
  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
urbanc@18313
    77
  and a1:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)"
urbanc@18313
    78
  and a2:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)"
urbanc@18313
    79
  and a3:    "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
urbanc@19218
    80
  and a4:    "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
urbanc@18313
    81
  shows "P x t s"
urbanc@18313
    82
proof -
urbanc@18313
    83
  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
urbanc@18313
    84
  proof (induct)
urbanc@18313
    85
    case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
urbanc@18313
    86
  next
urbanc@18313
    87
    case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
urbanc@18313
    88
  next
urbanc@18313
    89
    case (b3 a s1 s2)
urbanc@18313
    90
    have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
urbanc@18313
    91
    have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
urbanc@18313
    92
    show ?case 
urbanc@18313
    93
    proof (simp)
urbanc@18313
    94
      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
urbanc@18313
    95
	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
urbanc@18313
    96
      then obtain c::"name" 
urbanc@18313
    97
	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
urbanc@18313
    98
	by (force simp add: fresh_prod fresh_atm)
urbanc@18313
    99
      have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))"
urbanc@18313
   100
	using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
urbanc@18313
   101
      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
urbanc@18313
   102
	by (simp add: lam.inject alpha)
urbanc@18313
   103
      have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
urbanc@18313
   104
	by (simp add: lam.inject alpha)
urbanc@18313
   105
      show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))"
urbanc@18313
   106
	using x alpha1 alpha2 by (simp only: pt_name2)
urbanc@18313
   107
    qed
urbanc@18313
   108
  next
urbanc@18313
   109
    case (b4 a s1 s2)
urbanc@18313
   110
    show ?case
urbanc@18313
   111
    proof (simp add: subst_eqvt)
urbanc@18313
   112
      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
urbanc@18313
   113
	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
urbanc@18313
   114
      then obtain c::"name" 
urbanc@19218
   115
	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
urbanc@18313
   116
	by (force simp add: fresh_prod fresh_atm)
urbanc@18313
   117
      have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)])"
urbanc@18313
   118
	using a4 f2 by (blast intro!: eqvt_beta)
urbanc@18313
   119
      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
urbanc@18313
   120
	by (simp add: lam.inject alpha)
urbanc@18313
   121
      have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
urbanc@18313
   122
	using f3 by (simp only: subst_rename[symmetric] pt_name2)
urbanc@18313
   123
      show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
urbanc@18313
   124
	using x alpha1 alpha2 by (simp only: pt_name2)
urbanc@18313
   125
    qed
urbanc@18313
   126
  qed
urbanc@18313
   127
  hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast 
urbanc@18313
   128
  thus ?thesis by simp
urbanc@18313
   129
qed
urbanc@18106
   130
urbanc@18378
   131
lemma supp_beta: 
urbanc@18378
   132
  assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
urbanc@18378
   133
  shows "(supp s)\<subseteq>((supp t)::name set)"
urbanc@18378
   134
using a
urbanc@18378
   135
by (induct)
urbanc@18378
   136
   (auto intro!: simp add: abs_supp lam.supp subst_supp)
urbanc@18378
   137
urbanc@18313
   138
urbanc@18106
   139
lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
urbanc@18106
   140
apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
urbanc@18106
   141
apply(auto simp add: lam.distinct lam.inject)
urbanc@18106
   142
apply(auto simp add: alpha)
urbanc@18106
   143
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
urbanc@18106
   144
apply(rule conjI)
urbanc@18106
   145
apply(rule sym)
urbanc@18106
   146
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
urbanc@18106
   147
apply(simp)
urbanc@18106
   148
apply(rule pt_name3)
urbanc@18106
   149
apply(simp add: at_ds5[OF at_name_inst])
urbanc@18106
   150
apply(rule conjI)
urbanc@18106
   151
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
urbanc@18106
   152
apply(force dest!: supp_beta simp add: fresh_def)
urbanc@18106
   153
apply(force intro!: eqvt_beta)
urbanc@18106
   154
done
urbanc@18106
   155
urbanc@18313
   156
lemma beta_subst: 
urbanc@18106
   157
  assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
urbanc@18106
   158
  shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
urbanc@18106
   159
using a
urbanc@18313
   160
apply(nominal_induct M M' avoiding: x N rule: beta_induct)
urbanc@18383
   161
apply(auto simp add: fresh_atm subst_lemma)
urbanc@18106
   162
done
urbanc@18106
   163
urbanc@18383
   164
section {* types *}
urbanc@18383
   165
urbanc@18106
   166
datatype ty =
urbanc@18106
   167
    TVar "string"
urbanc@18106
   168
  | TArr "ty" "ty" (infix "\<rightarrow>" 200)
urbanc@18106
   169
urbanc@18106
   170
primrec
urbanc@18106
   171
 "pi\<bullet>(TVar s) = TVar s"
urbanc@18106
   172
 "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
urbanc@18106
   173
urbanc@18106
   174
lemma perm_ty[simp]:
urbanc@18106
   175
  fixes pi ::"name prm"
urbanc@18106
   176
  and   \<tau>  ::"ty"
urbanc@18106
   177
  shows "pi\<bullet>\<tau> = \<tau>"
urbanc@18106
   178
  by (cases \<tau>, simp_all)
urbanc@18106
   179
urbanc@18106
   180
lemma fresh_ty:
urbanc@18106
   181
  fixes a ::"name"
urbanc@18106
   182
  and   \<tau>  ::"ty"
urbanc@18106
   183
  shows "a\<sharp>\<tau>"
urbanc@18106
   184
  by (simp add: fresh_def supp_def)
urbanc@18106
   185
urbanc@18106
   186
instance ty :: pt_name
urbanc@18106
   187
apply(intro_classes)   
urbanc@18106
   188
apply(simp_all)
urbanc@18106
   189
done
urbanc@18106
   190
urbanc@18106
   191
instance ty :: fs_name
urbanc@18106
   192
apply(intro_classes)
urbanc@18106
   193
apply(simp add: supp_def)
urbanc@18106
   194
done
urbanc@18106
   195
urbanc@18106
   196
(* valid contexts *)
urbanc@18106
   197
urbanc@18106
   198
consts
urbanc@18106
   199
  "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
urbanc@18106
   200
primrec
urbanc@18106
   201
  "dom_ty []    = []"
urbanc@18106
   202
  "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
urbanc@18106
   203
urbanc@18106
   204
consts
urbanc@18106
   205
  ctxts :: "((name\<times>ty) list) set" 
urbanc@18106
   206
  valid :: "(name\<times>ty) list \<Rightarrow> bool"
urbanc@18106
   207
translations
urbanc@18106
   208
  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
urbanc@18106
   209
inductive ctxts
urbanc@18106
   210
intros
urbanc@18106
   211
v1[intro]: "valid []"
urbanc@18106
   212
v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
urbanc@18106
   213
urbanc@18106
   214
lemma valid_eqvt:
urbanc@18106
   215
  fixes   pi:: "name prm"
urbanc@18106
   216
  assumes a: "valid \<Gamma>"
urbanc@18106
   217
  shows   "valid (pi\<bullet>\<Gamma>)"
urbanc@18106
   218
using a
urbanc@18106
   219
apply(induct)
urbanc@18654
   220
apply(auto simp add: fresh_eqvt)
urbanc@18106
   221
done
urbanc@18106
   222
urbanc@18106
   223
(* typing judgements *)
urbanc@18106
   224
urbanc@18106
   225
lemma fresh_context[rule_format]: 
urbanc@18106
   226
  fixes  \<Gamma> :: "(name\<times>ty)list"
urbanc@18106
   227
  and    a :: "name"
urbanc@18378
   228
  assumes a: "a\<sharp>\<Gamma>"
urbanc@18378
   229
  shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
urbanc@18378
   230
using a
urbanc@18378
   231
apply(induct \<Gamma>)
urbanc@18106
   232
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
urbanc@18106
   233
done
urbanc@18106
   234
urbanc@18106
   235
lemma valid_elim: 
urbanc@18106
   236
  fixes  \<Gamma> :: "(name\<times>ty)list"
urbanc@18106
   237
  and    pi:: "name prm"
urbanc@18106
   238
  and    a :: "name"
urbanc@18106
   239
  and    \<tau> :: "ty"
urbanc@18106
   240
  shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
urbanc@18106
   241
apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
urbanc@18106
   242
done
urbanc@18106
   243
urbanc@18106
   244
lemma valid_unicity[rule_format]: 
urbanc@18378
   245
  assumes a: "valid \<Gamma>"
urbanc@18378
   246
  and     b: "(c,\<sigma>)\<in>set \<Gamma>"
urbanc@18378
   247
  and     c: "(c,\<tau>)\<in>set \<Gamma>"
urbanc@18378
   248
  shows "\<sigma>=\<tau>" 
urbanc@18378
   249
using a b c
urbanc@18378
   250
apply(induct \<Gamma>)
urbanc@18106
   251
apply(auto dest!: valid_elim fresh_context)
urbanc@18106
   252
done
urbanc@18106
   253
urbanc@18106
   254
consts
urbanc@18106
   255
  typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
urbanc@18106
   256
syntax
urbanc@18106
   257
  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
urbanc@18106
   258
translations
urbanc@18106
   259
  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
urbanc@18106
   260
urbanc@18106
   261
inductive typing
urbanc@18106
   262
intros
urbanc@18106
   263
t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
urbanc@18106
   264
t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
urbanc@18106
   265
t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
urbanc@18106
   266
urbanc@18313
   267
lemma eqvt_typing: 
urbanc@18106
   268
  fixes  \<Gamma> :: "(name\<times>ty) list"
urbanc@18106
   269
  and    t :: "lam"
urbanc@18106
   270
  and    \<tau> :: "ty"
urbanc@18106
   271
  and    pi:: "name prm"
urbanc@18106
   272
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
urbanc@18106
   273
  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
urbanc@18106
   274
using a
urbanc@18106
   275
proof (induct)
urbanc@18106
   276
  case (t1 \<Gamma> \<tau> a)
urbanc@18106
   277
  have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
urbanc@18106
   278
  moreover
urbanc@18106
   279
  have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
urbanc@18313
   280
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
urbanc@18654
   281
    using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
urbanc@18106
   282
next 
urbanc@18106
   283
  case (t3 \<Gamma> \<sigma> \<tau> a t)
urbanc@18654
   284
  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
urbanc@18313
   285
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
urbanc@18106
   286
qed (auto)
urbanc@18106
   287
urbanc@18313
   288
lemma typing_induct[consumes 1, case_names t1 t2 t3]:
urbanc@18313
   289
  fixes  P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"
urbanc@18106
   290
  and    \<Gamma> :: "(name\<times>ty) list"
urbanc@18106
   291
  and    t :: "lam"
urbanc@18106
   292
  and    \<tau> :: "ty"
urbanc@18106
   293
  and    x :: "'a::fs_name"
urbanc@18106
   294
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
urbanc@18313
   295
  and a1:    "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"
urbanc@18313
   296
  and a2:    "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. 
urbanc@18313
   297
              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P z \<Gamma> t2 \<tau>)
urbanc@18313
   298
              \<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"
urbanc@18313
   299
  and a3:    "\<And>a \<Gamma> \<tau> \<sigma> t x. a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)
urbanc@18313
   300
              \<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"
urbanc@18313
   301
  shows "P x \<Gamma> t \<tau>"
urbanc@18313
   302
proof -
urbanc@18313
   303
  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
urbanc@18313
   304
  proof (induct)
urbanc@18313
   305
    case (t1 \<Gamma> \<tau> a)
urbanc@18313
   306
    have j1: "valid \<Gamma>" by fact
urbanc@18313
   307
    have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
urbanc@18313
   308
    from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
urbanc@18313
   309
    from j2 have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
urbanc@18313
   310
    hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
urbanc@18313
   311
    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
urbanc@18313
   312
  next
urbanc@18313
   313
    case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
urbanc@18313
   314
    thus ?case using a2 by (simp, blast intro: eqvt_typing)
urbanc@18313
   315
  next
urbanc@18313
   316
    case (t3 \<Gamma> \<sigma> \<tau> a t)
urbanc@18313
   317
    have k1: "a\<sharp>\<Gamma>" by fact
urbanc@18313
   318
    have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
urbanc@18313
   319
    have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
urbanc@18313
   320
    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
urbanc@18313
   321
      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
urbanc@18313
   322
    then obtain c::"name" 
urbanc@18313
   323
      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
urbanc@18313
   324
      by (force simp add: fresh_prod at_fresh[OF at_name_inst])
urbanc@18313
   325
    from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
urbanc@18313
   326
      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
urbanc@18313
   327
                    pt_rev_pi[OF pt_name_inst, OF at_name_inst])
urbanc@18313
   328
    have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
urbanc@18313
   329
      by (simp only: pt2[OF pt_name_inst], rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
urbanc@18313
   330
    have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using k3 by force
urbanc@18313
   331
    hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1
urbanc@18313
   332
      by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
urbanc@18313
   333
    have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule eqvt_typing)
urbanc@18313
   334
    hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
urbanc@18313
   335
      by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
urbanc@18313
   336
    have l4: "P x (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using f2 f4 l2 l3 a3 by auto
urbanc@18313
   337
    have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
urbanc@18313
   338
      by (simp add: lam.inject alpha)
urbanc@18313
   339
    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" using l4 alpha 
urbanc@18313
   340
      by (simp only: pt2[OF pt_name_inst], simp)
urbanc@18313
   341
  qed
urbanc@18313
   342
  hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast
urbanc@18313
   343
  thus "P x \<Gamma> t \<tau>" by simp
urbanc@18313
   344
qed
urbanc@18106
   345
urbanc@18106
   346
constdefs
urbanc@18106
   347
  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
urbanc@18106
   348
  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
urbanc@18106
   349
urbanc@18313
   350
lemma weakening: 
urbanc@18313
   351
  assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" 
urbanc@18313
   352
  and     b: "valid \<Gamma>2" 
urbanc@18313
   353
  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
urbanc@18313
   354
  shows "\<Gamma>2 \<turnstile> t:\<sigma>"
urbanc@18313
   355
using a b c
urbanc@18313
   356
apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct)
urbanc@18106
   357
apply(auto simp add: sub_def)
urbanc@18313
   358
(* FIXME: before using meta-connectives and the new induction *)
urbanc@18313
   359
(* method, this was completely automatic *)
urbanc@18313
   360
apply(atomize)
urbanc@18313
   361
apply(auto)
urbanc@18106
   362
done
urbanc@18106
   363
urbanc@18378
   364
lemma in_ctxt: 
urbanc@18378
   365
  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
urbanc@18378
   366
  shows "a\<in>set(dom_ty \<Gamma>)"
urbanc@18378
   367
using a
urbanc@18383
   368
apply(induct \<Gamma>, auto)
urbanc@18106
   369
done
urbanc@18106
   370
urbanc@18106
   371
lemma free_vars: 
urbanc@18106
   372
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
urbanc@18106
   373
  shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
urbanc@18106
   374
using a
urbanc@18106
   375
apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct)
urbanc@18106
   376
apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt)
urbanc@18106
   377
done
urbanc@18106
   378
urbanc@18106
   379
lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
urbanc@18106
   380
apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
urbanc@18106
   381
apply(auto simp add: lam.inject lam.distinct)
urbanc@18106
   382
done
urbanc@18106
   383
urbanc@18106
   384
lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
urbanc@18106
   385
apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
urbanc@18106
   386
apply(auto simp add: lam.inject lam.distinct)
urbanc@18106
   387
done
urbanc@18106
   388
urbanc@18106
   389
lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
urbanc@18106
   390
apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
urbanc@18106
   391
apply(auto simp add: lam.distinct lam.inject alpha) 
urbanc@18313
   392
apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
urbanc@18106
   393
apply(simp)
urbanc@18106
   394
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
urbanc@18106
   395
apply(force simp add: calc_atm)
urbanc@18106
   396
(*A*)
urbanc@18106
   397
apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
urbanc@18106
   398
done
urbanc@18106
   399
urbanc@18106
   400
lemma typing_valid: 
urbanc@18106
   401
  assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
urbanc@18106
   402
  shows "valid \<Gamma>"
urbanc@18106
   403
using a by (induct, auto dest!: valid_elim)
urbanc@18106
   404
urbanc@18378
   405
lemma ty_subs:
urbanc@18378
   406
  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
urbanc@18378
   407
  and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
urbanc@18378
   408
  shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
urbanc@18378
   409
using a b
urbanc@18659
   410
proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam.induct)
urbanc@18313
   411
  case (Var a) 
urbanc@18378
   412
  have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
urbanc@18378
   413
  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
urbanc@18378
   414
  hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
urbanc@18378
   415
  from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
urbanc@18378
   416
  from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
urbanc@18378
   417
  show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
urbanc@18378
   418
  proof (cases "a=c", simp_all)
urbanc@18378
   419
    assume case1: "a=c"
urbanc@18378
   420
    show "\<Gamma> \<turnstile> t2:\<tau>" using a1
urbanc@18378
   421
    proof (cases "\<sigma>=\<tau>")
urbanc@18378
   422
      assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
urbanc@18378
   423
    next
urbanc@18378
   424
      assume a3: "\<sigma>\<noteq>\<tau>"
urbanc@18378
   425
      show ?thesis
urbanc@18378
   426
      proof (rule ccontr)
urbanc@18378
   427
	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
urbanc@18378
   428
	with case1 a25 show False by force 
urbanc@18106
   429
      qed
urbanc@18106
   430
    qed
urbanc@18378
   431
  next
urbanc@18378
   432
    assume case2: "a\<noteq>c"
urbanc@18378
   433
    with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
urbanc@18378
   434
    from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
urbanc@18106
   435
  qed
urbanc@18106
   436
next
urbanc@18313
   437
  case (App s1 s2)
urbanc@18383
   438
  have ih_s1: "\<And>c \<sigma> \<tau> t2 \<Gamma>. ((c,\<sigma>)#\<Gamma>) \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma>\<turnstile> t2: \<sigma> \<Longrightarrow> \<Gamma> \<turnstile> s1[c::=t2]:\<tau>" by fact
urbanc@18383
   439
  have ih_s2: "\<And>c \<sigma> \<tau> t2 \<Gamma>. ((c,\<sigma>)#\<Gamma>) \<turnstile> s2:\<tau> \<Longrightarrow> \<Gamma>\<turnstile> t2: \<sigma> \<Longrightarrow> \<Gamma> \<turnstile> s2[c::=t2]:\<tau>" by fact
urbanc@18383
   440
  have "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
urbanc@18383
   441
  hence "\<exists>\<tau>'. ((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by (rule t2_elim) 
urbanc@18383
   442
  then obtain \<tau>' where "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by blast
urbanc@18383
   443
  moreover
urbanc@18383
   444
  have "\<Gamma> \<turnstile>t2:\<sigma>" by fact
urbanc@18383
   445
  ultimately show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" using ih_s1 ih_s2 by (simp, blast)
urbanc@18106
   446
next
urbanc@18313
   447
  case (Lam a s)
urbanc@18313
   448
  have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
urbanc@18106
   449
  hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"
urbanc@18106
   450
    by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
urbanc@18378
   451
  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
urbanc@18378
   452
  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
urbanc@18378
   453
  then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
urbanc@18378
   454
  from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
urbanc@18378
   455
  hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
urbanc@18378
   456
    by (auto dest: valid_elim simp add: fresh_list_cons) 
urbanc@18378
   457
  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
urbanc@18378
   458
  proof -
urbanc@18378
   459
    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
urbanc@18378
   460
    have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
urbanc@18378
   461
      by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
urbanc@18378
   462
    from c12 c2 c3 show ?thesis by (force intro: weakening)
urbanc@18106
   463
  qed
urbanc@18378
   464
  assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
urbanc@18378
   465
  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
urbanc@18378
   466
  proof -
urbanc@18378
   467
    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
urbanc@18378
   468
    have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
urbanc@18378
   469
    with c8 c82 c83 show ?thesis by (force intro: weakening)
urbanc@18378
   470
  qed
urbanc@18378
   471
  show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
urbanc@18378
   472
    using c11 prems c14 c81 f1 by force
urbanc@18106
   473
qed
urbanc@18106
   474
urbanc@18378
   475
lemma subject: 
urbanc@18106
   476
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
urbanc@18378
   477
  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
urbanc@18378
   478
  shows "\<Gamma> \<turnstile> t2:\<tau>"
urbanc@18378
   479
using a b
urbanc@18378
   480
proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
urbanc@18383
   481
  case (b1 t s1 s2) --"App-case left"
urbanc@18383
   482
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
urbanc@18378
   483
  have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
urbanc@18378
   484
  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
urbanc@18383
   485
  then obtain \<sigma> where "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> t : \<sigma>" by blast
urbanc@18383
   486
  with ih show "\<Gamma> \<turnstile> App s2 t : \<tau>" by blast
urbanc@18106
   487
next
urbanc@18383
   488
  case (b2 t s1 s2) --"App-case right"
urbanc@18383
   489
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
urbanc@18378
   490
  have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
urbanc@18378
   491
  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
urbanc@18383
   492
  then obtain \<sigma> where "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
urbanc@18383
   493
  with ih show "\<Gamma> \<turnstile> App t s2 : \<tau>" by blast
urbanc@18106
   494
next
urbanc@18383
   495
  case (b3 a s1 s2) --"Lam-case"
urbanc@18383
   496
  have fr: "a\<sharp>\<Gamma>" "a\<sharp>\<tau>" by fact
urbanc@18383
   497
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
urbanc@18378
   498
  have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
urbanc@18383
   499
  with fr have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (simp add: t3_elim)
urbanc@18383
   500
  then obtain \<tau>1 \<tau>2 where "\<tau>=\<tau>1\<rightarrow>\<tau>2" and "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by blast
urbanc@18383
   501
  with ih show "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using fr by blast
urbanc@18106
   502
next
urbanc@18383
   503
  case (b4 a s1 s2) --"Beta-redex"
urbanc@18383
   504
  have fr: "a\<sharp>\<Gamma>" by fact
urbanc@18378
   505
  have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
urbanc@18383
   506
  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (simp add: t2_elim)
urbanc@18383
   507
  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
urbanc@18383
   508
  from a1 have "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using fr by (blast dest!: t3_elim)
urbanc@18383
   509
  with a2 show "\<Gamma> \<turnstile> s1[a::=s2] : \<tau>" by (simp add: ty_subs)
urbanc@18106
   510
qed
urbanc@18106
   511
urbanc@18378
   512
lemma subject_automatic: 
urbanc@18106
   513
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
urbanc@18378
   514
  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
urbanc@18378
   515
  shows "\<Gamma> \<turnstile> t2:\<tau>"
urbanc@18378
   516
using a b
urbanc@18313
   517
apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
urbanc@18313
   518
apply(auto dest!: t2_elim t3_elim intro: ty_subs)
urbanc@18106
   519
done
urbanc@18106
   520
urbanc@18106
   521
subsection {* some facts about beta *}
urbanc@18106
   522
urbanc@18106
   523
constdefs
urbanc@18106
   524
  "NORMAL" :: "lam \<Rightarrow> bool"
urbanc@18106
   525
  "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"
urbanc@18106
   526
urbanc@18383
   527
lemma NORMAL_Var:
urbanc@18383
   528
  shows "NORMAL (Var a)"
urbanc@18383
   529
proof -
urbanc@18383
   530
  { assume "\<exists>t'. (Var a) \<longrightarrow>\<^isub>\<beta> t'"
urbanc@18383
   531
    then obtain t' where "(Var a) \<longrightarrow>\<^isub>\<beta> t'" by blast
urbanc@18383
   532
    hence False by (cases, auto) 
urbanc@18383
   533
  }
urbanc@18383
   534
  thus "NORMAL (Var a)" by (force simp add: NORMAL_def)
urbanc@18383
   535
qed
urbanc@18383
   536
urbanc@18106
   537
constdefs
urbanc@18106
   538
  "SN" :: "lam \<Rightarrow> bool"
urbanc@18106
   539
  "SN t \<equiv> t\<in>termi Beta"
urbanc@18106
   540
urbanc@18383
   541
lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
urbanc@18106
   542
apply(simp add: SN_def)
urbanc@18106
   543
apply(drule_tac a="t2" in acc_downward)
urbanc@18106
   544
apply(auto)
urbanc@18106
   545
done
urbanc@18106
   546
urbanc@18383
   547
lemma SN_intro: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
urbanc@18106
   548
apply(simp add: SN_def)
urbanc@18106
   549
apply(rule accI)
urbanc@18106
   550
apply(auto)
urbanc@18106
   551
done
urbanc@18106
   552
urbanc@18106
   553
section {* Candidates *}
urbanc@18106
   554
urbanc@18106
   555
consts
urbanc@18106
   556
  RED :: "ty \<Rightarrow> lam set"
urbanc@18106
   557
primrec
urbanc@18106
   558
 "RED (TVar X) = {t. SN(t)}"
urbanc@18106
   559
 "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
urbanc@18106
   560
urbanc@18106
   561
constdefs
urbanc@18106
   562
  NEUT :: "lam \<Rightarrow> bool"
urbanc@18106
   563
  "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
urbanc@18106
   564
urbanc@18106
   565
(* a slight hack to get the first element of applications *)
urbanc@18106
   566
consts
urbanc@18106
   567
  FST :: "(lam\<times>lam) set"
urbanc@18106
   568
syntax 
urbanc@18106
   569
  "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
urbanc@18106
   570
translations 
urbanc@18106
   571
  "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
urbanc@18106
   572
inductive FST
urbanc@18378
   573
  intros
urbanc@18106
   574
fst[intro!]:  "(App t s) \<guillemotright> t"
urbanc@18106
   575
urbanc@18378
   576
lemma fst_elim[elim!]: 
urbanc@18378
   577
  shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
urbanc@18106
   578
apply(ind_cases "App t s \<guillemotright> t'")
urbanc@18106
   579
apply(simp add: lam.inject)
urbanc@18106
   580
done
urbanc@18106
   581
urbanc@18106
   582
lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
urbanc@18106
   583
apply(simp add: SN_def)
urbanc@18106
   584
apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
urbanc@18106
   585
apply(force)
urbanc@18106
   586
(*A*)
urbanc@18106
   587
apply(erule acc_induct)
urbanc@18106
   588
apply(clarify)
urbanc@18106
   589
apply(ind_cases "x \<guillemotright> z")
urbanc@18106
   590
apply(clarify)
urbanc@18106
   591
apply(rule accI)
urbanc@18106
   592
apply(auto intro: b1)
urbanc@18106
   593
done
urbanc@18106
   594
urbanc@18383
   595
section {* Candidates *}
urbanc@18383
   596
urbanc@18106
   597
constdefs
urbanc@18383
   598
  "CR1" :: "ty \<Rightarrow> bool"
urbanc@18383
   599
  "CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"
urbanc@18106
   600
urbanc@18383
   601
  "CR2" :: "ty \<Rightarrow> bool"
urbanc@18383
   602
  "CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>"
urbanc@18106
   603
urbanc@18383
   604
  "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"
urbanc@18383
   605
  "CR3_RED t \<tau> \<equiv> \<forall>t'. t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>" 
urbanc@18106
   606
urbanc@18383
   607
  "CR3" :: "ty \<Rightarrow> bool"
urbanc@18383
   608
  "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
urbanc@18106
   609
   
urbanc@18383
   610
  "CR4" :: "ty \<Rightarrow> bool"
urbanc@18383
   611
  "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
urbanc@18106
   612
urbanc@18106
   613
lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"
urbanc@18106
   614
apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)
urbanc@18106
   615
apply(blast)
urbanc@18106
   616
done
urbanc@18106
   617
urbanc@18106
   618
lemma sub_ind: 
urbanc@18106
   619
  "SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"
urbanc@18106
   620
apply(simp add: SN_def)
urbanc@18106
   621
apply(erule acc_induct)
urbanc@18106
   622
apply(auto)
urbanc@18106
   623
apply(simp add: CR3_def)
urbanc@18106
   624
apply(rotate_tac 5)
urbanc@18106
   625
apply(drule_tac x="App t x" in spec)
urbanc@18106
   626
apply(drule mp)
urbanc@18106
   627
apply(rule conjI)
urbanc@18106
   628
apply(force simp only: NEUT_def)
urbanc@18106
   629
apply(simp (no_asm) add: CR3_RED_def)
urbanc@18106
   630
apply(clarify)
urbanc@18106
   631
apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
urbanc@18106
   632
apply(simp_all add: lam.inject)
urbanc@18106
   633
apply(simp only:  CR3_RED_def)
urbanc@18106
   634
apply(drule_tac x="s2" in spec)
urbanc@18106
   635
apply(simp)
urbanc@18106
   636
apply(drule_tac x="s2" in spec)
urbanc@18106
   637
apply(simp)
urbanc@18106
   638
apply(drule mp)
urbanc@18106
   639
apply(simp (no_asm_use) add: CR2_def)
urbanc@18106
   640
apply(blast)
urbanc@18106
   641
apply(drule_tac x="ta" in spec)
urbanc@18106
   642
apply(force)
urbanc@18106
   643
apply(auto simp only: NEUT_def lam.inject lam.distinct)
urbanc@18106
   644
done
urbanc@18106
   645
urbanc@18383
   646
lemma RED_props: 
urbanc@18383
   647
  shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
urbanc@18383
   648
proof (induct \<tau>)
urbanc@18611
   649
  case (TVar a)
urbanc@18611
   650
  { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
urbanc@18611
   651
  next
urbanc@18611
   652
    case 2 show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
urbanc@18611
   653
  next
urbanc@18611
   654
    case 3 show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
urbanc@18611
   655
  }
urbanc@18599
   656
next
urbanc@18611
   657
  case (TArr \<tau>1 \<tau>2)
urbanc@18611
   658
  { case 1
urbanc@18611
   659
    have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
urbanc@18611
   660
    have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
urbanc@18611
   661
    show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
urbanc@18611
   662
    proof (simp add: CR1_def, intro strip)
urbanc@18611
   663
      fix t
urbanc@18611
   664
      assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
urbanc@18611
   665
      from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4) 
urbanc@18611
   666
      moreover
urbanc@18611
   667
      have "NEUT (Var a)" by (force simp add: NEUT_def)
urbanc@18611
   668
      moreover
urbanc@18611
   669
      have "NORMAL (Var a)" by (rule NORMAL_Var)
urbanc@18611
   670
      ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
urbanc@18611
   671
      with a have "App t (Var a) \<in> RED \<tau>2" by simp
urbanc@18611
   672
      hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
urbanc@18611
   673
      thus "SN(t)" by (rule qq3)
urbanc@18611
   674
    qed
urbanc@18611
   675
  next
urbanc@18611
   676
    case 2
urbanc@18611
   677
    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
urbanc@18611
   678
    have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
urbanc@18611
   679
    show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
urbanc@18611
   680
    proof (simp add: CR2_def, intro strip)
urbanc@18611
   681
      fix t1 t2 u
urbanc@18611
   682
      assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and>  t1 \<longrightarrow>\<^isub>\<beta> t2" 
urbanc@18611
   683
	and  "u \<in> RED \<tau>1"
urbanc@18611
   684
      hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
urbanc@18611
   685
      thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
urbanc@18611
   686
    qed
urbanc@18611
   687
  next
urbanc@18611
   688
    case 3
urbanc@18611
   689
    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
urbanc@18611
   690
    have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
urbanc@18611
   691
    have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
urbanc@18611
   692
    show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
urbanc@18611
   693
    proof (simp add: CR3_def, intro strip)
urbanc@18611
   694
      fix t u
urbanc@18611
   695
      assume a1: "u \<in> RED \<tau>1"
urbanc@18611
   696
      assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
urbanc@18611
   697
      from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
urbanc@18611
   698
      hence "u\<in>RED \<tau>1\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>1\<and>CR3 \<tau>2\<and>CR3_RED t (\<tau>1\<rightarrow>\<tau>2))\<longrightarrow>(App t u)\<in>RED \<tau>2)" 
urbanc@18611
   699
	by (rule sub_ind)
urbanc@18611
   700
      with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
urbanc@18611
   701
    qed
urbanc@18611
   702
  }
urbanc@18383
   703
qed
urbanc@18383
   704
    
urbanc@18106
   705
lemma double_acc_aux:
urbanc@18106
   706
  assumes a_acc: "a \<in> acc r"
urbanc@18106
   707
  and b_acc: "b \<in> acc r"
urbanc@18106
   708
  and hyp: "\<And>x z.
urbanc@18106
   709
    (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
urbanc@18106
   710
    (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
urbanc@18106
   711
    (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
urbanc@18106
   712
    (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
urbanc@18106
   713
  shows "P a b"
urbanc@18106
   714
proof -
urbanc@18106
   715
  from a_acc
urbanc@18106
   716
  have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
urbanc@18106
   717
  proof (induct a rule: acc.induct)
urbanc@18106
   718
    case (accI x)
urbanc@18106
   719
    note accI' = accI
urbanc@18106
   720
    have "b \<in> acc r" .
urbanc@18106
   721
    thus ?case
urbanc@18106
   722
    proof (induct b rule: acc.induct)
urbanc@18106
   723
      case (accI y)
urbanc@18106
   724
      show ?case
urbanc@18106
   725
	apply (rule hyp)
urbanc@18106
   726
	apply (erule accI')
urbanc@18106
   727
	apply (erule accI')
urbanc@18106
   728
	apply (rule acc.accI)
urbanc@18106
   729
	apply (erule accI)
urbanc@18106
   730
	apply (erule accI)
urbanc@18106
   731
	apply (erule accI)
urbanc@18106
   732
	done
urbanc@18106
   733
    qed
urbanc@18106
   734
  qed
urbanc@18106
   735
  from b_acc show ?thesis by (rule r)
urbanc@18106
   736
qed
urbanc@18106
   737
urbanc@18106
   738
lemma double_acc:
urbanc@18106
   739
  "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
urbanc@18106
   740
apply(rule_tac r="r" in double_acc_aux)
urbanc@18106
   741
apply(assumption)+
urbanc@18106
   742
apply(blast)
urbanc@18106
   743
done
urbanc@18106
   744
urbanc@18263
   745
lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
urbanc@18106
   746
apply(simp)
urbanc@18106
   747
apply(clarify)
urbanc@18106
   748
apply(subgoal_tac "t\<in>termi Beta")(*1*)
urbanc@18106
   749
apply(erule rev_mp)
urbanc@18106
   750
apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
urbanc@18106
   751
apply(erule rev_mp)
urbanc@18106
   752
apply(rule_tac a="t" and b="u" in double_acc)
urbanc@18106
   753
apply(assumption)
urbanc@18106
   754
apply(subgoal_tac "CR1 \<tau>")(*A*)
urbanc@18106
   755
apply(simp add: CR1_def SN_def)
urbanc@18106
   756
(*A*)
urbanc@18106
   757
apply(force simp add: RED_props)
urbanc@18106
   758
apply(simp)
urbanc@18106
   759
apply(clarify)
urbanc@18106
   760
apply(subgoal_tac "CR3 \<sigma>")(*B*)
urbanc@18106
   761
apply(simp add: CR3_def)
urbanc@18106
   762
apply(rotate_tac 6)
urbanc@18106
   763
apply(drule_tac x="App(Lam[x].xa ) z" in spec)
urbanc@18106
   764
apply(drule mp)
urbanc@18106
   765
apply(rule conjI)
urbanc@18106
   766
apply(force simp add: NEUT_def)
urbanc@18106
   767
apply(simp add: CR3_RED_def)
urbanc@18106
   768
apply(clarify)
urbanc@18106
   769
apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
urbanc@18106
   770
apply(auto simp add: lam.inject lam.distinct)
urbanc@18106
   771
apply(drule beta_abs)
urbanc@18106
   772
apply(auto)
urbanc@18106
   773
apply(drule_tac x="t''" in spec)
urbanc@18106
   774
apply(simp)
urbanc@18106
   775
apply(drule mp)
urbanc@18106
   776
apply(clarify)
urbanc@18106
   777
apply(drule_tac x="s" in bspec)
urbanc@18106
   778
apply(assumption)
urbanc@18106
   779
apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta>  t'' [ x ::= s ]")(*B*)
urbanc@18106
   780
apply(subgoal_tac "CR2 \<sigma>")(*C*)
urbanc@18106
   781
apply(simp (no_asm_use) add: CR2_def)
urbanc@18106
   782
apply(blast)
urbanc@18106
   783
(*C*)
urbanc@18106
   784
apply(force simp add: RED_props)
urbanc@18106
   785
(*B*)
urbanc@18106
   786
apply(force intro!: beta_subst)
urbanc@18106
   787
apply(assumption)
urbanc@18106
   788
apply(rotate_tac 3)
urbanc@18106
   789
apply(drule_tac x="s2" in spec)
urbanc@18106
   790
apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)
urbanc@18106
   791
apply(simp)
urbanc@18106
   792
(*D*)
urbanc@18106
   793
apply(subgoal_tac "CR2 \<tau>")(*E*)
urbanc@18106
   794
apply(simp (no_asm_use) add: CR2_def)
urbanc@18106
   795
apply(blast)
urbanc@18106
   796
(*E*)
urbanc@18106
   797
apply(force simp add: RED_props)
urbanc@18106
   798
apply(simp add: alpha)
urbanc@18106
   799
apply(erule disjE)
urbanc@18106
   800
apply(force)
urbanc@18106
   801
apply(auto)
urbanc@18106
   802
apply(simp add: subst_rename)
urbanc@18106
   803
apply(drule_tac x="z" in bspec)
urbanc@18106
   804
apply(assumption)
urbanc@18106
   805
(*B*)
urbanc@18106
   806
apply(force simp add: RED_props)
urbanc@18106
   807
(*1*)
urbanc@18106
   808
apply(drule_tac x="Var x" in bspec)
urbanc@18106
   809
apply(subgoal_tac "CR3 \<tau>")(*2*) 
urbanc@18106
   810
apply(drule CR3_CR4)
urbanc@18106
   811
apply(simp add: CR4_def)
urbanc@18106
   812
apply(drule_tac x="Var x" in spec)
urbanc@18106
   813
apply(drule mp)
urbanc@18106
   814
apply(rule conjI)
urbanc@18106
   815
apply(force simp add: NEUT_def)
urbanc@18106
   816
apply(simp add: NORMAL_def)
urbanc@18106
   817
apply(clarify)
urbanc@18106
   818
apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
urbanc@18106
   819
apply(auto simp add: lam.inject lam.distinct)
urbanc@18106
   820
apply(force simp add: RED_props)
urbanc@18106
   821
apply(simp add: id_subs)
urbanc@18106
   822
apply(subgoal_tac "CR1 \<sigma>")(*3*)
urbanc@18106
   823
apply(simp add: CR1_def SN_def)
urbanc@18106
   824
(*3*)
urbanc@18106
   825
apply(force simp add: RED_props)
urbanc@18106
   826
done
urbanc@18106
   827
urbanc@18378
   828
lemma fresh_domain: 
urbanc@18378
   829
  assumes a: "a\<sharp>\<theta>"
urbanc@18378
   830
  shows "a\<notin>set(domain \<theta>)"
urbanc@18378
   831
using a
urbanc@18378
   832
apply(induct \<theta>)
urbanc@18263
   833
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
urbanc@18263
   834
done
urbanc@18263
   835
urbanc@18383
   836
lemma fresh_at: 
urbanc@18383
   837
  assumes a: "a\<in>set(domain \<theta>)" 
urbanc@18383
   838
  and     b: "c\<sharp>\<theta>" 
urbanc@18383
   839
  shows "c\<sharp>(\<theta><a>)"
urbanc@18383
   840
using a b
urbanc@18383
   841
apply(induct \<theta>)   
urbanc@18263
   842
apply(auto simp add: fresh_prod fresh_list_cons)
urbanc@18263
   843
done
urbanc@18263
   844
urbanc@18383
   845
lemma psubst_subst: 
urbanc@18383
   846
  assumes a: "c\<sharp>\<theta>"
urbanc@18383
   847
  shows "(t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
urbanc@18383
   848
using a
urbanc@18659
   849
apply(nominal_induct t avoiding: \<theta> c s rule: lam.induct)
urbanc@18263
   850
apply(auto dest: fresh_domain)
urbanc@18263
   851
apply(drule fresh_at)
urbanc@18263
   852
apply(assumption)
urbanc@18263
   853
apply(rule forget)
urbanc@18263
   854
apply(assumption)
urbanc@18659
   855
apply(subgoal_tac "name\<sharp>((c,s)#\<theta>)")(*A*)
urbanc@18313
   856
apply(simp)
urbanc@18263
   857
(*A*)
urbanc@18263
   858
apply(simp add: fresh_list_cons fresh_prod)
urbanc@18263
   859
done
urbanc@18106
   860
lemma all_RED: 
urbanc@18345
   861
  assumes a: "\<Gamma>\<turnstile>t:\<tau>"
urbanc@18345
   862
  and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
urbanc@18345
   863
  shows "t[<\<theta>>]\<in>RED \<tau>"
urbanc@18345
   864
using a b
urbanc@18659
   865
proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
urbanc@18345
   866
  case (Lam a t) --"lambda case"
urbanc@18345
   867
  have ih: "\<And>\<Gamma> \<tau> \<theta>. \<Gamma> \<turnstile> t:\<tau> \<Longrightarrow> 
urbanc@18345
   868
                    (\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>) 
urbanc@18345
   869
                    \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 
urbanc@18345
   870
  and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>" 
urbanc@18345
   871
  and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 
urbanc@18345
   872
  and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
urbanc@18345
   873
  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp
urbanc@18345
   874
  then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast
urbanc@18345
   875
  from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
urbanc@18345
   876
    by (force dest: fresh_context simp add: psubst_subst)
urbanc@18345
   877
  hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
urbanc@18345
   878
  thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
urbanc@18345
   879
qed (force dest!: t1_elim t2_elim)+
urbanc@18345
   880
urbanc@19218
   881
urbanc@19218
   882
lemma all_RED: 
urbanc@19218
   883
  assumes a: "\<Gamma>\<turnstile>t:\<tau>"
urbanc@19218
   884
  and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
urbanc@19218
   885
  shows "t[<\<theta>>]\<in>RED \<tau>"
urbanc@19218
   886
using a b
urbanc@19218
   887
proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
urbanc@19218
   888
  case (Lam a t) --"lambda case"
urbanc@19218
   889
  have ih: "\<And>\<Gamma> \<tau> \<theta>. \<lbrakk>\<Gamma> \<turnstile> t:\<tau>; \<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>\<rbrakk> 
urbanc@19218
   890
                    \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 
urbanc@19218
   891
  and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>" 
urbanc@19218
   892
  and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 
urbanc@19218
   893
  and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
urbanc@19218
   894
  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp
urbanc@19218
   895
  then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast
urbanc@19218
   896
  from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
urbanc@19218
   897
    by (force dest: fresh_context simp add: psubst_subst)
urbanc@19218
   898
  hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
urbanc@19218
   899
  thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
urbanc@19218
   900
qed (force dest!: t1_elim t2_elim)+
urbanc@19218
   901
urbanc@18383
   902
(* identity substitution generated from a context \<Gamma> *)
urbanc@18382
   903
consts
urbanc@18382
   904
  "id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list"
urbanc@18382
   905
primrec
urbanc@18382
   906
  "id []    = []"
urbanc@18382
   907
  "id (x#\<Gamma>) = ((fst x),Var (fst x))#(id \<Gamma>)"
urbanc@18382
   908
urbanc@18382
   909
lemma id_var:
urbanc@18382
   910
  assumes a: "a \<in> set (domain (id \<Gamma>))"
urbanc@18382
   911
  shows "(id \<Gamma>)<a> = Var a"
urbanc@18382
   912
using a
urbanc@18382
   913
apply(induct \<Gamma>, auto)
urbanc@18382
   914
done
urbanc@18382
   915
urbanc@18382
   916
lemma id_fresh:
urbanc@18382
   917
  fixes a::"name"
urbanc@18382
   918
  assumes a: "a\<sharp>\<Gamma>"
urbanc@18382
   919
  shows "a\<sharp>(id \<Gamma>)"
urbanc@18382
   920
using a
urbanc@18382
   921
apply(induct \<Gamma>)
urbanc@18382
   922
apply(auto simp add: fresh_list_nil fresh_list_cons fresh_prod)
urbanc@18382
   923
done
urbanc@18382
   924
urbanc@18382
   925
lemma id_apply:  
urbanc@18382
   926
  shows "t[<(id \<Gamma>)>] = t"
urbanc@18659
   927
apply(nominal_induct t avoiding: \<Gamma> rule: lam.induct)
urbanc@18382
   928
apply(auto)
urbanc@18382
   929
apply(simp add: id_var)
urbanc@18382
   930
apply(drule id_fresh)+
urbanc@18382
   931
apply(simp)
urbanc@18382
   932
done
urbanc@18382
   933
urbanc@18382
   934
lemma id_mem:
urbanc@18382
   935
  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
urbanc@18382
   936
  shows "a \<in> set (domain (id \<Gamma>))"
urbanc@18382
   937
using a
urbanc@18382
   938
apply(induct \<Gamma>, auto)
urbanc@18382
   939
done
urbanc@18382
   940
urbanc@18383
   941
lemma id_prop:
urbanc@18383
   942
  shows "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain (id \<Gamma>))\<and>(id \<Gamma>)<a>\<in>RED \<sigma>)"
urbanc@18383
   943
apply(auto)
urbanc@18382
   944
apply(simp add: id_mem)
urbanc@18382
   945
apply(frule id_mem)
urbanc@18382
   946
apply(simp add: id_var)
urbanc@18383
   947
apply(subgoal_tac "CR3 \<sigma>")(*A*)
urbanc@18382
   948
apply(drule CR3_CR4)
urbanc@18382
   949
apply(simp add: CR4_def)
urbanc@18382
   950
apply(drule_tac x="Var a" in spec)
urbanc@18383
   951
apply(force simp add: NEUT_def NORMAL_Var)
urbanc@18383
   952
(*A*)
urbanc@18383
   953
apply(rule RED_props)
urbanc@18382
   954
done
urbanc@18382
   955
urbanc@18383
   956
lemma typing_implies_RED:  
urbanc@18383
   957
  assumes a: "\<Gamma>\<turnstile>t:\<tau>"
urbanc@18383
   958
  shows "t \<in> RED \<tau>"
urbanc@18383
   959
proof -
urbanc@18383
   960
  have "t[<id \<Gamma>>]\<in>RED \<tau>" 
urbanc@18383
   961
  proof -
urbanc@18383
   962
    have "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain (id \<Gamma>))\<and>(id \<Gamma>)<a>\<in>RED \<sigma>)" by (rule id_prop)
urbanc@18383
   963
    with a show ?thesis by (rule all_RED)
urbanc@18383
   964
  qed
urbanc@18383
   965
  thus"t \<in> RED \<tau>" by (simp add: id_apply)
urbanc@18383
   966
qed
urbanc@18383
   967
urbanc@18383
   968
lemma typing_implies_SN: 
urbanc@18383
   969
  assumes a: "\<Gamma>\<turnstile>t:\<tau>"
urbanc@18383
   970
  shows "SN(t)"
urbanc@18383
   971
proof -
urbanc@18383
   972
  from a have "t \<in> RED \<tau>" by (rule typing_implies_RED)
urbanc@18383
   973
  moreover
urbanc@18383
   974
  have "CR1 \<tau>" by (rule RED_props)
urbanc@18383
   975
  ultimately show "SN(t)" by (simp add: CR1_def)
urbanc@18383
   976
qed
urbanc@18382
   977
urbanc@18382
   978
end