# HG changeset patch # User Cezary Kaliszyk # Date 1259759506 -3600 # Node ID 767baada01dc956846c4c3268cf418fd9f2d4eff # Parent 7f97c52021c98f256255711cc9c25f160db6b2e2 New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet. diff -r 7f97c52021c9 -r 767baada01dc FSet.thy --- a/FSet.thy Wed Dec 02 12:07:54 2009 +0100 +++ b/FSet.thy Wed Dec 02 14:11:46 2009 +0100 @@ -333,6 +333,8 @@ apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done +ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} + lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) done @@ -343,7 +345,6 @@ lemma cheat: "P" sorry -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) @@ -396,6 +397,28 @@ apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) done +lemma list_induct_part: + assumes a: "P (x :: 'a list) ([] :: 'c list)" + assumes b: "\e t. P x t \ P x (e # t)" + shows "P x l" + apply (rule_tac P="P x" in list.induct) + apply (rule a) + apply (rule b) + apply (assumption) + done + +lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +lemma "P (x :: 'a fset) ([] :: 'c list) \ (\e t. P x t \ P x (e # t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + quotient_def fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" where @@ -431,115 +454,6 @@ apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) done -lemma list_induct_part: - assumes a: "P (x :: 'a list) ([] :: 'c list)" - assumes b: "\e t. P x t \ P x (e # t)" - shows "P x l" - apply (rule_tac P="P x" in list.induct) - apply (rule a) - apply (rule b) - apply (assumption) - done - -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} +thm all_prs -(* Construction site starts here *) -lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" -apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) -apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -prefer 2 -apply (tactic {* clean_tac @{context} [quot] defs 1 *}) -apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) -apply (rule FUN_QUOTIENT) -apply (rule FUN_QUOTIENT) -apply (rule IDENTITY_QUOTIENT) -apply (rule FUN_QUOTIENT) -apply (rule QUOTIENT_fset) -apply (rule IDENTITY_QUOTIENT) -apply (rule IDENTITY_QUOTIENT) -apply (rule IDENTITY_QUOTIENT) -prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) -prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) -apply (rule IDENTITY_QUOTIENT) -apply (rule FUN_QUOTIENT) -apply (rule QUOTIENT_fset) -apply (rule IDENTITY_QUOTIENT) -prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) -prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) -apply (rule IDENTITY_QUOTIENT) -apply (rule FUN_QUOTIENT) -apply (rule QUOTIENT_fset) -apply (rule IDENTITY_QUOTIENT) -prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) -prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply assumption -apply (rule refl) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply assumption -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) -apply (rule IDENTITY_QUOTIENT) -apply (rule FUN_QUOTIENT) -apply (rule QUOTIENT_fset) -apply (rule IDENTITY_QUOTIENT) -prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) -prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply assumption -apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) -apply (rule IDENTITY_QUOTIENT) -apply (rule FUN_QUOTIENT) -apply (rule QUOTIENT_fset) -apply (rule IDENTITY_QUOTIENT) -prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) -prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) -done - -ML {* #quot_thm (hd (quotdata_dest @{theory})) *} -print_quotients -thm QUOTIENT_fset end diff -r 7f97c52021c9 -r 767baada01dc QuotMain.thy --- a/QuotMain.thy Wed Dec 02 12:07:54 2009 +0100 +++ b/QuotMain.thy Wed Dec 02 14:11:46 2009 +0100 @@ -875,6 +875,33 @@ *} ML {* +val APPLY_RSP_TAC' = + Subgoal.FOCUS (fn {concl, asms, context,...} => + case ((HOLogic.dest_Trueprop (term_of concl))) of + ((R2 $ (f $ x) $ (g $ y))) => + let + val (asmf, asma) = find_qt_asm (map term_of asms); + in + if (fastype_of asmf) = (fastype_of f) then no_tac else let + val ty_a = fastype_of x; + val ty_b = fastype_of asma; + val ty_c = range_type (type_of f); + val ty_d = range_type (type_of asmf); + val thy = ProofContext.theory_of context; + val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; + val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; + val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; + val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} + (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) + in + rtac thm 1 + end + end + | _ => no_tac) +*} + + +ML {* fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) *} @@ -1019,7 +1046,8 @@ (FIRST' [ (* "cong" rule of the of the relation / transitivity*) (* (op =) (R a b) (R c d) ----> \R a c; R b d\ *) - NDT ctxt "1" (resolve_tac trans2), + NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), @@ -1049,7 +1077,7 @@ THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), (* R (t $ \) (t' $ \) ----> APPLY_RSP provided type of t needs lifting *) - NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN' + NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),