src/Provers/project_rule.ML

Transform mutual rule into projection.

(*  Title:      Provers/project_rule.ML
    ID:         $Id$
    Author:     Makarius

Transform mutual rule:
  HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
into projection:
  xi:Ai ==> HH ==> Pi xi
*)

signature PROJECT_RULE_DATA =
sig
  val conjunct1: thm
  val conjunct2: thm
  val mp: thm
end;

signature PROJECT_RULE =
sig
  val project: thm -> int -> thm
  val projections: thm -> thm list
end;

functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
struct

fun conj1 th = th RS Data.conjunct1;
fun conj2 th = th RS Data.conjunct2;
fun imp th = th RS Data.mp;

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

fun project rule i =
  let
    fun proj 1 th = the_default th (try conj1 th)
      | proj k th = proj (k - 1) (conj2 th);
    fun prems k th =
      (case try imp th of
        NONE => (k, th)
      | SOME th' => prems (k + 1) th');
  in
    rule
    |> freeze
    |> proj i
    |> prems 0 |-> (fn k =>
      Thm.permute_prems 0 (~ k)
      #> Drule.standard'
      #> RuleCases.save rule
      #> RuleCases.add_consumes k)
  end;

fun projections rule =
  let
    fun projs k th =
      (case try conj2 th of
        NONE => k
      | SOME th' => projs (k + 1) th');
    val n = projs 1 (freeze rule);
  in map (project rule) (1 upto n) end;

end;