author | urbanc |
Tue, 27 Mar 2007 18:28:22 +0200 | |
changeset 22533 | 62c76754da32 |
parent 22418 | 49e2d9744ae1 |
child 22650 | 0c5b22076fb3 |
permissions | -rw-r--r-- |
18269 | 1 |
(* $Id$ *) |
18105 | 2 |
|
19496 | 3 |
theory Weakening |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
4 |
imports "../Nominal" |
18105 | 5 |
begin |
6 |
||
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
7 |
section {* Weakening Example for the Simply-Typed Lambda-Calculus *} |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
8 |
(*================================================================*) |
18105 | 9 |
|
10 |
atom_decl name |
|
11 |
||
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
12 |
nominal_datatype lam = |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
13 |
Var "name" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
14 |
| App "lam" "lam" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
15 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
18105 | 16 |
|
18352 | 17 |
nominal_datatype ty = |
18 |
TVar "nat" |
|
18105 | 19 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
20 |
||
22533 | 21 |
lemma ty_fresh: |
22 |
fixes x::"name" |
|
23 |
and T::"ty" |
|
24 |
shows "x\<sharp>T" |
|
25 |
by (nominal_induct T rule: ty.induct) |
|
26 |
(auto simp add: fresh_nat) |
|
18105 | 27 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
28 |
text {* valid contexts *} |
22533 | 29 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
30 |
inductive2 |
18105 | 31 |
valid :: "(name\<times>ty) list \<Rightarrow> bool" |
21364 | 32 |
where |
33 |
v1[intro]: "valid []" |
|
34 |
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
|
18105 | 35 |
|
22533 | 36 |
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
|
37 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
38 |
text{* typing judgements *} |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
39 |
inductive2 |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
40 |
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
21364 | 41 |
where |
22533 | 42 |
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
43 |
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
22533 | 44 |
| 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
|
45 |
|
22533 | 46 |
(* automatically deriving the strong induction principle *) |
47 |
nominal_inductive typing |
|
48 |
by (simp_all add: abs_fresh ty_fresh) |
|
18105 | 49 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
50 |
text {* definition of a subcontext *} |
18105 | 51 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
52 |
abbreviation |
22533 | 53 |
"sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) |
54 |
where |
|
55 |
"\<Gamma>1 \<lless> \<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
|
56 |
|
22533 | 57 |
text {* Now it comes: The Weakening Lemma *} |
18105 | 58 |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
59 |
lemma weakening_version1: |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
60 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
61 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
62 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
63 |
shows "\<Gamma>2 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
64 |
using a b c |
22533 | 65 |
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
|
66 |
(auto | atomize)+ |
18105 | 67 |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
68 |
lemma weakening_version2: |
18105 | 69 |
fixes \<Gamma>1::"(name\<times>ty) list" |
70 |
and t ::"lam" |
|
71 |
and \<tau> ::"ty" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
72 |
assumes a: "\<Gamma>1 \<turnstile> t:T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
73 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
74 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
75 |
shows "\<Gamma>2 \<turnstile> t:T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
76 |
using a b c |
22533 | 77 |
proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
78 |
case (t_Var \<Gamma>1 x T) (* variable case *) |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
79 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
80 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
81 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
82 |
moreover |
22533 | 83 |
have "(x,T)\<in> set \<Gamma>1" by fact |
84 |
ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto |
|
18105 | 85 |
next |
22533 | 86 |
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
87 |
have vc: "x\<sharp>\<Gamma>2" by fact (* variable convention *) |
|
88 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((x,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t:T2" by fact |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
89 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
22533 | 90 |
then have "((x,T1)#\<Gamma>1) \<lless> ((x,T1)#\<Gamma>2)" by simp |
18105 | 91 |
moreover |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
92 |
have "valid \<Gamma>2" by fact |
22533 | 93 |
then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2) |
94 |
ultimately have "((x,T1)#\<Gamma>2) \<turnstile> t:T2" using ih by simp |
|
95 |
with vc show "\<Gamma>2 \<turnstile> (Lam [x].t) : T1\<rightarrow>T2" by auto |
|
21488 | 96 |
qed (auto) (* app case *) |
18105 | 97 |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
98 |
lemma weakening_version3: |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
99 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
100 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
101 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
102 |
shows "\<Gamma>2 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
103 |
using a b c |
22533 | 104 |
proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
105 |
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
|
106 |
have vc: "x\<sharp>\<Gamma>2" by fact (* variable convention *) |
|
107 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((x,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
108 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
22533 | 109 |
then have "((x,T1)#\<Gamma>1) \<lless> ((x,T1)#\<Gamma>2)" by simp |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
110 |
moreover |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
111 |
have "valid \<Gamma>2" by fact |
22533 | 112 |
then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2) |
113 |
ultimately have "((x,T1)#\<Gamma>2) \<turnstile> t : T2" using ih by simp |
|
114 |
with vc show "\<Gamma>2 \<turnstile> (Lam [x].t) : T1 \<rightarrow> T2" by auto |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
115 |
qed (auto) (* app and var case *) |
18105 | 116 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
117 |
text{* The original induction principle for the typing relation |
21488 | 118 |
is not strong enough - even this simple lemma fails: *} |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
119 |
lemma weakening_too_weak: |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
120 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
121 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
122 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
123 |
shows "\<Gamma>2 \<turnstile> t : T" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
124 |
using a b c |
20503 | 125 |
proof (induct arbitrary: \<Gamma>2) |
22533 | 126 |
case (t_Var \<Gamma>1 x T) (* variable case *) |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
127 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
128 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
129 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
130 |
moreover |
22533 | 131 |
have "(x,T) \<in> (set \<Gamma>1)" by fact |
132 |
ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto |
|
18105 | 133 |
next |
22533 | 134 |
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
21488 | 135 |
(* all assumptions available in this case*) |
22533 | 136 |
have a0: "x\<sharp>\<Gamma>1" by fact |
137 |
have a1: "((x,T1)#\<Gamma>1) \<turnstile> t : T2" by fact |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
138 |
have a2: "\<Gamma>1 \<lless> \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
139 |
have a3: "valid \<Gamma>2" by fact |
22533 | 140 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((x,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
141 |
have "((x,T1)#\<Gamma>1) \<lless> ((x,T1)#\<Gamma>2)" using a2 by simp |
|
18105 | 142 |
moreover |
22533 | 143 |
have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) |
19496 | 144 |
oops |
18105 | 145 |
|
19496 | 146 |
end |