author | urbanc |
Thu, 22 May 2008 16:34:41 +0200 | |
changeset 26966 | 071f40487734 |
parent 25867 | c24395ea4e71 |
child 28042 | 1471f2974eb1 |
permissions | -rw-r--r-- |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
1 |
(* $Id$ *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
2 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
3 |
(* Formalisation of weakening using locally nameless *) |
25867 | 4 |
(* terms; the nominal infrastructure can also derive *) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
5 |
(* strong induction principles for such representations *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
6 |
(* *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
7 |
(* Authors: Christian Urban and Randy Pollack *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
8 |
theory LocalWeakening |
25867 | 9 |
imports "../Nominal" |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
10 |
begin |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
11 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
12 |
atom_decl name |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
13 |
|
25867 | 14 |
text {* |
15 |
Curry-style lambda terms in locally nameless |
|
16 |
representation without any binders |
|
17 |
*} |
|
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
18 |
nominal_datatype llam = |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
19 |
lPar "name" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
20 |
| lVar "nat" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
21 |
| lApp "llam" "llam" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
22 |
| lLam "llam" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
23 |
|
23233 | 24 |
text {* definition of vsub - at the moment a bit cumbersome *} |
25 |
||
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
26 |
lemma llam_cases: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
27 |
"(\<exists>a. t = lPar a) \<or> (\<exists>n. t = lVar n) \<or> (\<exists>t1 t2. t = lApp t1 t2) \<or> |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
28 |
(\<exists>t1. t = lLam t1)" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25867
diff
changeset
|
29 |
by (induct t rule: llam.induct) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
30 |
(auto simp add: llam.inject) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
31 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
32 |
consts llam_size :: "llam \<Rightarrow> nat" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
33 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
34 |
nominal_primrec |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
35 |
"llam_size (lPar a) = 1" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
36 |
"llam_size (lVar n) = 1" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
37 |
"llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
38 |
"llam_size (lLam t) = 1 + (llam_size t)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
39 |
by (rule TrueI)+ |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
40 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
41 |
function |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
42 |
vsub :: "llam \<Rightarrow> nat \<Rightarrow> llam \<Rightarrow> llam" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
43 |
where |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
44 |
vsub_lPar: "vsub (lPar p) x s = lPar p" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
45 |
| vsub_lVar: "vsub (lVar n) x s = (if n < x then (lVar n) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
46 |
else (if n = x then s else (lVar (n - 1))))" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
47 |
| vsub_lApp: "vsub (lApp t u) x s = (lApp (vsub t x s) (vsub u x s))" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
48 |
| vsub_lLam: "vsub (lLam t) x s = (lLam (vsub t (x + 1) s))" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
49 |
using llam_cases |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
50 |
apply(auto simp add: llam.inject) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
51 |
apply(rotate_tac 4) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
52 |
apply(drule_tac x="a" in meta_spec) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
53 |
apply(blast) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
54 |
done |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
55 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
56 |
termination vsub |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
57 |
proof |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
58 |
show "wf (measure (llam_size \<circ> fst))" by simp |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
59 |
qed (auto) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
60 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
61 |
lemma vsub_eqvt[eqvt]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
62 |
fixes pi::"name prm" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
63 |
shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25867
diff
changeset
|
64 |
by (induct t arbitrary: n rule: llam.induct) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
65 |
(simp_all add: perm_nat_def) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
66 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
67 |
constdefs |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
68 |
freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
69 |
"freshen t p \<equiv> vsub t 0 (lPar p)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
70 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
71 |
lemma freshen_eqvt[eqvt]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
72 |
fixes pi::"name prm" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
73 |
shows "pi\<bullet>(freshen t p) = freshen (pi\<bullet>t) (pi\<bullet>p)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
74 |
by (simp add: vsub_eqvt freshen_def perm_nat_def) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
75 |
|
23233 | 76 |
text {* types *} |
77 |
||
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
78 |
nominal_datatype ty = |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
79 |
TVar "nat" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
80 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
81 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
82 |
lemma ty_fresh[simp]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
83 |
fixes x::"name" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
84 |
and T::"ty" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
85 |
shows "x\<sharp>T" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25867
diff
changeset
|
86 |
by (induct T rule: ty.induct) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
87 |
(simp_all add: fresh_nat) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
88 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
89 |
text {* valid contexts *} |
23233 | 90 |
|
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
91 |
types cxt = "(name\<times>ty) list" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
92 |
|
23760 | 93 |
inductive |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
94 |
valid :: "cxt \<Rightarrow> bool" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
95 |
where |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
96 |
v1[intro]: "valid []" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
97 |
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,T)#\<Gamma>)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
98 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
99 |
equivariance valid |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
100 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
101 |
lemma v2_elim: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
102 |
assumes a: "valid ((a,T)#\<Gamma>)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
103 |
shows "a\<sharp>\<Gamma> \<and> valid \<Gamma>" |
25867 | 104 |
using a by (cases) (auto) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
105 |
|
23233 | 106 |
text {* "weak" typing relation *} |
107 |
||
23760 | 108 |
inductive |
23233 | 109 |
typing :: "cxt\<Rightarrow>llam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
110 |
where |
25867 | 111 |
t_lPar[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lPar x : T" |
112 |
| t_lApp[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lApp t1 t2 : T2" |
|
113 |
| t_lLam[intro]: "\<lbrakk>x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> freshen t x : T2\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lLam t : T1\<rightarrow>T2" |
|
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
114 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
115 |
equivariance typing |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
116 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
117 |
lemma typing_implies_valid: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
118 |
assumes a: "\<Gamma> \<turnstile> t : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
119 |
shows "valid \<Gamma>" |
25867 | 120 |
using a by (induct) (auto dest: v2_elim) |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
121 |
|
25867 | 122 |
text {* |
123 |
we have to explicitly state that nominal_inductive should strengthen |
|
124 |
over the variable x (since x is not a binder) |
|
125 |
*} |
|
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
126 |
nominal_inductive typing |
23233 | 127 |
avoids t_lLam: x |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
128 |
by (auto simp add: fresh_prod dest: v2_elim typing_implies_valid) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
129 |
|
23233 | 130 |
text {* strong induction principle for typing *} |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
131 |
thm typing.strong_induct |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
132 |
|
23233 | 133 |
text {* sub-contexts *} |
134 |
||
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
135 |
abbreviation |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
136 |
"sub_context" :: "cxt \<Rightarrow> cxt \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
137 |
where |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
138 |
"\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
139 |
|
23233 | 140 |
lemma weakening_almost_automatic: |
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
23760
diff
changeset
|
141 |
fixes \<Gamma>1 \<Gamma>2 :: cxt |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
142 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
143 |
and b: "\<Gamma>1 \<subseteq> \<Gamma>2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
144 |
and c: "valid \<Gamma>2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
145 |
shows "\<Gamma>2 \<turnstile> t : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
146 |
using a b c |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
147 |
apply(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
23233 | 148 |
apply(auto) |
149 |
apply(drule_tac x="(x,T1)#\<Gamma>2" in meta_spec) |
|
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
150 |
apply(auto intro!: t_lLam) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
151 |
done |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
152 |
|
23233 | 153 |
lemma weakening_in_more_detail: |
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
23760
diff
changeset
|
154 |
fixes \<Gamma>1 \<Gamma>2 :: cxt |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
155 |
assumes a: "\<Gamma>1 \<turnstile> t : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
156 |
and b: "\<Gamma>1 \<subseteq> \<Gamma>2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
157 |
and c: "valid \<Gamma>2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
158 |
shows "\<Gamma>2 \<turnstile> t : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
159 |
using a b c |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
160 |
proof(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
161 |
case (t_lPar \<Gamma>1 x T \<Gamma>2) (* variable case *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
162 |
have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
163 |
moreover |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
164 |
have "valid \<Gamma>2" by fact |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
165 |
moreover |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
166 |
have "(x,T)\<in> set \<Gamma>1" by fact |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
167 |
ultimately show "\<Gamma>2 \<turnstile> lPar x : T" by auto |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
168 |
next |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
169 |
case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *) |
23467 | 170 |
have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact+ (* variable convention *) |
23233 | 171 |
have ih: "\<lbrakk>(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2; valid ((x,T1)#\<Gamma>2)\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" by fact |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
172 |
have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
173 |
then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
174 |
moreover |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
175 |
have "valid \<Gamma>2" by fact |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
176 |
then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2) |
23233 | 177 |
ultimately have "(x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" using ih by simp |
23315 | 178 |
with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by auto |
179 |
next |
|
25867 | 180 |
case (t_lApp \<Gamma>1 t1 T1 T2 t2 \<Gamma>2) |
181 |
then show "\<Gamma>2 \<turnstile> lApp t1 t2 : T2" by auto |
|
23315 | 182 |
qed |
23143
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
183 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
184 |
end |