author | wenzelm |
Fri, 17 Nov 2006 02:20:03 +0100 | |
changeset 21404 | eb85850d3eb7 |
parent 21210 | c17fd2df4e9e |
child 22272 | aac2ac7c32fd |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Eta.thy |
2 |
ID: $Id$ |
|
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
3 |
Author: Tobias Nipkow and Stefan Berghofer |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
4 |
Copyright 1995, 2005 TU Muenchen |
1269 | 5 |
*) |
6 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
7 |
header {* Eta-reduction *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
8 |
|
16417 | 9 |
theory Eta imports ParRed begin |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
10 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
11 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
12 |
subsection {* Definition of eta-reduction and relatives *} |
1269 | 13 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
14 |
consts |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
15 |
free :: "dB => nat => bool" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
16 |
primrec |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
17 |
"free (Var j) i = (j = i)" |
12011 | 18 |
"free (s \<degree> t) i = (free s i \<or> free t i)" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
19 |
"free (Abs s) i = free s (i + 1)" |
1269 | 20 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
21 |
consts |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
22 |
eta :: "(dB \<times> dB) set" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
23 |
|
19363 | 24 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
25 |
eta_red :: "[dB, dB] => bool" (infixl "-e>" 50) where |
19363 | 26 |
"s -e> t == (s, t) \<in> eta" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
27 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
28 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
29 |
eta_reds :: "[dB, dB] => bool" (infixl "-e>>" 50) where |
19363 | 30 |
"s -e>> t == (s, t) \<in> eta^*" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
31 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
32 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
33 |
eta_red0 :: "[dB, dB] => bool" (infixl "-e>=" 50) where |
19363 | 34 |
"s -e>= t == (s, t) \<in> eta^=" |
1269 | 35 |
|
1789 | 36 |
inductive eta |
11638 | 37 |
intros |
12011 | 38 |
eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]" |
39 |
appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u" |
|
40 |
appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t" |
|
11638 | 41 |
abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
42 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
43 |
inductive_cases eta_cases [elim!]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
44 |
"Abs s -e> z" |
12011 | 45 |
"s \<degree> t -e> u" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
46 |
"Var i -e> t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
47 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
48 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
49 |
subsection "Properties of eta, subst and free" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
50 |
|
18241 | 51 |
lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]" |
20503 | 52 |
by (induct s arbitrary: i t u) (simp_all add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
53 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
54 |
lemma free_lift [simp]: |
18241 | 55 |
"free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))" |
20503 | 56 |
apply (induct t arbitrary: i k) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19656
diff
changeset
|
57 |
apply (auto cong: conj_cong) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
58 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
59 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
60 |
lemma free_subst [simp]: |
18241 | 61 |
"free (s[t/k]) i = |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
62 |
(free s k \<and> free t i \<or> free s (if i < k then i else i + 1))" |
20503 | 63 |
apply (induct s arbitrary: i k t) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
64 |
prefer 2 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
65 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
66 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
67 |
prefer 2 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
68 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
69 |
apply (simp add: diff_Suc subst_Var split: nat.split) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
70 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
71 |
|
18257 | 72 |
lemma free_eta: "s -e> t ==> free t i = free s i" |
20503 | 73 |
by (induct arbitrary: i set: eta) (simp_all cong: conj_cong) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
74 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
75 |
lemma not_free_eta: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
76 |
"[| s -e> t; \<not> free s i |] ==> \<not> free t i" |
18241 | 77 |
by (simp add: free_eta) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
78 |
|
18241 | 79 |
lemma eta_subst [simp]: |
18257 | 80 |
"s -e> t ==> s[u/i] -e> t[u/i]" |
20503 | 81 |
by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
82 |
|
18241 | 83 |
theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s" |
20503 | 84 |
by (induct s arbitrary: i dummy) simp_all |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
85 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
86 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
87 |
subsection "Confluence of eta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
88 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
89 |
lemma square_eta: "square eta eta (eta^=) (eta^=)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
90 |
apply (unfold square_def id_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
91 |
apply (rule impI [THEN allI [THEN allI]]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
92 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
93 |
apply (erule eta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
94 |
apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
95 |
apply safe |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
96 |
prefer 5 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
97 |
apply (blast intro!: eta_subst intro: free_eta [THEN iffD1]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
98 |
apply blast+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
99 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
100 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
101 |
theorem eta_confluent: "confluent eta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
102 |
apply (rule square_eta [THEN square_reflcl_confluent]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
103 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
104 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
105 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
106 |
subsection "Congruence rules for eta*" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
107 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
108 |
lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'" |
18241 | 109 |
by (induct set: rtrancl) |
110 |
(blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
111 |
|
12011 | 112 |
lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t" |
18241 | 113 |
by (induct set: rtrancl) |
114 |
(blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
115 |
|
12011 | 116 |
lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'" |
18241 | 117 |
by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
118 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
119 |
lemma rtrancl_eta_App: |
12011 | 120 |
"[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'" |
18241 | 121 |
by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
122 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
123 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
124 |
subsection "Commutation of beta and eta" |
1900 | 125 |
|
18241 | 126 |
lemma free_beta: |
18257 | 127 |
"s -> t ==> free t i \<Longrightarrow> free s i" |
20503 | 128 |
by (induct arbitrary: i set: beta) auto |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
129 |
|
18257 | 130 |
lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]" |
20503 | 131 |
by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
132 |
|
18241 | 133 |
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]" |
20503 | 134 |
by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
135 |
|
18257 | 136 |
lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i" |
20503 | 137 |
by (induct arbitrary: i set: eta) simp_all |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
138 |
|
18241 | 139 |
lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]" |
20503 | 140 |
apply (induct u arbitrary: s t i) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
141 |
apply (simp_all add: subst_Var) |
18241 | 142 |
apply blast |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
143 |
apply (blast intro: rtrancl_eta_App) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
144 |
apply (blast intro!: rtrancl_eta_Abs eta_lift) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
145 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
146 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
147 |
lemma square_beta_eta: "square beta eta (eta^*) (beta^=)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
148 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
149 |
apply (rule impI [THEN allI [THEN allI]]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
150 |
apply (erule beta.induct) |
11183 | 151 |
apply (slowsimp intro: rtrancl_eta_subst eta_subst) |
152 |
apply (blast intro: rtrancl_eta_AppL) |
|
153 |
apply (blast intro: rtrancl_eta_AppR) |
|
154 |
apply simp; |
|
155 |
apply (slowsimp intro: rtrancl_eta_Abs free_beta |
|
9858 | 156 |
iff del: dB.distinct simp: dB.distinct) (*23 seconds?*) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
157 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
158 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
159 |
lemma confluent_beta_eta: "confluent (beta \<union> eta)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
160 |
apply (assumption | |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
161 |
rule square_rtrancl_reflcl_commute confluent_Un |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
162 |
beta_confluent eta_confluent square_beta_eta)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
163 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
164 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
165 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
166 |
subsection "Implicit definition of eta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
167 |
|
12011 | 168 |
text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *} |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
169 |
|
18241 | 170 |
lemma not_free_iff_lifted: |
171 |
"(\<not> free s i) = (\<exists>t. s = lift t i)" |
|
20503 | 172 |
apply (induct s arbitrary: i) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
173 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
174 |
apply (rule iffI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
175 |
apply (erule linorder_neqE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
176 |
apply (rule_tac x = "Var nat" in exI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
177 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
178 |
apply (rule_tac x = "Var (nat - 1)" in exI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
179 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
180 |
apply clarify |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
181 |
apply (rule notE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
182 |
prefer 2 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
183 |
apply assumption |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
184 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
185 |
apply (case_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
186 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
187 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
188 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
189 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
190 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
191 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
192 |
apply (rule iffI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
193 |
apply (elim conjE exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
194 |
apply (rename_tac u1 u2) |
12011 | 195 |
apply (rule_tac x = "u1 \<degree> u2" in exI) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
196 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
197 |
apply (erule exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
198 |
apply (erule rev_mp) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
199 |
apply (case_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
200 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
201 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
202 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
203 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
204 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
205 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
206 |
apply (rule iffI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
207 |
apply (erule exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
208 |
apply (rule_tac x = "Abs t" in exI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
209 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
210 |
apply (erule exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
211 |
apply (erule rev_mp) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
212 |
apply (case_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
213 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
214 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
215 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
216 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
217 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
218 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
219 |
theorem explicit_is_implicit: |
12011 | 220 |
"(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) = |
221 |
(\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)" |
|
18241 | 222 |
by (auto simp add: not_free_iff_lifted) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
223 |
|
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
224 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
225 |
subsection {* Parallel eta-reduction *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
226 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
227 |
consts |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
228 |
par_eta :: "(dB \<times> dB) set" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
229 |
|
19363 | 230 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
231 |
par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50) where |
19363 | 232 |
"s =e> t == (s, t) \<in> par_eta" |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
233 |
|
21210 | 234 |
notation (xsymbols) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
235 |
par_eta_red (infixl "\<Rightarrow>\<^sub>\<eta>" 50) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
236 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
237 |
inductive par_eta |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
238 |
intros |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
239 |
var [simp, intro]: "Var x \<Rightarrow>\<^sub>\<eta> Var x" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
240 |
eta [simp, intro]: "\<not> free s 0 \<Longrightarrow> s \<Rightarrow>\<^sub>\<eta> s'\<Longrightarrow> Abs (s \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> s'[dummy/0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
241 |
app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
242 |
abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
243 |
|
18241 | 244 |
lemma free_par_eta [simp]: |
245 |
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
|
246 |
shows "free t i = free s i" using eta |
|
20503 | 247 |
by (induct arbitrary: i) (simp_all cong: conj_cong) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
248 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
249 |
lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
250 |
by (induct t) simp_all |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
251 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
252 |
lemma par_eta_lift [simp]: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
253 |
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
18241 | 254 |
shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta |
20503 | 255 |
by (induct arbitrary: i) simp_all |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
256 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
257 |
lemma par_eta_subst [simp]: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
258 |
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
18241 | 259 |
shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta |
20503 | 260 |
by (induct arbitrary: u u' i) (simp_all add: subst_subst [symmetric] subst_Var) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
261 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
262 |
theorem eta_subset_par_eta: "eta \<subseteq> par_eta" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
263 |
apply (rule subsetI) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
264 |
apply clarify |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
265 |
apply (erule eta.induct) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
266 |
apply (blast intro!: par_eta_refl)+ |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
267 |
done |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
268 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
269 |
theorem par_eta_subset_eta: "par_eta \<subseteq> eta\<^sup>*" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
270 |
apply (rule subsetI) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
271 |
apply clarify |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
272 |
apply (erule par_eta.induct) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
273 |
apply blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
274 |
apply (rule rtrancl_into_rtrancl) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
275 |
apply (rule rtrancl_eta_Abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
276 |
apply (rule rtrancl_eta_AppL) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
277 |
apply assumption |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
278 |
apply (rule eta.eta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
279 |
apply simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
280 |
apply (rule rtrancl_eta_App) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
281 |
apply assumption+ |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
282 |
apply (rule rtrancl_eta_Abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
283 |
apply assumption |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
284 |
done |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
285 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
286 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
287 |
subsection {* n-ary eta-expansion *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
288 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
289 |
consts eta_expand :: "nat \<Rightarrow> dB \<Rightarrow> dB" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
290 |
primrec |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
291 |
eta_expand_0: "eta_expand 0 t = t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
292 |
eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
293 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
294 |
lemma eta_expand_Suc': |
18241 | 295 |
"eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))" |
20503 | 296 |
by (induct n arbitrary: t) simp_all |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
297 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
298 |
theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
299 |
by (induct k) (simp_all add: lift_lift) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
300 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
301 |
theorem eta_expand_beta: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
302 |
assumes u: "u => u'" |
18241 | 303 |
shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]" |
20503 | 304 |
proof (induct k arbitrary: t t') |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
305 |
case 0 |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
306 |
with u show ?case by simp |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
307 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
308 |
case (Suc k) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
309 |
hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
310 |
by (blast intro: par_beta_lift) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
311 |
with Suc show ?case by (simp del: eta_expand_Suc add: eta_expand_Suc') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
312 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
313 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
314 |
theorem eta_expand_red: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
315 |
assumes t: "t => t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
316 |
shows "eta_expand k t => eta_expand k t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
317 |
by (induct k) (simp_all add: t) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
318 |
|
18241 | 319 |
theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'" |
20503 | 320 |
proof (induct k arbitrary: t t') |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
321 |
case 0 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
322 |
show ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
323 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
324 |
case (Suc k) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
325 |
have "Abs (lift (eta_expand k t) 0 \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> lift t' 0[arbitrary/0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
326 |
by (fastsimp intro: par_eta_lift Suc) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
327 |
thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
328 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
329 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
330 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
331 |
subsection {* Elimination rules for parallel eta reduction *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
332 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
333 |
theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u" |
18241 | 334 |
shows "u = u1' \<degree> u2' \<Longrightarrow> |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
335 |
\<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta |
20503 | 336 |
proof (induct arbitrary: u1' u2') |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
337 |
case (app s s' t t') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
338 |
have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
339 |
with app show ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
340 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
341 |
case (eta dummy s s') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
342 |
then obtain u1'' u2'' where s': "s' = u1'' \<degree> u2''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
343 |
by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
344 |
then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
345 |
then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)" |
17589 | 346 |
and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
347 |
from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
348 |
by (simp_all del: free_par_eta add: free_par_eta [symmetric]) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
349 |
with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
350 |
by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
351 |
moreover from u1 par_eta_refl have "u1[dummy/0] \<Rightarrow>\<^sub>\<eta> u1''[dummy/0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
352 |
by (rule par_eta_subst) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
353 |
moreover from u2 par_eta_refl have "u2[dummy/0] \<Rightarrow>\<^sub>\<eta> u2''[dummy/0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
354 |
by (rule par_eta_subst) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
355 |
ultimately show ?case using eta s' |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
356 |
by (simp only: subst.simps dB.simps) blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
357 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
358 |
case var thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
359 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
360 |
case abs thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
361 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
362 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
363 |
theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'" |
18241 | 364 |
shows "t' = Abs u' \<Longrightarrow> |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
365 |
\<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta |
20503 | 366 |
proof (induct arbitrary: u') |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
367 |
case (abs s t) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
368 |
have "Abs s = eta_expand 0 (Abs s)" by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
369 |
with abs show ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
370 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
371 |
case (eta dummy s s') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
372 |
then obtain u'' where s': "s' = Abs u''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
373 |
by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
374 |
then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta) |
17589 | 375 |
then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
376 |
from eta u s' have "\<not> free u (Suc 0)" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
377 |
by (simp del: free_par_eta add: free_par_eta [symmetric]) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
378 |
with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
379 |
by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
380 |
moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] \<Rightarrow>\<^sub>\<eta> u''[lift dummy 0/Suc 0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
381 |
by (rule par_eta_subst) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
382 |
ultimately show ?case using eta s' by fastsimp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
383 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
384 |
case var thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
385 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
386 |
case app thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
387 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
388 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
389 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
390 |
subsection {* Eta-postponement theorem *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
391 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
392 |
text {* |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
393 |
Based on a proof by Masako Takahashi \cite{Takahashi-IandC}. |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
394 |
*} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
395 |
|
18241 | 396 |
theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u" |
20503 | 397 |
proof (induct t arbitrary: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule) |
18460 | 398 |
case (less t) |
399 |
from `t => u` |
|
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
400 |
show ?case |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
401 |
proof cases |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
402 |
case (var n) |
18460 | 403 |
with less show ?thesis |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
404 |
by (auto intro: par_beta_refl) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
405 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
406 |
case (abs r' r'') |
18460 | 407 |
with less have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
408 |
then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r \<Rightarrow>\<^sub>\<eta> r'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
409 |
by (blast dest: par_eta_elim_abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
410 |
from abs have "size r' < size t" by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
411 |
with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''" |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18460
diff
changeset
|
412 |
by (blast dest: less(1)) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
413 |
with s abs show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
414 |
by (auto intro: eta_expand_red eta_expand_eta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
415 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
416 |
case (app q' q'' r' r'') |
18460 | 417 |
with less have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
418 |
then obtain q r k where s: "s = eta_expand k (q \<degree> r)" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
419 |
and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
420 |
by (blast dest: par_eta_elim_app [OF _ refl]) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
421 |
from app have "size q' < size t" and "size r' < size t" by simp_all |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
422 |
with app(2,3) qq rr obtain t' t'' where "q => t'" and |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
423 |
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''" |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18460
diff
changeset
|
424 |
by (blast dest: less(1)) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
425 |
with s app show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
426 |
by (fastsimp intro: eta_expand_red eta_expand_eta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
427 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
428 |
case (beta q' q'' r' r'') |
18460 | 429 |
with less have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
430 |
then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) \<degree> r)" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
431 |
and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
432 |
by (blast dest: par_eta_elim_app par_eta_elim_abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
433 |
from beta have "size q' < size t" and "size r' < size t" by simp_all |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
434 |
with beta(2-3) qq rr obtain t' t'' where "q => t'" and |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
435 |
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''" |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18460
diff
changeset
|
436 |
by (blast dest: less(1)) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
437 |
with s beta show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
438 |
by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
439 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
440 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
441 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
442 |
theorem eta_postponement': assumes eta: "s -e>> t" |
18241 | 443 |
shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u" |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
444 |
using eta [simplified rtrancl_subset |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
445 |
[OF eta_subset_par_eta par_eta_subset_eta, symmetric]] |
20503 | 446 |
proof (induct arbitrary: u) |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
447 |
case 1 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
448 |
thus ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
449 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
450 |
case (2 s' s'' s''') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
451 |
from 2 obtain t' where s': "s' => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> s'''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
452 |
by (auto dest: par_eta_beta) |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18460
diff
changeset
|
453 |
from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" using 2 |
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18460
diff
changeset
|
454 |
by blast |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
455 |
from par_eta_subset_eta t' have "t' -e>> s'''" .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
456 |
with t'' have "t'' -e>> s'''" by (rule rtrancl_trans) |
17589 | 457 |
with s show ?case by iprover |
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
458 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
459 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
460 |
theorem eta_postponement: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
461 |
assumes st: "(s, t) \<in> (beta \<union> eta)\<^sup>*" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
462 |
shows "(s, t) \<in> eta\<^sup>* O beta\<^sup>*" using st |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
463 |
proof induct |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
464 |
case 1 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
465 |
show ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
466 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
467 |
case (2 s' s'') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
468 |
from 2(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' -e>> s'" by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
469 |
from 2(2) show ?case |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
470 |
proof |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
471 |
assume "s' -> s''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
472 |
with beta_subset_par_beta have "s' => s''" .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
473 |
with t' obtain t'' where st: "t' => t''" and tu: "t'' -e>> s''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
474 |
by (auto dest: eta_postponement') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
475 |
from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
476 |
with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtrancl_trans) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
477 |
thus ?thesis using tu .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
478 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
479 |
assume "s' -e> s''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
480 |
with t' have "t' -e>> s''" .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
481 |
with s show ?thesis .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
482 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
483 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
484 |
|
11638 | 485 |
end |