diff -r 3da18bf6886c -r 4f00ca4f5ef4 FSet.thy --- a/FSet.thy Fri Oct 23 16:34:20 2009 +0200 +++ b/FSet.thy Fri Oct 23 18:20:06 2009 +0200 @@ -172,26 +172,38 @@ thm fun_map.simps text {* Respectfullness *} -lemma mem_respects: +lemma memb_rsp: fixes z assumes a: "list_eq x y" shows "(z memb x) = (z memb y)" using a by induct auto +lemma ho_memb_rsp: + "(op = ===> (op \ ===> op =)) (op memb) (op memb)" + apply (simp add: FUN_REL.simps) + apply (metis memb_rsp) + done + lemma card1_rsp: fixes a b :: "'a list" assumes e: "a \ b" shows "card1 a = card1 b" using e apply induct - apply (simp_all add:mem_respects) + apply (simp_all add:memb_rsp) done -lemma cons_preserves: +lemma cons_rsp: fixes z assumes a: "xs \ ys" shows "(z # xs) \ (z # ys)" using a by (rule list_eq.intros(5)) +lemma ho_cons_rsp: + "op = ===> op \ ===> op \ op # op #" + apply (simp add: FUN_REL.simps) + apply (metis cons_rsp) + done + lemma append_respects_fst: assumes a : "list_eq l1 l2" shows "list_eq (l1 @ s) (l2 @ s)" @@ -251,6 +263,16 @@ *} ML {* +fun LAMBDA_RES_TAC ctxt = + case (term_of o #concl o fst) (Subgoal.focus ctxt 1 (Isar.goal ())) of + (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => + (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' + (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) + | _ => fn _ => no_tac +*} + + +ML {* fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = (FIRST' [ rtac @{thm FUN_QUOTIENT}, @@ -258,10 +280,12 @@ rtac @{thm IDENTITY_QUOTIENT}, rtac @{thm ext}, rtac trans_thm, + LAMBDA_RES_TAC ctxt, res_forall_rsp_tac ctxt, (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), + rtac refl, (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), - rtac reflex_thm, + rtac reflex_thm, atac, ( (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) @@ -280,15 +304,13 @@ 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"} *} + prove list_induct_tr: trm_r apply (atomize(full)) (* APPLY_RSP_TAC *) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) (* LAMBDA_RES_TAC *) -apply (simp only: FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule impI) +apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) (* MK_COMB_TAC *) apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) (* MK_COMB_TAC *) @@ -300,14 +322,11 @@ (* MK_COMB_TAC *) apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) (* REFL_TAC *) -apply (simp) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) (* APPLY_RSP_TAC *) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -apply (simp only: FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule impI) +apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) (* MK_COMB_TAC *) apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) (* MK_COMB_TAC *) @@ -319,19 +338,14 @@ (* MK_COMB_TAC *) apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) (* REFL_TAC *) -apply (simp) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) (* W(C (curry op THEN) (G... *) +apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) (* CONS respects *) -apply (simp add: FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (rule cons_preserves) -apply (assumption) +apply (rule ho_cons_rsp) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -apply (simp only: FUN_REL.simps) +apply (subst FUN_REL.simps) apply (rule allI) apply (rule allI) apply (rule impI) @@ -360,48 +374,26 @@ prove m2_t_p: m2_t_g apply (atomize(full)) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -apply (simp add: FUN_REL.simps) prefer 2 -apply (simp only: FUN_REL.simps) +apply (subst FUN_REL.simps) apply (rule allI) apply (rule allI) apply (rule impI) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) prefer 2 -apply (simp only: FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -apply (simp only: FUN_REL.simps) +apply (subst FUN_REL.simps) apply (rule allI) apply (rule allI) apply (rule impI) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -apply (simp only: FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (simp add:mem_respects) -apply (simp only: FUN_REL.simps) +apply (subst FUN_REL.simps) apply (rule allI) apply (rule allI) apply (rule impI) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (simp add:cons_preserves) -apply (simp only: FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (rule allI) -apply (rule allI) -apply (rule impI) -apply (simp add:mem_respects) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +apply (rule ho_memb_rsp) +apply (rule ho_cons_rsp) +apply (rule ho_memb_rsp) apply (auto) done @@ -413,7 +405,6 @@ lemma id_apply2 [simp]: "id x \ x" by (simp add: id_def) - thm LAMBDA_PRS ML {* val t = prop_of @{thm LAMBDA_PRS} @@ -443,9 +434,9 @@ ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} -ML {* rwrs; m2_t' *} -ML {* eqsubst_thm @{context} [rwrs] m2_t' *} -thm INSERT_def +ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *} +ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} +ML {* ObjectLogic.rulify rthm *} ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} @@ -474,7 +465,7 @@ shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" unfolding IN_def EMPTY_def apply(rule_tac f="(op =) False" in arg_cong) -apply(rule mem_respects) +apply(rule memb_rsp) apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) apply(rule list_eq.intros) done @@ -493,7 +484,7 @@ unfolding IN_def INSERT_def apply(rule_tac f="(op \) (x=y)" in arg_cong) apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) -apply(rule mem_respects) +apply(rule memb_rsp) apply(rule list_eq.intros(3)) apply(unfold REP_fset_def ABS_fset_def) apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) @@ -554,7 +545,7 @@ REPEAT_ALL_NEW (FIRST' [ rtac @{thm list_eq_refl}, rtac @{thm cons_preserves}, - rtac @{thm mem_respects}, + rtac @{thm memb_rsp}, rtac @{thm card1_rsp}, rtac @{thm QUOT_TYPE_I_fset.R_trans2}, CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),