1(* ========================================================================= *)
2(* Tools for reasoning about positive reals (posreals).                      *)
3(* ========================================================================= *)
4
5signature posrealTools =
6sig
7
8  (* Case splitting posreals into finite and infinite *)
9  val pcases    : Tactic.tactic
10  val pcases_on : Term.term frag list -> Tactic.tactic
11
12  (* Case splitting posreals into zero, finite non-zero and infinite *)
13  val pcases3    : Tactic.tactic
14  val pcases3_on : Term.term frag list -> Tactic.tactic
15
16  (* Useful rewrites for basic posreal arithmetic *)
17  val posreal_SS : simpLib.ssfrag
18  val posreal_ss : simpLib.simpset                (* real + posreal *)
19
20  (* A calculator for rational posreals *)
21  val posreal_reduce_SS : simpLib.ssfrag
22  val posreal_reduce_ss : simpLib.simpset         (* reduce + posreal_reduce *)
23
24  (* AC normalizer for multiplication *)
25  val permute_mul_conv : Abbrev.conv
26
27end
28