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