src/Tools/case_product.ML
 author wenzelm Sat Jul 27 16:35:51 2013 +0200 (2013-07-27) changeset 52732 b4da1f2ec73f parent 48902 44a6967240b7 child 54742 7a86358a3c0b permissions -rw-r--r--
standardized aliases;
```     1 (*  Title:      Tools/case_product.ML
```
```     2     Author:     Lars Noschinski, TU Muenchen
```
```     3
```
```     4 Combine 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 (*instantiate 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 Return 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) = take_prefix is_consumes (Thm.prems_of thm1)
```
```    52     val (p_cons2, p_cases2) = take_prefix 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) p_cases2) p_cases1
```
```    62
```
```    63     val prems = p_cons1 :: p_cons2 :: p_cases_prod
```
```    64   in
```
```    65     (concl, prems)
```
```    66   end
```
```    67
```
```    68 fun case_product_tac prems struc thm1 thm2 =
```
```    69   let
```
```    70     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
```
```    71     val thm2' = thm2 OF p_cons2
```
```    72   in
```
```    73     rtac (thm1 OF p_cons1)
```
```    74      THEN' EVERY' (map (fn p =>
```
```    75        rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
```
```    76   end
```
```    77
```
```    78 fun combine ctxt thm1 thm2 =
```
```    79   let
```
```    80     val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
```
```    81     val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
```
```    82   in
```
```    83     Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
```
```    84       case_product_tac prems prems_rich i_thm1 i_thm2 1)
```
```    85     |> singleton (Variable.export ctxt' ctxt)
```
```    86   end
```
```    87
```
```    88 fun annotation_rule thm1 thm2 =
```
```    89   let
```
```    90     val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
```
```    91     val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
```
```    92     val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2
```
```    93   in
```
```    94     Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
```
```    95   end
```
```    96
```
```    97 fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
```
```    98
```
```    99 fun combine_annotated ctxt thm1 thm2 =
```
```   100   combine ctxt thm1 thm2
```
```   101   |> annotation_rule thm1 thm2
```
```   102
```
```   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
```