author  wenzelm 
Wed, 26 Jul 2006 19:37:41 +0200  
changeset 20218  be3bfb0699ba 
parent 19905  7f480338b66e 
child 22568  ed7aa5a350ef 
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'); 

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; 