wenzelm@41883: (*  Title:      Tools/case_product.ML
wenzelm@41883:     Author:     Lars Noschinski, TU Muenchen
noschinl@41826: 
wenzelm@45375: Combine two case rules into a single one.
noschinl@41826: 
noschinl@41826: Assumes that the theorems are of the form
noschinl@41826:   "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
noschinl@41826: where m is given by the "consumes" attribute of the theorem.
noschinl@41826: *)
noschinl@41826: 
noschinl@41826: signature CASE_PRODUCT =
wenzelm@41883: sig
noschinl@41826:   val combine: Proof.context -> thm -> thm -> thm
noschinl@41826:   val combine_annotated: Proof.context -> thm -> thm -> thm
wenzelm@58826:   val annotation: thm -> thm -> attribute
wenzelm@45375: end
noschinl@41826: 
noschinl@41826: structure Case_Product: CASE_PRODUCT =
noschinl@41826: struct
noschinl@41826: 
wenzelm@45375: (*instantiate the conclusion of thm2 to the one of thm1*)
noschinl@41826: fun inst_concl thm1 thm2 =
noschinl@41826:   let
noschinl@41826:     val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
noschinl@41826:   in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end
noschinl@41826: 
noschinl@41826: fun inst_thms thm1 thm2 ctxt =
noschinl@41826:   let
noschinl@41826:     val import = yield_singleton (apfst snd oo Variable.import true)
noschinl@41826:     val (i_thm1, ctxt') = import thm1 ctxt
noschinl@41826:     val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt'
noschinl@41826:   in ((i_thm1, i_thm2), ctxt'') end
noschinl@41826: 
noschinl@41826: (*
wenzelm@45375: Return list of prems, where loose bounds have been replaced by frees.
noschinl@41826: FIXME: Focus
noschinl@41826: *)
noschinl@41826: fun free_prems t ctxt =
noschinl@41826:   let
noschinl@41826:     val bs = Term.strip_all_vars t
noschinl@41826:     val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt
noschinl@41826:     val subst = map Free (names ~~ map snd bs)
noschinl@41826:     val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t)
noschinl@41826:   in ((t', subst), ctxt') end
noschinl@41826: 
noschinl@41826: fun build_concl_prems thm1 thm2 ctxt =
noschinl@41826:   let
noschinl@41826:     val concl = Thm.concl_of thm1
noschinl@41826: 
noschinl@41826:     fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
wenzelm@48902:     val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
wenzelm@48902:     val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
noschinl@41826: 
noschinl@41826:     val p_cases_prod = map (fn p1 => map (fn p2 =>
noschinl@41826:       let
noschinl@41826:         val (((t1, subst1), (t2, subst2)), _) = ctxt
noschinl@41826:           |> free_prems p1 ||>> free_prems p2
noschinl@41826:       in
noschinl@41826:         Logic.list_implies (t1 @ t2, concl)
noschinl@41826:         |> fold_rev Logic.all (subst1 @ subst2)
wenzelm@45375:       end) p_cases2) p_cases1
noschinl@41826: 
noschinl@41826:     val prems = p_cons1 :: p_cons2 :: p_cases_prod
noschinl@41826:   in
noschinl@41826:     (concl, prems)
noschinl@41826:   end
noschinl@41826: 
wenzelm@54742: fun case_product_tac ctxt prems struc thm1 thm2 =
noschinl@41826:   let
noschinl@41826:     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
noschinl@41826:     val thm2' = thm2 OF p_cons2
noschinl@41826:   in
wenzelm@58838:     resolve_tac [thm1 OF p_cons1]
noschinl@41826:      THEN' EVERY' (map (fn p =>
wenzelm@58838:        resolve_tac [thm2'] THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
noschinl@41826:   end
noschinl@41826: 
noschinl@41826: fun combine ctxt thm1 thm2 =
noschinl@41826:   let
noschinl@41826:     val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
noschinl@41826:     val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
noschinl@41826:   in
wenzelm@54742:     Goal.prove ctxt' [] (flat prems_rich) concl
wenzelm@54742:       (fn {context = ctxt'', prems} =>
wenzelm@54742:         case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1)
noschinl@41826:     |> singleton (Variable.export ctxt' ctxt)
wenzelm@45375:   end
noschinl@41826: 
wenzelm@45375: fun annotation_rule thm1 thm2 =
noschinl@41826:   let
nipkow@44045:     val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
nipkow@44045:     val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
wenzelm@45375:     val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2
noschinl@41826:   in
wenzelm@45375:     Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
noschinl@41826:   end
noschinl@41826: 
wenzelm@45375: fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
wenzelm@45375: 
noschinl@41826: fun combine_annotated ctxt thm1 thm2 =
noschinl@41826:   combine ctxt thm1 thm2
wenzelm@45375:   |> annotation_rule thm1 thm2
noschinl@41826: 
wenzelm@45375: 
wenzelm@45375: (* attribute setup *)
noschinl@41826: 
wenzelm@58826: val _ =
wenzelm@58826:   Theory.setup
wenzelm@58826:    (Attrib.setup @{binding case_product}
wenzelm@58826:       let
wenzelm@58826:         fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
wenzelm@58826:       in
wenzelm@58826:         Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
wenzelm@58826:           combine_list (Context.proof_of ctxt) thms thm))
wenzelm@58826:       end
wenzelm@58826:     "product with other case rules")
noschinl@41826: 
wenzelm@45375: end