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