1.1 --- a/src/Pure/conv.ML Thu Oct 04 16:59:29 2007 +0200
1.2 +++ b/src/Pure/conv.ML Thu Oct 04 16:59:30 2007 +0200
1.3 @@ -18,8 +18,7 @@
1.4 val every_conv: conv list -> conv
1.5 val try_conv: conv -> conv
1.6 val repeat_conv: conv -> conv
1.7 - val cache_conv: conv -> conv
1.8 - val abs_conv: conv -> conv
1.9 + val abs_conv: (Proof.context -> conv) -> Proof.context -> conv
1.10 val combination_conv: conv -> conv -> conv
1.11 val comb_conv: conv -> conv
1.12 val arg_conv: conv -> conv
1.13 @@ -27,7 +26,7 @@
1.14 val arg1_conv: conv -> conv
1.15 val fun2_conv: conv -> conv
1.16 val binop_conv: conv -> conv
1.17 - val forall_conv: int -> conv -> conv
1.18 + val forall_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
1.19 val concl_conv: int -> conv -> conv
1.20 val prems_conv: int -> conv -> conv
1.21 val fconv_rule: conv -> thm -> thm
1.22 @@ -65,29 +64,19 @@
1.23 fun try_conv cv = cv else_conv all_conv;
1.24 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
1.25
1.26 -fun cache_conv cv =
1.27 - let
1.28 - val cache = ref Termtab.empty;
1.29 - fun conv ct =
1.30 - (case Termtab.lookup (! cache) (Thm.term_of ct) of
1.31 - SOME th => th
1.32 - | NONE =>
1.33 - let val th = cv ct
1.34 - in change cache (Termtab.update (Thm.term_of ct, th)); th end);
1.35 - in conv end;
1.36 -
1.37
1.38
1.39 (** Pure conversions **)
1.40
1.41 (* lambda terms *)
1.42
1.43 -fun abs_conv cv ct =
1.44 +fun abs_conv cv ctxt ct =
1.45 (case Thm.term_of ct of
1.46 Abs (x, _, _) =>
1.47 let
1.48 - val (v, ct') = Thm.dest_abs (SOME (gensym "gensym_abs_")) ct;
1.49 - val eq = cv ct';
1.50 + val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
1.51 + val (v, ct') = Thm.dest_abs (SOME u) ct;
1.52 + val eq = (cv ctxt') ct';
1.53 in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
1.54 | _ => raise CTERM ("abs_conv", [ct]));
1.55
1.56 @@ -108,10 +97,10 @@
1.57 (* logic *)
1.58
1.59 (*rewrite B in !!x1 ... xn. B*)
1.60 -fun forall_conv n cv ct =
1.61 +fun forall_conv n cv ctxt ct =
1.62 if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
1.63 - then arg_conv (abs_conv (forall_conv (n - 1) cv)) ct
1.64 - else cv ct;
1.65 + then arg_conv (abs_conv (forall_conv (n - 1) cv) ctxt) ct
1.66 + else cv ctxt ct;
1.67
1.68 (*rewrite B in A1 ==> ... ==> An ==> B*)
1.69 fun concl_conv 0 cv ct = cv ct