# HG changeset patch
# User wenzelm
# Date 1183658493 -7200
# Node ID f8381a95c49c8c9d3e3c6dcea2ff13a731f39650
# Parent  7ca68a2c85751cb3870a0112f1a90219bb75beb0
moved type conv to thm.ML;
renamed Conv.is_refl to Thm.is_reflexive;
misc tuning of basic conversions;

diff -r 7ca68a2c8575 -r f8381a95c49c src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Jul 05 20:01:32 2007 +0200
+++ b/src/Pure/conv.ML	Thu Jul 05 20:01:33 2007 +0200
@@ -8,13 +8,10 @@
 infix 1 then_conv;
 infix 0 else_conv;
 
-type conv = cterm -> thm;
-
 signature CONV =
 sig
   val no_conv: conv
   val all_conv: conv
-  val is_refl: thm -> bool
   val then_conv: conv * conv -> conv
   val else_conv: conv * conv -> conv
   val first_conv: conv list -> conv
@@ -42,20 +39,16 @@
 
 (* conversionals *)
 
-type conv = cterm -> thm;
-
 fun no_conv _ = raise CTERM ("no conversion", []);
 val all_conv = Thm.reflexive;
 
-val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
-
 fun (cv1 then_conv cv2) ct =
   let
     val eq1 = cv1 ct;
     val eq2 = cv2 (Thm.rhs_of eq1);
   in
-    if is_refl eq1 then eq2
-    else if is_refl eq2 then eq1
+    if Thm.is_reflexive eq1 then eq2
+    else if Thm.is_reflexive eq2 then eq1
     else Thm.transitive eq1 eq2
   end;
 
@@ -92,8 +85,10 @@
 fun abs_conv cv ct =
   (case Thm.term_of ct of
     Abs (x, _, _) =>
-      let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
-      in Thm.abstract_rule x v (cv ct') end
+      let
+        val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct;
+        val eq = cv ct';
+      in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   | _ => raise CTERM ("abs_conv", [ct]));
 
 fun combination_conv cv1 cv2 ct =
@@ -113,18 +108,10 @@
 (* logic *)
 
 (*rewrite B in !!x1 ... xn. B*)
-fun forall_conv 0 cv ct = cv ct
-  | forall_conv n cv ct =
-      (case try Thm.dest_comb ct of
-        NONE => cv ct
-      | SOME (A, B) =>
-          (case (Thm.term_of A, Thm.term_of B) of
-            (Const ("all", _), Abs (x, _, _)) =>
-              let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
-                Thm.combination (all_conv A)
-                  (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
-              end
-          | _ => cv ct));
+fun forall_conv n cv ct =
+  if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
+  then arg_conv (abs_conv (forall_conv (n - 1) cv)) ct
+  else cv ct;
 
 (*rewrite B in A1 ==> ... ==> An ==> B*)
 fun concl_conv 0 cv ct = cv ct
@@ -134,22 +121,30 @@
       | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
 
 (*rewrite the A's in A1 ==> ... ==> An ==> B*)
-fun prems_conv 0 _ = all_conv
-  | prems_conv n cv =
-      let
-        fun conv i ct =
-          if i = n + 1 then all_conv ct
-          else
-            (case try Thm.dest_implies ct of
-              NONE => all_conv ct
-            | SOME (A, B) => Drule.imp_cong_rule (cv A) (conv (i + 1) B));
-  in conv 1 end;
+fun prems_conv 0 _ ct = all_conv ct
+  | prems_conv n cv ct =
+      (case try Thm.dest_implies ct of
+        NONE => all_conv ct
+      | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
+
+
+(* conversions as rules *)
 
-fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
+(*forward conversion, cf. FCONV_RULE in LCF*)
+fun fconv_rule cv th =
+  let val eq = cv (Thm.cprop_of th) in
+    if Thm.is_reflexive eq then th
+    else Thm.equal_elim eq th
+  end;
 
-fun gconv_rule cv i = Drule.with_subgoal i (fn th =>
-  (case try (Thm.dest_implies o Thm.cprop_of) th of
-    SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th
-  | NONE => raise THM ("gconv_rule", i, [th])));
+(*goal conversion*)
+fun gconv_rule cv i th =
+  (case try (Thm.cprem_of th) i of
+    SOME ct =>
+      let val eq = cv ct in
+        if Thm.is_reflexive eq then th
+        else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
+      end
+  | NONE => raise THM ("gconv_rule", i, [th]));
 
 end;