author | urbanc |
Mon, 11 Feb 2008 15:19:17 +0100 | |
changeset 26055 | a7a537e0413a |
parent 25751 | a4e69ce247e0 |
child 26262 | f5cb9602145f |
permissions | -rw-r--r-- |
18269 | 1 |
(* $Id$ *) |
18105 | 2 |
|
19496 | 3 |
theory Weakening |
25722 | 4 |
imports "../Nominal" |
18105 | 5 |
begin |
6 |
||
26055 | 7 |
text {* |
8 |
A simple proof of the Weakening Property in the simply-typed |
|
9 |
lambda-calculus. The proof is simple, because we can make use |
|
10 |
of the variable convention. *} |
|
18105 | 11 |
|
12 |
atom_decl name |
|
13 |
||
25751 | 14 |
text {* Terms and Types *} |
26055 | 15 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
16 |
nominal_datatype lam = |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
17 |
Var "name" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
18 |
| App "lam" "lam" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
19 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
18105 | 20 |
|
18352 | 21 |
nominal_datatype ty = |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
22 |
TVar "string" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
23 |
| TArr "ty" "ty" ("_ \<rightarrow> _" [100,100] 100) |
18105 | 24 |
|
22533 | 25 |
lemma ty_fresh: |
26 |
fixes x::"name" |
|
27 |
and T::"ty" |
|
28 |
shows "x\<sharp>T" |
|
29 |
by (nominal_induct T rule: ty.induct) |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
30 |
(auto simp add: fresh_string) |
18105 | 31 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
32 |
text {* |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
33 |
Valid contexts (at the moment we have no type for finite |
26055 | 34 |
sets yet, therefore typing-contexts are lists). *} |
35 |
||
23760 | 36 |
inductive |
18105 | 37 |
valid :: "(name\<times>ty) list \<Rightarrow> bool" |
21364 | 38 |
where |
39 |
v1[intro]: "valid []" |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
40 |
| v2[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)" |
18105 | 41 |
|
22533 | 42 |
equivariance valid |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
21488
diff
changeset
|
43 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
44 |
text{* Typing judgements *} |
26055 | 45 |
|
23760 | 46 |
inductive |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
47 |
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
21364 | 48 |
where |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
49 |
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
50 |
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
51 |
| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2" |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
52 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
53 |
text {* |
25722 | 54 |
We derive the strong induction principle for the typing |
55 |
relation (this induction principle has the variable convention |
|
26055 | 56 |
already built-in). *} |
57 |
||
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
58 |
equivariance typing |
22533 | 59 |
nominal_inductive typing |
60 |
by (simp_all add: abs_fresh ty_fresh) |
|
18105 | 61 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
62 |
text {* Abbreviation for the notion of subcontexts. *} |
26055 | 63 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
64 |
abbreviation |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
65 |
"sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) |
22533 | 66 |
where |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
67 |
"\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2" |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
68 |
|
22533 | 69 |
text {* Now it comes: The Weakening Lemma *} |
18105 | 70 |
|
26055 | 71 |
text {* |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
72 |
The first version is, after setting up the induction, |
26055 | 73 |
completely automatic except for use of atomize. *} |
74 |
||
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
75 |
lemma weakening_version1: |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
76 |
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
77 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
78 |
and b: "valid \<Gamma>2" |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
79 |
and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
80 |
shows "\<Gamma>2 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
81 |
using a b c |
22533 | 82 |
by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
83 |
(auto | atomize)+ |
18105 | 84 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
85 |
text {* |
26055 | 86 |
The second version gives the details for the variable |
87 |
and lambda case. *} |
|
88 |
||
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
89 |
lemma weakening_version2: |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
90 |
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" |
18105 | 91 |
and t ::"lam" |
92 |
and \<tau> ::"ty" |
|
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
93 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
94 |
and b: "valid \<Gamma>2" |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
95 |
and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
96 |
shows "\<Gamma>2 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
97 |
using a b c |
22533 | 98 |
proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
99 |
case (t_Var \<Gamma>1 x T) (* variable case *) |
|
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
100 |
have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
101 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
102 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
103 |
moreover |
22533 | 104 |
have "(x,T)\<in> set \<Gamma>1" by fact |
105 |
ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto |
|
18105 | 106 |
next |
22533 | 107 |
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
108 |
have vc: "x\<sharp>\<Gamma>2" by fact (* variable convention *) |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
109 |
have ih: "\<lbrakk>valid ((x,T1)#\<Gamma>2); (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> t:T2" by fact |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
110 |
have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
111 |
then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp |
18105 | 112 |
moreover |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
113 |
have "valid \<Gamma>2" by fact |
22533 | 114 |
then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2) |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
115 |
ultimately have "(x,T1)#\<Gamma>2 \<turnstile> t : T2" using ih by simp |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
116 |
with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto |
21488 | 117 |
qed (auto) (* app case *) |
18105 | 118 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
119 |
text{* |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
120 |
The original induction principle for the typing relation |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
121 |
is not strong enough - even this simple lemma fails to be |
26055 | 122 |
simple ;o) *} |
123 |
||
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
124 |
lemma weakening_not_straigh_forward: |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
125 |
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
126 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
127 |
and b: "valid \<Gamma>2" |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
128 |
and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
129 |
shows "\<Gamma>2 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
130 |
using a b c |
20503 | 131 |
proof (induct arbitrary: \<Gamma>2) |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
132 |
case (t_Var \<Gamma>1 x T) (* variable case still works *) |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
133 |
have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
134 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
135 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
136 |
moreover |
22533 | 137 |
have "(x,T) \<in> (set \<Gamma>1)" by fact |
138 |
ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto |
|
18105 | 139 |
next |
22533 | 140 |
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
141 |
(* These are all assumptions available in this case*) |
22533 | 142 |
have a0: "x\<sharp>\<Gamma>1" by fact |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
143 |
have a1: "(x,T1)#\<Gamma>1 \<turnstile> t : T2" by fact |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
144 |
have a2: "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
145 |
have a3: "valid \<Gamma>2" by fact |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
146 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22533
diff
changeset
|
147 |
have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" using a2 by simp |
18105 | 148 |
moreover |
22533 | 149 |
have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) |
19496 | 150 |
oops |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
151 |
|
26055 | 152 |
text{* |
153 |
To show that the proof is not simple, here proof without using |
|
154 |
the variable convention. |
|
155 |
||
156 |
*} |
|
25751 | 157 |
|
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
158 |
lemma weakening_with_explicit_renaming: |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
159 |
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
160 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
161 |
and b: "valid \<Gamma>2" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
162 |
and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
163 |
shows "\<Gamma>2 \<turnstile> t : T" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
164 |
using a b c |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
165 |
proof (induct arbitrary: \<Gamma>2) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
166 |
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
167 |
have fc0: "x\<sharp>\<Gamma>1" by fact |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
168 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
169 |
obtain c::"name" where fc1: "c\<sharp>(x,t,\<Gamma>1,\<Gamma>2)" (* we obtain a fresh name *) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
170 |
by (rule exists_fresh) (auto simp add: fs_name1) |
25138 | 171 |
have "Lam [c].([(c,x)]\<bullet>t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *) |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
172 |
by (auto simp add: lam.inject alpha fresh_prod fresh_atm) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
173 |
moreover |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
174 |
have "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
175 |
proof - |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
176 |
(* we establish (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2) and valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2)) *) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
177 |
have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
178 |
proof - |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
179 |
have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
180 |
then have "[(c,x)]\<bullet>((x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc0 fc1 |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
181 |
by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
182 |
then show "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" by (rule perm_boolE) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
183 |
qed |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
184 |
moreover |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
185 |
have "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
186 |
proof - |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
187 |
have "valid \<Gamma>2" by fact |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
188 |
then show "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc1 |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
189 |
by (auto intro!: v2 simp add: fresh_left calc_atm eqvts) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
190 |
qed |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
191 |
(* these two facts give us by induction hypothesis the following *) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
192 |
ultimately have "(x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2" using ih by simp |
25138 | 193 |
(* we now apply renamings to get to our goal *) |
25137
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
194 |
then have "[(c,x)]\<bullet>((x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2)" by (rule perm_boolI) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
195 |
then have "(c,T1)#\<Gamma>2 \<turnstile> ([(c,x)]\<bullet>t) : T2" using fc1 |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
196 |
by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh) |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
197 |
then show "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" using fc1 by auto |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
198 |
qed |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
199 |
ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp |
0835ac64834a
polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc
parents:
24231
diff
changeset
|
200 |
qed (auto) |
18105 | 201 |
|
25138 | 202 |
text {* |
26055 | 203 |
Moral: compare the proof with explicit renamings to weakening_version1 |
204 |
and weakening_version2, and imagine you are proving something more substantial |
|
205 |
than the weakening lemma. *} |
|
25138 | 206 |
|
19496 | 207 |
end |