src/Tools/case_product.ML
author wenzelm
Sat Apr 16 16:15:37 2011 +0200 (2011-04-16)
changeset 42361 23f352990944
parent 41883 392364739e5d
child 44045 2814ff2a6e3e
permissions -rw-r--r--
modernized structure Proof_Context;
     1 (*  Title:      Tools/case_product.ML
     2     Author:     Lars Noschinski, TU Muenchen
     3 
     4 Combines two case rules into a single one.
     5 
     6 Assumes that the theorems are of the form
     7   "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
     8 where m is given by the "consumes" attribute of the theorem.
     9 *)
    10 
    11 signature CASE_PRODUCT =
    12 sig
    13   val combine: Proof.context -> thm -> thm -> thm
    14   val combine_annotated: Proof.context -> thm -> thm -> thm
    15   val setup: theory -> theory
    16 end;
    17 
    18 structure Case_Product: CASE_PRODUCT =
    19 struct
    20 
    21 (*Instantiates the conclusion of thm2 to the one of thm1.*)
    22 fun inst_concl thm1 thm2 =
    23   let
    24     val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
    25   in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end
    26 
    27 fun inst_thms thm1 thm2 ctxt =
    28   let
    29     val import = yield_singleton (apfst snd oo Variable.import true)
    30     val (i_thm1, ctxt') = import thm1 ctxt
    31     val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt'
    32   in ((i_thm1, i_thm2), ctxt'') end
    33 
    34 (*
    35 Returns list of prems, where loose bounds have been replaced by frees.
    36 FIXME: Focus
    37 *)
    38 fun free_prems t ctxt =
    39   let
    40     val bs = Term.strip_all_vars t
    41     val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt
    42     val subst = map Free (names ~~ map snd bs)
    43     val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t)
    44   in ((t', subst), ctxt') end
    45 
    46 fun build_concl_prems thm1 thm2 ctxt =
    47   let
    48     val concl = Thm.concl_of thm1
    49 
    50     fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
    51     val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1)
    52     val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2)
    53 
    54     val p_cases_prod = map (fn p1 => map (fn p2 =>
    55       let
    56         val (((t1, subst1), (t2, subst2)), _) = ctxt
    57           |> free_prems p1 ||>> free_prems p2
    58       in
    59         Logic.list_implies (t1 @ t2, concl)
    60         |> fold_rev Logic.all (subst1 @ subst2)
    61       end
    62       ) p_cases2) p_cases1
    63 
    64     val prems = p_cons1 :: p_cons2 :: p_cases_prod
    65   in
    66     (concl, prems)
    67   end
    68 
    69 fun case_product_tac prems struc thm1 thm2 =
    70   let
    71     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
    72     val thm2' = thm2 OF p_cons2
    73   in
    74     (Tactic.rtac (thm1 OF p_cons1)
    75      THEN' EVERY' (map (fn p =>
    76        Tactic.rtac thm2'
    77        THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
    78     )
    79   end
    80 
    81 fun combine ctxt thm1 thm2 =
    82   let
    83     val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
    84     val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
    85   in
    86     Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
    87       case_product_tac prems prems_rich i_thm1 i_thm2 1)
    88     |> singleton (Variable.export ctxt' ctxt)
    89   end;
    90 
    91 fun annotation thm1 thm2 =
    92   let
    93     val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
    94     val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
    95     val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
    96   in
    97     Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
    98   end
    99 
   100 fun combine_annotated ctxt thm1 thm2 =
   101   combine ctxt thm1 thm2
   102   |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt)
   103 
   104 (* Attribute setup *)
   105 
   106 val case_prod_attr =
   107   let
   108     fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
   109   in
   110     Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
   111       combine_list (Context.proof_of ctxt) thms thm))
   112   end
   113 
   114 val setup =
   115  Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules"
   116 
   117 end;