src/Pure/conv.ML
changeset 23596 f8381a95c49c
parent 23587 46d01f5e1e5b
child 23656 4bdcb024e95d
     1.1 --- a/src/Pure/conv.ML	Thu Jul 05 20:01:32 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu Jul 05 20:01:33 2007 +0200
     1.3 @@ -8,13 +8,10 @@
     1.4  infix 1 then_conv;
     1.5  infix 0 else_conv;
     1.6  
     1.7 -type conv = cterm -> thm;
     1.8 -
     1.9  signature CONV =
    1.10  sig
    1.11    val no_conv: conv
    1.12    val all_conv: conv
    1.13 -  val is_refl: thm -> bool
    1.14    val then_conv: conv * conv -> conv
    1.15    val else_conv: conv * conv -> conv
    1.16    val first_conv: conv list -> conv
    1.17 @@ -42,20 +39,16 @@
    1.18  
    1.19  (* conversionals *)
    1.20  
    1.21 -type conv = cterm -> thm;
    1.22 -
    1.23  fun no_conv _ = raise CTERM ("no conversion", []);
    1.24  val all_conv = Thm.reflexive;
    1.25  
    1.26 -val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    1.27 -
    1.28  fun (cv1 then_conv cv2) ct =
    1.29    let
    1.30      val eq1 = cv1 ct;
    1.31      val eq2 = cv2 (Thm.rhs_of eq1);
    1.32    in
    1.33 -    if is_refl eq1 then eq2
    1.34 -    else if is_refl eq2 then eq1
    1.35 +    if Thm.is_reflexive eq1 then eq2
    1.36 +    else if Thm.is_reflexive eq2 then eq1
    1.37      else Thm.transitive eq1 eq2
    1.38    end;
    1.39  
    1.40 @@ -92,8 +85,10 @@
    1.41  fun abs_conv cv ct =
    1.42    (case Thm.term_of ct of
    1.43      Abs (x, _, _) =>
    1.44 -      let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
    1.45 -      in Thm.abstract_rule x v (cv ct') end
    1.46 +      let
    1.47 +        val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct;
    1.48 +        val eq = cv ct';
    1.49 +      in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
    1.50    | _ => raise CTERM ("abs_conv", [ct]));
    1.51  
    1.52  fun combination_conv cv1 cv2 ct =
    1.53 @@ -113,18 +108,10 @@
    1.54  (* logic *)
    1.55  
    1.56  (*rewrite B in !!x1 ... xn. B*)
    1.57 -fun forall_conv 0 cv ct = cv ct
    1.58 -  | forall_conv n cv ct =
    1.59 -      (case try Thm.dest_comb ct of
    1.60 -        NONE => cv ct
    1.61 -      | SOME (A, B) =>
    1.62 -          (case (Thm.term_of A, Thm.term_of B) of
    1.63 -            (Const ("all", _), Abs (x, _, _)) =>
    1.64 -              let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
    1.65 -                Thm.combination (all_conv A)
    1.66 -                  (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
    1.67 -              end
    1.68 -          | _ => cv ct));
    1.69 +fun forall_conv n cv ct =
    1.70 +  if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
    1.71 +  then arg_conv (abs_conv (forall_conv (n - 1) cv)) ct
    1.72 +  else cv ct;
    1.73  
    1.74  (*rewrite B in A1 ==> ... ==> An ==> B*)
    1.75  fun concl_conv 0 cv ct = cv ct
    1.76 @@ -134,22 +121,30 @@
    1.77        | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
    1.78  
    1.79  (*rewrite the A's in A1 ==> ... ==> An ==> B*)
    1.80 -fun prems_conv 0 _ = all_conv
    1.81 -  | prems_conv n cv =
    1.82 -      let
    1.83 -        fun conv i ct =
    1.84 -          if i = n + 1 then all_conv ct
    1.85 -          else
    1.86 -            (case try Thm.dest_implies ct of
    1.87 -              NONE => all_conv ct
    1.88 -            | SOME (A, B) => Drule.imp_cong_rule (cv A) (conv (i + 1) B));
    1.89 -  in conv 1 end;
    1.90 +fun prems_conv 0 _ ct = all_conv ct
    1.91 +  | prems_conv n cv ct =
    1.92 +      (case try Thm.dest_implies ct of
    1.93 +        NONE => all_conv ct
    1.94 +      | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
    1.95 +
    1.96 +
    1.97 +(* conversions as rules *)
    1.98  
    1.99 -fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
   1.100 +(*forward conversion, cf. FCONV_RULE in LCF*)
   1.101 +fun fconv_rule cv th =
   1.102 +  let val eq = cv (Thm.cprop_of th) in
   1.103 +    if Thm.is_reflexive eq then th
   1.104 +    else Thm.equal_elim eq th
   1.105 +  end;
   1.106  
   1.107 -fun gconv_rule cv i = Drule.with_subgoal i (fn th =>
   1.108 -  (case try (Thm.dest_implies o Thm.cprop_of) th of
   1.109 -    SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th
   1.110 -  | NONE => raise THM ("gconv_rule", i, [th])));
   1.111 +(*goal conversion*)
   1.112 +fun gconv_rule cv i th =
   1.113 +  (case try (Thm.cprem_of th) i of
   1.114 +    SOME ct =>
   1.115 +      let val eq = cv ct in
   1.116 +        if Thm.is_reflexive eq then th
   1.117 +        else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
   1.118 +      end
   1.119 +  | NONE => raise THM ("gconv_rule", i, [th]));
   1.120  
   1.121  end;