author | wenzelm |
Thu, 15 Jun 2006 23:08:54 +0200 | |
changeset 19897 | fe661eb3b0e7 |
parent 19874 | cc4b2b882e4c |
child 19905 | 7f480338b66e |
permissions | -rw-r--r-- |
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'); |
|
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19874
diff
changeset
|
40 |
val ([rule], ctxt') = Variable.import true [raw_rule] ctxt; |
19874 | 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'); |
|
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19874
diff
changeset
|
60 |
val ([rule], _) = Variable.import true [raw_rule] ctxt; |
19874 | 61 |
in projects ctxt (1 upto projs 1 rule) raw_rule end; |
18483 | 62 |
|
63 |
end; |