Structure ConseqConv


Source File Identifier index Theory binding index

signature ConseqConv =
sig

include Abbrev


(*
  trace "DEPTH_CONSEQ_CONV" can be used to get debug information
  on DEPTH_CONSEQ_CONV and related conversions
*)


(* A consequence conversion is a function
   that given a term t returns a theorem of the form

   |- t' ==> t (STRENGTHEN) or
   |- t ==> t' (WEAKEN) or
   |- t <=> t' (EQUIVALENT)
*)
type conseq_conv = term -> thm;


(* Directed consequence conversions allow specifying, whether
   strengthening or weakening is desired. *)
datatype CONSEQ_CONV_direction =
         CONSEQ_CONV_STRENGTHEN_direction
       | CONSEQ_CONV_WEAKEN_direction
       | CONSEQ_CONV_UNKNOWN_direction;

type directed_conseq_conv = CONSEQ_CONV_direction -> conseq_conv;


(* Some basic consequence conversions. Most are trivial,
   but useful building blocks for writing more interesting ones. *)
val FALSE_CONSEQ_CONV       : conseq_conv;
val TRUE_CONSEQ_CONV        : conseq_conv;
val REFL_CONSEQ_CONV        : conseq_conv;
val FORALL_EQ___CONSEQ_CONV : conseq_conv;
val EXISTS_EQ___CONSEQ_CONV : conseq_conv;

val TRUE_FALSE_REFL_CONSEQ_CONV : directed_conseq_conv

(* Consequence Conversions can be combined. There are similar
   operations as for conversions. *)

val CHANGED_CONSEQ_CONV    : conseq_conv -> conseq_conv;
val QCHANGED_CONSEQ_CONV   : conseq_conv -> conseq_conv;
val ORELSE_CONSEQ_CONV     : conseq_conv -> conseq_conv -> conseq_conv
val THEN_CONSEQ_CONV       : conseq_conv -> conseq_conv -> conseq_conv;
val FIRST_CONSEQ_CONV      : conseq_conv list -> conseq_conv;
val EVERY_CONSEQ_CONV      : conseq_conv list -> conseq_conv;

val FORALL_CONSEQ_CONV     : conseq_conv -> conseq_conv;
val EXISTS_CONSEQ_CONV     : conseq_conv -> conseq_conv;
val QUANT_CONSEQ_CONV      : conseq_conv -> conseq_conv;

(* Enforce a consequence conversion to operate in only one direction *)
val STRENGTHEN_CONSEQ_CONV : conseq_conv -> directed_conseq_conv;
val WEAKEN_CONSEQ_CONV     : conseq_conv -> directed_conseq_conv;


(* Rules *)
val STRENGTHEN_CONSEQ_CONV_RULE  : directed_conseq_conv -> thm -> thm;
val WEAKEN_CONSEQ_CONV_RULE      : directed_conseq_conv -> thm -> thm;


(* Tactics *)
val CONSEQ_CONV_TAC              : directed_conseq_conv -> tactic;
val ASM_CONSEQ_CONV_TAC          : (thm list -> directed_conseq_conv) -> tactic
val DISCH_ASM_CONSEQ_CONV_TAC    : directed_conseq_conv -> tactic;



(* DEPTH_CONSEQ_CONV

   For equality, it is comparatively simple to write a conversion that
   looks at subterms. For consequence conversion one needs to exploit
   semantic information about boolean operations one wants operate on.

   However, for the common operators

   - conjunction
   - disjunction
   - negation
   - implication
   - if-then-else
   - universal quantification
   - existential quantification

   this is provided by the ConseqConv library. This leads to easily usable
   consequence conversions and corresponding tactics that traverse a term.
*)

val DEPTH_CONSEQ_CONV              : directed_conseq_conv -> directed_conseq_conv;
val REDEPTH_CONSEQ_CONV            : directed_conseq_conv -> directed_conseq_conv;
val ONCE_DEPTH_CONSEQ_CONV         : directed_conseq_conv -> directed_conseq_conv;

val DEPTH_CONSEQ_CONV_TAC          : directed_conseq_conv -> tactic;
val REDEPTH_CONSEQ_CONV_TAC        : directed_conseq_conv -> tactic;
val ONCE_DEPTH_CONSEQ_CONV_TAC     : directed_conseq_conv -> tactic;

val DEPTH_STRENGTHEN_CONSEQ_CONV   : conseq_conv -> conseq_conv;
val REDEPTH_STRENGTHEN_CONSEQ_CONV : conseq_conv -> conseq_conv;


