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