src/Tools/case_product.ML
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 52732 b4da1f2ec73f
child 54742 7a86358a3c0b
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41883
392364739e5d observe standard header format;
wenzelm
parents: 41826
diff changeset
     1
(*  Title:      Tools/case_product.ML
392364739e5d observe standard header format;
wenzelm
parents: 41826
diff changeset
     2
    Author:     Lars Noschinski, TU Muenchen
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
     3
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
     4
Combine two case rules into a single one.
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
     5
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
     6
Assumes that the theorems are of the form
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
     7
  "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
     8
where m is given by the "consumes" attribute of the theorem.
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
     9
*)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    10
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    11
signature CASE_PRODUCT =
41883
392364739e5d observe standard header format;
wenzelm
parents: 41826
diff changeset
    12
sig
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    13
  val combine: Proof.context -> thm -> thm -> thm
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    14
  val combine_annotated: Proof.context -> thm -> thm -> thm
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    15
  val setup: theory -> theory
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    16
end
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    17
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    18
structure Case_Product: CASE_PRODUCT =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    19
struct
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    20
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    21
(*instantiate the conclusion of thm2 to the one of thm1*)
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    22
fun inst_concl thm1 thm2 =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    23
  let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    24
    val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    25
  in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    26
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    27
fun inst_thms thm1 thm2 ctxt =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    28
  let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    29
    val import = yield_singleton (apfst snd oo Variable.import true)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    30
    val (i_thm1, ctxt') = import thm1 ctxt
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    31
    val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt'
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    32
  in ((i_thm1, i_thm2), ctxt'') end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    33
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    34
(*
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    35
Return list of prems, where loose bounds have been replaced by frees.
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    36
FIXME: Focus
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    37
*)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    38
fun free_prems t ctxt =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    39
  let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    40
    val bs = Term.strip_all_vars t
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    41
    val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    42
    val subst = map Free (names ~~ map snd bs)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    43
    val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    44
  in ((t', subst), ctxt') end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    45
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    46
fun build_concl_prems thm1 thm2 ctxt =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    47
  let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    48
    val concl = Thm.concl_of thm1
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    49
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    50
    fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
48902
44a6967240b7 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents: 45375
diff changeset
    51
    val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
44a6967240b7 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents: 45375
diff changeset
    52
    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    53
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    54
    val p_cases_prod = map (fn p1 => map (fn p2 =>
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    55
      let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    56
        val (((t1, subst1), (t2, subst2)), _) = ctxt
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    57
          |> free_prems p1 ||>> free_prems p2
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    58
      in
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    59
        Logic.list_implies (t1 @ t2, concl)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    60
        |> fold_rev Logic.all (subst1 @ subst2)
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    61
      end) p_cases2) p_cases1
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    62
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    63
    val prems = p_cons1 :: p_cons2 :: p_cases_prod
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    64
  in
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    65
    (concl, prems)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    66
  end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    67
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    68
fun case_product_tac prems struc thm1 thm2 =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    69
  let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    70
    val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    71
    val thm2' = thm2 OF p_cons2
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    72
  in
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 48902
diff changeset
    73
    rtac (thm1 OF p_cons1)
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    74
     THEN' EVERY' (map (fn p =>
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 48902
diff changeset
    75
       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    76
  end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    77
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    78
fun combine ctxt thm1 thm2 =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    79
  let
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    80
    val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    81
    val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    82
  in
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    83
    Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    84
      case_product_tac prems prems_rich i_thm1 i_thm2 1)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    85
    |> singleton (Variable.export ctxt' ctxt)
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    86
  end
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    87
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    88
fun annotation_rule thm1 thm2 =
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    89
  let
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42361
diff changeset
    90
    val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42361
diff changeset
    91
    val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    92
    val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    93
  in
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    94
    Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    95
  end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    96
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    97
fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
    98
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
    99
fun combine_annotated ctxt thm1 thm2 =
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   100
  combine ctxt thm1 thm2
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
   101
  |> annotation_rule thm1 thm2
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   102
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
   103
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
   104
(* attribute setup *)
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   105
41883
392364739e5d observe standard header format;
wenzelm
parents: 41826
diff changeset
   106
val case_prod_attr =
392364739e5d observe standard header format;
wenzelm
parents: 41826
diff changeset
   107
  let
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   108
    fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   109
  in
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   110
    Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   111
      combine_list (Context.proof_of ctxt) thms thm))
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   112
  end
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   113
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   114
val setup =
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
   115
  Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
41826
18d4d2b60016 introduce attribute case_prod for combining case rules
noschinl
parents:
diff changeset
   116
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44045
diff changeset
   117
end