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