181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
182 |
182 |
183 end |
183 end |
184 |
184 |
185 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
185 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
186 lemma kpi_rsp[quotient_rsp]: |
186 lemma kpi_rsp[quot_respect]: |
187 "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry |
187 "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry |
188 lemma tconst_rsp[quotient_rsp]: |
188 lemma tconst_rsp[quot_respect]: |
189 "(op = ===> aty) TConst TConst" sorry |
189 "(op = ===> aty) TConst TConst" sorry |
190 lemma tapp_rsp[quotient_rsp]: |
190 lemma tapp_rsp[quot_respect]: |
191 "(aty ===> atrm ===> aty) TApp TApp" sorry |
191 "(aty ===> atrm ===> aty) TApp TApp" sorry |
192 lemma tpi_rsp[quotient_rsp]: |
192 lemma tpi_rsp[quot_respect]: |
193 "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry |
193 "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry |
194 lemma var_rsp[quotient_rsp]: |
194 lemma var_rsp[quot_respect]: |
195 "(op = ===> atrm) Var Var" sorry |
195 "(op = ===> atrm) Var Var" sorry |
196 lemma app_rsp[quotient_rsp]: |
196 lemma app_rsp[quot_respect]: |
197 "(atrm ===> atrm ===> atrm) App App" sorry |
197 "(atrm ===> atrm ===> atrm) App App" sorry |
198 lemma const_rsp[quotient_rsp]: |
198 lemma const_rsp[quot_respect]: |
199 "(op = ===> atrm) Const Const" sorry |
199 "(op = ===> atrm) Const Const" sorry |
200 lemma lam_rsp[quotient_rsp]: |
200 lemma lam_rsp[quot_respect]: |
201 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry |
201 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry |
202 |
202 |
203 lemma perm_kind_rsp[quotient_rsp]: |
203 lemma perm_kind_rsp[quot_respect]: |
204 "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry |
204 "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry |
205 lemma perm_ty_rsp[quotient_rsp]: |
205 lemma perm_ty_rsp[quot_respect]: |
206 "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry |
206 "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry |
207 lemma perm_trm_rsp[quotient_rsp]: |
207 lemma perm_trm_rsp[quot_respect]: |
208 "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry |
208 "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry |
209 |
209 |
210 lemma fv_ty_rsp[quotient_rsp]: |
210 lemma fv_ty_rsp[quot_respect]: |
211 "(aty ===> op =) fv_ty fv_ty" sorry |
211 "(aty ===> op =) fv_ty fv_ty" sorry |
212 lemma fv_kind_rsp[quotient_rsp]: |
212 lemma fv_kind_rsp[quot_respect]: |
213 "(akind ===> op =) fv_kind fv_kind" sorry |
213 "(akind ===> op =) fv_kind fv_kind" sorry |
214 lemma fv_trm_rsp[quotient_rsp]: |
214 lemma fv_trm_rsp[quot_respect]: |
215 "(atrm ===> op =) fv_trm fv_trm" sorry |
215 "(atrm ===> op =) fv_trm fv_trm" sorry |
216 |
216 |
217 |
217 |
218 thm akind_aty_atrm.induct |
218 thm akind_aty_atrm.induct |
219 thm kind_ty_trm.induct |
219 thm kind_ty_trm.induct |