author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 15522 | ec0fd05b2f2c |
child 17589 | 58eeffd73be1 |
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 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
24 |
syntax |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
25 |
"_eta" :: "[dB, dB] => bool" (infixl "-e>" 50) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
26 |
"_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
27 |
"_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50) |
1269 | 28 |
translations |
9827 | 29 |
"s -e> t" == "(s, t) \<in> eta" |
30 |
"s -e>> t" == "(s, t) \<in> eta^*" |
|
31 |
"s -e>= t" == "(s, t) \<in> eta^=" |
|
1269 | 32 |
|
1789 | 33 |
inductive eta |
11638 | 34 |
intros |
12011 | 35 |
eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]" |
36 |
appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u" |
|
37 |
appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t" |
|
11638 | 38 |
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
|
39 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
40 |
inductive_cases eta_cases [elim!]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
41 |
"Abs s -e> z" |
12011 | 42 |
"s \<degree> t -e> u" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
43 |
"Var i -e> t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
44 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
45 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
46 |
subsection "Properties of eta, subst and free" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
47 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
48 |
lemma subst_not_free [rule_format, simp]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
49 |
"\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
50 |
apply (induct_tac s) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
51 |
apply (simp_all add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
52 |
done |
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]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
55 |
"\<forall>i k. free (lift t k) i = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
56 |
(i < k \<and> free t i \<or> k < i \<and> free t (i - 1))" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
57 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
58 |
apply (auto cong: conj_cong) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
59 |
apply arith |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
60 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
61 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
62 |
lemma free_subst [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
63 |
"\<forall>i k t. free (s[t/k]) i = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
64 |
(free s k \<and> free t i \<or> free s (if i < k then i else i + 1))" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
65 |
apply (induct_tac s) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
66 |
prefer 2 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
67 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
68 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
69 |
prefer 2 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
70 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
71 |
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
|
72 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
73 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
74 |
lemma free_eta [rule_format]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
75 |
"s -e> t ==> \<forall>i. free t i = free s i" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
76 |
apply (erule eta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
77 |
apply (simp_all cong: conj_cong) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
78 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
79 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
80 |
lemma not_free_eta: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
81 |
"[| s -e> t; \<not> free s i |] ==> \<not> free t i" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
82 |
apply (simp add: free_eta) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
83 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
84 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
85 |
lemma eta_subst [rule_format, simp]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
86 |
"s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
87 |
apply (erule eta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
88 |
apply (simp_all add: subst_subst [symmetric]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
89 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
90 |
|
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
91 |
theorem lift_subst_dummy: "\<And>i dummy. \<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
92 |
by (induct s) simp_all |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
93 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
94 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
95 |
subsection "Confluence of eta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
96 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
97 |
lemma square_eta: "square eta eta (eta^=) (eta^=)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
98 |
apply (unfold square_def id_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
99 |
apply (rule impI [THEN allI [THEN allI]]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
100 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
101 |
apply (erule eta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
102 |
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
|
103 |
apply safe |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
104 |
prefer 5 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
105 |
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
|
106 |
apply blast+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
107 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
108 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
109 |
theorem eta_confluent: "confluent eta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
110 |
apply (rule square_eta [THEN square_reflcl_confluent]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
111 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
112 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
113 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
114 |
subsection "Congruence rules for eta*" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
115 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
116 |
lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
117 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
118 |
apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
119 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
120 |
|
12011 | 121 |
lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
122 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
123 |
apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
124 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
125 |
|
12011 | 126 |
lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
127 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
128 |
apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
129 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
130 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
131 |
lemma rtrancl_eta_App: |
12011 | 132 |
"[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'" |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
133 |
apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
134 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
135 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
136 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
137 |
subsection "Commutation of beta and eta" |
1900 | 138 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
139 |
lemma free_beta [rule_format]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
140 |
"s -> t ==> \<forall>i. free t i --> free s i" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
141 |
apply (erule beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
142 |
apply simp_all |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
143 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
144 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
145 |
lemma beta_subst [rule_format, intro]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
146 |
"s -> t ==> \<forall>u i. s[u/i] -> t[u/i]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
147 |
apply (erule beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
148 |
apply (simp_all add: subst_subst [symmetric]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
149 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
150 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
151 |
lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
152 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
153 |
apply (auto elim!: linorder_neqE simp: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
154 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
155 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
156 |
lemma eta_lift [rule_format, simp]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
157 |
"s -e> t ==> \<forall>i. lift s i -e> lift t i" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
158 |
apply (erule eta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
159 |
apply simp_all |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
160 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
161 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
162 |
lemma rtrancl_eta_subst [rule_format]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
163 |
"\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
164 |
apply (induct_tac u) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
165 |
apply (simp_all add: subst_Var) |
11183 | 166 |
apply (blast) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
167 |
apply (blast intro: rtrancl_eta_App) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
168 |
apply (blast intro!: rtrancl_eta_Abs eta_lift) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
169 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
170 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
171 |
lemma square_beta_eta: "square beta eta (eta^*) (beta^=)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
172 |
apply (unfold square_def) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
173 |
apply (rule impI [THEN allI [THEN allI]]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
174 |
apply (erule beta.induct) |
11183 | 175 |
apply (slowsimp intro: rtrancl_eta_subst eta_subst) |
176 |
apply (blast intro: rtrancl_eta_AppL) |
|
177 |
apply (blast intro: rtrancl_eta_AppR) |
|
178 |
apply simp; |
|
179 |
apply (slowsimp intro: rtrancl_eta_Abs free_beta |
|
9858 | 180 |
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
|
181 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
182 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
183 |
lemma confluent_beta_eta: "confluent (beta \<union> eta)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
184 |
apply (assumption | |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
185 |
rule square_rtrancl_reflcl_commute confluent_Un |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
186 |
beta_confluent eta_confluent square_beta_eta)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
187 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
188 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
189 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
190 |
subsection "Implicit definition of eta" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
191 |
|
12011 | 192 |
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
|
193 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
194 |
lemma not_free_iff_lifted [rule_format]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
195 |
"\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
196 |
apply (induct_tac s) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
197 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
198 |
apply clarify |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
199 |
apply (rule iffI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
200 |
apply (erule linorder_neqE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
201 |
apply (rule_tac x = "Var nat" in exI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
202 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
203 |
apply (rule_tac x = "Var (nat - 1)" in exI) |
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 clarify |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
206 |
apply (rule notE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
207 |
prefer 2 |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
208 |
apply assumption |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
209 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
210 |
apply (case_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
211 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
212 |
apply simp |
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 (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
216 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
217 |
apply (rule allI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
218 |
apply (rule iffI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
219 |
apply (elim conjE exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
220 |
apply (rename_tac u1 u2) |
12011 | 221 |
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
|
222 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
223 |
apply (erule exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
224 |
apply (erule rev_mp) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
225 |
apply (case_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
226 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
227 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
228 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
229 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
230 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
231 |
apply (erule thin_rl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
232 |
apply (rule allI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
233 |
apply (rule iffI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
234 |
apply (erule exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
235 |
apply (rule_tac x = "Abs t" in exI) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
236 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
237 |
apply (erule exE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
238 |
apply (erule rev_mp) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
239 |
apply (case_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
240 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
241 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
242 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
243 |
apply blast |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
244 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
245 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
246 |
theorem explicit_is_implicit: |
12011 | 247 |
"(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) = |
248 |
(\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
249 |
apply (auto simp add: not_free_iff_lifted) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
250 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9102
diff
changeset
|
251 |
|
15522
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
252 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
253 |
subsection {* Parallel eta-reduction *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
254 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
255 |
consts |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
256 |
par_eta :: "(dB \<times> dB) set" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
257 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
258 |
syntax |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
259 |
"_par_eta" :: "[dB, dB] => bool" (infixl "=e>" 50) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
260 |
translations |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
261 |
"s =e> t" == "(s, t) \<in> par_eta" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
262 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
263 |
syntax (xsymbols) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
264 |
"_par_eta" :: "[dB, dB] => bool" (infixl "\<Rightarrow>\<^sub>\<eta>" 50) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
265 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
266 |
inductive par_eta |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
267 |
intros |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
268 |
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
|
269 |
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
|
270 |
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
|
271 |
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
|
272 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
273 |
lemma free_par_eta [simp]: assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
274 |
shows "\<And>i. free t i = free s i" using eta |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
275 |
by induct (simp_all cong: conj_cong) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
276 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
277 |
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
|
278 |
by (induct t) simp_all |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
279 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
280 |
lemma par_eta_lift [simp]: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
281 |
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
282 |
shows "\<And>i. lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
283 |
by induct simp_all |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
284 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
285 |
lemma par_eta_subst [simp]: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
286 |
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
287 |
shows "\<And>u u' i. u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
288 |
by induct (simp_all add: subst_subst [symmetric] subst_Var) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
289 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
290 |
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
|
291 |
apply (rule subsetI) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
292 |
apply clarify |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
293 |
apply (erule eta.induct) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
294 |
apply (blast intro!: par_eta_refl)+ |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
295 |
done |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
296 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
297 |
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
|
298 |
apply (rule subsetI) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
299 |
apply clarify |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
300 |
apply (erule par_eta.induct) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
301 |
apply blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
302 |
apply (rule rtrancl_into_rtrancl) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
303 |
apply (rule rtrancl_eta_Abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
304 |
apply (rule rtrancl_eta_AppL) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
305 |
apply assumption |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
306 |
apply (rule eta.eta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
307 |
apply simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
308 |
apply (rule rtrancl_eta_App) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
309 |
apply assumption+ |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
310 |
apply (rule rtrancl_eta_Abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
311 |
apply assumption |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
312 |
done |
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 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
315 |
subsection {* n-ary eta-expansion *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
316 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
317 |
consts eta_expand :: "nat \<Rightarrow> dB \<Rightarrow> dB" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
318 |
primrec |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
319 |
eta_expand_0: "eta_expand 0 t = t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
320 |
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
|
321 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
322 |
lemma eta_expand_Suc': |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
323 |
"\<And>t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
324 |
by (induct n) simp_all |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
325 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
326 |
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
|
327 |
by (induct k) (simp_all add: lift_lift) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
328 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
329 |
theorem eta_expand_beta: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
330 |
assumes u: "u => u'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
331 |
shows "\<And>t t'. t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
332 |
proof (induct k) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
333 |
case 0 with u show ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
334 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
335 |
case (Suc k) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
336 |
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
|
337 |
by (blast intro: par_beta_lift) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
338 |
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
|
339 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
340 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
341 |
theorem eta_expand_red: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
342 |
assumes t: "t => t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
343 |
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
|
344 |
by (induct k) (simp_all add: t) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
345 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
346 |
theorem eta_expand_eta: "\<And>t t'. t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
347 |
proof (induct k) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
348 |
case 0 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
349 |
show ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
350 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
351 |
case (Suc k) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
352 |
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
|
353 |
by (fastsimp intro: par_eta_lift Suc) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
354 |
thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
355 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
356 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
357 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
358 |
subsection {* Elimination rules for parallel eta reduction *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
359 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
360 |
theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
361 |
shows "\<And>u1' u2'. u = u1' \<degree> u2' \<Longrightarrow> |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
362 |
\<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 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
363 |
proof induct |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
364 |
case (app s s' t t') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
365 |
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
|
366 |
with app show ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
367 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
368 |
case (eta dummy s s') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
369 |
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
|
370 |
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
|
371 |
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
|
372 |
then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
373 |
and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by rules |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
374 |
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
|
375 |
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
|
376 |
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
|
377 |
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
|
378 |
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
|
379 |
by (rule par_eta_subst) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
380 |
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
|
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' |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
383 |
by (simp only: subst.simps dB.simps) blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
384 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
385 |
case var thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
386 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
387 |
case abs thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
388 |
qed |
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 |
theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
391 |
shows "\<And>u'. t' = Abs u' \<Longrightarrow> |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
392 |
\<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
393 |
proof induct |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
394 |
case (abs s t) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
395 |
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
|
396 |
with abs show ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
397 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
398 |
case (eta dummy s s') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
399 |
then obtain u'' where s': "s' = Abs u''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
400 |
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
|
401 |
then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
402 |
then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by rules |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
403 |
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
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
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
|
408 |
by (rule par_eta_subst) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
409 |
ultimately show ?case using eta s' by fastsimp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
410 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
411 |
case var thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
412 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
413 |
case app thus ?case by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
414 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
415 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
416 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
417 |
subsection {* Eta-postponement theorem *} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
418 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
419 |
text {* |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
420 |
Based on a proof by Masako Takahashi \cite{Takahashi-IandC}. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
421 |
*} |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
422 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
423 |
theorem par_eta_beta: "\<And>s u. s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
424 |
proof (induct t rule: measure_induct [of size, rule_format]) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
425 |
case (1 t) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
426 |
from 1(3) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
427 |
show ?case |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
428 |
proof cases |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
429 |
case (var n) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
430 |
with 1 show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
431 |
by (auto intro: par_beta_refl) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
432 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
433 |
case (abs r' r'') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
434 |
with 1 have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
435 |
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
|
436 |
by (blast dest: par_eta_elim_abs) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
437 |
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
|
438 |
with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
439 |
by (blast dest: 1) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
440 |
with s abs show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
441 |
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
|
442 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
443 |
case (app q' q'' r' r'') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
444 |
with 1 have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
445 |
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
|
446 |
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
|
447 |
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
|
448 |
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
|
449 |
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
|
450 |
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
451 |
by (blast dest: 1) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
452 |
with s app show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
453 |
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
|
454 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
455 |
case (beta q' q'' r' r'') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
456 |
with 1 have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
457 |
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
|
458 |
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
|
459 |
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
|
460 |
from beta 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
|
461 |
with beta(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
|
462 |
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
463 |
by (blast dest: 1) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
464 |
with s beta show ?thesis |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
465 |
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
|
466 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
467 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
468 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
469 |
theorem eta_postponement': assumes eta: "s -e>> t" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
470 |
shows "\<And>u. t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
471 |
using eta [simplified rtrancl_subset |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
472 |
[OF eta_subset_par_eta par_eta_subset_eta, symmetric]] |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
473 |
proof induct |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
474 |
case 1 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
475 |
thus ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
476 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
477 |
case (2 s' s'' s''') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
478 |
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
|
479 |
by (auto dest: par_eta_beta) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
480 |
from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
481 |
by (blast dest: 2) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
482 |
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
|
483 |
with t'' have "t'' -e>> s'''" by (rule rtrancl_trans) |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
484 |
with s show ?case by rules |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
485 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
486 |
|
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
487 |
theorem eta_postponement: |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
488 |
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
|
489 |
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
|
490 |
proof induct |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
491 |
case 1 |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
492 |
show ?case by blast |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
493 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
494 |
case (2 s' s'') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
495 |
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
|
496 |
from 2(2) show ?case |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
497 |
proof |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
498 |
assume "s' -> s''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
499 |
with beta_subset_par_beta have "s' => s''" .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
500 |
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
|
501 |
by (auto dest: eta_postponement') |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
502 |
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
|
503 |
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
|
504 |
thus ?thesis using tu .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
505 |
next |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
506 |
assume "s' -e> s''" |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
507 |
with t' have "t' -e>> s''" .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
508 |
with s show ?thesis .. |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
509 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
510 |
qed |
ec0fd05b2f2c
Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents:
13187
diff
changeset
|
511 |
|
11638 | 512 |
end |