src/HOL/Lambda/Standardization.thy
author nipkow
Thu Dec 11 08:52:50 2008 +0100 (2008-12-11)
changeset 29106 25e28a4070f3
parent 25107 dbf09ca6a80e
child 36862 952b2b102a0a
permissions -rw-r--r--
Testfile for Stefan's code generator
berghofe@24538
     1
(*  Title:      HOL/Lambda/Standardization.thy
berghofe@24538
     2
    ID:         $Id$
berghofe@24538
     3
    Author:     Stefan Berghofer
berghofe@24538
     4
    Copyright   2005 TU Muenchen
berghofe@24538
     5
*)
berghofe@24538
     6
berghofe@24538
     7
header {* Standardization *}
berghofe@24538
     8
berghofe@24538
     9
theory Standardization
berghofe@24538
    10
imports NormalForm
berghofe@24538
    11
begin
berghofe@24538
    12
berghofe@24538
    13
text {*
berghofe@24538
    14
Based on lecture notes by Ralph Matthes \cite{Matthes-ESSLLI2000},
berghofe@24538
    15
original proof idea due to Ralph Loader \cite{Loader1998}.
berghofe@24538
    16
*}
berghofe@24538
    17
berghofe@24538
    18
berghofe@24538
    19
subsection {* Standard reduction relation *}
berghofe@24538
    20
berghofe@24538
    21
declare listrel_mono [mono_set]
berghofe@24538
    22
berghofe@24538
    23
inductive
berghofe@24538
    24
  sred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>s" 50)
berghofe@24538
    25
  and sredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>s]" 50)
berghofe@24538
    26
where
berghofe@24538
    27
  "s [\<rightarrow>\<^sub>s] t \<equiv> listrelp op \<rightarrow>\<^sub>s s t"
berghofe@24538
    28
| Var: "rs [\<rightarrow>\<^sub>s] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> rs'"
berghofe@24538
    29
| Abs: "r \<rightarrow>\<^sub>s r' \<Longrightarrow> ss [\<rightarrow>\<^sub>s] ss' \<Longrightarrow> Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> ss'"
berghofe@24538
    30
| Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t"
berghofe@24538
    31
berghofe@24538
    32
lemma refl_listrelp: "\<forall>x\<in>set xs. R x x \<Longrightarrow> listrelp R xs xs"
berghofe@24538
    33
  by (induct xs) (auto intro: listrelp.intros)
berghofe@24538
    34
berghofe@24538
    35
lemma refl_sred: "t \<rightarrow>\<^sub>s t"
berghofe@24538
    36
  by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros)
berghofe@24538
    37
berghofe@24538
    38
lemma refl_sreds: "ts [\<rightarrow>\<^sub>s] ts"
berghofe@24538
    39
  by (simp add: refl_sred refl_listrelp)
berghofe@24538
    40
berghofe@24538
    41
lemma listrelp_conj1: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp R x y"
berghofe@24538
    42
  by (erule listrelp.induct) (auto intro: listrelp.intros)
berghofe@24538
    43
berghofe@24538
    44
lemma listrelp_conj2: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp S x y"
berghofe@24538
    45
  by (erule listrelp.induct) (auto intro: listrelp.intros)
berghofe@24538
    46
berghofe@24538
    47
lemma listrelp_app:
berghofe@24538
    48
  assumes xsys: "listrelp R xs ys"
berghofe@24538
    49
  shows "listrelp R xs' ys' \<Longrightarrow> listrelp R (xs @ xs') (ys @ ys')" using xsys
berghofe@24538
    50
  by (induct arbitrary: xs' ys') (auto intro: listrelp.intros)
berghofe@24538
    51
berghofe@24538
    52
lemma lemma1:
berghofe@24538
    53
  assumes r: "r \<rightarrow>\<^sub>s r'" and s: "s \<rightarrow>\<^sub>s s'"
berghofe@24538
    54
  shows "r \<degree> s \<rightarrow>\<^sub>s r' \<degree> s'" using r
berghofe@24538
    55
