# HG changeset patch # User Cezary Kaliszyk # Date 1259048188 -3600 # Node ID 51aafebf4d06cc1c4d1e9d5a6fce927c05400896 # Parent abc6bfd0576e31863d552c88238b4ee79d84ce53 Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better. diff -r abc6bfd0576e -r 51aafebf4d06 FSet.thy --- a/FSet.thy Tue Nov 24 08:35:04 2009 +0100 +++ b/FSet.thy Tue Nov 24 08:36:28 2009 +0100 @@ -306,51 +306,38 @@ 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 {* 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 {* lift_thm_fset @{context} @{thm m2} *} +ML {* lift_thm_fset @{context} @{thm m2} *} ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \ IN x xa)"} *} + ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *} ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \ INSERT a x = INSERT a xa"} *} + ML {* lift_thm_fset @{context} @{thm card1_suc} *} -ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \ \a b. \ IN a b \ x = INSERT a b"} *} +ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \ \a b. \ IN a b \ x = INSERT a b"} *} + ML {* lift_thm_fset @{context} @{thm not_mem_card1} *} ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\ IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *} + ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} + (* Doesn't work with 'a, 'b, but works with 'b, 'a *) - 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_fset @{context} @{thm append_assoc} *} -ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} -ML {* lift_thm_fset @{context} @{thm map_append} *} -ML {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} - -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *} +ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} -ML {* val qtrm = atomize_goal @{theory} gl *} -ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *} - -ML {* val a = Syntax.check_term @{context} a *} -ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *} - -ML {* lift_thm_g_fset @{context} @{thm map_append} gl *} - - +ML {* lift_thm_fset @{context} @{thm map_append} *} +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 {* 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"} *} - - - (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) quotient_def @@ -381,11 +368,60 @@ 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 *} + +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 (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} +ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} +ML {* val consts = lookup_quot_consts defs *} + +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.recs} *} + + + + 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} *}