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 232 38810e1df801
parent 231 c643938b846a
parent 228 268a727b0f10
child 233 fcff14e578d3
equal deleted inserted replaced
231:c643938b846a 232:38810e1df801 
   204   fixes a b :: "'a list"
 
   204   fixes a b :: "'a list"
 
   205   assumes e: "a \<approx> b"
 
   205   assumes e: "a \<approx> b"
 
   206   shows "card1 a = card1 b"
 
   206   shows "card1 a = card1 b"
 
   207   using e by induct (simp_all add:memb_rsp)
 
   207   using e by induct (simp_all add:memb_rsp)
 
   208 
   208 
   209 lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
 
   209 lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
 
   210   by (simp add: card1_rsp)
 
   210   by (simp add: card1_rsp)
 
   211 
   211 
   212 lemma cons_rsp:
 
   212 lemma cons_rsp:
 
   213   fixes z
 
   213   fixes z
 
   214   assumes a: "xs \<approx> ys"
 
   214   assumes a: "xs \<approx> ys"
 
   215   shows "(z # xs) \<approx> (z # ys)"
 
   215   shows "(z # xs) \<approx> (z # ys)"
 
   216   using a by (rule list_eq.intros(5))
 
   216   using a by (rule list_eq.intros(5))
 
   217 
   217 
   218 lemma ho_cons_rsp:
 
   218 lemma ho_cons_rsp:
 
   219   "op = ===> op \<approx> ===> op \<approx> op # op #"
 
   219   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   220   by (simp add: cons_rsp)
 
   220   by (simp add: cons_rsp)
 
   221 
   221 
   222 lemma append_rsp_fst:
 
   222 lemma append_rsp_fst:
 
   223   assumes a : "list_eq l1 l2"
 
   223   assumes a : "list_eq l1 l2"
 
   224   shows "(l1 @ s) \<approx> (l2 @ s)"
 
   224   shows "(l1 @ s) \<approx> (l2 @ s)"
 
   271   using b apply (assumption)
 
   271   using b apply (assumption)
 
   272   apply (rule append_sym_rsp)
 
   272   apply (rule append_sym_rsp)
 
   273   done
 
   273   done
 
   274 
   274 
   275 lemma ho_append_rsp:
 
   275 lemma ho_append_rsp:
 
   276   "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
 
   276   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   277   by (simp add: append_rsp)
 
   277   by (simp add: append_rsp)
 
   278 
   278 
   279 lemma map_rsp:
 
   279 lemma map_rsp:
 
   280   assumes a: "a \<approx> b"
 
   280   assumes a: "a \<approx> b"
 
   281   shows "map f a \<approx> map f b"
 
   281   shows "map f a \<approx> map f b"
 
   283   apply (induct)
 
   283   apply (induct)
 
   284   apply(auto intro: list_eq.intros)
 
   284   apply(auto intro: list_eq.intros)
 
   285   done
 
   285   done
 
   286 
   286 
   287 lemma fun_rel_id:
 
   287 lemma fun_rel_id:
 
   288   "op = ===> op = \<equiv> op ="
 
   288   "(op = ===> op =) \<equiv> op ="
 
   289   apply (rule eq_reflection)
 
   289   apply (rule eq_reflection)
 
   290   apply (rule ext)
 
   290   apply (rule ext)
 
   291   apply (rule ext)
 
   291   apply (rule ext)
 
   292   apply (simp)
 
   292   apply (simp)
 
   293   apply (auto)
 
   293   apply (auto)
 
   294   apply (rule ext)
 
   294   apply (rule ext)
 
   295   apply (simp)
 
   295   apply (simp)
 
   296   done
 
   296   done
 
   297 
   297 
   298 lemma ho_map_rsp:
 
   298 lemma ho_map_rsp:
 
   299   "op = ===> op = ===> op \<approx> ===> op \<approx> map map"
 
   299   "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map"
 
   300   by (simp add: fun_rel_id map_rsp)
 
   300   by (simp add: fun_rel_id map_rsp)
 
   301 
   301 
   302 lemma map_append :
 
   302 lemma map_append :
 
   303   "(map f ((a::'a list) @ b)) \<approx>
 
   303   "(map f ((a::'a list) @ b)) \<approx>
 
   304   ((map f a) ::'a list) @ (map f b)"
 
   304   ((map f a) ::'a list) @ (map f b)"
 
   305  by simp (rule list_eq_refl)
 
   305  by simp (rule list_eq_refl)
 
   306 
   306 
   307 thm list.induct
 
   307 ML {* val rty = @{typ "'a list"} *}
 
   308 lemma list_induct_hol4:
 
   308 ML {* val qty = @{typ "'a fset"} *}
 
   309   fixes P :: "'a list \<Rightarrow> bool"
 
   309 ML {* val rel = @{term "list_eq"} *}
 
   310   assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
 
   310 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
 
   311   shows "\<forall>l. (P l)"
 
   311 ML {* val rel_refl = @{thm list_eq_refl} *}
 
   312   using a
 
   312 ML {* val quot = @{thm QUOTIENT_fset} *}
 
   313   apply (rule_tac allI)
 
   313 ML {* val rsp_thms =
 
   314   apply (induct_tac "l")
 
   314   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}
 
   315   apply (simp)
 
   315   @ @{thms ho_all_prs ho_ex_prs} *}
 
   316   apply (metis)
 
   316 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}
 
   317   done
 
   317 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}
 
   318 
   318 ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 
   319 ML {* (atomize_thm @{thm list_induct_hol4}) *}
 
   319 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 
   320 
       
   321 ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
 
       
   322 
       
   323 prove list_induct_r: {*
 
       
   324    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
 
       
   325   apply (simp only: equiv_res_forall[OF equiv_list_eq])
 
       
   326   thm RIGHT_RES_FORALL_REGULAR
 
       
   327   apply (rule RIGHT_RES_FORALL_REGULAR)
 
       
   328   prefer 2
 
       
   329   apply (assumption)
 
       
   330   apply (metis)
 
       
   331   done
 
       
   332 
       
   333 (* The all_prs and ex_prs should be proved for the instance... *)
 
       
   334 ML {*
 
   320 ML {*
 
   335 fun r_mk_comb_tac_fset ctxt =
 
   321   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
 
   336   r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
 
   322                 @{const_name "membship"}, @{const_name "card1"},
 
   337   (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 
   323                 @{const_name "append"}, @{const_name "fold1"},
 
   338 *}
 
   324                 @{const_name "map"}];
 
   339 
   325 *}
 
   340 
   326 
   341 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
 
   327 ML {* fun lift_thm_fset lthy t =
 
   342 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
   328   lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
 
   343 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
   329 *}
 
   344 
   330 
   345 ML {* val rty = @{typ "'a list"} *}
 
   331 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
 
   346 
   332 by (simp add: list_eq_refl)
 
   347 ML {*
 
   333 
   348 fun r_mk_comb_tac_fset ctxt =
 
   334 ML {* lift_thm_fset @{context} @{thm m1} *}
 
   349   r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
 
   335 ML {* lift_thm_fset @{context} @{thm m2} *}
 
   350   (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 
   336 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 
   351 *}
 
   337 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 
   352 
   338 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 
   353 
   339 ML {* lift_thm_fset @{context} @{thm map_append} *}
 
   354 ML {* trm_r *}
 
   340 ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *}
 
   355 prove list_induct_tr: trm_r
 
       
   356 apply (atomize(full))
 
       
   357 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   358 done
 
       
   359 
       
   360 prove list_induct_t: trm
 
       
   361 apply (simp only: list_induct_tr[symmetric])
 
       
   362 apply (tactic {* rtac thm 1 *})
 
       
   363 done
 
       
   364 
       
   365 thm m2
 
       
   366 ML {* atomize_thm @{thm m2} *}
 
       
   367 
       
   368 prove m2_r_p: {*
 
       
   369    build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
 
       
   370   apply (simp add: equiv_res_forall[OF equiv_list_eq])
 
       
   371 done
 
       
   372 
       
   373 ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *}
 
       
   374 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
   375 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
   376 prove m2_t_p: m2_t_g
 
       
   377 apply (atomize(full))
 
       
   378 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   379 done
 
       
   380 
       
   381 prove m2_t: m2_t
 
       
   382 apply (simp only: m2_t_p[symmetric])
 
       
   383 apply (tactic {* rtac m2_r 1 *})
 
       
   384 done
 
       
   385 
       
   386 lemma id_apply2 [simp]: "id x \<equiv> x"
 
       
   387   by (simp add: id_def)
 
       
   388 
       
   389 ML {* val quot = @{thm QUOTIENT_fset} *}
 
       
   390 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
 
       
   391 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 
       
   392 
       
   393 ML {*
 
       
   394   fun simp_lam_prs lthy thm =
 
       
   395     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
 
       
   396     handle _ => thm
 
       
   397 *}
 
       
   398 
       
   399 ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *}
 
       
   400 
       
   401 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *}
 
       
   402 
       
   403 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 
       
   404 ML {* ObjectLogic.rulify rthm *}
 
       
   405 
       
   406 
       
   407 ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *}
 
       
   408 
       
   409 prove card1_suc_r_p: {*
 
       
   410    build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
 
       
   411   apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
 
       
   412 done
 
       
   413 
       
   414 ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *}
 
       
   415 ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
   416 ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
   417 prove card1_suc_t_p: card1_suc_t_g
 
       
   418 apply (atomize(full))
 
       
   419 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   420 done
 
       
   421 
       
   422 prove card1_suc_t: card1_suc_t
 
       
   423 apply (simp only: card1_suc_t_p[symmetric])
 
       
   424 apply (tactic {* rtac card1_suc_r 1 *})
 
       
   425 done
 
       
   426 
       
   427 ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
 
       
   428 ML {* val card1_suc_t' = simp_lam_prs @{context} @{thm card1_suc_t} *}
 
       
   429 ML {* val ithm = simp_allex_prs @{context} quot card1_suc_t' *}
 
       
   430 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 
       
   431 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
 
       
   432 ML {* ObjectLogic.rulify qthm *}
 
       
   433 
   341 
   434 thm fold1.simps(2)
 
   342 thm fold1.simps(2)
 
   435 thm list.recs(2)
 
   343 thm list.recs(2)
 
   436 thm map_append
 
       
   437 
   344 
   438 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
 
   345 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
 
   439 (*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
 
   346 (*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
 
   440   ML_prf {*  fun tac ctxt =
 
   347   ML_prf {*  fun tac ctxt =
 
   441        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
 
   348        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
 
   447 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
 
   354 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
 
   448 ML {*
 
   355 ML {*
 
   449   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
 
   356   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
 
   450   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 
   357   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 
   451 *}
 
   358 *}
 
   452 
   359 (*prove rg
 
   453 prove rg
 
       
   454 apply(atomize(full))
 
   360 apply(atomize(full))
 
   455 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
   361 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
   456 done
 
   362 done*)
 
   457 
       
   458 ML {* val ind_r_t =
 
   363 ML {* val ind_r_t =
 
   459   Toplevel.program (fn () =>
 
   364   Toplevel.program (fn () =>
 
   460   repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
 
   365   repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
 
   461    @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
 
   366    @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
 
   462    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 
   367    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 
   463   )
 
   368   )
 
   464 *}
 
   369 *}
 
   465 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *}
 
   370 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
 
       
   371 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 
       
   372 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}
 
   466 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
 
   373 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
 
   467   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 
   374   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 
   468 done
 
   375 done
 
   469 
   376 
   470 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}
 
   377 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}
 
   472 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
 
   379 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
 
   473 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
 
   380 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
 
   474 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
 
   381 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
 
   475 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 
   382 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 
   476 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
 
   383 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
 
   477 ML {* val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *}
 
   384 ML {* val defs_sym = add_lower_defs @{context} defs *}
 
       
   385 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *}
 
   478 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 
   386 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 
   479 ML {* ObjectLogic.rulify ind_r_s *}
 
   387 ML {* ObjectLogic.rulify ind_r_s *}
 
   480 
   388 
   481 ML {*
 
   389 ML {*
 
   482 fun lift thm =
 
   390   fun lift_thm_fset_note name thm lthy =
 
   483 let
 
       
   484   val ind_r_a = atomize_thm thm;
 
       
   485   val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
 
       
   486   val ind_r_t =
 
       
   487     repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
 
       
   488      @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
 
       
   489      (@{thms ho_memb_rsp ho_cons_rsp  ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs});
 
       
   490   val ind_r_l = simp_lam_prs @{context} ind_r_t;
 
       
   491   val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
 
       
   492   val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a;
 
       
   493   val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
 
       
   494 in
 
       
   495   ObjectLogic.rulify ind_r_s
 
       
   496 end
 
       
   497 *}
 
       
   498 ML fset_defs
 
       
   499 
       
   500 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
 
       
   501 by (simp add: list_eq_refl)
 
       
   502 
       
   503 
       
   504 ML {* lift @{thm m2} *}
 
       
   505 ML {* lift @{thm m1} *}
 
       
   506 ML {* lift @{thm list_eq.intros(4)} *}
 
       
   507 ML {* lift @{thm list_eq.intros(5)} *}
 
       
   508 ML {* lift @{thm card1_suc} *}
 
       
   509 ML {* lift @{thm map_append} *}
 
       
   510 ML {* lift @{thm eq_r[OF append_assoc]} *}
 
       
   511 
       
   512 
       
   513 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 
       
   514 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
       
   515 
       
   516 (*
 
       
   517 ML {*
 
       
   518   fun lift_theorem_fset_aux thm lthy =
 
       
   519     let
 
   391     let
 
   520       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
 
   392       val lifted_thm = lift_thm_fset lthy thm;
 
   521       val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};
 
       
   522       val cgoal = cterm_of @{theory} goal;
 
       
   523       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
 
       
   524       val tac = transconv_fset_tac' @{context};
 
       
   525       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
 
       
   526       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
 
       
   527       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
 
       
   528       val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
 
       
   529     in
 
       
   530       nthm3
 
       
   531     end
 
       
   532 *}
 
       
   533 *)
 
       
   534 
       
   535 (*
 
       
   536 ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
 
       
   537 ML {*
 
       
   538   fun lift_theorem_fset name thm lthy =
 
       
   539     let
 
       
   540       val lifted_thm = lift_theorem_fset_aux thm lthy;
 
       
   541       val (_, lthy2) = note (name, lifted_thm) lthy;
 
   393       val (_, lthy2) = note (name, lifted_thm) lthy;
 
   542     in
 
   394     in
 
   543       lthy2
 
   395       lthy2
 
   544     end;
 
   396     end;
 
   545 *}
 
   397 *}
 
   546 *)
 
   398 
   547 
   399 local_setup {*
 
   548 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
 
   400   lift_thm_fset_note @{binding "m1l"} @{thm m1} #>
 
   549 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 
   401   lift_thm_fset_note @{binding "m2l"} @{thm m2} #>
 
   550 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 
   402   lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #>
 
   551 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
 
   403   lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)}
 
   552 thm m1_lift
 
   404 *}
 
   553 thm leqi4_lift
 
   405 thm m1l
 
   554 thm leqi5_lift
 
   406 thm m2l
 
   555 thm m2_lift
 
   407 thm leqi4l
 
   556 ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
 
   408 thm leqi5l
 
   557 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"}
 
       
   558      (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*)
 
       
   559 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
       
   560 
       
   561 thm leqi4_lift
 
       
   562 ML {*
 
       
   563   val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
 
       
   564   val (_, l) = dest_Type typ
 
       
   565   val t = Type ("FSet.fset", l)
 
       
   566   val v = Var (nam, t)
 
       
   567   val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
 
       
   568 *}
 
       
   569 
       
   570 
   409 
   571 end
 
   410 end
nominal2