introduce attribute case_prod for combining case rules
authornoschinl
Wed Dec 08 18:18:36 2010 +0100 (2010-12-08)
changeset 4182618d4d2b60016
parent 41825 49d5af6a3d1b
child 41827 98eda7ffde79
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(-)
src/Tools/case_product.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/case_product.ML	Wed Dec 08 18:18:36 2010 +0100
     1.3 @@ -0,0 +1,117 @@
     1.4 +(*   Title: case_product.ML
     1.5 +     Author: Lars Noschinski
     1.6 +
     1.7 +Combines two case rules into a single one.
     1.8 +
     1.9 +Assumes that the theorems are of the form
    1.10 +  "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
    1.11 +where m is given by the "consumes" attribute of the theorem.
    1.12 +*)
    1.13 +
    1.14 +signature CASE_PRODUCT =
    1.15 +  sig
    1.16 +
    1.17 +  val combine: Proof.context -> thm -> thm -> thm
    1.18 +  val combine_annotated: Proof.context -> thm -> thm -> thm
    1.19 +  val setup: theory -> theory
    1.20 +end;
    1.21 +
    1.22 +structure Case_Product: CASE_PRODUCT =
    1.23 +struct
    1.24 +
    1.25 +(*Instantiates the conclusion of thm2 to the one of thm1.*)
    1.26 +fun inst_concl thm1 thm2 =
    1.27 +  let
    1.28 +    val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
    1.29 +  in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end
    1.30 +
    1.31 +fun inst_thms thm1 thm2 ctxt =
    1.32 +  let
    1.33 +    val import = yield_singleton (apfst snd oo Variable.import true)
    1.34 +    val (i_thm1, ctxt') = import thm1 ctxt
    1.35 +    val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt'
    1.36 +  in ((i_thm1, i_thm2), ctxt'') end
    1.37 +
    1.38 +(*
    1.39 +Returns list of prems, where loose bounds have been replaced by frees.
    1.40 +FIXME: Focus
    1.41 +*)
    1.42 +fun free_prems t ctxt =
    1.43 +  let
    1.44 +    val bs = Term.strip_all_vars t
    1.45 +    val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt
    1.46 +    val subst = map Free (names ~~ map snd bs)
    1.47 +    val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t)
    1.48 +  in ((t', subst), ctxt') end
    1.49 +
    1.50 +fun build_concl_prems thm1 thm2 ctxt =
    1.51 +  let
    1.52 +    val concl = Thm.concl_of thm1
    1.53 +
    1.54 +    fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
    1.55 +    val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1)
    1.56 +    val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2)
    1.57 +
    1.58 +    val p_cases_prod = map (fn p1 => map (fn p2 =>
    1.59 +      let
    1.60 +        val (((t1, subst1), (t2, subst2)), _) = ctxt
    1.61 +          |> free_prems p1 ||>> free_prems p2
    1.62 +      in
    1.63 +        Logic.list_implies (t1 @ t2, concl)
    1.64 +        |> fold_rev Logic.all (subst1 @ subst2)
    1.65 +      end
    1.66 +      ) p_cases2) p_cases1
    1.67 +
    1.68 +    val prems = p_cons1 :: p_cons2 :: p_cases_prod
    1.69 +  in
    1.70 +    (concl, prems)
    1.71 +  end
    1.72 +
    1.73 +fun case_product_tac prems struc thm1 thm2 =
    1.74 +  let
    1.75 +    val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
    1.76 +    val thm2' = thm2 OF p_cons2
    1.77 +  in
    1.78 +    (Tactic.rtac (thm1 OF p_cons1)
    1.79 +     THEN' EVERY' (map (fn p =>
    1.80 +       Tactic.rtac thm2'
    1.81 +       THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss)
    1.82 +    )
    1.83 +  end
    1.84 +
    1.85 +fun combine ctxt thm1 thm2 =
    1.86 +  let
    1.87 +    val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
    1.88 +    val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
    1.89 +  in
    1.90 +    Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
    1.91 +      case_product_tac prems prems_rich i_thm1 i_thm2 1)
    1.92 +    |> singleton (Variable.export ctxt' ctxt)
    1.93 +  end;
    1.94 +
    1.95 +fun annotation thm1 thm2 =
    1.96 +  let
    1.97 +    val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
    1.98 +    val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
    1.99 +    val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
   1.100 +  in
   1.101 +    Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
   1.102 +  end
   1.103 +
   1.104 +fun combine_annotated ctxt thm1 thm2 =
   1.105 +  combine ctxt thm1 thm2
   1.106 +  |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt)
   1.107 +
   1.108 +(* Attribute setup *)
   1.109 +
   1.110 +val case_prod_attr = let
   1.111 +    fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
   1.112 +  in
   1.113 +    Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
   1.114 +      combine_list (Context.proof_of ctxt) thms thm))
   1.115 +  end
   1.116 +
   1.117 +val setup =
   1.118 + Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules"
   1.119 +
   1.120 +end;