# HG changeset patch # User Christian Urban # Date 1259201918 -3600 # Node ID 58947b7232ef934e493d39422f8737089d214f60 # Parent 1dd6a21cdd1c5f9cb14940b2b01cac844807c393# Parent d67240113f68016356e3f56e97eb1dcb0fa474e6 merged diff -r d67240113f68 -r 58947b7232ef FSet.thy --- a/FSet.thy Wed Nov 25 21:48:32 2009 +0100 +++ b/FSet.thy Thu Nov 26 03:18:38 2009 +0100 @@ -341,10 +341,50 @@ apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) done +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 cheat: "P" sorry + +lemma imp_refl: "P \ P" by simp + +thm Set.conj_mono +thm Set.imp_mono +ML {* Inductive.get_monos @{context} *} + 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 {* procedure_tac @{thm list.induct} @{context} 1 *}) +defer +apply(rule cheat) +apply(rule cheat) +apply(atomize (full)) +apply(rule my_equiv_res_forallR) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(rule my_equiv_res_forallR) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(rule Set.imp_mono) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(rule my_equiv_res_forallL) +apply(rule cheat) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) +apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) done +lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" +apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) +defer +apply(rule cheat) +apply(rule cheat) +apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) +oops + quotient_def fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" where diff -r d67240113f68 -r 58947b7232ef QuotMain.thy --- a/QuotMain.thy Wed Nov 25 21:48:32 2009 +0100 +++ b/QuotMain.thy Thu Nov 26 03:18:38 2009 +0100 @@ -474,23 +474,40 @@ *) -lemma my_equiv_res_forall2: +lemma my_equiv_res_forallR: fixes P::"'a \ bool" fixes Q::"'b \ bool" - assumes a: "(All Q) \ (All P)" + assumes b: "(All Q) \ (All P)" shows "(All Q) \ Ball (Respects E) P" -using a by auto +using b by auto -lemma my_equiv_res_exists: +lemma my_equiv_res_forallL: + fixes P::"'a \ bool" + fixes Q::"'b \ bool" + assumes a: "EQUIV E" + assumes b: "(All Q) \ (All P)" + shows "Ball (Respects E) P \ (All P)" +using a b +unfolding EQUIV_def +by (metis IN_RESPECTS) + +lemma my_equiv_res_existsR: fixes P::"'a \ bool" fixes Q::"'b \ bool" assumes a: "EQUIV E" and b: "(Ex Q) \ (Ex P)" shows "(Ex Q) \ Bex (Respects E) P" -apply(subst equiv_res_exists) -apply(rule a) -apply(rule b) -done +using a b +unfolding EQUIV_def +by (metis IN_RESPECTS) + +lemma my_equiv_res_existsL: + fixes P::"'a \ bool" + fixes Q::"'b \ bool" + assumes b: "(Ex Q) \ (Ex P)" + shows "Bex (Respects E) Q \ (Ex P)" +using b +by (auto) lemma universal_twice: assumes *: "\x. (P x \ Q x)" @@ -499,26 +516,10 @@ lemma implication_twice: assumes a: "c \ a" - assumes b: "a \ b \ d" + assumes b: "b \ d" shows "(a \ b) \ (c \ d)" using a b by auto -ML {* -(* FIXME: get_rid of rel_refl rel_eqv *) -fun REGULARIZE_tac lthy rel_refl rel_eqv = - (REPEAT1 o FIRST1) - [rtac rel_refl, - atac, - rtac @{thm universal_twice}, - rtac @{thm impI} THEN' atac, - rtac @{thm implication_twice}, - rtac @{thm my_equiv_res_forall2}, - rtac (rel_eqv RS @{thm my_equiv_res_exists}), - (* For a = b \ a \ b *) - rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, - rtac @{thm RIGHT_RES_FORALL_REGULAR}] -*} - (* version of REGULARIZE_tac including debugging information *) ML {* fun my_print_tac ctxt s thm = @@ -543,8 +544,8 @@ DT lthy "3" (rtac @{thm universal_twice}), DT lthy "4" (rtac @{thm impI} THEN' atac), DT lthy "5" (rtac @{thm implication_twice}), - DT lthy "6" (rtac @{thm my_equiv_res_forall2}), - DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})), + DT lthy "6" (rtac @{thm my_equiv_res_forallR}), + DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})), (* For a = b \ a \ b *) DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] @@ -557,7 +558,7 @@ rtac rel_refl, atac, rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), + rtac @{thm impI} THEN' atac, rtac @{thm implication_twice}, EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), @@ -568,11 +569,30 @@ ]); *} +ML {* +fun regularize_tac ctxt rel_eqv rel_refl = + (ObjectLogic.full_atomize_tac) THEN' + REPEAT_ALL_NEW (FIRST' + [(K (print_tac "start")) THEN' (K no_tac), + DT ctxt "1" (rtac rel_refl), + DT ctxt "2" atac, + DT ctxt "3" (rtac @{thm universal_twice}), + DT ctxt "4" (rtac @{thm impI} THEN' atac), + DT ctxt "5" (rtac @{thm implication_twice}), + DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])]), + (* For a = b \ a \ b *) + DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) + ]); +*} + +thm RIGHT_RES_FORALL_REGULAR + +section {* Injections of REP and ABSes *} (* -Injections of REP and Abses -*************************** - Injecting REPABS means: For abstractions: