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 498 e7bb6bbe7576
parent 496 8f1bf5266ebc
child 506 91c374abde06
equal deleted inserted replaced
497:b663bc007d00 498:e7bb6bbe7576 
   171   "fmap \<equiv> map"
 
   171   "fmap \<equiv> map"
 
   172 
   172 
   173 term map
 
   173 term map
 
   174 term fmap
 
   174 term fmap
 
   175 thm fmap_def
 
   175 thm fmap_def
 
   176 
       
   177 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 
       
   178 
   176 
   179 lemma memb_rsp:
 
   177 lemma memb_rsp:
 
   180   fixes z
 
   178   fixes z
 
   181   assumes a: "x \<approx> y"
 
   179   assumes a: "x \<approx> y"
 
   182   shows "(z memb x) = (z memb y)"
 
   180   shows "(z memb x) = (z memb y)"
 
   297 ML {* val rsp_thms =
 
   295 ML {* val rsp_thms =
 
   298   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
   296   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
   299 
   297 
   300 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   298 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   301 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 
   299 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 
   302 ML {* val consts = lookup_quot_consts defs *}
 
   300 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] *}
 
   303 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] defs *}
 
       
   304 
   301 
   305 lemma "IN x EMPTY = False"
 
   302 lemma "IN x EMPTY = False"
 
   306 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 
   303 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 
   307 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   304 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   308 apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   305 apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   309 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 
   306 apply(tactic {* clean_tac @{context} [quot] 1*})
 
   310 done
 
   307 done
 
   311 
   308 
   312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   309 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   313 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   310 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   314 
   311 
   349 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   350 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   347 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   351 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   348 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   352 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   349 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   353 prefer 2
 
   350 prefer 2
 
   354 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 
   351 apply(tactic {* clean_tac @{context} [quot] 1 *})
 
   355 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   352 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   353 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   357 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   354 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   358 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   355 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   359 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   431 quotient_def
 
   428 quotient_def
 
   432   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 
   429   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 
   433 where
 
   430 where
 
   434   "INSERT2 \<equiv> op #"
 
   431   "INSERT2 \<equiv> op #"
 
   435 
   432 
   436 ML {* val defs = @{thms EMPTY2_def INSERT2_def} @ defs *}
 
       
   437 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
 
   433 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
 
   438 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
 
   434 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
 
   439 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot defs *}
 
   435 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
 
   440 
   436 
   441 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"
 
   437 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"
 
   442 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   438 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   443 done
 
   439 done
 
   444 
   440 
   468   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   464   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   469   apply (auto simp add: FUN_REL_EQ)
 
   465   apply (auto simp add: FUN_REL_EQ)
 
   470   sorry
 
   466   sorry
 
   471 
   467 
   472 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   468 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   473 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
 
   469 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
 
   474 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot defs *}
 
       
   475 
   470 
   476 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   471 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   477 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   472 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   478 done
 
   473 done
 
   479 
   474 
   480 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
 
   475 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
 
   481 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 
   476 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 
   482 done
 
   477 done
 
   483 
   478 
   484 ML {* qconsts_lookup @{theory} "EMPTY" *}
 
       
   485 thm EMPTY_def
 
       
   486 
       
   487 
   479 
   488 end
 
   480 end
nominal2