basic_congs : unit -> thm list

SYNOPSIS

Lists the congruence rules used by the simplifier.

DESCRIPTION

The HOL Light simplifier (as invoked by SIMP_TAC etc.) uses congruence rules to determine how it uses context when descending through a term. These are essentially theorems showing how to decompose one equality to a series of other inequalities in context. A call to basic_congs() returns those congruences that are built into the system.

FAILURE CONDITIONS

Never fails.

EXAMPLE

Here is the effect in HOL Light's initial state:

  # basic_congs();;
  val it : thm list =
    [|- (!x. x IN s ==> f x = g x) ==> sum s (\i. f i) = sum s g;
     |- (!i. a <= i /\ i <= b ==> f i = g i)
        ==> sum (a..b) (\i. f i) = sum (a..b) g;
     |- (!x. p x ==> f x = g x) ==> sum {y | p y} (\i. f i) = sum {y | p y} g;
     |- (!x. x IN s ==> f x = g x) ==> nsum s (\i. f i) = nsum s g;
     |- (!i. a <= i /\ i <= b ==> f i = g i)
        ==> nsum (a..b) (\i. f i) = nsum (a..b) g;
     |- (!x. p x ==> f x = g x) ==> nsum {y | p y} (\i. f i) = nsum {y | p y} g;
     |- (g <=> g')
        ==> (g' ==> t = t')
        ==> (~g' ==> e = e')
        ==> (if g then t else e) = (if g' then t' else e');
     |- (p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')]