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