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