author | urbanc |
Thu, 31 May 2007 09:48:20 +0200 | |
changeset 23143 | f72bc42882ea |
child 23233 | 76462538f349 |
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 *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
4 |
(* terms; the nominal infrastructure can derive *) |
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 |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
9 |
imports "../Nominal" |
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 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
14 |
(* Curry-style lambda terms in locally nameless *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
15 |
(* representation without any binders *) |
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 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
22 |
lemma llam_cases: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
23 |
"(\<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
|
24 |
(\<exists>t1. t = lLam t1)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
25 |
by (induct t rule: llam.weak_induct) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
26 |
(auto simp add: llam.inject) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
27 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
28 |
consts llam_size :: "llam \<Rightarrow> nat" |
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 |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
31 |
"llam_size (lPar a) = 1" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
32 |
"llam_size (lVar n) = 1" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
33 |
"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
|
34 |
"llam_size (lLam t) = 1 + (llam_size t)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
35 |
by (rule TrueI)+ |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
36 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
37 |
function |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
38 |
vsub :: "llam \<Rightarrow> nat \<Rightarrow> llam \<Rightarrow> llam" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
39 |
where |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
40 |
vsub_lPar: "vsub (lPar p) x s = lPar p" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
41 |
| 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
|
42 |
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
|
43 |
| 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
|
44 |
| 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
|
45 |
using llam_cases |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
46 |
apply(auto simp add: llam.inject) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
47 |
apply(rotate_tac 4) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
48 |
apply(drule_tac x="a" in meta_spec) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
49 |
apply(blast) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
50 |
done |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
51 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
52 |
termination vsub |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
53 |
proof |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
54 |
show "wf (measure (llam_size \<circ> fst))" by simp |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
55 |
qed (auto) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
56 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
57 |
lemma vsub_eqvt[eqvt]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
58 |
fixes pi::"name prm" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
59 |
shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
60 |
by (induct t arbitrary: n rule: llam.weak_induct) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
61 |
(simp_all add: perm_nat_def) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
62 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
63 |
constdefs |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
64 |
freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
65 |
"freshen t p \<equiv> vsub t 0 (lPar p)" |
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 |
lemma freshen_eqvt[eqvt]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
68 |
fixes pi::"name prm" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
72 |
nominal_datatype ty = |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
73 |
TVar "nat" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
74 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
75 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
76 |
lemma ty_perm[simp]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
77 |
fixes pi ::"name prm" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
78 |
and T ::"ty" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
79 |
shows "pi\<bullet>T = T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
80 |
by (induct T rule: ty.weak_induct) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
81 |
(simp_all add: perm_nat_def) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
82 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
83 |
lemma ty_fresh[simp]: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
84 |
fixes x::"name" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
85 |
and T::"ty" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
86 |
shows "x\<sharp>T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
87 |
by (induct T rule: ty.weak_induct) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
88 |
(simp_all add: fresh_nat) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
89 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
90 |
text {* valid contexts *} |
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 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
93 |
inductive2 |
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>" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
104 |
using valid.cases[OF a] |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
105 |
by (auto) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
106 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
107 |
inductive2 |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
108 |
typing :: "cxt\<Rightarrow>llam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
109 |
where |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
110 |
t_lPar[intro]: "\<lbrakk>valid \<Gamma>; (a,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lPar a : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
111 |
| t_lApp[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lApp t1 t2 : T2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
112 |
| t_lLam[intro]: "\<lbrakk>a\<sharp>t; ((a,T1)#\<Gamma>) \<turnstile> (freshen t a) : T2\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lLam t : T1\<rightarrow>T2" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
113 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
114 |
equivariance typing |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
115 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
116 |
lemma typing_implies_valid: |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
117 |
assumes a: "\<Gamma> \<turnstile> t : T" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
118 |
shows "valid \<Gamma>" |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
119 |
using a |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
120 |
by (induct) (auto dest: v2_elim) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
121 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
122 |
nominal_inductive typing |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
123 |
avoids t_lLam: a |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
124 |
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
|
125 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
126 |
(* strong induction principle for typing *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
127 |
thm typing.strong_induct |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
128 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
129 |
abbreviation |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
130 |
"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
|
131 |
where |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
132 |
"\<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
|
133 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
134 |
lemma weakening_automatic: |
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) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
141 |
apply(auto)[1] |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
142 |
apply(auto)[1] |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
143 |
apply(drule_tac x="(a,T1)#\<Gamma>2" in meta_spec) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
144 |
apply(auto intro!: t_lLam) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
145 |
done |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
146 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
147 |
lemma weakening: |
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 *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
163 |
have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact (* variable convention *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
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 |
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) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
170 |
ultimately have "((x,T1)#\<Gamma>2) \<turnstile> freshen t x : T2" using ih by simp |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
171 |
with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by (auto simp add: fresh_prod) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
172 |
qed (auto) (* app case *) |
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
173 |
|
f72bc42882ea
a theory using locally nameless terms and strong induction principles
urbanc
parents:
diff
changeset
|
174 |
end |