# HG changeset patch # User Christian Urban # Date 1256690971 -3600 # Node ID 7610d2bbca48803186d4de5947314cea7c86d951 # Parent ca9eae5bd871b462142f7776f5d67f406fb0a0b0# Parent 80859cc80332dd99144f175b91b3e241d374e887 merged diff -r ca9eae5bd871 -r 7610d2bbca48 FSet.thy --- a/FSet.thy Wed Oct 28 01:48:45 2009 +0100 +++ b/FSet.thy Wed Oct 28 01:49:31 2009 +0100 @@ -187,8 +187,20 @@ *} ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} + +ML {* +fun add_lower_defs ctxt defs = + let + val defs_pre_sym = map symmetric defs + val defs_atom = map atomize_thm defs_pre_sym + val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) + in + map Thm.varifyT defs_all + end +*} ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} + lemma memb_rsp: fixes z assumes a: "list_eq x y" @@ -295,7 +307,7 @@ (* The all_prs and ex_prs should be proved for the instance... *) ML {* fun r_mk_comb_tac_fset ctxt = - r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} + r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) *} @@ -304,6 +316,15 @@ ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} +ML {* val rty = @{typ "'a list"} *} + +ML {* +fun r_mk_comb_tac_fset ctxt = + r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} + (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) +*} + + ML {* trm_r *} prove list_induct_tr: trm_r apply (atomize(full)) @@ -339,27 +360,6 @@ lemma id_apply2 [simp]: "id x \ x" by (simp add: id_def) -ML {* - val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]; - val lpist = @{thm "HOL.sym"} OF [lpis]; - val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist -*} - -text {* the proper way to do it *} -ML {* - fun findabs rty tm = - case tm of - Abs(_, T, b) => - let - val b' = subst_bound ((Free ("x", T)), b); - val tys = findabs rty b' - val ty = fastype_of tm - in if needs_lift rty ty then (ty :: tys) else tys - end - | f $ a => (findabs rty f) @ (findabs rty a) - | _ => [] -*} - ML {* val quot = @{thm QUOTIENT_fset} *} ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} @@ -370,10 +370,9 @@ handle _ => thm *} -ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} +ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *} ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} -ML fset_defs_sym ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} ML {* ObjectLogic.rulify rthm *} @@ -408,8 +407,9 @@ thm fold1.simps(2) thm list.recs(2) +thm map_append -ML {* val ind_r_a = atomize_thm @{thm map_append} *} +ML {* val ind_r_a = atomize_thm @{thm list.induct} *} (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} ML_prf {* fun tac ctxt = (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @@ -423,33 +423,20 @@ val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); *} + prove rg apply(atomize(full)) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -apply (auto) done -ML {* val (g, thm, othm) = +ML {* val ind_r_t = Toplevel.program (fn () => - repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} + repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) ) *} -ML {* - fun tac2 ctxt = - (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) - THEN' (rtac othm); *} -(* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1); -*} *) - -ML {* - val ind_r_t2 = - Toplevel.program (fn () => - repabs_eq2 @{context} (g, thm, othm) - ) -*} -ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} +ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *} lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) done @@ -458,13 +445,10 @@ ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} -ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} +ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} - - -ML {* hd fset_defs_sym *} -ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} +ML {* val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *} ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} ML {* ObjectLogic.rulify ind_r_s *} @@ -473,14 +457,13 @@ let val ind_r_a = atomize_thm thm; val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context}; - val (g, t, ot) = - repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} + val ind_r_t = + repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} - (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}); - val ind_r_t = repabs_eq2 @{context} (g, t, ot); + (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); val ind_r_l = simp_lam_prs @{context} ind_r_t; - val ind_r_a = simp_allex_prs @{context} ind_r_l; - val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; + val ind_r_a = simp_allex_prs @{context} quot ind_r_l; + val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d in ObjectLogic.rulify ind_r_s @@ -488,15 +471,19 @@ *} ML fset_defs +lemma eq_r: "a = b \ a \ b" +by (simp add: list_eq_refl) + ML {* lift @{thm m2} *} ML {* lift @{thm m1} *} ML {* lift @{thm list_eq.intros(4)} *} ML {* lift @{thm list_eq.intros(5)} *} ML {* lift @{thm card1_suc} *} -(* ML {* lift @{thm append_assoc} *} *) +ML {* lift @{thm map_append} *} +ML {* lift @{thm eq_r[OF append_assoc]} *} -thm +thm (*notation ( output) "prop" ("#_" [1000] 1000) *) diff -r ca9eae5bd871 -r 7610d2bbca48 IntEx.thy --- a/IntEx.thy Wed Oct 28 01:48:45 2009 +0100 +++ b/IntEx.thy Wed Oct 28 01:49:31 2009 +0100 @@ -3,7 +3,7 @@ begin fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" where "intrel (x, y) (u, v) = (x + v = u + y)" @@ -123,7 +123,7 @@ lemma intrel_refl: "intrel a a" sorry -lemma ho_plus_rsp : +lemma ho_plus_rsp: "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" by (simp) @@ -168,22 +168,16 @@ ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} -ML {* val (g, thm, othm) = +ML {* val t_t = Toplevel.program (fn () => - repabs_eq @{context} t_r consts rty qty + repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms ) *} -ML {* - val t_t2 = - Toplevel.program (fn () => - repabs_eq2 @{context} (g, thm, othm) - ) -*} - ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} + ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} ML {* @@ -191,8 +185,8 @@ simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) handle _ => thm *} -ML {* t_t2 *} -ML {* val t_l = simp_lam_prs @{context} t_t2 *} +ML {* t_t *} +ML {* val t_l = simp_lam_prs @{context} t_t *} ML {* val t_a = simp_allex_prs @{context} quot t_l *} diff -r ca9eae5bd871 -r 7610d2bbca48 QuotMain.thy --- a/QuotMain.thy Wed Oct 28 01:48:45 2009 +0100 +++ b/QuotMain.thy Wed Oct 28 01:49:31 2009 +0100 @@ -708,14 +708,26 @@ | _ => fn _ => no_tac) i st *} +ML {* +fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => + let + val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; + val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); + val insts = Thm.match (pat, concl) +in + if needs_lift rty (type_of f) then + rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 + else no_tac +end +handle _ => no_tac) +*} ML {* -fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = +fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, rtac @{thm IDENTITY_QUOTIENT}, - rtac @{thm ext}, rtac trans_thm, LAMBDA_RES_TAC ctxt, res_forall_rsp_tac ctxt, @@ -726,8 +738,10 @@ ), (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), rtac refl, - rtac @{thm arg_cong2[of _ _ _ _ "op ="]}, - (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), +(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) + (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), + Cong_Tac.cong_tac @{thm cong}, + rtac @{thm ext}, rtac reflex_thm, atac, ( @@ -739,27 +753,15 @@ *} ML {* -fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = +fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = let val rt = build_repabs_term lthy thm constructors rty qty; val rg = Logic.mk_equals ((Thm.prop_of thm), rt); fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' - (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms)); + (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); in - (rt, cthm, thm) - end -*} - -ML {* -fun repabs_eq2 lthy (rt, thm, othm) = - let - fun tac2 ctxt = - (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) - THEN' (rtac othm); - val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1); - in - cthm + @{thm Pure.equal_elim_rule1} OF [cthm, thm] end *} @@ -777,18 +779,27 @@ val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); in - Simplifier.rewrite_rule [rt] thm + @{thm Pure.equal_elim_rule1} OF [rt,thm] end *} +ML {* + fun repeat_eqsubst_thm ctxt thms thm = + repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) + handle _ => thm +*} + text {* expects atomized definition *} ML {* fun add_lower_defs_aux ctxt thm = let - val e1 = @{thm fun_cong} OF [thm] - val f = eqsubst_thm ctxt @{thms fun_map.simps} e1 + val e1 = @{thm fun_cong} OF [thm]; + val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; + val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; + val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g; + val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h in - thm :: (add_lower_defs_aux ctxt f) + thm :: (add_lower_defs_aux ctxt i) end handle _ => [thm] *} @@ -855,14 +866,13 @@ fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let val t_a = atomize_thm t; val t_r = regularize t_a rty rel rel_eqv lthy; - val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; - val t_t2 = repabs_eq2 lthy t_t1; + val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val abs = findabs rty (prop_of t_a); val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; fun simp_lam_prs lthy thm = simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) handle _ => thm - val t_l = simp_lam_prs lthy t_t2; + val t_l = simp_lam_prs lthy t_t; val t_a = simp_allex_prs lthy quot t_l; val t_defs_sym = add_lower_defs lthy t_defs; val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;