# HG changeset patch # User Cezary Kaliszyk # Date 1260267601 -3600 # Node ID 8dfae5d97387e035e0524663afdd962c39eff52d # Parent ca37f4b6457c26f2139686ae0d31b8ab2de3d422# Parent 20b8585ad1e0c1e7d7eb09499f85a18d432fca7d merge diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/Examples/FSet.thy Tue Dec 08 11:20:01 2009 +0100 @@ -303,7 +303,7 @@ lemma "IN x EMPTY = False" apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} 1 *}) apply(tactic {* clean_tac @{context} 1*}) done @@ -331,8 +331,6 @@ apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [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 @@ -348,7 +346,7 @@ apply(tactic {* regularize_tac @{context} 1 *}) defer apply(tactic {* clean_tac @{context} 1 *}) -apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ +apply(tactic {* inj_repabs_tac @{context} 1*})+ done lemma list_induct_part: @@ -390,10 +388,6 @@ where "INSERT2 \ op #" -ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} - lemma "P (x :: 'a fset2) (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 @@ -425,9 +419,6 @@ apply (auto) sorry -ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} - lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) done diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/Examples/IntEx.thy Tue Dec 08 11:20:01 2009 +0100 @@ -136,15 +136,6 @@ shows "(intrel ===> intrel ===> intrel) my_plus my_plus" by (simp) -ML {* val qty = @{typ "my_int"} *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} - -ML {* fun lift_tac_intex lthy t = lift_tac lthy t *} - -ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} -ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} - lemma test1: "my_plus a b = my_plus a b" apply(rule refl) done @@ -152,7 +143,7 @@ lemma "PLUS a b = PLUS a b" apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -168,7 +159,7 @@ apply(rule ballI) apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) apply(simp only: in_respects) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -180,7 +171,7 @@ apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) apply(rule impI) apply(rule plus_rsp) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -188,7 +179,7 @@ lemma "PLUS a b = PLUS b a" apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -203,7 +194,7 @@ lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -214,7 +205,7 @@ lemma "foldl PLUS x [] = x" apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) done @@ -225,7 +216,7 @@ lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) done @@ -236,7 +227,7 @@ lemma "foldl f (x::my_int) ([]::my_int list) = x" apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) (* TODO: does not work when this is added *) (* apply(tactic {* lambda_prs_tac @{context} 1 *})*) apply(tactic {* clean_tac @{context} 1 *}) @@ -249,7 +240,7 @@ lemma "(\x. (x, x)) (y::my_int) = (y, y)" apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(simp add: pair_prs) done @@ -325,7 +316,7 @@ lemma "(\(y :: my_int). y) = (\(x :: my_int). x)" apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) defer -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(subst babs_rsp) apply(tactic {* clean_tac @{context} 1 *}) @@ -343,7 +334,7 @@ lemma "(\(y :: my_int => my_int). y) = (\(x :: my_int => my_int). x)" apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *}) defer -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(subst babs_rsp) apply(tactic {* clean_tac @{context} 1 *}) diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/Examples/IntEx2.thy Tue Dec 08 11:20:01 2009 +0100 @@ -166,10 +166,6 @@ text{*The integers form a @{text comm_ring_1}*} -ML {* val qty = @{typ "int"} *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *} - instance int :: comm_ring_1 proof fix i j k :: int diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/LFex.thy --- a/Quot/Examples/LFex.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/Examples/LFex.thy Tue Dec 08 11:20:01 2009 +0100 @@ -218,12 +218,6 @@ thm akind_aty_atrm.induct thm kind_ty_trm.induct -ML {* - val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} - val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot - val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot -*} lemma assumes a0: @@ -261,7 +255,7 @@ apply - apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} 1 *}) apply(fold perm_kind_def perm_ty_def perm_trm_def) apply(tactic {* clean_tac @{context} 1 *}) (* diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/Examples/LamEx.thy Tue Dec 08 11:20:01 2009 +0100 @@ -169,54 +169,48 @@ apply (simp_all add: rlam.inject alpha_refl) done -ML {* val qty = @{typ "lam"} *} -ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} - -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} -ML {* fun lift_tac_lam lthy t = lift_tac lthy t *} lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" -apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) +apply (tactic {* lift_tac @{context} @{thm pi_var_com} 1 *}) done lemma pi_app: "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" -apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *}) +apply (tactic {* lift_tac @{context} @{thm pi_app_com} 1 *}) done lemma pi_lam: "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" -apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *}) +apply (tactic {* lift_tac @{context} @{thm pi_lam_com} 1 *}) done lemma fv_var: "fv (Var (a\name)) = {a}" -apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) +apply (tactic {* lift_tac @{context} @{thm rfv_var} 1 *}) done lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" -apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *}) +apply (tactic {* lift_tac @{context} @{thm rfv_app} 1 *}) done lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" -apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *}) +apply (tactic {* lift_tac @{context} @{thm rfv_lam} 1 *}) done lemma a1: "(a\name) = (b\name) \ Var a = Var b" -apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *}) +apply (tactic {* lift_tac @{context} @{thm a1} 1 *}) done lemma a2: "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" -apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) +apply (tactic {* lift_tac @{context} @{thm a2} 1 *}) done lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" -apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) +apply (tactic {* lift_tac @{context} @{thm a3} 1 *}) done lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ \ P" -apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) +apply (tactic {* lift_tac @{context} @{thm alpha.cases} 1 *}) done lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); @@ -224,16 +218,16 @@ \(x\lam) (a\name) (b\name) xa\lam. \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ \ qxb qx qxa" -apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) +apply (tactic {* lift_tac @{context} @{thm alpha.induct} 1 *}) done lemma var_inject: "(Var a = Var b) = (a = b)" -apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) +apply (tactic {* lift_tac @{context} @{thm rvar_inject} 1 *}) done lemma lam_induct:" \\name. P (Var name); \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); \name lam. P lam \ P (Lam name lam)\ \ P lam" -apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *}) +apply (tactic {* lift_tac @{context} @{thm rlam.induct} 1 *}) done lemma var_supp: diff -r ca37f4b6457c -r 8dfae5d97387 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/QuotMain.thy Tue Dec 08 11:20:01 2009 +0100 @@ -144,11 +144,10 @@ declare [[map * = (prod_fun, prod_rel)]] declare [[map "fun" = (fun_map, fun_rel)]] -(* FIXME: This should throw an exception: -declare [[map "option" = (bla, blu)]] -*) -(* identity quotient is not here as it has to be applied first *) +(* Throws now an exception: *) +(* declare [[map "option" = (bla, blu)]] *) + lemmas [quotient_thm] = fun_quotient prod_quotient @@ -160,22 +159,17 @@ lemmas [quotient_equiv] = identity_equivp prod_equivp -ML {* maps_lookup @{theory} "*" *} -ML {* maps_lookup @{theory} "fun" *} - - (* definition of the quotient types *) (* FIXME: should be called quotient_typ.ML *) use "quotient.ML" - (* lifting of constants *) use "quotient_def.ML" section {* Simset setup *} -(* since HOL_basic_ss is too "big", we need to set up *) -(* our own minimal simpset *) +(* Since HOL_basic_ss is too "big" for us, *) +(* we set up our own minimal simpset. *) ML {* fun mk_minimal_ss ctxt = Simplifier.context ctxt empty_ss @@ -184,11 +178,10 @@ *} ML {* -(* TODO/FIXME not needed anymore? *) -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +fun OF1 thm1 thm2 = thm2 RS thm1 *} -section {* atomize *} +section {* Atomize Infrastructure *} lemma atomize_eqv[atomize]: shows "(Trueprop A \ Trueprop B) \ (A \ B)" @@ -220,24 +213,20 @@ end *} -section {* infrastructure about id *} +section {* Infrastructure about id *} + +print_attributes (* TODO: think where should this be *) lemma prod_fun_id: "prod_fun id id \ id" by (rule eq_reflection) (simp add: prod_fun_def) -(* FIXME: make it a list and add map_id to it *) -lemmas id_simps = +lemmas [id_simps] = fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] prod_fun_id -ML {* -fun simp_ids thm = - MetaSimplifier.rewrite_rule @{thms id_simps} thm -*} - section {* Debugging infrastructure for testing tactics *} ML {* @@ -265,7 +254,7 @@ fun NDT ctxt s tac thm = tac thm *} -section {* Matching of terms and types *} +section {* Matching of Terms and Types *} ML {* fun matches_typ (ty, ty') = @@ -278,9 +267,7 @@ then (List.all matches_typ (tys ~~ tys')) else false | _ => false -*} -ML {* fun matches_term (trm, trm') = case (trm, trm') of (_, Var _) => true @@ -292,37 +279,7 @@ | _ => false *} -section {* Infrastructure for collecting theorems for starting the lifting *} - -ML {* -fun lookup_quot_data lthy qty = - let - val qty_name = fst (dest_Type qty) - val SOME quotdata = quotdata_lookup lthy qty_name - (* TODO: Should no longer be needed *) - val rty = Logic.unvarifyT (#rtyp quotdata) - val rel = #rel quotdata - val rel_eqv = #equiv_thm quotdata - val rel_refl = @{thm equivp_reflp} OF [rel_eqv] - in - (rty, rel, rel_refl, rel_eqv) - end -*} - -ML {* -fun lookup_quot_thms lthy qty_name = - let - val thy = ProofContext.theory_of lthy; - val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") - val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") - val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") - val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) - in - (trans2, reps_same, absrep, quot) - end -*} - -section {* Regularization *} +section {* Computation of the Regularize Goal *} (* Regularizing an rtrm means: @@ -489,13 +446,13 @@ raise (LIFT_MATCH "regularize (default)") *} +section {* Regularize Tactic *} + ML {* fun equiv_tac ctxt = (K (print_tac "equiv tac")) THEN' REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) -*} -ML {* fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac *} @@ -537,7 +494,7 @@ SOME thm2 end handle _ => NONE -(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *) +(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) *} ML {* @@ -560,20 +517,23 @@ shows "equivp R \ a = b \ R a b" by (simp add: equivp_reflp) -(* FIXME/TODO: How does regularizing work? *) -(* FIXME/TODO: needs to be adapted -To prove that the raw theorem implies the regularised one, -we try in order: +(* Regularize Tactic *) - - Reflexivity of the relation - - Assumption - - Elimnating quantifiers on both sides of toplevel implication - - Simplifying implications on both sides of toplevel implication - - Ball (Respects ?E) ?P = All ?P - - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q +(* 0. preliminary simplification step according to *) +thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) + ball_reg_eqv_range bex_reg_eqv_range +(* 1. eliminating simple Ball/Bex instances*) +thm ball_reg_right bex_reg_left +(* 2. monos *) +(* 3. commutation rules for ball and bex *) +thm ball_all_comm bex_ex_comm +(* 4. then rel-equality (which need to be instantiated to avoid loops *) +thm eq_imp_rel +(* 5. then simplification like 0 *) +(* finally jump back to 1 *) -*) + ML {* fun regularize_tac ctxt = let @@ -586,24 +546,19 @@ addsimprocs [simproc] addSolver equiv_solver (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) (* can this cause loops in equiv_tac ? *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) + val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) in simp_tac simpset THEN' REPEAT_ALL_NEW (CHANGED o FIRST' [ - rtac @{thm ball_reg_right}, - rtac @{thm bex_reg_left}, + resolve_tac @{thms ball_reg_right bex_reg_left}, resolve_tac (Inductive.get_monos ctxt), - rtac @{thm ball_all_comm}, - rtac @{thm bex_ex_comm}, + resolve_tac @{thms ball_all_comm bex_ex_comm}, resolve_tac eq_eqvs, - (* should be equivalent to the above, but causes loops: *) - (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *) - (* the culprit is aslread rtac @{thm eq_imp_rel} *) simp_tac simpset]) end *} -section {* Injections of rep and abses *} +section {* Calculation of the Injected Goal *} (* Injecting repabs means: @@ -658,8 +613,7 @@ val yvar = Free (y, T) val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) in - if rty = qty - then result + if rty = qty then result else mk_repabs lthy (rty, qty) result end @@ -667,8 +621,7 @@ (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) | (Free (_, T), Free (_, T')) => - if T = T' - then rtrm + if T = T' then rtrm else mk_repabs lthy (T, T') rtrm | (_, Const (@{const_name "op ="}, _)) => rtrm @@ -678,35 +631,33 @@ let val rty = fastype_of rtrm in - if rty = T' - then rtrm + if rty = T' then rtrm else mk_repabs lthy (rty, T') rtrm end | _ => raise (LIFT_MATCH "injection") *} -section {* RepAbs Injection Tactic *} +section {* Injection Tactic *} ML {* fun quotient_tac ctxt = REPEAT_ALL_NEW (FIRST' [rtac @{thm identity_quotient}, resolve_tac (quotient_rules_get ctxt)]) -*} -(* solver for the simplifier *) -ML {* fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac *} ML {* fun solve_quotient_assums ctxt thm = - let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in - thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] - end - handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" +let + val goal = hd (Drule.strip_imp_prems (cprop_of thm)) +in + thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] +end +handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" *} (* Not used *) @@ -914,9 +865,9 @@ (* reflexivity of operators arising from Cong_tac *) | Const (@{const_name "op ="},_) $ _ $ _ - => rtac @{thm refl} ORELSE' + => rtac @{thm refl} (*ORELSE' (resolve_tac trans2 THEN' RANGE [ - quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) (* TODO: These patterns should should be somehow combined and generalized... *) | (Const (@{const_name fun_rel}, _) $ _ $ _) $ @@ -943,32 +894,49 @@ *} ML {* -fun inj_repabs_tac ctxt rel_refl trans2 = +fun inj_repabs_step_tac ctxt rel_refl trans2 = (FIRST' [ - inj_repabs_tac_match ctxt trans2, + NDT ctxt "0" (inj_repabs_tac_match ctxt trans2), (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) + NDT ctxt "A" (apply_rsp_tac ctxt THEN' - (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), + + (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *) + NDT ctxt "B" (resolve_tac trans2 THEN' + RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), + (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) (* merge with previous tactic *) - NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' + NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), + (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) - NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), + NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), + (* resolving with R x y assumptions *) NDT ctxt "E" (atac), + (* reflexivity of the basic relations *) (* R \ \ *) - NDT ctxt "D" (resolve_tac rel_refl) + NDT ctxt "F" (resolve_tac rel_refl) ]) *} ML {* -fun all_inj_repabs_tac ctxt rel_refl trans2 = - REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) +fun inj_repabs_tac ctxt = +let + val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) + val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt) +in + inj_repabs_step_tac ctxt rel_refl trans2 +end + +fun all_inj_repabs_tac ctxt = + REPEAT_ALL_NEW (inj_repabs_tac ctxt) *} -section {* Cleaning of the theorem *} +section {* Cleaning of the Theorem *} ML {* fun make_inst lhs t = @@ -1017,7 +985,7 @@ val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); val ti = (let - val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) in Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts @@ -1026,7 +994,7 @@ val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te in - MetaSimplifier.rewrite_rule @{thms id_simps} td + MetaSimplifier.rewrite_rule (id_simps_get ctxt) td end); val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then (tracing "lambda_prs"; @@ -1049,39 +1017,24 @@ fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) *} -(* - Cleaning the theorem consists of three rewriting steps. - The first two need to be done before fun_map is unfolded - - 1) lambda_prs: - (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f - - Implemented as conversion since it is not a pattern. - - 2) all_prs (the same for exists): - Ball (Respects R) ((abs ---> id) f) ----> All f - - Rewriting with definitions from the argument defs - (rep ---> abs) oldConst ----> newconst - - 3) Quotient_rel_rep: - Rel (Rep x) (Rep y) ----> x = y - - Quotient_abs_rep: - Abs (Rep x) ----> x - - id_simps; fun_map.simps -*) +(* 1. conversion (is not a pattern) *) +thm lambda_prs +(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) +(* and simplification with *) +thm all_prs ex_prs +(* 3. simplification with *) +thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps +(* 4. Test for refl *) ML {* fun clean_tac lthy = let val thy = ProofContext.theory_of lthy; val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) - (* FIXME: shouldn't the definitions already be varified? *) + (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) val thms1 = @{thms all_prs ex_prs} @ defs - val thms2 = @{thms eq_reflection[OF fun_map.simps]} - @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} + val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) + @ @{thms Quotient_abs_rep Quotient_rel_rep} fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver in EVERY' [lambda_prs_tac lthy, @@ -1091,7 +1044,7 @@ end *} -section {* Genralisation of free variables in a goal *} +section {* Tactic for genralisation of free variables in a goal *} ML {* fun inst_spec ctrm = @@ -1121,7 +1074,7 @@ end) *} -section {* General outline of the lifting procedure *} +section {* General Shape of the Lifting Procedure *} (* - A is the original raw theorem *) (* - B is the regularized theorem *) @@ -1138,8 +1091,8 @@ and c: "B = C" and d: "C = D" shows "D" - using a b c d - by simp +using a b c d +by simp ML {* fun lift_match_error ctxt fun_str rtrm qtrm = @@ -1162,11 +1115,9 @@ val reg_goal = Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "Regularization done." val inj_goal = Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "RepAbs Injection done." in Drule.instantiate' [] [SOME (cterm_of thy rtrm'), @@ -1175,42 +1126,40 @@ end *} -(* Left for debugging *) ML {* +(* the tactic leaves three subgoals to be proved *) fun procedure_tac ctxt rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => + THEN' CSUBGOAL (fn (goal, i) => let val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} + val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) + val bare_goal = snd (Thm.dest_comb goal) + val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i} in - (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i + (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i end) *} +(* automatic proofs *) +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) + +fun WARN (tac, msg) i st = + case Seq.pull ((SOLVES' tac) i st) of + NONE => (warning msg; Seq.single st) + | seqcell => Seq.make (fn () => seqcell) + +fun RANGE_WARN xs = RANGE (map WARN xs) +*} + ML {* -(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) - fun lift_tac ctxt rthm = - ObjectLogic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) - val quotients = quotient_rules_get ctxt - val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} - in - (rtac rule THEN' - RANGE [rtac rthm', - regularize_tac ctxt, - rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, - clean_tac ctxt]) i - end) + procedure_tac ctxt rthm + THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), + (all_inj_repabs_tac ctxt, "Injection proof failed."), + (clean_tac ctxt, "Cleaning proof failed.")] *} end diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Quotients.thy --- a/Quot/Quotients.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/Quotients.thy Tue Dec 08 11:20:01 2009 +0100 @@ -42,10 +42,6 @@ "sum_map f1 f2 (Inl a) = Inl (f1 a)" | "sum_map f1 f2 (Inr a) = Inr (f2 a)" - - - - fun noption_map::"('a \ 'b) \ ('a noption) \ ('b noption)" where diff -r ca37f4b6457c -r 8dfae5d97387 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/quotient_info.ML Tue Dec 08 11:20:01 2009 +0100 @@ -26,6 +26,7 @@ val equiv_rules_get: Proof.context -> thm list val equiv_rules_add: attribute val rsp_rules_get: Proof.context -> thm list + val id_simps_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute end; @@ -62,6 +63,10 @@ val tyname = Sign.intern_type thy tystr val mapname = Sign.intern_const thy mapstr val relname = Sign.intern_const thy relstr + + fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt) + handle _ => error ("Constant " ^ s ^ " not declared.") + val _ = map check [mapname, relname] in maps_attribute_aux tyname {mapfun = mapname, relfun = relname} end @@ -170,6 +175,9 @@ OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) +(* FIXME/TODO: check the various lemmas conform *) +(* with the required shape *) + (* equivalence relation theorems *) structure EquivRules = Named_Thms (val name = "quotient_equiv" @@ -185,6 +193,13 @@ val rsp_rules_get = RspRules.get +(* respectfulness theorems *) +structure IdSimps = Named_Thms + (val name = "id_simps" + val description = "Identity simp rules for maps.") + +val id_simps_get = IdSimps.get + (* quotient theorems *) structure QuotientRules = Named_Thms (val name = "quotient_thm" @@ -197,6 +212,7 @@ val _ = Context.>> (Context.map_theory (EquivRules.setup #> RspRules.setup #> + IdSimps.setup #> QuotientRules.setup)) end; (* structure *)