# Structure realSimps

signature realSimps =
sig
include Abbrev
(* eliminates common factors in divisions *)
val elim_common_factor : Term.term -> Thm.thm
(* Useful rewrites for basic real arithmetic *)
val real_SS : simpLib.ssfrag
(* performs calculations over rational values *)
val REAL_REDUCE_ss : simpLib.ssfrag
(* Incorporates simpsets for bool, pair, and arithmetic as well *)
val real_ss : simpLib.simpset
(* AC rewrites for + and *: occasionally useful *)
val real_ac_SS : simpLib.ssfrag
(* the RealArith decision procedure *)
val REAL_ARITH_ss : simpLib.ssfrag
val arith_cache : Cache.cache (* the cache of results behind it *)
(* Incorporates the real simpset *)
val real_ac_ss : simpLib.simpset
(* canonicalise additive and multiplicative terms; with addcanon calling
mulcanon on each summand *)
val REALADDCANON : conv
val REALMULCANON : conv
val RMULCANON_ss : simpLib.ssfrag
val RADDCANON_ss : simpLib.ssfrag
(* put literal values into a canonical form:
- integral values are left alone
- inverses applied to integers are turned into 1/n
- negative signs are moved to denominators
- fractions are reduced by gcds
*)
val REAL_LITCANON : conv
(* eliminate common terms from either side of a relation symbol, factoring
as necessary. Arguments:
1. relation symbol;
2. list of (theorem * selector-fn) pairs.
The theorem justifies removal of common factors on left and the
common factor must be the first universally quantified variable in
the theorem statement. The selector-fn identifies where in the
equation the smaller-term appears. (For example, in the
inequalities, it's always x * y R x * z <=> _ R _
so the selector-fn is just rhs, but for equality we have
x * y = x * z <=> x = 0 \/ y = z
so the selector-fn is (rand o rhs);
3. solver to discharge side conditions to do with non-zero ness and
signs. The list passed to it is the stack of previous side
condition attempts.
*)
val mulrelnorm : term -> (thm * (term -> term)) list ->
(term list -> term -> thm) ->
term list -> term -> thm
val RMULRELNORM_ss : simpLib.ssfrag
val real_compset : unit -> computeLib.compset
end

*HOL 4, Kananaskis-14*