# HG changeset patch # User noschinl # Date 1291828716 -3600 # Node ID 18d4d2b600161ec663e2e5f0829f4c021b812f7d # Parent 49d5af6a3d1bbd6a6c2c06d753cec36fdd7e1143 introduce attribute case_prod for combining case rules * * * [PATCH 1/9] Make tac independent of consumes From 1a53ef4c070f924ff8e69529b0c1b13fa2844722 Mon Sep 17 00:00:00 2001 --- case_product.ML | 11 ++++++----- 1 files changed, 6 insertions(+), 5 deletions(-) * * * [PATCH 2/9] Replace MRS by OF From da55d08ae287bfdc18dec554067b45a3e298c243 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) * * * [PATCH 3/9] Clean up tactic From d26d50caaa3526c8c0625d7395467c6914f1a8d9 Mon Sep 17 00:00:00 2001 --- case_product.ML | 13 +++++-------- 1 files changed, 5 insertions(+), 8 deletions(-) * * * [PATCH 4/9] Move out get_consumes a bit more From 6ed5415f29cc43cea30c216edb1e74ec6c0f6c33 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) * * * [PATCH 5/9] Clean up tactic From d301cfe6377e9f7db74b190fb085e0e66eeadfb5 Mon Sep 17 00:00:00 2001 --- case_product.ML | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) * * * [PATCH 6/9] Cleanup build_concl_prems From c30889e131e74a92caac5b1e6d3d816890406ca7 Mon Sep 17 00:00:00 2001 --- case_product.ML | 18 ++++++++---------- 1 files changed, 8 insertions(+), 10 deletions(-) * * * [PATCH 7/9] Split logic & annotation a bit From e065606118308c96e013fad72ab9ad89b5a4b945 Mon Sep 17 00:00:00 2001 --- case_product.ML | 26 ++++++++++++++++++-------- 1 files changed, 18 insertions(+), 8 deletions(-) * * * [PATCH 8/9] Remove dependency on consumes attribute From e2a4de044481586d6127bbabd0ef48d0e3ab57c0 Mon Sep 17 00:00:00 2001 --- case_product.ML | 46 ++++++++++++++++++++++------------------------ 1 files changed, 22 insertions(+), 24 deletions(-) * * * [PATCH 9/9] whitespace From 59f5036bd8f825da4a362970292a34ec06c0f1a2 Mon Sep 17 00:00:00 2001 --- case_product.ML | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff -r 49d5af6a3d1b -r 18d4d2b60016 src/Tools/case_product.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/case_product.ML Wed Dec 08 18:18:36 2010 +0100 @@ -0,0 +1,117 @@ +(* Title: case_product.ML + Author: Lars Noschinski + +Combines two case rules into a single one. + +Assumes that the theorems are of the form + "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P" +where m is given by the "consumes" attribute of the theorem. +*) + +signature CASE_PRODUCT = + sig + + val combine: Proof.context -> thm -> thm -> thm + val combine_annotated: Proof.context -> thm -> thm -> thm + val setup: theory -> theory +end; + +structure Case_Product: CASE_PRODUCT = +struct + +(*Instantiates the conclusion of thm2 to the one of thm1.*) +fun inst_concl thm1 thm2 = + let + val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of + in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end + +fun inst_thms thm1 thm2 ctxt = + let + val import = yield_singleton (apfst snd oo Variable.import true) + val (i_thm1, ctxt') = import thm1 ctxt + val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt' + in ((i_thm1, i_thm2), ctxt'') end + +(* +Returns list of prems, where loose bounds have been replaced by frees. +FIXME: Focus +*) +fun free_prems t ctxt = + let + val bs = Term.strip_all_vars t + val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt + val subst = map Free (names ~~ map snd bs) + val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t) + in ((t', subst), ctxt') end + +fun build_concl_prems thm1 thm2 ctxt = + let + val concl = Thm.concl_of thm1 + + fun is_consumes t = not (Logic.strip_assums_concl t aconv concl) + val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1) + val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2) + + val p_cases_prod = map (fn p1 => map (fn p2 => + let + val (((t1, subst1), (t2, subst2)), _) = ctxt + |> free_prems p1 ||>> free_prems p2 + in + Logic.list_implies (t1 @ t2, concl) + |> fold_rev Logic.all (subst1 @ subst2) + end + ) p_cases2) p_cases1 + + val prems = p_cons1 :: p_cons2 :: p_cases_prod + in + (concl, prems) + end + +fun case_product_tac prems struc thm1 thm2 = + let + val (p_cons1 :: p_cons2 :: premss) = unflat struc prems + val thm2' = thm2 OF p_cons2 + in + (Tactic.rtac (thm1 OF p_cons1) + THEN' EVERY' (map (fn p => + Tactic.rtac thm2' + THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss) + ) + end + +fun combine ctxt thm1 thm2 = + let + val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt + val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt' + in + Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} => + case_product_tac prems prems_rich i_thm1 i_thm2 1) + |> singleton (Variable.export ctxt' ctxt) + end; + +fun annotation thm1 thm2 = + let + val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1) + val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2) + val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2 + in + Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2) + end + +fun combine_annotated ctxt thm1 thm2 = + combine ctxt thm1 thm2 + |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt) + +(* Attribute setup *) + +val case_prod_attr = let + fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x) + in + Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm => + combine_list (Context.proof_of ctxt) thms thm)) + end + +val setup = + Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules" + +end;