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.
FSet.thy
changeset 507 f7569f994195
parent 506 91c374abde06
child 509 d62b6517a0ab
equal deleted inserted replaced
506:91c374abde06 507:f7569f994195 
   406 
   406 
   407 ML {* quot *}
 
   407 ML {* quot *}
 
   408 thm quotient_thm
 
   408 thm quotient_thm
 
   409 
   409 
   410 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   410 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   411 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   411 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
       
   412 apply(tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 
       
   413 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
       
   414 prefer 2
 
       
   415 apply(tactic {* clean_tac @{context} 1 *})
 
       
   416 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   417 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   418 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   419 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   420 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   421 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   422 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   423 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   424 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   425 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   426 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   427 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   428 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   429 apply(tactic {* APPLY_RSP_TAC @{context} 1*})
 
       
   430 thm quotient_thm
 
       
   431 apply(rule quotient_thm(3))
 
       
   432 apply(rule quotient_thm)
 
       
   433 apply(rule quotient_thm)
 
       
   434 apply(rule quotient_thm)
 
       
   435 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   436 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   437 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   438 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   439 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   440 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   441 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   442 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   443 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   444 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   445 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   446 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   447 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   448 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   449 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   450 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   451 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   452 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   453 apply(tactic {* APPLY_RSP_TAC @{context} 1*})
 
       
   454 thm quotient_thm
 
       
   455 apply(rule quotient_thm(3))
 
       
   456 apply(rule quotient_thm)
 
       
   457 apply(rule quotient_thm)
 
       
   458 apply(rule quotient_thm)
 
       
   459 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   460 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   461 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   462 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   463 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   464 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   465 apply(tactic {* APPLY_RSP_TAC @{context} 1*})
 
       
   466 thm quotient_thm
 
       
   467 apply(rule quotient_thm(3))
 
       
   468 apply(rule quotient_thm)
 
       
   469 apply(rule quotient_thm)
 
       
   470 apply(rule quotient_thm)
 
       
   471 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   472 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   473 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   474 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   475 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   476 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   477 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   478 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   479 apply(tactic {* APPLY_RSP_TAC @{context} 1*})
 
       
   480 thm quotient_thm
 
       
   481 apply(rule quotient_thm(3))
 
       
   482 apply(rule quotient_thm)
 
       
   483 apply(rule quotient_thm)
 
       
   484 apply(rule quotient_thm)
 
       
   485 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   486 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   487 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   488 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   489 apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
 
       
   490 (* apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) *)
 
   412 done
 
   491 done
 
   413 
   492 
   414 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   493 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   415 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   494 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   416 done
 
   495 done
 
   432   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 
   511   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 
   433 where
 
   512 where
 
   434   "INSERT2 \<equiv> op #"
 
   513   "INSERT2 \<equiv> op #"
 
   435 
   514 
   436 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
 
   515 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
 
   437 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
 
   516 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   438 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
 
   517 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
   439 
   518 
   440 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   519 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   441 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   520 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   442 done
 
   521 done
 
   443 
   522 
   467   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   546   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   468   apply (auto simp add: FUN_REL_EQ)
 
   547   apply (auto simp add: FUN_REL_EQ)
 
   469   sorry
 
   548   sorry
 
   470 
   549 
   471 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   550 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   472 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
 
   551 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv]  *}
 
   473 
   552 
   474 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   553 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   475 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   554 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   476 done
 
   555 done
 
   477 
   556
nominal2