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


20 
val project: thm > int > thm


21 
val projections: thm > thm list


22 
end;


23 


24 
functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =


25 
struct


26 


27 
fun conj1 th = th RS Data.conjunct1;


28 
fun conj2 th = th RS Data.conjunct2;


29 
fun imp th = th RS Data.mp;


30 


31 
val freeze = Drule.zero_var_indexes #> Drule.freeze_all;


32 


33 
fun project rule i =


34 
let


35 
fun proj 1 th = the_default th (try conj1 th)


36 
 proj k th = proj (k  1) (conj2 th);


37 
fun prems k th =


38 
(case try imp th of


39 
NONE => (k, th)


40 
 SOME th' => prems (k + 1) th');


41 
in


42 
rule


43 
> freeze


44 
> proj i


45 
> prems 0 > (fn k =>


46 
Thm.permute_prems 0 (~ k)


47 
#> Drule.standard'


48 
#> RuleCases.save rule


49 
#> RuleCases.add_consumes k)


50 
end;


51 


52 
fun projections rule =


53 
let


54 
fun projs k th =


55 
(case try conj2 th of


56 
NONE => k


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


58 
val n = projs 1 (freeze rule);


59 
in map (project rule) (1 upto n) end;


60 


61 
end;