proof induct
berghofe@24538
    56
  case (Var rs rs' x)
berghofe@24538
    57
  then have "rs [\<rightarrow>\<^sub>s] rs'" by (rule listrelp_conj1)
berghofe@24538
    58
  moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
berghofe@24538
    59
  ultimately have "rs @ [s] [\<rightarrow>\<^sub>s] rs' @ [s']" by (rule listrelp_app)
berghofe@24538
    60
  hence "Var x \<degree>\<degree> (rs @ [s]) \<rightarrow>\<^sub>s Var x \<degree>\<degree> (rs' @ [s'])" by (rule sred.Var)
berghofe@24538
    61
  thus ?case by (simp only: app_last)
berghofe@24538
    62
next
berghofe@24538
    63
  case (Abs r r' ss ss')
berghofe@24538
    64
  from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1)
berghofe@24538
    65
  moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
berghofe@24538
    66
  ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app)
berghofe@24538
    67
  with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
berghofe@24538
    68
    by (rule sred.Abs)
berghofe@24538
    69
  thus ?case by (simp only: app_last)
berghofe@24538
    70
next
berghofe@24538
    71
  case (Beta r u ss t)
berghofe@24538
    72
  hence "r[u/0] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last)
berghofe@24538
    73
  hence "Abs r \<degree> u \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (rule sred.Beta)
berghofe@24538
    74
  thus ?case by (simp only: app_last)
berghofe@24538
    75
qed
berghofe@24538
    76
berghofe@24538
    77
lemma lemma1':
berghofe@24538
    78
  assumes ts: "ts [\<rightarrow>\<^sub>s] ts'"
berghofe@24538
    79
  shows "r \<rightarrow>\<^sub>s r' \<Longrightarrow> r \<degree>\<degree> ts \<rightarrow>\<^sub>s r' \<degree>\<degree> ts'" using ts
