From e45b4888a9fb55df3fd061617f00858191c77ee2 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Mon, 17 Jun 2024 11:01:47 +1000 Subject: [PATCH 1/3] Add realLib.prefer_num_floor --- examples/probability/large_numberScript.sml | 6 +----- src/real/realLib.sig | 4 +++- src/real/realLib.sml | 14 ++++++++++++++ 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/examples/probability/large_numberScript.sml b/examples/probability/large_numberScript.sml index c232b82ff1..02e917304f 100644 --- a/examples/probability/large_numberScript.sml +++ b/examples/probability/large_numberScript.sml @@ -42,11 +42,7 @@ val _ = hide "W"; val _ = intLib.deprecate_int (); val _ = ratLib.deprecate_rat (); -(* NOTE: The above deprecate settings do not cover "flr" and "clg", which - are overloaded again in intrealTheory. - *) -val _ = bring_to_front_overload "flr" {Name = "NUM_FLOOR", Thy = "real"}; -val _ = bring_to_front_overload "clg" {Name = "NUM_CEILING", Thy = "real"}; +val _ = realLib.prefer_num_floor (); (* ------------------------------------------------------------------------- *) (* Definitions *) diff --git a/src/real/realLib.sig b/src/real/realLib.sig index e35691f84d..b545c3e311 100644 --- a/src/real/realLib.sig +++ b/src/real/realLib.sig @@ -11,11 +11,13 @@ sig val REAL_ARITH : term -> thm val REAL_ASM_ARITH_TAC : tactic - val real_ss : simpLib.simpset (* Incorporates simpsets for bool, pair, and arithmetic *) + val real_ss : simpLib.simpset (* syntax *) val prefer_real : unit -> unit val deprecate_real : unit -> unit + val prefer_num_floor : unit -> unit + end diff --git a/src/real/realLib.sml b/src/real/realLib.sml index d20b08a2c2..c053b3f168 100644 --- a/src/real/realLib.sml +++ b/src/real/realLib.sml @@ -44,6 +44,20 @@ struct List.app doit operators end + (* NOTE: intrealTheory also contains overloads of ‘flr’ and ‘clg’ *) + val flr_operators = [("flr", realSyntax.NUM_FLOOR_tm), + ("clg", realSyntax.NUM_CEILING_tm)]; + + (* Prefer NUM_FLOOR (and also NUM_CEILING) (again INT_FLOOR, etc., maybe) *) + fun prefer_num_floor () = let + fun doit (s, t) = + let val {Name,Thy,...} = dest_thy_const t in + Parse.temp_bring_to_front_overload s {Name = Name, Thy = Thy} + end + in + List.app doit flr_operators + end + (* The default REAL_ARITH, etc. can be switched here. *) val REAL_ARITH_TAC = TRY(RealArith.OLD_REAL_ARITH_TAC) THEN RealField.REAL_ARITH_TAC; From f87b8c8b2ff6ed1409034581d2184ad9c857c684 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Mon, 17 Jun 2024 11:06:27 +1000 Subject: [PATCH 2/3] Move NUM_FLOOR and NUM_CEILING to realaxTheory --- src/real/realScript.sml | 13 +++---------- src/real/realSyntax.sig | 2 ++ src/real/realSyntax.sml | 12 ++++++++---- src/real/realaxScript.sml | 12 ++++++++++++ 4 files changed, 25 insertions(+), 14 deletions(-) diff --git a/src/real/realScript.sml b/src/real/realScript.sml index 9ebe90648d..0b9a8bb37a 100644 --- a/src/real/realScript.sml +++ b/src/real/realScript.sml @@ -3797,19 +3797,12 @@ val lt_int = store_thm( Q.EXISTS_TAC `0` THEN SRW_TAC [][REAL_NEG_LE0] ]); - (*---------------------------------------------------------------------------*) -(* Floor and ceiling (nums) *) +(* Floor and ceiling (nums) (NOTE: Their definitions are moved to realax) *) (*---------------------------------------------------------------------------*) -val NUM_FLOOR_def = zDefine` - NUM_FLOOR (x:real) = LEAST (n:num). real_of_num (n+1) > x`; - -val NUM_CEILING_def = zDefine` - NUM_CEILING (x:real) = LEAST (n:num). x <= real_of_num n`; - -val _ = overload_on ("flr",``NUM_FLOOR``); -val _ = overload_on ("clg",``NUM_CEILING``); +Theorem NUM_FLOOR_def = NUM_FLOOR_def +Theorem NUM_CEILING_def = NUM_CEILING_def val lem = SIMP_RULE arith_ss [REAL_POS,REAL_ADD_RID] (Q.SPECL[`y`,`&n`,`0r`,`1r`] REAL_LTE_ADD2); diff --git a/src/real/realSyntax.sig b/src/real/realSyntax.sig index 10c77a57c7..a5beb0fec8 100644 --- a/src/real/realSyntax.sig +++ b/src/real/realSyntax.sig @@ -12,6 +12,8 @@ sig val negate_tm : term val real_injection : term (* the injection from :num -> :real *) val inv_tm : term + val NUM_FLOOR_tm : term + val NUM_CEILING_tm : term (* binary operators *) val div_tm : term diff --git a/src/real/realSyntax.sml b/src/real/realSyntax.sml index 85aa6d1ad9..dc19359645 100644 --- a/src/real/realSyntax.sml +++ b/src/real/realSyntax.sml @@ -1,9 +1,9 @@ structure realSyntax :> realSyntax = struct - - local open realaxTheory in end; open HolKernel Abbrev; + local open realaxTheory numSyntax in end; + val ERR = mk_HOL_ERR "realSyntax"; (* Fundamental terms, mainly constants *) @@ -12,8 +12,9 @@ struct val real_ty = mk_thy_type {Thy = "realax", Tyop = "real", Args = []} val bop_ty = real_ty --> real_ty --> real_ty val rel_ty = real_ty --> real_ty --> bool + val num_ty = numSyntax.num - val real_injection = mk_raconst("real_of_num", numSyntax.num --> real_ty) + val real_injection = mk_raconst("real_of_num", num_ty --> real_ty) val zero_tm = mk_comb(real_injection, numSyntax.zero_tm) val one_tm = mk_comb(real_injection, numSyntax.mk_numeral (Arbnum.fromInt 1)) @@ -23,7 +24,7 @@ struct val minus_tm = mk_raconst("real_sub", bop_ty) val mult_tm = mk_raconst("real_mul", bop_ty) val div_tm = mk_raconst("/", bop_ty) - val exp_tm = mk_raconst("pow", real_ty --> numSyntax.num --> real_ty) + val exp_tm = mk_raconst("pow", real_ty --> num_ty --> real_ty) val real_eq_tm = mk_thy_const { Thy = "min", Name = "=", Ty = rel_ty} val less_tm = mk_raconst("real_lt", rel_ty) @@ -34,6 +35,9 @@ struct val min_tm = mk_raconst("min", bop_ty) val max_tm = mk_raconst("max", bop_ty) + val NUM_FLOOR_tm = mk_raconst("NUM_FLOOR", real_ty --> num_ty); + val NUM_CEILING_tm = mk_raconst("NUM_CEILING", real_ty --> num_ty); + (* Functions *) fun dest1 c fnm nm t = let diff --git a/src/real/realaxScript.sml b/src/real/realaxScript.sml index eee3609b3e..bcae92e4af 100644 --- a/src/real/realaxScript.sml +++ b/src/real/realaxScript.sml @@ -284,6 +284,18 @@ Proof end QED +(* Floor and ceiling (nums) *) +Definition NUM_FLOOR_def[nocompute] : + NUM_FLOOR (x:real) = LEAST (n:num). real_of_num (n+1) > x +End + +Definition NUM_CEILING_def[nocompute] : + NUM_CEILING (x:real) = LEAST (n:num). x <= real_of_num n +End + +Overload flr = “NUM_FLOOR” +Overload clg = “NUM_CEILING” + (* ------------------------------------------------------------------------- *) (* Some elementary "bootstrapping" lemmas needed by RealArith.sml *) (* *) From ba16d007acb7fc329c0894ef6606c356a1ce22f0 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Mon, 17 Jun 2024 13:42:15 +1000 Subject: [PATCH 3/3] Canceled prefer_num_floor(), using (redefined) Overload instead --- examples/probability/large_numberScript.sml | 6 +++++- src/real/realLib.sig | 2 -- src/real/realLib.sml | 14 -------------- 3 files changed, 5 insertions(+), 17 deletions(-) diff --git a/examples/probability/large_numberScript.sml b/examples/probability/large_numberScript.sml index 02e917304f..448036c05a 100644 --- a/examples/probability/large_numberScript.sml +++ b/examples/probability/large_numberScript.sml @@ -42,7 +42,11 @@ val _ = hide "W"; val _ = intLib.deprecate_int (); val _ = ratLib.deprecate_rat (); -val _ = realLib.prefer_num_floor (); +(* Prefer NUM_FLOOR and NUM_CEILING (over INT_FLOOR/INT_CEILING) by redefining + their overloads. + *) +Overload flr = “realax$NUM_FLOOR” +Overload clg = “realax$NUM_CEILING” (* ------------------------------------------------------------------------- *) (* Definitions *) diff --git a/src/real/realLib.sig b/src/real/realLib.sig index b545c3e311..fdf4009b2b 100644 --- a/src/real/realLib.sig +++ b/src/real/realLib.sig @@ -18,6 +18,4 @@ sig val prefer_real : unit -> unit val deprecate_real : unit -> unit - val prefer_num_floor : unit -> unit - end diff --git a/src/real/realLib.sml b/src/real/realLib.sml index c053b3f168..d20b08a2c2 100644 --- a/src/real/realLib.sml +++ b/src/real/realLib.sml @@ -44,20 +44,6 @@ struct List.app doit operators end - (* NOTE: intrealTheory also contains overloads of ‘flr’ and ‘clg’ *) - val flr_operators = [("flr", realSyntax.NUM_FLOOR_tm), - ("clg", realSyntax.NUM_CEILING_tm)]; - - (* Prefer NUM_FLOOR (and also NUM_CEILING) (again INT_FLOOR, etc., maybe) *) - fun prefer_num_floor () = let - fun doit (s, t) = - let val {Name,Thy,...} = dest_thy_const t in - Parse.temp_bring_to_front_overload s {Name = Name, Thy = Thy} - end - in - List.app doit flr_operators - end - (* The default REAL_ARITH, etc. can be switched here. *) val REAL_ARITH_TAC = TRY(RealArith.OLD_REAL_ARITH_TAC) THEN RealField.REAL_ARITH_TAC;