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