(* A bit uncommon is a generalisation of ONCE_DEPTH_CONSEQ_CONV, which at most
   performs 1 step. This generalisation allows specifying how many steps should
   at most be taken. *)
val NUM_DEPTH_CONSEQ_CONV  : directed_conseq_conv -> int ->
                             directed_conseq_conv;
val NUM_REDEPTH_CONSEQ_CONV: directed_conseq_conv -> int ->
                             directed_conseq_conv


(* The most common application of DEPTH_CONSEQ_CONV is a tool similar to
   REWRITE_CONV. The directed consequence conversion CONSEQ_TOP_REWRITE_CONV gets
   a triple (both_thmL,strengthen_thmL,weaken_thmL) of theorem lists. The theorem
   lists are preprocessed (most prominently by getting their body conjuncts, but
   also by moving quantifiers around a bit). Moreover, equivalence theorems
   might be split into two implications. The resulting theorems lists are used as follows:


   strengthen_thmL:
   These theorems are used for strengthening. This means, given a term "t0" and
   a theorem "|- t' ==> t" in the preprocessed strengthen list. Then CONSEQ_TOP_REWRITE_CONV
   tries to match t0 with t, which would result in a theorem "|- t0' ==> t0".

   weaken_thmL:
   These theorems are used for weakening.

   both_thmL:
   These theorems are used for both strengthening and weakening.

   CONSEQ_TOP_REWRITE_CONV searches (depending on the given direction) for a theorem to
   strengthen or weaken its input term with. The first one it finds is applied and the
   resulting theorem returned. If none is found, UNCHANGED is raised.

   CONSEQ_TOP_HO_REWRITE_CONV is similar, but uses higher order matching instead of
   first order one.
*)

val CONSEQ_TOP_REWRITE_CONV     : (thm list * thm list * thm list) -> directed_conseq_conv;
val CONSEQ_TOP_HO_REWRITE_CONV  : (thm list * thm list * thm list) -> directed_conseq_conv;


(* Combined with various versions of DEPTH_CONSEQ_CONV, this leads to a powerful tools for
   applying implicational theorems. *)

val CONSEQ_REWRITE_CONV         : (thm list * thm list * thm list) -> directed_conseq_conv;
val CONSEQ_HO_REWRITE_CONV      : (thm list * thm list * thm list) -> directed_conseq_conv;
val ONCE_CONSEQ_REWRITE_CONV    : (thm list * thm list * thm list) -> directed_conseq_conv;
val ONCE_CONSEQ_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;

val CONSEQ_REWRITE_TAC          : (thm list * thm list * thm list) -> tactic;
val CONSEQ_HO_REWRITE_TAC       : (thm list * thm list * thm list) -> tactic;
val ONCE_CONSEQ_REWRITE_TAC     : (thm list * thm list * thm list) -> tactic;
val ONCE_CONSEQ_HO_REWRITE_TAC  : (thm list * thm list * thm list) -> tactic;

val CONSEQ_TOP_REWRITE_TAC      : (thm list * thm list * thm list) -> tactic;
val CONSEQ_TOP_HO_REWRITE_TAC   : (thm list * thm list * thm list) -> tactic;


(* General rules and tactics. These were implemented to might be useful in general *)
val GEN_ASSUM               : term -> thm -> thm;
val GEN_IMP                 : term -> thm -> thm;
val LIST_GEN_IMP            : term list -> thm -> thm;
val GEN_EQ                  : term -> thm -> thm;
val LIST_GEN_EQ             : term list -> thm -> thm;
val EXISTS_INTRO_IMP        : term -> thm -> thm;
val LIST_EXISTS_INTRO_IMP   : term list -> thm -> thm;

val SPEC_ALL_TAC            : tactic;
val REMOVE_TRUE_TAC         : tactic;
val DISCH_ASM_CONV_TAC      : conv -> tactic;



(******************************************************************)
(******************************************************************)
(* ADVANCED USAGE                                                 *)
(******************************************************************)
(******************************************************************)


(* The functionality shown above mimics for implications some of the
   infrastructure for equations. However, for equational reasoning the
   simplifier is available, which allows to use context
   information. Something like is also beneficial for reasoning with
   implications. The implementation underlying the simple DEPTH
   conversions above allows in it's full detail:

   - using context information
   - providing a list of congruence rules
   - caching intermediate steps
   - fine control over counting steps
   - control over reiterating of already modified subterms
*)

type conseq_conv_congruence_syscall =
   term list -> thm list -> int -> CONSEQ_CONV_direction -> term -> (int * thm option)

