diff -r f7dee6e808eb -r e99c0334d8bf FSet.thy --- a/FSet.thy Wed Nov 25 03:47:07 2009 +0100 +++ b/FSet.thy Wed Nov 25 10:34:03 2009 +0100 @@ -337,155 +337,21 @@ apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done -ML {* - -fun lambda_prs_conv ctxt quot ctrm = - case (Thm.term_of ctrm) of - (Const (@{const_name "fun_map"}, _) $ y $ z) $ (Abs (_, T, x)) => - let - val _ = tracing "AAA"; - val lty = T; - val rty = fastype_of x; - val thy = ProofContext.theory_of ctxt; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [SOME lcty, NONE, SOME rcty]; - val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; - val tac = - (compose_tac (false, lpi, 2)) THEN_ALL_NEW - (quotient_tac quot); - val gc = Drule.strip_imp_concl (cprop_of lpi); - val t = Goal.prove_internal [] gc (fn _ => tac 1) - val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t - val te = @{thm eq_reflection} OF [ts] - val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm)); - val _ = tracing (Syntax.string_of_term @{context} (term_of (Thm.lhs_of te))); - val insts = matching_prs (ProofContext.theory_of ctxt) (term_of ctrm) (term_of (Thm.lhs_of te)); - val ti = Drule.instantiate insts te; - val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti))); - in - Conv.rewr_conv (eq_reflection OF [ti]) ctrm - end - | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm - | _ => Conv.all_conv ctrm -*} - -ML {* -fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => - CONVERSION - (Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv - Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) -*} - -ML {* -val ctrm = @{cterm "((ABS_fset ---> id) ---> id) (\x. id ((REP_fset ---> id) x))"} -val pat = @{cpat "((ABS_fset ---> id) ---> id) (\x. ?f ((REP_fset ---> id) x))"} -*} - -ML {* matching_prs @{theory} (term_of pat) (term_of ctrm); *} - -ML {* - lambda_prs_conv @{context} quot ctrm -*} - - -ML {* -val t = @{thm LAMBDA_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT] IDENTITY_QUOTIENT]} -val te = @{thm eq_reflection} OF [t] -val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te -val tl = Thm.lhs_of ts - *} - -ML {* val inst = matching_prs @{theory} (term_of tl) (term_of ctrm); *} - -ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\(P\('a list \ bool)). - All ((REP_fset ---> id) (\(list\('a list)). - (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \ - True \ (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list))))))"} *} - -ML {* - lambda_prs_conv @{context} quot trm -*} - - - -(*ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\(?P\('a list \ bool)). (g (id P)"} *} *) - - - -lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" -apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) -apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) -apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) -apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) -apply(tactic {* lambda_prs_tac @{context} quot 1 *}) - - -ML_prf {* Subgoal.focus @{context} 1 (#goal (Isar.goal ())) *} - -apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) - - -thm LAMBDA_PRS -apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) - -apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) - -apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) - -apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) -apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) -ML {* lift_thm_fset @{context} @{thm list.induct} *} -ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l"} *} - - - - -thm map_append lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" -apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) -apply(tactic {* prepare_tac 1 *}) -thm map_append apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) done - - lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) done -ML {* atomize_thm @{thm fold1.simps(2)} *} -(*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = - (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*) - - -*) -ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} - - -ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\x xa a. x = xa \ INSERT a x = INSERT a xa"}) *} - - -ML {* lift_thm_fset @{context} @{thm map_append} *} - - -(* -apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) -apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) -apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) -apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) -apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *}) -apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *}) -ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} -apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) -apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) -*) - - - -(*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) +ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} +lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" +apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) +done quotient_def fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" @@ -510,67 +376,35 @@ apply (auto simp add: FUN_REL_EQ) sorry - ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} -thm list.recs(2) -ML {* lift_thm_fset @{context} @{thm list.recs(2)} *} -ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} +ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} +lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" +apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) +apply (tactic {* (simp_tac (HOL_ss addsimps + @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *}) +ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) +done + +ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} -ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} -ML {* val t_a = atomize_thm @{thm list.recs(2)} *} -ML {* val qtrm = atomize_goal @{theory} gl *} -ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *} -ML {* val rg2 = cterm_of @{theory}(my_reg @{context} rel rty (prop_of t_a)) *} - -ML {* val t_r = regularize_goal @{context} t_a rel_eqv rel_refl qtrm *} -ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} - -ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (inj_REPABS @{context} ((prop_of t_r), qtrm))) *} -ML {* val rg2 = cterm_of @{theory} (build_repabs_term @{context} t_r consts rty qty) *} -ML {* val t_t = repabs_goal @{context} t_r rty quot rel_refl trans2 rsp_thms qtrm *} -ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} -ML {* - val lthy = @{context} - val (alls, exs) = findallex lthy rty qty (prop_of t_a); - val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls - val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs - val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t - val abs = findabs rty (prop_of t_a); - val aps = findaps rty (prop_of t_a); - val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; - val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; - val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; - val defs_sym = flat (map (add_lower_defs lthy) defs); - val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; - val t_id = simp_ids lthy t_l; - val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; - val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; - val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; - val t_rv = ObjectLogic.rulify t_r - -*} - - - - - - -ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} - - - - -ML {* atomize_thm @{thm m1} *} -ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} -ML {* lift_thm_fset @{context} @{thm m1} *} -(* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *) - +ML {* map (lift_thm_fset @{context}) @{thms list.cases(2)} *} +lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" +apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) +done lemma list_induct_part: assumes a: "P (x :: 'a list) ([] :: 'a list)" @@ -583,6 +417,7 @@ done + (* Construction site starts here *) @@ -590,7 +425,6 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} -thm list.recs(2) ML {* val t_a = atomize_thm @{thm list_induct_part} *} @@ -754,26 +588,4 @@ ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} - -ML {* - fun lift_thm_fset_note name thm lthy = - let - val lifted_thm = lift_thm_fset lthy thm; - val (_, lthy2) = note (name, lifted_thm) lthy; - in - lthy2 - end; -*} - -local_setup {* - lift_thm_fset_note @{binding "m1l"} @{thm m1} #> - lift_thm_fset_note @{binding "m2l"} @{thm m2} #> - lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #> - lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)} -*} -thm m1l -thm m2l -thm leqi4l -thm leqi5l - end