281        (simp_tac ((Simplifier.context lthy HOL_ss) addsimps

   281        atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps

   283          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN'

   283          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW

   284          (rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN'

   284          ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN'

   285          (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []);

   285          (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []));

   395 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =

   395 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =

   402 (*    val tac2 =

   402   in

   403      (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [cthm]))

   403     (rt, cthm, thm)

   404      THEN' (rtac thm);

   404   end

   405     val cgoal = cterm_of (ProofContext.theory_of lthy) rt;

   405 *}

   406     val cthm = Goal.prove_internal [] cgoal (fn _ => tac2); *)

   406 

   407 ML {*

   408 fun repabs_eq2 lthy (rt, thm, othm) =

   409   let

   410     fun tac2 ctxt =

   411      (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))

   412      THEN' (rtac othm);

   413     val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);

   468  val t = prop_of @{thm LAMBDA_PRS}

   468    val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];

   469  val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}

   469    val lpist = @{thm "HOL.sym"} OF [lpis];

   470  val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]

   470    val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist

   471  val tttt = @{thm "HOL.sym"} OF [ttt]

   471 *}

   472 *}

   472 

   473 ML {*

   473 text {* the proper way to do it *}

   474  val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt

   474 ML {*

   475  val zzz = @{thm m2_t}

   475  val lpi = Drule.instantiate'

   476 *}

   476    [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS};

   477 prove asdfasdf : {* concl_of tt *}

   477 *}

   478 prove asdfasdf : {* concl_of lpi *}

   499 ML ttttt

   499 

   500 ML {* val m2_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm m2_t} *}

   500 (* @{thms HOL.sym[OF asdfasdf,simplified]} *)

   501 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}

   501 

   502 ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}

   502 ML {*

   503 ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *}

   503   fun simp_lam_prs lthy thm = 

   504     simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] thm)

   505     handle _ => thm

   506 *}

   507 

   508 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}

   509 

   510 ML {*

   511   fun simp_allex_prs lthy thm =

   512     let

   513       val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]};

   514       val rwfs = @{thm "HOL.sym"} OF [spec OF [rwf]];

   515       val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};

   516       val rwes = @{thm "HOL.sym"} OF [spec OF [rwe]]

   517     in

   518       (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))

   519     end

   520     handle _ => thm

   521 *}

   522 

   523 ML {* val ithm = simp_allex_prs @{context} m2_t' *}

   532 ML {* val ithm = eqsubst_thm @{context} [rwrs] card1_suc_t'' *}

   552 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *}

   533 ML {* val rwr = @{thm EXISTS_PRS[OF QUOTIENT_fset]} *}

   553 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}

   534 ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}

   535 ML {* val jthm = eqsubst_thm @{context} [rwrs] ithm *}

   536 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym jthm *}

   540 

   557 thm fold1.simps(2)

   541 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}

   558 

   542 prove fold1_def_2_r: {*

   559 

   543  Logic.mk_implies

   560 ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *}

   544    ((prop_of li),

   561 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}

   545    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}

   562 ML {*

   546   apply (simp add: equiv_res_forall[OF equiv_list_eq])

   563   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}

   547   done

   564   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);

   548 

   565 *}

   549 ML {* @{thm fold1_def_2_r} OF [li] *}

   566 (*prove rg

   550 

   567 apply(atomize(full))

   551 

   568 apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})*)

   552 lemma yy:

   569 ML {* val (g, thm, othm) =

   553   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"

   570   Toplevel.program (fn () =>

   554 unfolding IN_def EMPTY_def

   571   repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}

   555 apply(rule_tac f="(op =) False" in arg_cong)

   572    @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}

   556 apply(rule memb_rsp)

   573    @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}

   557 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   574   )

   558 apply(rule list_eq.intros)

   575 *}

   559 done

   576 ML {*

   560 

   577     fun tac2 ctxt =

   561 lemma

   578      (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))

   562   shows "IN (x::nat) EMPTY = False"

   579      THEN' (rtac othm); *}

   563 using m1

   580 (* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);

   564 apply -

   581 *} *)

   565 apply(rule yy[THEN iffD1, symmetric])

   582 

   566 apply(simp)

   583 ML {*

   567 done

   584   val ind_r_t2 =

   568 

   585   Toplevel.program (fn () =>

   569 lemma

   586     repabs_eq2 @{context} (g, thm, othm)

   570   shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =

   587   )

   571          ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"

   588 *}

   572 unfolding IN_def INSERT_def

   589 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}

   573 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)

   590 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *}

   574 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)

   591 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *}

   575 apply(rule memb_rsp)

   592 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}

   576 apply(rule list_eq.intros(3))

   593 

   577 apply(unfold REP_fset_def ABS_fset_def)

   594 ML {*

   578 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])

   595 fun lift thm =

   579 apply(rule list_eq_refl)

   596 let

   580 done

   597   val ind_r_a = atomize_thm thm;

   581 

   598   val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};

   582 lemma yyy:

   599   val (g, t, ot) =

   583   shows "

   600     repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}

   584     (

   601      @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}

   585      (UNION EMPTY s = s) &

   602      @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp};

   586      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))

   603   val ind_r_t = repabs_eq2 @{context} (g, t, ot);

   587     ) = (

   604   val ind_r_l = simp_lam_prs @{context} ind_r_t;

   588      ((ABS_fset ([] @ REP_fset s)) = s) &

   605   val ind_r_a = simp_allex_prs @{context} ind_r_l;

   589      ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))

   606   val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;

   590     )"

   607   val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d

   591   unfolding UNION_def EMPTY_def INSERT_def

   608 in

   592   apply(rule_tac f="(op &)" in arg_cong2)

   609   ObjectLogic.rulify ind_r_s

   593   apply(rule_tac f="(op =)" in arg_cong2)

   610 end

   594   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

   611 *}

   595   apply(rule append_respects_fst)

   612 

   596   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   613 ML {* lift @{thm m2} *}

   597   apply(rule list_eq_refl)

   614 ML {* lift @{thm m1} *}

   598   apply(simp)

   615 ML {* lift @{thm list_eq.intros(4)} *}

   599   apply(rule_tac f="(op =)" in arg_cong2)

   616 ML {* lift @{thm list_eq.intros(5)} *}

   600   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

   601   apply(rule append_respects_fst)

   602   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   603   apply(rule list_eq_refl)

   604   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

   605   apply(rule list_eq.intros(5))

   606   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   607   apply(rule list_eq_refl)

   608 done

   609 

   610 lemma

   611   shows "

   612      (UNION EMPTY s = s) &

   613      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"

   614   apply (simp add: yyy)

   615   apply (simp add: QUOT_TYPE_I_fset.thm10)

   616   done

   617 

   618 ML {*

   619   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))

   620 *}

   621 

   622 ML {*

   623 cterm_of @{theory} (prop_of m1_novars);

   624 cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});

   625 *}

   626