author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 33368  b1cf34f1855c 
permissions  rwrr 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
22568
diff
changeset

1 
(* Title: Tools/project_rule.ML 
18483  2 
Author: Makarius 
3 

4 
Transform mutual rule: 

30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
22568
diff
changeset

5 

18483  6 
HH ==> (x1:A1 > P1 x1) & ... & (xn:An > Pn xn) 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
22568
diff
changeset

7 

18483  8 
into projection: 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
22568
diff
changeset

9 

18483  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 

19874  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 

18483  25 
end; 
26 

32172  27 
functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE = 
18483  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 

19874  34 
fun projects ctxt is raw_rule = 
18483  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'); 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30160
diff
changeset

42 
val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt; 
19874  43 
fun result i = 
44 
rule 

45 
> proj i 

46 
> prems 0 > (fn k => 

47 
Thm.permute_prems 0 (~ k) 

19905  48 
#> singleton (Variable.export ctxt' ctxt) 
19874  49 
#> Drule.zero_var_indexes 
33368  50 
#> Rule_Cases.save raw_rule 
51 
#> Rule_Cases.add_consumes k); 

19874  52 
in map result is end; 
18483  53 

19874  54 
fun project ctxt i th = hd (projects ctxt [i] th); 
55 

56 
fun projections ctxt raw_rule = 

18483  57 
let 
58 
fun projs k th = 

59 
(case try conj2 th of 

60 
NONE => k 

61 
 SOME th' => projs (k + 1) th'); 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30160
diff
changeset

62 
val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt; 
19874  63 
in projects ctxt (1 upto projs 1 rule) raw_rule end; 
18483  64 

65 
end; 