# HG changeset patch # User Cezary Kaliszyk # Date 1256547770 -3600 # Node ID f8fc085db38ff2606ccf108fc67cf10237406011 # Parent 9ca545f783f6c34543bd04883a55a63d82c46b0b Cleaning and fixing. diff -r 9ca545f783f6 -r f8fc085db38f FSet.thy --- a/FSet.thy Mon Oct 26 02:06:01 2009 +0100 +++ b/FSet.thy Mon Oct 26 10:02:50 2009 +0100 @@ -218,8 +218,10 @@ apply(rule list_eq_refl) done +(* Need stronger induction... *) lemma "(a @ b) \ (b @ a)" -sorry + apply(induct a) + sorry lemma (* ho_append_rsp: *) "op \ ===> op \ ===> op \ op @ op @" @@ -237,23 +239,6 @@ apply (metis) done -ML {* -fun regularize thm rty rel rel_eqv lthy = - let - val g = build_regularize_goal thm rty rel lthy; - fun tac ctxt = - (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW - (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' - (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); - val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); - in - cthm OF [thm] - end -*} - - prove list_induct_r: {* build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \"} @{context} *} apply (simp only: equiv_res_forall[OF equiv_list_eq]) @@ -265,94 +250,6 @@ done ML {* -fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => -let - val pat = Drule.strip_imp_concl (cprop_of thm) - val insts = Thm.match (pat, concl) -in - rtac (Drule.instantiate insts thm) 1 -end -handle _ => no_tac -) -*} - -ML {* -fun res_forall_rsp_tac ctxt = - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) - THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} - THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) -*} - -ML {* -fun res_exists_rsp_tac ctxt = - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) - THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} - THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) -*} - - -ML {* -fun quotient_tac quot_thm = - REPEAT_ALL_NEW (FIRST' [ - rtac @{thm FUN_QUOTIENT}, - rtac quot_thm, - rtac @{thm IDENTITY_QUOTIENT} - ]) -*} - -ML {* -fun LAMBDA_RES_TAC ctxt i st = - (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) 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) i st -*} - -ML {* -fun WEAK_LAMBDA_RES_TAC ctxt i st = - (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of - (_ $ (_ $ _$(Abs(_,_,_)))) => - (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' - (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) - | (_ $ (_ $ (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) i st -*} - - -ML {* -fun r_mk_comb_tac ctxt 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, - res_exists_rsp_tac ctxt, - ( - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs}))) - THEN_ALL_NEW (fn _ => no_tac) - ), - (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, - atac, - ( - (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) - THEN_ALL_NEW (fn _ => no_tac) - ), - WEAK_LAMBDA_RES_TAC ctxt - ]) -*} - -ML {* fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = let val rt = build_repabs_term lthy thm constructors rty qty; @@ -377,10 +274,11 @@ end *} - +(* 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} @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} + r_mk_comb_tac ctxt @{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}) *} @@ -467,20 +365,7 @@ done thm HOL.sym[OF lambda_prs_lb_b,simplified] -ML {* -fun eqsubst_thm ctxt thms thm = - let - val goalstate = Goal.init (Thm.cprop_of thm) - val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of - NONE => error "eqsubst_thm" - | SOME th => cprem_of th 1 - val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 - 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 - end -*} + ML {* @@ -497,9 +382,9 @@ fun simp_allex_prs lthy thm = let val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]}; - val rwfs = @{thm "HOL.sym"} OF [spec OF [rwf]]; + val rwfs = @{thm "HOL.sym"} OF [rwf]; val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]}; - val rwes = @{thm "HOL.sym"} OF [spec OF [rwe]] + val rwes = @{thm "HOL.sym"} OF [rwe] in (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm)) end @@ -564,7 +449,7 @@ Toplevel.program (fn () => repabs_eq @{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_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}) ) *} ML {* @@ -592,6 +477,7 @@ ML {* val ind_r_a = simp_allex_prs @{context} 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 {* val ind_r_d = MetaSimplifier.rewrite_rule 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 *} @@ -604,7 +490,7 @@ val (g, t, ot) = repabs_eq @{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_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); val ind_r_l = simp_lam_prs @{context} ind_r_t; val ind_r_a = simp_allex_prs @{context} ind_r_l; @@ -614,6 +500,8 @@ ObjectLogic.rulify ind_r_s end *} +ML fset_defs + ML {* lift @{thm m2} *} ML {* lift @{thm m1} *} diff -r 9ca545f783f6 -r f8fc085db38f QuotMain.thy --- a/QuotMain.thy Mon Oct 26 02:06:01 2009 +0100 +++ b/QuotMain.thy Mon Oct 26 10:02:50 2009 +0100 @@ -547,6 +547,22 @@ (regularise (prop_of thm) rty rel lthy)) *} +ML {* +fun regularize thm rty rel rel_eqv lthy = + let + val g = build_regularize_goal thm rty rel lthy; + fun tac ctxt = + (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW + (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' + (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); + val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); + in + cthm OF [thm] + end +*} + section {* RepAbs injection *} (* Needed to have a meta-equality *) @@ -616,4 +632,110 @@ Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) *} +ML {* +fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => +let + val pat = Drule.strip_imp_concl (cprop_of thm) + val insts = Thm.match (pat, concl) +in + rtac (Drule.instantiate insts thm) 1 end +handle _ => no_tac +) +*} + +ML {* +fun res_forall_rsp_tac ctxt = + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) +*} + +ML {* +fun res_exists_rsp_tac ctxt = + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) +*} + + +ML {* +fun quotient_tac quot_thm = + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm FUN_QUOTIENT}, + rtac quot_thm, + rtac @{thm IDENTITY_QUOTIENT} + ]) +*} + +ML {* +fun LAMBDA_RES_TAC ctxt i st = + (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) 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) i st +*} + +ML {* +fun WEAK_LAMBDA_RES_TAC ctxt i st = + (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of + (_ $ (_ $ _$(Abs(_,_,_)))) => + (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' + (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) + | (_ $ (_ $ (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) i st +*} + + +ML {* +fun r_mk_comb_tac ctxt 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, + res_exists_rsp_tac ctxt, + ( + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) + THEN_ALL_NEW (fn _ => no_tac) + ), + (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, + atac, + ( + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN_ALL_NEW (fn _ => no_tac) + ), + WEAK_LAMBDA_RES_TAC ctxt + ]) +*} + +section {* Cleaning the goal *} + +text {* Does the same as 'subst' in a given theorem *} +ML {* +fun eqsubst_thm ctxt thms thm = + let + val goalstate = Goal.init (Thm.cprop_of thm) + val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of + NONE => error "eqsubst_thm" + | SOME th => cprem_of th 1 + val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 + 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 + end +*} + +end diff -r 9ca545f783f6 -r f8fc085db38f QuotScript.thy --- a/QuotScript.thy Mon Oct 26 02:06:01 2009 +0100 +++ b/QuotScript.thy Mon Oct 26 10:02:50 2009 +0100 @@ -495,9 +495,6 @@ |- !R abs rep. QUOTIENT R abs rep ==> !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f), - |- !R abs rep. - QUOTIENT R abs rep ==> - !a b c. (if a then b else c) = abs (if a then rep b else rep c)] : *) lemma FORALL_PRS: assumes a: "QUOTIENT R absf repf" @@ -512,8 +509,16 @@ using a unfolding QUOTIENT_def by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) - -lemma ho_all_prs: + +lemma COND_PRS: + assumes a: "QUOTIENT R absf repf" + shows "(if a then b else c) = absf (if a then repf b else repf c)" + using a + unfolding QUOTIENT_def + sorry + +(* These are the fixed versions, general ones need to be proved. *) +lemma ho_all_prs: shows "op = ===> op = ===> op = All All" by auto