author | haftmann |
Tue, 09 Apr 2019 16:59:00 +0000 | |
changeset 70093 | e38900000009 |
parent 67522 | 9e712280cc37 |
permissions | -rw-r--r-- |
41883 | 1 |
(* Title: Tools/case_product.ML |
2 |
Author: Lars Noschinski, TU Muenchen |
|
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
3 |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
4 |
Combine two case rules into a single one. |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
5 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
6 |
Assumes that the theorems are of the form |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
7 |
"[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P" |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
8 |
where m is given by the "consumes" attribute of the theorem. |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
9 |
*) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
10 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
11 |
signature CASE_PRODUCT = |
41883 | 12 |
sig |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
13 |
val combine: Proof.context -> thm -> thm -> thm |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
14 |
val combine_annotated: Proof.context -> thm -> thm -> thm |
58826 | 15 |
val annotation: thm -> thm -> attribute |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
16 |
end |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
17 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
18 |
structure Case_Product: CASE_PRODUCT = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
19 |
struct |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
20 |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
21 |
(*instantiate the conclusion of thm2 to the one of thm1*) |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
22 |
fun inst_concl thm1 thm2 = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
23 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
24 |
val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
25 |
in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
26 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
27 |
fun inst_thms thm1 thm2 ctxt = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
28 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
29 |
val import = yield_singleton (apfst snd oo Variable.import true) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
30 |
val (i_thm1, ctxt') = import thm1 ctxt |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
31 |
val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt' |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
32 |
in ((i_thm1, i_thm2), ctxt'') end |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
33 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
34 |
(* |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
35 |
Return list of prems, where loose bounds have been replaced by frees. |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
36 |
FIXME: Focus |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
37 |
*) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
38 |
fun free_prems t ctxt = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
39 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
40 |
val bs = Term.strip_all_vars t |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
41 |
val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
42 |
val subst = map Free (names ~~ map snd bs) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
43 |
val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
44 |
in ((t', subst), ctxt') end |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
45 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
46 |
fun build_concl_prems thm1 thm2 ctxt = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
47 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
48 |
val concl = Thm.concl_of thm1 |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
49 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
50 |
fun is_consumes t = not (Logic.strip_assums_concl t aconv concl) |
67522 | 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) |
|
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
53 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
54 |
val p_cases_prod = map (fn p1 => map (fn p2 => |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
55 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
56 |
val (((t1, subst1), (t2, subst2)), _) = ctxt |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
57 |
|> free_prems p1 ||>> free_prems p2 |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
58 |
in |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
59 |
Logic.list_implies (t1 @ t2, concl) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
60 |
|> fold_rev Logic.all (subst1 @ subst2) |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
61 |
end) p_cases2) p_cases1 |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
62 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
63 |
val prems = p_cons1 :: p_cons2 :: p_cases_prod |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
64 |
in |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
65 |
(concl, prems) |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
66 |
end |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
67 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
68 |
fun case_product_tac ctxt prems struc thm1 thm2 = |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
69 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
70 |
val (p_cons1 :: p_cons2 :: premss) = unflat struc prems |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
71 |
val thm2' = thm2 OF p_cons2 |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
72 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
73 |
resolve_tac ctxt [thm1 OF p_cons1] |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
74 |
THEN' EVERY' (map (fn p => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
75 |
resolve_tac ctxt [thm2'] THEN' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
76 |
EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss) |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
77 |
end |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
78 |
|
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
79 |
fun combine ctxt thm1 thm2 = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
80 |
let |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
81 |
val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
82 |
val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt' |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
83 |
in |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
84 |
Goal.prove ctxt' [] (flat prems_rich) concl |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
85 |
(fn {context = ctxt'', prems} => |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
86 |
case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1) |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
87 |
|> singleton (Variable.export ctxt' ctxt) |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
88 |
end |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
89 |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
90 |
fun annotation_rule thm1 thm2 = |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
91 |
let |
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42361
diff
changeset
|
92 |
val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1) |
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42361
diff
changeset
|
93 |
val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2) |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
94 |
val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2 |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
95 |
in |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
96 |
Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2)) |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
97 |
end |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
98 |
|
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
59498
diff
changeset
|
99 |
fun annotation thm1 thm2 = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
59498
diff
changeset
|
100 |
Thm.rule_attribute [thm1, thm2] (K (annotation_rule thm1 thm2)) |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
101 |
|
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
102 |
fun combine_annotated ctxt thm1 thm2 = |
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
103 |
combine ctxt thm1 thm2 |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
104 |
|> annotation_rule thm1 thm2 |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
105 |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
106 |
|
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
107 |
(* attribute setup *) |
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
108 |
|
58826 | 109 |
val _ = |
110 |
Theory.setup |
|
67149 | 111 |
(Attrib.setup \<^binding>\<open>case_product\<close> |
58826 | 112 |
let |
113 |
fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x) |
|
114 |
in |
|
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
59498
diff
changeset
|
115 |
Attrib.thms >> (fn thms => Thm.rule_attribute thms (fn ctxt => fn thm => |
58826 | 116 |
combine_list (Context.proof_of ctxt) thms thm)) |
117 |
end |
|
118 |
"product with other case rules") |
|
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset
|
119 |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset
|
120 |
end |