src/Pure/conv.ML
changeset 22905 dab6a898b47c
child 22926 fb6917e426da
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/conv.ML	Thu May 10 00:39:51 2007 +0200
     1.3 @@ -0,0 +1,95 @@
     1.4 +(*  Title:      Pure/conv.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb and Makarius
     1.7 +
     1.8 +Conversions: primitive equality reasoning.
     1.9 +*)
    1.10 +
    1.11 +infix 1 AND;
    1.12 +infix 0 OR;
    1.13 +
    1.14 +signature CONV =
    1.15 +sig
    1.16 +  type conv = cterm -> thm
    1.17 +  val no_conv: conv
    1.18 +  val all_conv: conv
    1.19 +  val option_conv: conv -> cterm -> thm option
    1.20 +  val AND: conv * conv -> conv
    1.21 +  val OR: conv * conv -> conv
    1.22 +  val forall_conv: int -> conv -> conv
    1.23 +  val concl_conv: int -> conv -> conv
    1.24 +  val prems_conv: int -> (int -> conv) -> conv
    1.25 +  val goals_conv: (int -> bool) -> conv -> conv
    1.26 +  val fconv_rule: conv -> thm -> thm
    1.27 +end;
    1.28 +
    1.29 +structure Conv: CONV =
    1.30 +struct
    1.31 +
    1.32 +(* conversionals *)
    1.33 +
    1.34 +type conv = cterm -> thm
    1.35 +
    1.36 +fun no_conv _ = raise CTERM ("no conversion", []);
    1.37 +val all_conv = Thm.reflexive;
    1.38 +
    1.39 +val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    1.40 +
    1.41 +fun option_conv conv ct =
    1.42 +  (case try conv ct of
    1.43 +    NONE => NONE
    1.44 +  | SOME eq => if is_refl eq then NONE else SOME eq);
    1.45 +
    1.46 +fun (conv1 AND conv2) ct =
    1.47 +  let
    1.48 +    val eq1 = conv1 ct;
    1.49 +    val eq2 = conv2 (Thm.rhs_of eq1);
    1.50 +  in
    1.51 +    if is_refl eq1 then eq2
    1.52 +    else if is_refl eq2 then eq1
    1.53 +    else Thm.transitive eq1 eq2
    1.54 +  end;
    1.55 +
    1.56 +fun (conv1 OR conv2) ct =
    1.57 +  (case try conv1 ct of SOME eq => eq | NONE => conv2 ct);
    1.58 +
    1.59 +
    1.60 +(* Pure conversions *)
    1.61 +
    1.62 +(*rewrite B in !!x1 ... xn. B*)
    1.63 +fun forall_conv 0 cv ct = cv ct
    1.64 +  | forall_conv n cv ct =
    1.65 +      (case try Thm.dest_comb ct of
    1.66 +        NONE => cv ct
    1.67 +      | SOME (A, B) =>
    1.68 +          (case (term_of A, term_of B) of
    1.69 +            (Const ("all", _), Abs (x, _, _)) =>
    1.70 +              let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
    1.71 +                Thm.combination (Thm.reflexive A)
    1.72 +                  (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
    1.73 +              end
    1.74 +          | _ => cv ct));
    1.75 +
    1.76 +(*rewrite B in A1 ==> ... ==> An ==> B*)
    1.77 +fun concl_conv 0 cv ct = cv ct
    1.78 +  | concl_conv n cv ct =
    1.79 +      (case try Thm.dest_implies ct of
    1.80 +        NONE => cv ct
    1.81 +      | SOME (A, B) => Drule.imp_cong_rule (reflexive A) (concl_conv (n - 1) cv B));
    1.82 +
    1.83 +(*rewrite the A's in A1 ==> ... ==> An ==> B*)
    1.84 +fun prems_conv 0 _ = reflexive
    1.85 +  | prems_conv n cv =
    1.86 +      let
    1.87 +        fun conv i ct =
    1.88 +          if i = n + 1 then reflexive ct
    1.89 +          else
    1.90 +            (case try Thm.dest_implies ct of
    1.91 +              NONE => reflexive ct
    1.92 +            | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
    1.93 +  in conv 1 end;
    1.94 +
    1.95 +fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
    1.96 +fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.97 +
    1.98 +end;