author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 39157  b98909faaea8 
child 58622  aa99568f56de 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs 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{MatthesESSLLI2000}, 
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  147 
from Abs(4) have "lift s 0 \<rightarrow>\<^sub>s lift s' 0" by (rule sred_lift) 
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  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 