more conversions;
authorwenzelm
Thu May 10 18:10:32 2007 +0200 (2007-05-10)
changeset 22926fb6917e426da
parent 22925 86b4a7d04d43
child 22927 0b53bd36258b
more conversions;
tuned;
src/Pure/conv.ML
     1.1 --- a/src/Pure/conv.ML	Thu May 10 15:51:59 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu May 10 18:10:32 2007 +0200
     1.3 @@ -5,17 +5,28 @@
     1.4  Conversions: primitive equality reasoning.
     1.5  *)
     1.6  
     1.7 -infix 1 AND;
     1.8 -infix 0 OR;
     1.9 +infix 1 thenc;
    1.10 +infix 0 orelsec;
    1.11  
    1.12  signature CONV =
    1.13  sig
    1.14    type conv = cterm -> thm
    1.15    val no_conv: conv
    1.16    val all_conv: conv
    1.17 -  val option_conv: conv -> cterm -> thm option
    1.18 -  val AND: conv * conv -> conv
    1.19 -  val OR: conv * conv -> conv
    1.20 +  val thenc: conv * conv -> conv
    1.21 +  val orelsec: conv * conv -> conv
    1.22 +  val first_conv: conv list -> conv
    1.23 +  val every_conv: conv list -> conv
    1.24 +  val tryc: conv -> conv
    1.25 +  val repeatc: conv -> conv
    1.26 +  val cache_conv: conv -> conv
    1.27 +  val abs_conv: conv -> conv
    1.28 +  val combination_conv: conv -> conv -> conv
    1.29 +  val comb_conv: conv -> conv
    1.30 +  val arg_conv: conv -> conv
    1.31 +  val fun_conv: conv -> conv
    1.32 +  val arg1_conv: conv -> conv
    1.33 +  val fun2_conv: conv -> conv
    1.34    val forall_conv: int -> conv -> conv
    1.35    val concl_conv: int -> conv -> conv
    1.36    val prems_conv: int -> (int -> conv) -> conv
    1.37 @@ -28,33 +39,69 @@
    1.38  
    1.39  (* conversionals *)
    1.40  
    1.41 -type conv = cterm -> thm
    1.42 +type conv = cterm -> thm;
    1.43  
    1.44  fun no_conv _ = raise CTERM ("no conversion", []);
    1.45  val all_conv = Thm.reflexive;
    1.46  
    1.47  val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    1.48  
    1.49 -fun option_conv conv ct =
    1.50 -  (case try conv ct of
    1.51 -    NONE => NONE
    1.52 -  | SOME eq => if is_refl eq then NONE else SOME eq);
    1.53 -
    1.54 -fun (conv1 AND conv2) ct =
    1.55 +fun (cv1 thenc cv2) ct =
    1.56    let
    1.57 -    val eq1 = conv1 ct;
    1.58 -    val eq2 = conv2 (Thm.rhs_of eq1);
    1.59 +    val eq1 = cv1 ct;
    1.60 +    val eq2 = cv2 (Thm.rhs_of eq1);
    1.61    in
    1.62      if is_refl eq1 then eq2
    1.63      else if is_refl eq2 then eq1
    1.64      else Thm.transitive eq1 eq2
    1.65    end;
    1.66  
    1.67 -fun (conv1 OR conv2) ct =
    1.68 -  (case try conv1 ct of SOME eq => eq | NONE => conv2 ct);
    1.69 +fun (cv1 orelsec cv2) ct =
    1.70 +  (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
    1.71 +
    1.72 +fun first_conv cvs = fold_rev (curry op orelsec) cvs no_conv;
    1.73 +fun every_conv cvs = fold_rev (curry op thenc) cvs all_conv;
    1.74 +
    1.75 +fun tryc cv = cv orelsec all_conv;
    1.76 +fun repeatc cv ct = tryc (cv thenc repeatc cv) ct;
    1.77 +
    1.78 +fun cache_conv cv =
    1.79 +  let
    1.80 +    val cache = ref Termtab.empty;
    1.81 +    fun conv ct =
    1.82 +      (case Termtab.lookup (! cache) (term_of ct) of
    1.83 +        SOME th => th
    1.84 +      | NONE =>
    1.85 +          let val th = cv ct
    1.86 +          in change cache (Termtab.update (term_of ct, th)); th end);
    1.87 + in conv end;
    1.88 +
    1.89  
    1.90  
    1.91 -(* Pure conversions *)
    1.92 +(** Pure conversions **)
    1.93 +
    1.94 +(* lambda terms *)
    1.95 +
    1.96 +fun abs_conv cv ct =
    1.97 +  (case term_of ct of
    1.98 +    Abs (x, _, _) =>
    1.99 +      let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
   1.100 +      in Thm.abstract_rule x v (cv ct') end
   1.101 +  | _ => raise CTERM ("abs_conv", [ct]));
   1.102 +
   1.103 +fun combination_conv cv1 cv2 ct =
   1.104 +  let val (ct1, ct2) = Thm.dest_comb ct
   1.105 +  in Thm.combination (cv1 ct1) (cv2 ct2) end;
   1.106 +
   1.107 +fun comb_conv cv = combination_conv cv cv;
   1.108 +fun arg_conv cv = combination_conv all_conv cv;
   1.109 +fun fun_conv cv = combination_conv cv all_conv;
   1.110 +
   1.111 +val arg1_conv = fun_conv o arg_conv;
   1.112 +val fun2_conv = fun_conv o fun_conv;
   1.113 +
   1.114 +
   1.115 +(* logic *)
   1.116  
   1.117  (*rewrite B in !!x1 ... xn. B*)
   1.118  fun forall_conv 0 cv ct = cv ct
   1.119 @@ -65,7 +112,7 @@
   1.120            (case (term_of A, term_of B) of
   1.121              (Const ("all", _), Abs (x, _, _)) =>
   1.122                let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
   1.123 -                Thm.combination (Thm.reflexive A)
   1.124 +                Thm.combination (all_conv A)
   1.125                    (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
   1.126                end
   1.127            | _ => cv ct));
   1.128 @@ -75,17 +122,17 @@
   1.129    | concl_conv n cv ct =
   1.130        (case try Thm.dest_implies ct of
   1.131          NONE => cv ct
   1.132 -      | SOME (A, B) => Drule.imp_cong_rule (reflexive A) (concl_conv (n - 1) cv B));
   1.133 +      | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
   1.134  
   1.135  (*rewrite the A's in A1 ==> ... ==> An ==> B*)
   1.136 -fun prems_conv 0 _ = reflexive
   1.137 +fun prems_conv 0 _ = all_conv
   1.138    | prems_conv n cv =
   1.139        let
   1.140          fun conv i ct =
   1.141 -          if i = n + 1 then reflexive ct
   1.142 +          if i = n + 1 then all_conv ct
   1.143            else
   1.144              (case try Thm.dest_implies ct of
   1.145 -              NONE => reflexive ct
   1.146 +              NONE => all_conv ct
   1.147              | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
   1.148    in conv 1 end;
   1.149