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');

19874

40 
val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;


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');

19874

60 
val ([rule], _) = ProofContext.import true [raw_rule] ctxt;


61 
in projects ctxt (1 upto projs 1 rule) raw_rule end;

18483

62 


63 
end;
