Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LFex.thy
changeset 441 42e7f323913a
parent 440 0af649448a11
child 445 f1c0a66284d3
equal deleted inserted replaced
440:0af649448a11 441:42e7f323913a 
   179   perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
 
   179   perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
 
   180 where
 
   180 where
 
   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 (* TODO/FIXME: Think whether these RSP theorems are true. *)
 
   183 (* TODO/FIXME: Think whether these RSP theorems are true. *)
 
   184 lemma KPi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi"
 
   184 lemma kpi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
 
   185 sorry
 
   185 lemma tconst_rsp: "(op = ===> aty) TConst TConst" sorry
 
   186 
   186 lemma tapp_rsp: "(aty ===> atrm ===> aty) TApp TApp" sorry
 
   187 lemma perm_kind_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>"
 
   187 lemma tpi_rsp: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
 
   188 sorry
 
   188 lemma var_rsp: "(op = ===> atrm) Var Var" sorry
 
   189 
   189 lemma app_rsp: "(atrm ===> atrm ===> atrm) App App" sorry
 
   190 lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty"
 
   190 lemma const_rsp: "(op = ===> atrm) Const Const" sorry
 
   191 sorry
 
   191 lemma lam_rsp: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
   192 
   192 
   193 lemma fv_kind_rsp: "(akind ===> op =) fv_kind fv_kind"
 
   193 lemma perm_kind_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
 
   194 sorry
 
   194 lemma perm_ty_rsp: "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
 
       
   195 lemma perm_trm_rsp: "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
       
   196 
       
   197 lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty" sorry
 
       
   198 lemma fv_kind_rsp: "(akind ===> op =) fv_kind fv_kind" sorry
 
       
   199 lemma fv_trm_rsp: "(atrm ===> op =) fv_trm fv_trm" sorry
 
       
   200 
   195 
   201 
   196 thm akind_aty_atrm.induct
 
   202 thm akind_aty_atrm.induct
 
   197 
   203 
   198 
   204 
   199 ML {* val defs =
 
   205 ML {* val defs =
 
   316 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
   322 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
   317 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   323 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   318 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
 
   324 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
 
   319 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   325 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   320 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
 
   326 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
 
   321 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms KPi_rsp}) 1*})
 
   327 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
 
   322 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   328 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   323 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   329 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   324 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   330 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   325 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 
   331 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 
   326 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 
   332 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 
   348 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
 
   354 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
 
   349 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 
   355 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 
   350 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
 
   356 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
 
   351 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 
   357 apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 
   352 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
   358 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
   353 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms KPi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
 
   359 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
 
   354 
   360 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   355 
   361 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
 
   356 
   362 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   357 
   363 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   358 
   364 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   359 
   365 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   360 
   366 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   361 
   367 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   362 
   368 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   363 
   369 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   364 
   370 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
   365 
   371 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   372 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   373 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   374 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   375 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   376 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   377 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   378 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
       
   379 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   380 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
       
   381 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   382 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
       
   383 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   384 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
       
   385 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 
       
   386 apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 
       
   387 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
       
   388 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
 
       
   389 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
 
       
   390 apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 
       
   391 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
 
       
   392 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   393 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
 
       
   394 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   395 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
 
       
   396 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   397 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
 
       
   398 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   399 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
 
       
   400 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   401 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   402 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   403 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   404 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   405 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   406 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   407 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   408 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   409 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   410 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   411 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   412 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   413 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   414 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   415 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   416 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   417 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   418 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   419 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
       
   420 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   421 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
       
   422 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
 
       
   423 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   424 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   425 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   426 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   427 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   428 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   429 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   430 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   431 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   432 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   433 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   434 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   435 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   436 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   437 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   438 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   439 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   440 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   441 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   442 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   443 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   444 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   445 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   446 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   447 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   448 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
       
   449 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   450 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
       
   451 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   452 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
 
       
   453 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   454 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
 
       
   455 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   456 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
 
       
   457 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
 
       
   458 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   459 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
 
       
   460 apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 
       
   461 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
 
       
   462 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
 
       
   463 done
 
   366 
   464 
   367 print_quotients
 
   465 print_quotients
 
   368 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*})
 
       
   369 
       
   370 
       
   371 ML {* val consts = lookup_quot_consts defs *}
 
       
   372 
       
   373 ML {*
 
       
   374 val rty_qty_rel =
 
       
   375   [(@{typ kind}, (@{typ KIND}, @{term akind})),
 
       
   376    (@{typ ty}, (@{typ TY}, @{term aty})),
 
       
   377    (@{typ trm}, (@{typ TRM}, @{term atrm}))]
 
       
   378 *}
 
       
   379 
       
   380 print_quotients
 
       
   381 
       
   382 ML {* val rty = [@{typ }] *}
 
       
   383 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 
       
   384 ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *}
 
       
   385 prove {* build_regularize_goal t_a rty rel @{context}
 
       
   386 
   466 
   387 end
 
   467 end
 
   388 
   468 
   389 
   469 
   390 
   470
nominal2