src/Tools/case_product.ML
 changeset 45375 7fe19930dfc9 parent 44045 2814ff2a6e3e child 48902 44a6967240b7
```     1.1 --- a/src/Tools/case_product.ML	Sun Nov 06 21:17:45 2011 +0100
1.2 +++ b/src/Tools/case_product.ML	Sun Nov 06 21:51:46 2011 +0100
1.3 @@ -1,7 +1,7 @@
1.4  (*  Title:      Tools/case_product.ML
1.5      Author:     Lars Noschinski, TU Muenchen
1.6
1.7 -Combines two case rules into a single one.
1.8 +Combine two case rules into a single one.
1.9
1.10  Assumes that the theorems are of the form
1.11    "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
1.12 @@ -13,12 +13,12 @@
1.13    val combine: Proof.context -> thm -> thm -> thm
1.14    val combine_annotated: Proof.context -> thm -> thm -> thm
1.15    val setup: theory -> theory
1.16 -end;
1.17 +end
1.18
1.19  structure Case_Product: CASE_PRODUCT =
1.20  struct
1.21
1.22 -(*Instantiates the conclusion of thm2 to the one of thm1.*)
1.23 +(*instantiate the conclusion of thm2 to the one of thm1*)
1.24  fun inst_concl thm1 thm2 =
1.25    let
1.26      val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
1.27 @@ -32,7 +32,7 @@
1.28    in ((i_thm1, i_thm2), ctxt'') end
1.29
1.30  (*
1.31 -Returns list of prems, where loose bounds have been replaced by frees.
1.32 +Return list of prems, where loose bounds have been replaced by frees.
1.33  FIXME: Focus
1.34  *)
1.35  fun free_prems t ctxt =
1.36 @@ -58,8 +58,7 @@
1.37        in
1.38          Logic.list_implies (t1 @ t2, concl)
1.39          |> fold_rev Logic.all (subst1 @ subst2)
1.40 -      end
1.41 -      ) p_cases2) p_cases1
1.42 +      end) p_cases2) p_cases1
1.43
1.44      val prems = p_cons1 :: p_cons2 :: p_cases_prod
1.45    in
1.46 @@ -71,11 +70,10 @@
1.47      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
1.48      val thm2' = thm2 OF p_cons2
1.49    in
1.50 -    (Tactic.rtac (thm1 OF p_cons1)
1.51 +    Tactic.rtac (thm1 OF p_cons1)
1.52       THEN' EVERY' (map (fn p =>
1.53         Tactic.rtac thm2'
1.54         THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
1.55 -    )
1.56    end
1.57
1.58  fun combine ctxt thm1 thm2 =
1.59 @@ -86,22 +84,25 @@
1.60      Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
1.61        case_product_tac prems prems_rich i_thm1 i_thm2 1)
1.62      |> singleton (Variable.export ctxt' ctxt)
1.63 -  end;
1.64 +  end
1.65
1.66 -fun annotation thm1 thm2 =
1.67 +fun annotation_rule thm1 thm2 =
1.68    let
1.69      val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
1.70      val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
1.71 -    val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
1.72 +    val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2
1.73    in
1.74 -    Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
1.75 +    Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
1.76    end
1.77
1.78 +fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
1.79 +
1.80  fun combine_annotated ctxt thm1 thm2 =
1.81    combine ctxt thm1 thm2
1.82 -  |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt)
1.83 +  |> annotation_rule thm1 thm2
1.84
1.85 -(* Attribute setup *)
1.86 +
1.87 +(* attribute setup *)
1.88
1.89  val case_prod_attr =
1.90    let
1.91 @@ -112,6 +113,6 @@
1.92    end
1.93
1.94  val setup =
1.95 - Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules"
1.96 +  Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
1.97
1.98 -end;
1.99 +end
```