author  wenzelm 
Thu, 15 Jun 2006 23:08:54 +0200  
changeset 19897  fe661eb3b0e7 
parent 19874  cc4b2b882e4c 
child 19905  7f480338b66e 
permissions  rwrr 
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; 