equal
deleted
inserted
replaced
105 |
105 |
106 inductive |
106 inductive |
107 valid2 :: "(name \<times> ty) fset \<Rightarrow> bool" |
107 valid2 :: "(name \<times> ty) fset \<Rightarrow> bool" |
108 where |
108 where |
109 v2_Empty[intro]: "valid2 {||}" |
109 v2_Empty[intro]: "valid2 {||}" |
110 | v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (insert_fset (x, T) Gamma)" |
110 | v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (finsert (x, T) Gamma)" |
111 |
111 |
112 equivariance valid2 |
112 equivariance valid2 |
113 |
113 |
114 inductive |
114 inductive |
115 typing2 :: "(name \<times> ty) fset \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ 2\<turnstile> _ : _" [60,60,60] 60) |
115 typing2 :: "(name \<times> ty) fset \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ 2\<turnstile> _ : _" [60,60,60] 60) |
116 where |
116 where |
117 t2_Var[intro]: "\<lbrakk>valid2 \<Gamma>; (x, T) |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Var x : T" |
117 t2_Var[intro]: "\<lbrakk>valid2 \<Gamma>; (x, T) |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Var x : T" |
118 | t2_App[intro]: "\<lbrakk>\<Gamma> 2\<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> 2\<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> App t1 t2 : T2" |
118 | t2_App[intro]: "\<lbrakk>\<Gamma> 2\<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> 2\<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> App t1 t2 : T2" |
119 | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; insert_fset (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2" |
119 | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; finsert (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2" |
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" |
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_ty) |
136 apply(simp add: fresh_finsert fresh_ty) |
137 apply(simp) |
137 apply(force) |
138 apply(drule_tac x="xa" in meta_spec) |
|
139 apply(drule meta_mp) |
|
140 apply(simp add: fresh_at_base) |
|
141 apply(simp add: insert_fset_left_comm) |
|
142 done |
138 done |
143 |
139 |
144 lemma weakening_version4: |
140 lemma weakening_version4: |
145 fixes \<Gamma>::"(name \<times> ty) fset" |
141 fixes \<Gamma>::"(name \<times> ty) fset" |
146 assumes a: "\<Gamma> 2\<turnstile> t : T" |
142 assumes a: "\<Gamma> 2\<turnstile> t : T" |
153 apply(simp) |
149 apply(simp) |
154 apply(rule_tac ?'a="name" and x="(x, xa, t, T', \<Gamma>)" in obtain_fresh) |
150 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) |
151 apply(rule_tac t= "Lam [x]. t" and s="Lam [a]. ((a \<leftrightarrow> x) \<bullet> t)" in subst) |
156 defer |
152 defer |
157 apply(rule t2_Lam) |
153 apply(rule t2_Lam) |
158 apply(simp add: fresh_insert_fset) |
154 apply(simp add: fresh_finsert) |
159 oops |
155 oops |
160 |
156 |
161 |
157 |
162 |
158 |
163 end |
159 end |