type conseq_conv_congruence =
   thm list -> conseq_conv_congruence_syscall ->
   CONSEQ_CONV_direction -> term -> (int * thm)

type depth_conseq_conv_cache

type depth_conseq_conv_cache_opt =
   ((unit -> depth_conseq_conv_cache) * ((term * (int * thm option)) -> bool)) option

val EXT_DEPTH_NUM_CONSEQ_CONV  :
    conseq_conv_congruence list ->    (*congruence_list*)
    depth_conseq_conv_cache_opt ->    (*use cache*)
    int option ->                     (*max no of steps, NONE for unbounded *)
    bool ->                           (*redepth ?*)
    (bool * int option * (thm list -> directed_conseq_conv)) list ->
         (*conversion list:
           (1: true : apply before descending into subterms
               false : apply after returning from descend
            2: weight, how many steps are counted, 0 means that it does
               not count
            3: context -> conversion
          *)
    thm list ->                       (*context that might be used*)
    CONSEQ_CONV_direction -> term ->
    (int * thm option)
      (* number of steps taken + theorem option. NONE might be returned if nothing changed. *)


(***************)
(* Congruences *)
(***************)

(* conseq_conv_congruences are used for moving consequence conversions
   through boolean terms.

   A congruence gets 4 arguments

     context : thm list
       A list of theorems from the context it may use.

     sys : conseq_conv_congruence_syscall
       A callback for actually trying to work on subterms (see below)

     dir : CONSEQ_CONV_direction
       The direction it should work in.

     t : term
       The term to work on

   It results in the number of steps performed and a resulting theorem.
   If the congruence fails, it raises an exception.

   The job of a congruence is to call the system callback sys on suitable
   subterms and recombine the results.

   The system callback gets the following arguments

     new_context : term list
       new context information that may be assumed theorems are build
       via ASSUME from these terms, it's the job of the congruence to
       remove the resulting assumptions

     old_context : thm list
       the old context theorems that can be used

     m : int
       number of steps already taken so far

     dir : CONSEQ_CONV_direction
       the direction

     t : term
       term to work on

   The syscall returns the number of steps performed as well a
   potential resulting theorem.
*)



(* For the common operations, i.e. for

   - conjunction
   - disjunction
   - negation
   - implication
   - if-then-else
   - universal quantification
   - existential quantification

   there are already defined congruences. These come with
   different levels of using context information. If more
   context is used, potentially more can be done. However,
   there is a speed penalty. CONSEQ_CONV_get_context_congruences
   returns lists of congruences for these operations for
   different levels of using context information.
*)


datatype CONSEQ_CONV_context =
  (* do not use context at all *)
  CONSEQ_CONV_NO_CONTEXT

  (* use just the antecedents of implications *)
| CONSEQ_CONV_IMP_CONTEXT

  (* use all available context (from and, or, ...) *)
| CONSEQ_CONV_FULL_CONTEXT;


val CONSEQ_CONV_get_context_congruences :
    CONSEQ_CONV_context -> conseq_conv_congruence list;



(***************)
(* Cashing     *)
(***************)

(* There is support for caching results. A depth_conseq_conv_cache
   is a reference a dictionary for looking up previously recorded results. *)

(* make a new, empty cache *)
val mk_DEPTH_CONSEQ_CONV_CACHE : unit -> depth_conseq_conv_cache;

(* clear an existing cache, i.e. remove all entries *)
val clear_CONSEQ_CONV_CACHE     : depth_conseq_conv_cache -> unit


(* However, at top-level, no cache, but a depth_conseq_conv_cache_opt is
   passed around. If such an option is NONE, no caching is used.
   Otherwise, it consists of a function for getting a cache and a
   predicate that determines which new results are added to the cache.

   The result for getting the cache is called once before traversing
   the term begins. It can create a fresh cache or return a previously
   used cache containing already useful results. If a result is not
   found in the cache and newly computed, the predicate passed
   determines, whether it is added to the cache. *)


(* The default cache-option. It always creates a fresh cache and
   stores all results in this cache. *)
val CONSEQ_CONV_default_cache_opt : depth_conseq_conv_cache_opt

(* Always create a fresh cache and use given predicate. *)
val mk_DEPTH_CONSEQ_CONV_CACHE_OPT : ((term * (int * thm option)) -> bool) -> depth_conseq_conv_cache_opt;

(* Create a cache just once and keep it for multiple calls.
   Use the given predicate. *)
val mk_PERSISTENT_DEPTH_CONSEQ_CONV_CACHE_OPT : ((term * (int * thm option)) -> bool) -> depth_conseq_conv_cache_opt;

(* A function to clear the cache of a persistent cache-option. *)
val clear_CONSEQ_CONV_CACHE_OPT : depth_conseq_conv_cache_opt -> unit



(********************)
(* Derived DEPTH    *)
(* consequence      *)
(* conversions      *)
(********************)

(* ignore the number of steps result and raise UNCHANGED, if no thm is returned *)
val EXT_DEPTH_CONSEQ_CONV  :
    conseq_conv_congruence list ->    (*congruence_list*)
    depth_conseq_conv_cache_opt ->    (*use cache*)
    int option ->                     (*no of steps, NONE for unbounded *)
    bool ->                           (*redepth ?*)
    (bool * int option * (thm list -> directed_conseq_conv)) list ->
         (*conversion list:
           (1: apply before or after descending in subterms
            2: weight, how many steps are counted, 0 means that it does
               not count
            3: context -> conversion
          *)
    thm list ->                       (*context that might be used*)
    directed_conseq_conv

(* Use congruences for given context level and argument consequence consequence conv
   might use context. *)
val CONTEXT_DEPTH_CONSEQ_CONV      : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv;
val CONTEXT_REDEPTH_CONSEQ_CONV    : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv;
val CONTEXT_ONCE_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv;
val CONTEXT_NUM_DEPTH_CONSEQ_CONV  : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> int ->
                                     directed_conseq_conv;
val CONTEXT_NUM_REDEPTH_CONSEQ_CONV: (thm list -> directed_conseq_conv) -> int ->
                                     directed_conseq_conv




(**********************)
(* Fancy REWRITE      *)
(**********************)

(* Allowing full access to all parameters leads for
   CONSEQ_REWRITE_CONV to the following function.

   Most arguments are known from EXT_DEPTH_NUM_CONSEQ_CONV or
   CONSEQ_REWRITE_CONV. the list of conversions corresponds to the
   list of directed_conseq_conv for EXT_DEPTH_NUM_CONSEQ_CONV.
   However, here really conversions, not consequence conversions are
   required. *)

val FULL_EXT_CONSEQ_REWRITE_CONV        :
   conseq_conv_congruence list -> (* congruences *)
   depth_conseq_conv_cache_opt -> (* cache *)
   int option ->                  (* steps *)
   bool ->                        (* redepth *)
   bool ->                        (* higher order rewriting ? *)
   thm list ->                    (* context *)
   (bool * int option * (thm list -> conv)) list -> (* conversions *)
   (thm list * thm list * thm list) -> (*consequence rewrites *)
   directed_conseq_conv


(* Derived functions *)
val EXT_CONSEQ_REWRITE_CONV             : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
val EXT_CONSEQ_HO_REWRITE_CONV          : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
val EXT_CONTEXT_CONSEQ_REWRITE_CONV     : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
val EXT_CONTEXT_CONSEQ_HO_REWRITE_CONV  : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;

val EXT_CONSEQ_REWRITE_TAC              :                        (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;
val EXT_CONTEXT_CONSEQ_REWRITE_TAC      : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;
val EXT_CONSEQ_HO_REWRITE_TAC           :                        (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;
val EXT_CONTEXT_CONSEQ_HO_REWRITE_TAC   : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;




(*************************************************************************)
(* Technical Stuff for writing own, low level consequence conversion     *)
(*************************************************************************)

val asm_marker_tm         : term
val dest_asm_marker       : term -> term * term
val is_asm_marker         : term -> bool
val mk_asm_marker         : term -> term -> term
val mk_asm_marker_random  : term -> term
val dest_neg_asm_marker   : term -> term * term
val is_neg_asm_marker     : term -> bool
val asm_marker_ELIM_CONV  : conv
val asm_marker_INTRO_CONV : term -> conv


val CONSEQ_CONV_DIRECTION_NEGATE      : CONSEQ_CONV_direction -> CONSEQ_CONV_direction;
val CONSEQ_CONV___GET_SIMPLIFIED_TERM : thm -> term -> term;
val CONSEQ_CONV___GET_DIRECTION       : thm -> term -> CONSEQ_CONV_direction;
val THEN_CONSEQ_CONV___combine        : thm -> thm -> term -> thm;
val CONSEQ_CONV___APPLY_CONV_RULE     : thm -> term -> (term -> thm) -> thm;


val step_opt_sub          : int option -> int -> int option
val step_opt_allows_steps : int option -> int -> int option -> bool


end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13