|
1 (* Title: case_product.ML |
|
2 Author: Lars Noschinski |
|
3 |
|
4 Combines two case rules into a single one. |
|
5 |
|
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 *) |
|
10 |
|
11 signature CASE_PRODUCT = |
|
12 sig |
|
13 |
|
14 val combine: Proof.context -> thm -> thm -> thm |
|
15 val combine_annotated: Proof.context -> thm -> thm -> thm |
|
16 val setup: theory -> theory |
|
17 end; |
|
18 |
|
19 structure Case_Product: CASE_PRODUCT = |
|
20 struct |
|
21 |
|
22 (*Instantiates the conclusion of thm2 to the one of thm1.*) |
|
23 fun inst_concl thm1 thm2 = |
|
24 let |
|
25 val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of |
|
26 in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end |
|
27 |
|
28 fun inst_thms thm1 thm2 ctxt = |
|
29 let |
|
30 val import = yield_singleton (apfst snd oo Variable.import true) |
|
31 val (i_thm1, ctxt') = import thm1 ctxt |
|
32 val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt' |
|
33 in ((i_thm1, i_thm2), ctxt'') end |
|
34 |
|
35 (* |
|
36 Returns list of prems, where loose bounds have been replaced by frees. |
|
37 FIXME: Focus |
|
38 *) |
|
39 fun free_prems t ctxt = |
|
40 let |
|
41 val bs = Term.strip_all_vars t |
|
42 val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt |
|
43 val subst = map Free (names ~~ map snd bs) |
|
44 val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t) |
|
45 in ((t', subst), ctxt') end |
|
46 |
|
47 fun build_concl_prems thm1 thm2 ctxt = |
|
48 let |
|
49 val concl = Thm.concl_of thm1 |
|
50 |
|
51 fun is_consumes t = not (Logic.strip_assums_concl t aconv concl) |
|
52 val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1) |
|
53 val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2) |
|
54 |
|
55 val p_cases_prod = map (fn p1 => map (fn p2 => |
|
56 let |
|
57 val (((t1, subst1), (t2, subst2)), _) = ctxt |
|
58 |> free_prems p1 ||>> free_prems p2 |
|
59 in |
|
60 Logic.list_implies (t1 @ t2, concl) |
|
61 |> fold_rev Logic.all (subst1 @ subst2) |
|
62 end |
|
63 ) p_cases2) p_cases1 |
|
64 |
|
65 val prems = p_cons1 :: p_cons2 :: p_cases_prod |
|
66 in |
|
67 (concl, prems) |
|
68 end |
|
69 |
|
70 fun case_product_tac prems struc thm1 thm2 = |
|
71 let |
|
72 val (p_cons1 :: p_cons2 :: premss) = unflat struc prems |
|
73 val thm2' = thm2 OF p_cons2 |
|
74 in |
|
75 (Tactic.rtac (thm1 OF p_cons1) |
|
76 THEN' EVERY' (map (fn p => |
|
77 Tactic.rtac thm2' |
|
78 THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss) |
|
79 ) |
|
80 end |
|
81 |
|
82 fun combine ctxt thm1 thm2 = |
|
83 let |
|
84 val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt |
|
85 val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt' |
|
86 in |
|
87 Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} => |
|
88 case_product_tac prems prems_rich i_thm1 i_thm2 1) |
|
89 |> singleton (Variable.export ctxt' ctxt) |
|
90 end; |
|
91 |
|
92 fun annotation thm1 thm2 = |
|
93 let |
|
94 val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1) |
|
95 val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2) |
|
96 val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2 |
|
97 in |
|
98 Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2) |
|
99 end |
|
100 |
|
101 fun combine_annotated ctxt thm1 thm2 = |
|
102 combine ctxt thm1 thm2 |
|
103 |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt) |
|
104 |
|
105 (* Attribute setup *) |
|
106 |
|
107 val case_prod_attr = let |
|
108 fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x) |
|
109 in |
|
110 Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm => |
|
111 combine_list (Context.proof_of ctxt) thms thm)) |
|
112 end |
|
113 |
|
114 val setup = |
|
115 Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules" |
|
116 |
|
117 end; |