# HG changeset patch # User Christian Urban # Date 1260219254 -3600 # Node ID bb5d3278f02eac68ea294ff2d8d9c26f3ed91877 # Parent 2bee5ca44ef567a900b96124e27fcfb5af6a19b9# Parent 6ce4f274b0fab0b4571e232840d57daaaa455fc9 merged diff -r 6ce4f274b0fa -r bb5d3278f02e Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Mon Dec 07 21:25:49 2009 +0100 +++ b/Quot/Examples/FSet.thy Mon Dec 07 21:54:14 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 6ce4f274b0fa -r bb5d3278f02e Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Mon Dec 07 21:25:49 2009 +0100 +++ b/Quot/Examples/IntEx.thy Mon Dec 07 21:54:14 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 @@ -162,13 +153,15 @@ apply(rule refl) done + + lemma "PLUS a = PLUS a" apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) apply(rule impI) 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 +173,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 +181,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 +196,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 +207,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 +218,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 +229,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 +242,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 @@ -311,7 +304,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 *}) @@ -329,7 +322,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 6ce4f274b0fa -r bb5d3278f02e Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Mon Dec 07 21:25:49 2009 +0100 +++ b/Quot/Examples/IntEx2.thy Mon Dec 07 21:54:14 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 6ce4f274b0fa -r bb5d3278f02e Quot/Examples/LFex.thy --- a/Quot/Examples/LFex.thy Mon Dec 07 21:25:49 2009 +0100 +++ b/Quot/Examples/LFex.thy Mon Dec 07 21:54:14 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 6ce4f274b0fa -r bb5d3278f02e Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Mon Dec 07 21:25:49 2009 +0100 +++ b/Quot/Examples/LamEx.thy Mon Dec 07 21:54:14 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 6ce4f274b0fa -r bb5d3278f02e Quot/QuotMain.thy --- a/Quot/QuotMain.thy Mon Dec 07 21:25:49 2009 +0100 +++ b/Quot/QuotMain.thy Mon Dec 07 21:54:14 2009 +0100 @@ -186,6 +186,8 @@ 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 *} @@ -292,36 +294,6 @@ | _ => 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 *} (* @@ -703,10 +675,12 @@ 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 +888,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,29 +917,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 (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) + val trans2 = map (fn x => @{thm equals_rsp} OF [x]) (quotient_rules_get ctxt) +in + inj_repabs_step_tac ctxt rel_refl trans2 +end +*} + +ML {* +fun all_inj_repabs_tac ctxt = + REPEAT_ALL_NEW (inj_repabs_tac ctxt) +(* if this is too slow we can inline the code above *) *} section {* Cleaning of the theorem *} @@ -1191,24 +1185,19 @@ *} 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) => + THEN' CSUBGOAL (fn (goal, 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} + val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) + val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb goal))] @{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, + rtac thm THEN' all_inj_repabs_tac ctxt, clean_tac ctxt]) i end) *}