18483
|
1 |
(* Title: Provers/project_rule.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Transform mutual rule:
|
|
6 |
HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
|
|
7 |
into projection:
|
|
8 |
xi:Ai ==> HH ==> Pi xi
|
|
9 |
*)
|
|
10 |
|
|
11 |
signature PROJECT_RULE_DATA =
|
|
12 |
sig
|
|
13 |
val conjunct1: thm
|
|
14 |
val conjunct2: thm
|
|
15 |
val mp: thm
|
|
16 |
end;
|
|
17 |
|
|
18 |
signature PROJECT_RULE =
|
|
19 |
sig
|
19874
|
20 |
val project: Proof.context -> int -> thm -> thm
|
|
21 |
val projects: Proof.context -> int list -> thm -> thm list
|
|
22 |
val projections: Proof.context -> thm -> thm list
|
18483
|
23 |
end;
|
|
24 |
|
|
25 |
functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
|
|
26 |
struct
|
|
27 |
|
|
28 |
fun conj1 th = th RS Data.conjunct1;
|
|
29 |
fun conj2 th = th RS Data.conjunct2;
|
|
30 |
fun imp th = th RS Data.mp;
|
|
31 |
|
19874
|
32 |
fun projects ctxt is raw_rule =
|
18483
|
33 |
let
|
|
34 |
fun proj 1 th = the_default th (try conj1 th)
|
|
35 |
| proj k th = proj (k - 1) (conj2 th);
|
|
36 |
fun prems k th =
|
|
37 |
(case try imp th of
|
|
38 |
NONE => (k, th)
|
|
39 |
| SOME th' => prems (k + 1) th');
|
19874
|
40 |
val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
|
|
41 |
fun result i =
|
|
42 |
rule
|
|
43 |
|> proj i
|
|
44 |
|> prems 0 |-> (fn k =>
|
|
45 |
Thm.permute_prems 0 (~ k)
|
|
46 |
#> ProofContext.export ctxt' ctxt
|
|
47 |
#> Drule.zero_var_indexes
|
|
48 |
#> RuleCases.save raw_rule
|
|
49 |
#> RuleCases.add_consumes k);
|
|
50 |
in map result is end;
|
18483
|
51 |
|
19874
|
52 |
fun project ctxt i th = hd (projects ctxt [i] th);
|
|
53 |
|
|
54 |
fun projections ctxt raw_rule =
|
18483
|
55 |
let
|
|
56 |
fun projs k th =
|
|
57 |
(case try conj2 th of
|
|
58 |
NONE => k
|
|
59 |
| SOME th' => projs (k + 1) th');
|
19874
|
60 |
val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
|
|
61 |
in projects ctxt (1 upto projs 1 rule) raw_rule end;
|
18483
|
62 |
|
|
63 |
end;
|