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