# HG changeset patch
# User berghofe
# Date 1012652811 -3600
# Node ID c00df77656561385fda2e131493215ceb479b89a
# Parent  6b3484b8d5725f68738ce2d29701baae62dd0f21
Rewrite procedure now works for both compact and full proof objects.

diff -r 6b3484b8d572 -r c00df7765656 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jan 30 14:05:29 2002 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Feb 02 13:26:51 2002 +0100
@@ -9,7 +9,8 @@
 
 signature PROOF_REWRITE_RULES =
 sig
-  val rprocs : (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
+  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
+  val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
   val setup : (theory -> theory) list
 end;
 
@@ -18,100 +19,159 @@
 
 open Proofterm;
 
-fun rew _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
-      (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-      (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
-  | rew _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-      (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
-          Some (equal_intr_axm % B % A %% prf2 %% prf1)
+fun rew b =
+  let
+    fun ? x = if b then Some x else None;
+    fun ax (prf as PAxm (s, prop, _)) Ts =
+      if b then PAxm (s, prop, Some Ts) else prf;
+    fun ty T = if b then
+        let val Type (_, [Type (_, [U, _]), _]) = T
+        in Some T end
+      else None;
+    val equal_intr_axm = ax equal_intr_axm [];
+    val equal_elim_axm = ax equal_elim_axm [];
+    val symmetric_axm = ax symmetric_axm [propT];
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
-      (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
-        _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
-      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
-      Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
+    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
+        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
+      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
+            Some (equal_intr_axm % B % A %% prf2 %% prf1)
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
-      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
         (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
-           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
-      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
-      Some (tg %> B %% (equal_elim_axm %> A %> B %%
-        (symmetric_axm % None % None %% prf1) %% prf2))
+          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
+        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
+        Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
-      (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
-        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
-           (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
-      let
-        val _ $ A $ C = Envir.beta_norm X;
-        val _ $ B $ D = Envir.beta_norm Y
-      in Some (AbsP ("H1", None, AbsP ("H2", None,
-        equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
-          (PBound 1 %% (equal_elim_axm %> B %> A %%
-            (symmetric_axm % None % None %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
-      end
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
+             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
+        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
+        Some (tg %> B %% (equal_elim_axm %> A %> B %%
+          (symmetric_axm % ? B % ? A %% prf1) %% prf2))
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
-      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
         (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
           (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
-             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
-      let
-        val _ $ A $ C = Envir.beta_norm Y;
-        val _ $ B $ D = Envir.beta_norm X
-      in Some (AbsP ("H1", None, AbsP ("H2", None,
-        equal_elim_axm %> D %> C %%
-          (symmetric_axm % None % None %% incr_pboundvars 2 0 prf2)
-            %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
-      end
+             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
+        let
+          val _ $ A $ C = Envir.beta_norm X;
+          val _ $ B $ D = Envir.beta_norm Y
+        in Some (AbsP ("H1", ? X, AbsP ("H2", ? B,
+          equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
+            (PBound 1 %% (equal_elim_axm %> B %> A %%
+              (symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
+        end
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
-      (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
-        (PAxm ("ProtoPure.reflexive", _, _) % _) %%
-          (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
-      let
-        val _ $ P = Envir.beta_norm X;
-        val _ $ Q = Envir.beta_norm Y;
-      in Some (AbsP ("H", None, Abst ("x", None,
-          equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
-            (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
-      end
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
+            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
+               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
+        let
+          val _ $ A $ C = Envir.beta_norm Y;
+          val _ $ B $ D = Envir.beta_norm X
+        in Some (AbsP ("H1", ? X, AbsP ("H2", ? A,
+          equal_elim_axm %> D %> C %%
+            (symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
+              %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
+        end
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
-      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
         (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
           (PAxm ("ProtoPure.reflexive", _, _) % _) %%
-            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
-      let
-        val _ $ P = Envir.beta_norm X;
-        val _ $ Q = Envir.beta_norm Y;
-      in Some (AbsP ("H", None, Abst ("x", None,
-        equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
-          (symmetric_axm % None % None %% (incr_pboundvars 1 1 prf %> Bound 0))
-            %% (PBound 0 %> Bound 0))))
-      end
+            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
+        let
+          val Const (_, T) $ P = Envir.beta_norm X;
+          val _ $ Q = Envir.beta_norm Y;
+        in Some (AbsP ("H", ? X, Abst ("x", ty T,
+            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
+              (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
+        end
+
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
+          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
+            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
+              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
+        let
+          val Const (_, T) $ P = Envir.beta_norm X;
+          val _ $ Q = Envir.beta_norm Y;
+          val t = incr_boundvars 1 P $ Bound 0;
+          val u = incr_boundvars 1 Q $ Bound 0
+        in Some (AbsP ("H", ? X, Abst ("x", ty T,
+          equal_elim_axm %> t %> u %%
+            (symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
+              %% (PBound 0 %> Bound 0))))
+        end
+
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
+        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
+           Some (equal_elim_axm %> B %> C %% prf2 %%
+             (equal_elim_axm %> A %> B %% prf1 %% prf3))
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+          (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
+           Some (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
+             (equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))
+
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
+
+      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = Some prf
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
-      (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
-         Some (equal_elim_axm %> B %> C %% prf2 %%
-           (equal_elim_axm %> A %> B %% prf1 %% prf3))
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
-      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
-         Some (equal_elim_axm %> B %> C %% (symmetric_axm % None % None %% prf1) %%
-           (equal_elim_axm %> A %> B %% (symmetric_axm % None % None %% prf2) %% prf3))
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
+          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
+            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
+              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
+          Some (equal_elim_axm %> C %> D %% prf2 %%
+            (equal_elim_axm %> A %> C %% prf3 %%
+              (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))
+
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
+            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
+              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
+                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
+          Some (equal_elim_axm %> A %> B %% prf1 %%
+            (equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
+              (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))
 
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-      (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
-  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
-      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
-        (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
+          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
+              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
+                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
+          Some (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
+            (equal_elim_axm %> B %> D %% prf3 %%
+              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
 
-  | rew _ _ = None;
+      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
+            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
+                (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
+                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
+          Some (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
+            (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
+              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
 
-val rprocs = [("Pure/meta_equality", rew)];
-val setup = [Proofterm.add_prf_rprocs rprocs];
+      | rew' _ _ = None;
+  in rew' end;
+
+fun rprocs b = [("Pure/meta_equality", rew b)];
+val setup = [Proofterm.add_prf_rprocs (rprocs false)];
 
 end;