equal
deleted
inserted
replaced
47 |
47 |
48 text {* Strong induction principle for typing judgements *} |
48 text {* Strong induction principle for typing judgements *} |
49 |
49 |
50 nominal_inductive typing |
50 nominal_inductive typing |
51 avoids t_Lam: "x" |
51 avoids t_Lam: "x" |
52 by (simp_all add: fresh_star_def fresh_ty lam.fresh) |
52 by (simp_all add: fresh_star_def fresh_ty) |
53 |
53 |
54 |
54 |
55 abbreviation |
55 abbreviation |
56 "sub_context" :: "(name \<times> ty) list \<Rightarrow> (name \<times> ty) list \<Rightarrow> bool" (infixr "\<subseteq>" 60) |
56 "sub_context" :: "(name \<times> ty) list \<Rightarrow> (name \<times> ty) list \<Rightarrow> bool" (infixr "\<subseteq>" 60) |
57 where |
57 where |
120 |
120 |
121 equivariance typing2 |
121 equivariance typing2 |
122 |
122 |
123 nominal_inductive typing2 |
123 nominal_inductive typing2 |
124 avoids t2_Lam: "x" |
124 avoids t2_Lam: "x" |
125 by (simp_all add: fresh_star_def fresh_ty lam.fresh) |
125 by (simp_all add: fresh_star_def fresh_ty) |
126 |
126 |
127 lemma weakening_version3: |
127 lemma weakening_version3: |
128 fixes \<Gamma>::"(name \<times> ty) fset" |
128 fixes \<Gamma>::"(name \<times> ty) fset" |
129 assumes a: "\<Gamma> 2\<turnstile> t : T" |
129 assumes a: "\<Gamma> 2\<turnstile> t : T" |
130 and b: "(x, T') |\<notin>| \<Gamma>" |
130 and b: "(x, T') |\<notin>| \<Gamma>" |
131 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
131 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
132 using a b |
132 using a b |
133 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct) |
133 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct) |
134 apply(auto)[2] |
134 apply(auto)[2] |
135 apply(rule t2_Lam) |
135 apply(rule t2_Lam) |
136 apply(simp add: fresh_insert_fset fresh_Pair fresh_ty) |
136 apply(simp add: fresh_insert_fset fresh_ty) |
137 apply(simp) |
137 apply(simp) |
138 apply(drule_tac x="xa" in meta_spec) |
138 apply(drule_tac x="xa" in meta_spec) |
139 apply(drule meta_mp) |
139 apply(drule meta_mp) |
140 apply(simp add: fresh_at_base) |
140 apply(simp add: fresh_at_base) |
141 apply(simp add: insert_fset_left_comm) |
141 apply(simp add: insert_fset_left_comm) |
145 fixes \<Gamma>::"(name \<times> ty) fset" |
145 fixes \<Gamma>::"(name \<times> ty) fset" |
146 assumes a: "\<Gamma> 2\<turnstile> t : T" |
146 assumes a: "\<Gamma> 2\<turnstile> t : T" |
147 and b: "(x, T') |\<notin>| \<Gamma>" |
147 and b: "(x, T') |\<notin>| \<Gamma>" |
148 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
148 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
149 using a b |
149 using a b |
150 apply(induct \<Gamma> t T arbitrary: x) |
150 apply(induct \<Gamma> t T arbitrary: x T') |
151 apply(auto)[2] |
151 apply(auto)[2] |
|
152 apply(blast) |
|
153 apply(simp) |
|
154 apply(rule_tac ?'a="name" and x="(x, xa, t, T', \<Gamma>)" in obtain_fresh) |
|
155 apply(rule_tac t= "Lam [x]. t" and s="Lam [a]. ((a \<leftrightarrow> x) \<bullet> t)" in subst) |
|
156 defer |
152 apply(rule t2_Lam) |
157 apply(rule t2_Lam) |
|
158 apply(simp add: fresh_insert_fset) |
153 oops |
159 oops |
|
160 |
|
161 |
154 |
162 |
155 end |
163 end |
156 |
164 |
157 |
165 |
158 |
166 |