berghofe@24538
    80
  by (induct arbitrary: r r') (auto intro: lemma1)
berghofe@24538
    81
berghofe@24538
    82
lemma lemma2_1:
berghofe@24538
    83
  assumes beta: "t \<rightarrow>\<^sub>\<beta> u"
berghofe@24538
    84
  shows "t \<rightarrow>\<^sub>s u" using beta
berghofe@24538
    85
proof induct
berghofe@24538
    86
  case (beta s t)
berghofe@24538
    87
  have "Abs s \<degree> t \<degree>\<degree> [] \<rightarrow>\<^sub>s s[t/0] \<degree>\<degree> []" by (iprover intro: sred.Beta refl_sred)
berghofe@24538
    88
  thus ?case by simp
berghofe@24538
    89
next
berghofe@24538
    90
  case (appL s t u)
berghofe@24538
    91
  thus ?case by (iprover intro: lemma1 refl_sred)
berghofe@24538
    92
next
berghofe@24538
    93
  case (appR s t u)
berghofe@24538
    94
  thus ?case by (iprover intro: lemma1 refl_sred)
berghofe@24538
    95
next
berghofe@24538
    96
  case (abs s t)
berghofe@24538
    97
  hence "Abs s \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs t \<degree>\<degree> []" by (iprover intro: sred.Abs listrelp.Nil)
berghofe@24538
    98
  thus ?case by simp
berghofe@24538
    99
qed
berghofe@24538
   100
berghofe@24538
   101
lemma listrelp_betas:
berghofe@24538
   102
  assumes ts: "listrelp op \<rightarrow>\<^sub>\<beta>\<^sup>* ts ts'"
berghofe@24538
   103
  shows "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<degree>\<degree> ts'" using ts
berghofe@24538
   104
  by induct auto
berghofe@24538
   105
berghofe@24538
   106
lemma lemma2_2:
berghofe@24538
   107
  assumes t: "t \<rightarrow>\<^sub>s u"
berghofe@24538
   108
  shows "t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using t
berghofe@24538
   109
  by induct (auto dest: listrelp_conj2
berghofe@24538
   110
    intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)
berghofe@24538
   111
berghofe@24538
   112
lemma sred_lift:
berghofe@24538
   113
  assumes s: "s \<rightarrow>\<^sub>s t"
berghofe@24538
   114
  shows "lift s i \<rightarrow>\<^sub>s lift t i" using s
berghofe@24538
   115
proof (induct arbitrary: i)
berghofe@24538
   116
  case (Var rs rs' x)
berghofe@24538
   117
  hence "map (\<lambda>t. lift t i) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) rs'"
berghofe@24538
   118
    by induct (auto intro: listrelp.intros)
berghofe@24538
   119
  thus ?case by (cases "x < i") (auto intro: sred.Var)
berghofe@24538
   120
next
berghofe@24538
   121
  case (Abs r r' ss ss')
berghofe@24538
   122
  from Abs(3) have "map (\<lambda>t. lift t i) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) ss'"
berghofe@24538
   123
    by induct (auto intro: listrelp.intros)
berghofe@24538
   124
  thus ?case by (auto intro: sred.Abs Abs)
berghofe@24538
   125
next
berghofe@24538
   126
  case (Beta r s ss t)
berghofe@24538
   127
  thus ?case by (auto intro: sred.Beta)
berghofe@24538
   128
qed
berghofe@24538
   129
berghofe@24538
   130
lemma lemma3:
berghofe@24538
   131
  assumes r: "r \<rightarrow>\<^sub>s r'"
berghofe@24538
   132
  shows "s \<rightarrow>\<^sub>s s' \<Longrightarrow> r[s/x] \<rightarrow>\<^sub>s r'[s'/x]" using r
berghofe@24538
   133
proof (induct arbitrary: s s' x)
berghofe@24538
   134
  case (Var rs rs' y)
berghofe@24538
   135
  hence "map (\<lambda>t. t[s/x]) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) rs'"
berghofe@24538
   136
    by induct (auto intro: listrelp.intros Var)
berghofe@24538
   137
  moreover have "Var y[s/x] \<rightarrow>\<^sub>s Var y[s'/x]"
berghofe@24538
   138
  proof (cases "y < x")
berghofe@24538
   139
    case True thus ?thesis by simp (rule refl_sred)
berghofe@24538
   140
  next
berghofe@24538
   141
    case False
berghofe@24538
   142
    thus ?thesis
berghofe@24538
   143
      by (cases "y = x") (auto simp add: Var intro: refl_sred)
berghofe@24538
   144
  qed
berghofe@24538
   145
  ultimately show ?case by simp (rule lemma1')
berghofe@24538
   146
next
berghofe@24538
   147
  case (Abs r r' ss ss')
wenzelm@25107
   148
  from Abs(4) have "lift s 0 \<rightarrow>\<^sub>s lift s' 0" by (rule sred_lift)
wenzelm@25107
   149
  hence "r[lift s 0/Suc x] \<rightarrow>\<^sub>s r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps)
berghofe@24538
   150
  moreover from Abs(3) have "map (\<lambda>t. t[s/x]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) ss'"
berghofe@24538
   151
    by induct (auto intro: listrelp.intros Abs)
berghofe@24538
   152
  ultimately show ?case by simp (rule sred.Abs)
berghofe@24538
   153
next
berghofe@24538
   154
  case (Beta r u ss t)
berghofe@24538
   155
  thus ?case by (auto simp add: subst_subst intro: sred.Beta)
berghofe@24538
   156
qed
berghofe@24538
   157
berghofe@24538
   158
lemma lemma4_aux:
berghofe@24538
   159
  assumes rs: "listrelp (\<lambda>t u. t \<rightarrow>\<^sub>s u \<and> (\<forall>r. u \<rightarrow>\<^sub>\<beta> r \<longrightarrow> t \<rightarrow>\<^sub>s r)) rs rs'"
berghofe@24538
   160
  shows "rs' => ss \<Longrightarrow> rs [\<rightarrow>\<^sub>s] ss" using rs
berghofe@24538
   161
proof (induct arbitrary: ss)
berghofe@24538
   162
  case Nil
berghofe@24538
   163
  thus ?case by cases (auto intro: listrelp.Nil)
berghofe@24538
   164
next
berghofe@24538
   165
  case (Cons x y xs ys)
berghofe@24538
   166
  note Cons' = Cons
berghofe@24538
   167
  show ?case
berghofe@24538
   168
  proof (cases ss)
berghofe@24538
   169
    case Nil with Cons show ?thesis by simp
berghofe@24538
   170
  next
berghofe@24538
   171
    case (Cons y' ys')
berghofe@24538
   172
    hence ss: "ss = y' # ys'" by simp
berghofe@24538
   173
    from Cons Cons' have "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys \<or> y' = y \<and> ys => ys'" by simp
berghofe@24538
   174
    hence "x # xs [\<rightarrow>\<^sub>s] y' # ys'"
berghofe@24538
   175
    proof
berghofe@24538
   176
      assume H: "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys"
berghofe@24538
   177
      with Cons' have "x \<rightarrow>\<^sub>s y'" by blast
berghofe@24538
   178
      moreover from Cons' have "xs [\<rightarrow>\<^sub>s] ys" by (iprover dest: listrelp_conj1)
berghofe@24538
   179
      ultimately have "x # xs [\<rightarrow>\<^sub>s] y' # ys" by (rule listrelp.Cons)
berghofe@24538
   180
      with H show ?thesis by simp
berghofe@24538
   181
    next
berghofe@24538
   182
      assume H: "y' = y \<and> ys => ys'"
berghofe@24538
   183
      with Cons' have "x \<rightarrow>\<^sub>s y'" by blast
berghofe@24538
   184
      moreover from H have "xs [\<rightarrow>\<^sub>s] ys'" by (blast intro: Cons')
berghofe@24538
   185
      ultimately show ?thesis by (rule listrelp.Cons)
berghofe@24538
   186
    qed
berghofe@24538
   187
    with ss show ?thesis by simp
berghofe@24538
   188
  qed
berghofe@24538
   189
qed
berghofe@24538
   190
berghofe@24538
   191
lemma lemma4:
berghofe@24538
   192
  assumes r: "r \<rightarrow>\<^sub>s r'"
berghofe@24538
   193
  shows "r' \<rightarrow>\<^sub>\<beta> r'' \<Longrightarrow> r \<rightarrow>\<^sub>s r''" using r
berghofe@24538
   194
proof (induct arbitrary: r'')
berghofe@24538
   195
  case (Var rs rs' x)
berghofe@24538
   196
  then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x \<degree>\<degree> ss"
berghofe@24538
   197
    by (blast dest: head_Var_reduction)
berghofe@24538
   198
  from Var(1) rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux)
berghofe@24538
   199
  hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var)
berghofe@24538
   200
  with r'' show ?case by simp
berghofe@24538
   201
next
berghofe@24538
   202
  case (Abs r r' ss ss')
berghofe@24538
   203
  from `Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''` show ?case
berghofe@24538
   204
  proof
berghofe@24538
   205
    fix s
berghofe@24538
   206
    assume r'': "r'' = s \<degree>\<degree> ss'"
berghofe@24538
   207
    assume "Abs r' \<rightarrow>\<^sub>\<beta> s"
berghofe@24538
   208
    then obtain r''' where s: "s = Abs r'''" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" by cases auto
berghofe@24538
   209
    from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs)
berghofe@24538
   210
    moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1)
berghofe@24538
   211
    ultimately have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r''' \<degree>\<degree> ss'" by (rule sred.Abs)
berghofe@24538
   212
    with r'' s show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
berghofe@24538
   213
  next
berghofe@24538
   214
    fix rs'
berghofe@24538
   215
    assume "ss' => rs'"
berghofe@24538
   216
    with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux)
berghofe@24538
   217
    with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
berghofe@24538
   218
    moreover assume "r'' = Abs r' \<degree>\<degree> rs'"
berghofe@24538
   219
    ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
berghofe@24538
   220
  next
berghofe@24538
   221
    fix t u' us'
berghofe@24538
   222
    assume "ss' = u' # us'"
berghofe@24538
   223
    with Abs(3) obtain u us where
berghofe@24538
   224
      ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'"
berghofe@24538
   225
      by cases (auto dest!: listrelp_conj1)
wenzelm@25107
   226
    have "r[u/0] \<rightarrow>\<^sub>s r'[u'/0]" using Abs(1) and u by (rule lemma3)
berghofe@24538
   227
    with us have "r[u/0] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule lemma1')
berghofe@24538
   228
    hence "Abs r \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule sred.Beta)
berghofe@24538
   229
    moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] \<degree>\<degree> us'"
berghofe@24538
   230
    ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" using ss by simp
berghofe@24538
   231
  qed
berghofe@24538
   232
next
berghofe@24538
   233
  case (Beta r s ss t)
berghofe@24538
   234
  show ?case
berghofe@24538
   235
    by (rule sred.Beta) (rule Beta)+
berghofe@24538
   236
qed
berghofe@24538
   237
berghofe@24538
   238
lemma rtrancl_beta_sred:
berghofe@24538
   239
  assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'"
berghofe@24538
   240
  shows "r \<rightarrow>\<^sub>s r'" using r
berghofe@24538
   241
  by induct (iprover intro: refl_sred lemma4)+
berghofe@24538
   242
berghofe@24538
   243
berghofe@24538
   244
subsection {* Leftmost reduction and weakly normalizing terms *}
berghofe@24538
   245
berghofe@24538
   246
inductive
berghofe@24538
   247
  lred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>l" 50)
berghofe@24538
   248
  and lredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>l]" 50)
berghofe@24538
   249
where
berghofe@24538
   250
  "s [\<rightarrow>\<^sub>l] t \<equiv> listrelp op \<rightarrow>\<^sub>l s t"
berghofe@24538
   251
| Var: "rs [\<rightarrow>\<^sub>l] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>l Var x \<degree>\<degree> rs'"
berghofe@24538
   252
| Abs: "r \<rightarrow>\<^sub>l r' \<Longrightarrow> Abs r \<rightarrow>\<^sub>l Abs r'"
berghofe@24538
   253
| Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>l t"
berghofe@24538
   254
berghofe@24538
   255
lemma lred_imp_sred:
berghofe@24538
   256
  assumes lred: "s \<rightarrow>\<^sub>l t"
berghofe@24538
   257
  shows "s \<rightarrow>\<^sub>s t" using lred
berghofe@24538
   258
proof induct
berghofe@24538
   259
  case (Var rs rs' x)
berghofe@24538
   260
  then have "rs [\<rightarrow>\<^sub>s] rs'"
berghofe@24538
   261
    by induct (iprover intro: listrelp.intros)+
berghofe@24538
   262
  then show ?case by (rule sred.Var)
berghofe@24538
   263
next
berghofe@24538
   264
  case (Abs r r')
berghofe@24538
   265
  from `r \<rightarrow>\<^sub>s r'`
berghofe@24538
   266
  have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil
berghofe@24538
   267
    by (rule sred.Abs)
berghofe@24538
   268
  then show ?case by simp
berghofe@24538
   269
next
berghofe@24538
   270
  case (Beta r s ss t)
berghofe@24538
   271
  from `r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t`
berghofe@24538
   272
  show ?case by (rule sred.Beta)
berghofe@24538
   273
qed
berghofe@24538
   274
berghofe@24538
   275
inductive WN :: "dB => bool"
berghofe@24538
   276
  where
berghofe@24538
   277
    Var: "listsp WN rs \<Longrightarrow> WN (Var n \<degree>\<degree> rs)"
berghofe@24538
   278
  | Lambda: "WN r \<Longrightarrow> WN (Abs r)"
berghofe@24538
   279
  | Beta: "WN ((r[s/0]) \<degree>\<degree> ss) \<Longrightarrow> WN ((Abs r \<degree> s) \<degree>\<degree> ss)"
berghofe@24538
   280
berghofe@24538
   281
lemma listrelp_imp_listsp1:
berghofe@24538
   282
  assumes H: "listrelp (\<lambda>x y. P x) xs ys"
berghofe@24538
   283
  shows "listsp P xs" using H
berghofe@24538
   284
  by induct auto
berghofe@24538
   285
berghofe@24538
   286
lemma listrelp_imp_listsp2:
berghofe@24538
   287
  assumes H: "listrelp (\<lambda>x y. P y) xs ys"
berghofe@24538
   288
  shows "listsp P ys" using H
berghofe@24538
   289
  by induct auto
berghofe@24538
   290
berghofe@24538
   291
lemma lemma5:
berghofe@24538
   292
  assumes lred: "r \<rightarrow>\<^sub>l r'"
berghofe@24538
   293
  shows "WN r" and "NF r'" using lred
berghofe@24538
   294
  by induct
berghofe@24538
   295
    (iprover dest: listrelp_conj1 listrelp_conj2
berghofe@24538
   296
     listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros
berghofe@24538
   297
     NF.intros [simplified listall_listsp_eq])+
berghofe@24538
   298
berghofe@24538
   299
lemma lemma6:
berghofe@24538
   300
  assumes wn: "WN r"
berghofe@24538
   301
  shows "\<exists>r'. r \<rightarrow>\<^sub>l r'" using wn
berghofe@24538
   302
proof induct
berghofe@24538
   303
  case (Var rs n)
berghofe@24538
   304
  then have "\<exists>rs'. rs [\<rightarrow>\<^sub>l] rs'"
berghofe@24538
   305
    by induct (iprover intro: listrelp.intros)+
berghofe@24538
   306
  then show ?case by (iprover intro: lred.Var)
berghofe@24538
   307
qed (iprover intro: lred.intros)+
berghofe@24538
   308
berghofe@24538
   309
lemma lemma7:
berghofe@24538
   310
  assumes r: "r \<rightarrow>\<^sub>s r'"
berghofe@24538
   311
  shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r
berghofe@24538
   312
proof induct
berghofe@24538
   313
  case (Var rs rs' x)
berghofe@24538
   314
  from `NF (Var x \<degree>\<degree> rs')` have "listall NF rs'"
berghofe@24538
   315
    by cases simp_all
berghofe@24538
   316
  with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'"
berghofe@24538
   317
  proof induct
berghofe@24538
   318
    case Nil
berghofe@24538
   319
    show ?case by (rule listrelp.Nil)
berghofe@24538
   320
  next
berghofe@24538
   321
    case (Cons x y xs ys)
berghofe@24538
   322
    hence "x \<rightarrow>\<^sub>l y" and "xs [\<rightarrow>\<^sub>l] ys" by simp_all
berghofe@24538
   323
    thus ?case by (rule listrelp.Cons)
berghofe@24538
   324
  qed
berghofe@24538
   325
  thus ?case by (rule lred.Var)
berghofe@24538
   326
next
berghofe@24538
   327
  case (Abs r r' ss ss')
berghofe@24538
   328
  from `NF (Abs r' \<degree>\<degree> ss')`
berghofe@24538
   329
  have ss': "ss' = []" by (rule Abs_NF)
berghofe@24538
   330
  from Abs(3) have ss: "ss = []" using ss'
berghofe@24538
   331
    by cases simp_all
berghofe@24538
   332
  from ss' Abs have "NF (Abs r')" by simp
berghofe@24538
   333
  hence "NF r'" by cases simp_all
berghofe@24538
   334
  with Abs have "r \<rightarrow>\<^sub>l r'" by simp
berghofe@24538
   335
  hence "Abs r \<rightarrow>\<^sub>l Abs r'" by (rule lred.Abs)
berghofe@24538
   336
  with ss ss' show ?case by simp
berghofe@24538
   337
next
berghofe@24538
   338
  case (Beta r s ss t)
berghofe@24538
   339
  hence "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t" by simp
berghofe@24538
   340
  thus ?case by (rule lred.Beta)
berghofe@24538
   341
qed
berghofe@24538
   342
berghofe@24538
   343
lemma WN_eq: "WN t = (\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')"
berghofe@24538
   344
proof
berghofe@24538
   345
  assume "WN t"
berghofe@24538
   346
  then have "\<exists>t'. t \<rightarrow>\<^sub>l t'" by (rule lemma6)
berghofe@24538
   347
  then obtain t' where t': "t \<rightarrow>\<^sub>l t'" ..
berghofe@24538
   348
  then have NF: "NF t'" by (rule lemma5)
berghofe@24538
   349
  from t' have "t \<rightarrow>\<^sub>s t'" by (rule lred_imp_sred)
berghofe@24538
   350
  then have "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" by (rule lemma2_2)
berghofe@24538
   351
  with NF show "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by iprover
berghofe@24538
   352
next
berghofe@24538
   353
  assume "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
berghofe@24538
   354
  then obtain t' where t': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and NF: "NF t'"
berghofe@24538
   355
    by iprover
berghofe@24538
   356
  from t' have "t \<rightarrow>\<^sub>s t'" by (rule rtrancl_beta_sred)
berghofe@24538
   357
  then have "t \<rightarrow>\<^sub>l t'" using NF by (rule lemma7)
berghofe@24538
   358
  then show "WN t" by (rule lemma5)
berghofe@24538
   359
qed
berghofe@24538
   360
berghofe@24538
   361
end