src/Provers/project_rule.ML

+(*  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;