wenzelm@22905: (*  Title:      Pure/conv.ML
wenzelm@22905:     ID:         $Id$
wenzelm@22905:     Author:     Amine Chaieb and Makarius
wenzelm@22905: 
wenzelm@22905: Conversions: primitive equality reasoning.
wenzelm@22905: *)
wenzelm@22905: 
wenzelm@22905: infix 1 AND;
wenzelm@22905: infix 0 OR;
wenzelm@22905: 
wenzelm@22905: signature CONV =
wenzelm@22905: sig
wenzelm@22905:   type conv = cterm -> thm
wenzelm@22905:   val no_conv: conv
wenzelm@22905:   val all_conv: conv
wenzelm@22905:   val option_conv: conv -> cterm -> thm option
wenzelm@22905:   val AND: conv * conv -> conv
wenzelm@22905:   val OR: conv * conv -> conv
wenzelm@22905:   val forall_conv: int -> conv -> conv
wenzelm@22905:   val concl_conv: int -> conv -> conv
wenzelm@22905:   val prems_conv: int -> (int -> conv) -> conv
wenzelm@22905:   val goals_conv: (int -> bool) -> conv -> conv
wenzelm@22905:   val fconv_rule: conv -> thm -> thm
wenzelm@22905: end;
wenzelm@22905: 
wenzelm@22905: structure Conv: CONV =
wenzelm@22905: struct
wenzelm@22905: 
wenzelm@22905: (* conversionals *)
wenzelm@22905: 
wenzelm@22905: type conv = cterm -> thm
wenzelm@22905: 
wenzelm@22905: fun no_conv _ = raise CTERM ("no conversion", []);
wenzelm@22905: val all_conv = Thm.reflexive;
wenzelm@22905: 
wenzelm@22905: val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
wenzelm@22905: 
wenzelm@22905: fun option_conv conv ct =
wenzelm@22905:   (case try conv ct of
wenzelm@22905:     NONE => NONE
wenzelm@22905:   | SOME eq => if is_refl eq then NONE else SOME eq);
wenzelm@22905: 
wenzelm@22905: fun (conv1 AND conv2) ct =
wenzelm@22905:   let
wenzelm@22905:     val eq1 = conv1 ct;
wenzelm@22905:     val eq2 = conv2 (Thm.rhs_of eq1);
wenzelm@22905:   in
wenzelm@22905:     if is_refl eq1 then eq2
wenzelm@22905:     else if is_refl eq2 then eq1
wenzelm@22905:     else Thm.transitive eq1 eq2
wenzelm@22905:   end;
wenzelm@22905: 
wenzelm@22905: fun (conv1 OR conv2) ct =
wenzelm@22905:   (case try conv1 ct of SOME eq => eq | NONE => conv2 ct);
wenzelm@22905: 
wenzelm@22905: 
wenzelm@22905: (* Pure conversions *)
wenzelm@22905: 
wenzelm@22905: (*rewrite B in !!x1 ... xn. B*)
wenzelm@22905: fun forall_conv 0 cv ct = cv ct
wenzelm@22905:   | forall_conv n cv ct =
wenzelm@22905:       (case try Thm.dest_comb ct of
wenzelm@22905:         NONE => cv ct
wenzelm@22905:       | SOME (A, B) =>
wenzelm@22905:           (case (term_of A, term_of B) of
wenzelm@22905:             (Const ("all", _), Abs (x, _, _)) =>
wenzelm@22905:               let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
wenzelm@22905:                 Thm.combination (Thm.reflexive A)
wenzelm@22905:                   (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
wenzelm@22905:               end
wenzelm@22905:           | _ => cv ct));
wenzelm@22905: 
wenzelm@22905: (*rewrite B in A1 ==> ... ==> An ==> B*)
wenzelm@22905: fun concl_conv 0 cv ct = cv ct
wenzelm@22905:   | concl_conv n cv ct =
wenzelm@22905:       (case try Thm.dest_implies ct of
wenzelm@22905:         NONE => cv ct
wenzelm@22905:       | SOME (A, B) => Drule.imp_cong_rule (reflexive A) (concl_conv (n - 1) cv B));
wenzelm@22905: 
wenzelm@22905: (*rewrite the A's in A1 ==> ... ==> An ==> B*)
wenzelm@22905: fun prems_conv 0 _ = reflexive
wenzelm@22905:   | prems_conv n cv =
wenzelm@22905:       let
wenzelm@22905:         fun conv i ct =
wenzelm@22905:           if i = n + 1 then reflexive ct
wenzelm@22905:           else
wenzelm@22905:             (case try Thm.dest_implies ct of
wenzelm@22905:               NONE => reflexive ct
wenzelm@22905:             | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
wenzelm@22905:   in conv 1 end;
wenzelm@22905: 
wenzelm@22905: fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
wenzelm@22905: fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
wenzelm@22905: 
wenzelm@22905: end;