# HG changeset patch
# User wenzelm
# Date 1207596322 -7200
# Node ID 114da911bc41372a0c6496d216205dde3afa6edf
# Parent  dbc458262f4ce55c53cf61b9595b303f003e5181
abs_conv: extra argument for bound variable;
renamed iterated forall_conv to params_conv;
added forall_conv, implies_conv, implies_concl_conv, rewr_conv;

diff -r dbc458262f4c -r 114da911bc41 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Mon Apr 07 21:25:21 2008 +0200
+++ b/src/Pure/conv.ML	Mon Apr 07 21:25:22 2008 +0200
@@ -18,7 +18,7 @@
   val every_conv: conv list -> conv
   val try_conv: conv -> conv
   val repeat_conv: conv -> conv
-  val abs_conv: (Proof.context -> conv) -> Proof.context -> conv
+  val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val combination_conv: conv -> conv -> conv
   val comb_conv: conv -> conv
   val arg_conv: conv -> conv
@@ -26,9 +26,13 @@
   val arg1_conv: conv -> conv
   val fun2_conv: conv -> conv
   val binop_conv: conv -> conv
-  val forall_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
+  val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
+  val implies_conv: conv -> conv -> conv
+  val implies_concl_conv: conv -> conv
+  val rewr_conv: thm -> conv
+  val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
+  val prems_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
-  val prems_conv: int -> conv -> conv
   val fconv_rule: conv -> thm -> thm
   val gconv_rule: conv -> int -> thm -> thm
 end;
@@ -76,7 +80,7 @@
       let
         val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
         val (v, ct') = Thm.dest_abs (SOME u) ct;
-        val eq = cv ctxt' ct';
+        val eq = cv (v, ctxt') ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   | _ => raise CTERM ("abs_conv", [ct]));
 
@@ -94,14 +98,52 @@
 fun binop_conv cv = combination_conv (arg_conv cv) cv;
 
 
-(* logic *)
+(* primitive logic *)
+
+fun forall_conv cv ctxt ct =
+  (case Thm.term_of ct of
+    Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
+  | _ => raise CTERM ("forall_conv", [ct]));
+
+fun implies_conv cv1 cv2 ct =
+  (case Thm.term_of ct of
+    Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
+  | _ => raise CTERM ("implies_conv", [ct]));
+
+fun implies_concl_conv cv ct =
+  (case Thm.term_of ct of
+    Const ("==>", _) $ _ $ _ => arg_conv cv ct
+  | _ => raise CTERM ("implies_concl_conv", [ct]));
+
+
+(* single rewrite step, cf. REWR_CONV in HOL *)
+
+fun rewr_conv rule ct =
+  let
+    val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+    val lhs = Thm.lhs_of rule1;
+    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
+  in
+    Drule.instantiate (Thm.match (lhs, ct)) rule2
+      handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
+  end;
+
+
+(* conversions on HHF rules *)
 
 (*rewrite B in !!x1 ... xn. B*)
-fun forall_conv n cv ctxt ct =
+fun params_conv n cv ctxt ct =
   if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
-  then arg_conv (abs_conv (forall_conv (n - 1) cv) ctxt) ct
+  then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   else cv ctxt ct;
 
+(*rewrite the A's in A1 ==> ... ==> An ==> B*)
+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));
+
 (*rewrite B in A1 ==> ... ==> An ==> B*)
 fun concl_conv 0 cv ct = cv ct
   | concl_conv n cv ct =
@@ -109,15 +151,8 @@
         NONE => cv ct
       | 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 _ 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 *)
+(* conversions as inference rules *)
 
 (*forward conversion, cf. FCONV_RULE in LCF*)
 fun fconv_rule cv th =