author | haftmann |
Fri, 23 Feb 2007 08:39:28 +0100 | |
changeset 22355 | f9d35783d28d |
parent 20218 | be3bfb0699ba |
child 22568 | ed7aa5a350ef |
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'); |
|
20218
be3bfb0699ba
Variable.import(T): result includes fixed types/terms;
wenzelm
parents:
19905
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) |
|
19905 | 46 |
#> singleton (Variable.export ctxt' ctxt) |
19874 | 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'); |
|
20218
be3bfb0699ba
Variable.import(T): result includes fixed types/terms;
wenzelm
parents:
19905
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; |