From 09d12c69a01996d6297b516b9fef271dec47221a Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Fri, 22 Mar 2024 15:08:21 +1100 Subject: [PATCH 1/2] EXTENSIONAL and RESTRICTION ported from HOL-Light --- src/combin/combinScript.sml | 84 +++++++++++++++ src/pred_set/src/pred_setScript.sml | 154 ++++++++++++++++++++++++++++ src/relation/relationScript.sml | 23 +++-- 3 files changed, 254 insertions(+), 7 deletions(-) diff --git a/src/combin/combinScript.sml b/src/combin/combinScript.sml index c9044083ce..4a419a86ab 100644 --- a/src/combin/combinScript.sml +++ b/src/combin/combinScript.sml @@ -450,6 +450,90 @@ Overload flip = “C” val _ = remove_ovl_mapping "C" {Name="C", Thy = "combin"} +(* ------------------------------------------------------------------------- *) +(* "Extensional" functions, mapping to a fixed value ARB outside the domain. *) +(* Even though these are still total, they're a conveniently better model *) +(* of the partial function space (e.g. the space has the right cardinality). *) +(* *) +(* (Ported from HOL-Light's sets.ml by Chun Tian) *) +(* ------------------------------------------------------------------------- *) + +(* NOTE: the original definition in HOL-Light was: + + EXTENSIONAL s = {f :'a->'b | !x. x NOTIN s ==> f x = ARB} + *) +val EXTENSIONAL_def = new_definition + ("EXTENSIONAL_def", + “EXTENSIONAL s (f :'a->'b) <=> !x. ~(x IN s) ==> f x = ARB”); + +Theorem IN_EXTENSIONAL : + !s (f :'a->'b). f IN EXTENSIONAL s <=> (!x. ~(x IN s) ==> f x = ARB) +Proof + REWRITE_TAC [IN_DEF] + >> BETA_TAC + >> rpt GEN_TAC + >> REWRITE_TAC [FUN_EQ_THM, EXTENSIONAL_def, IN_DEF] + >> BETA_TAC + >> REWRITE_TAC [] +QED + +Theorem IN_EXTENSIONAL_UNDEFINED : + !s (f :'a->'b) x. f IN EXTENSIONAL s /\ ~(x IN s) ==> f x = ARB +Proof + REWRITE_TAC [IN_EXTENSIONAL] + >> rpt STRIP_TAC + >> FIRST_X_ASSUM MATCH_MP_TAC + >> ASM_REWRITE_TAC [] +QED + +(* ------------------------------------------------------------------------- *) +(* Restriction of a function to an EXTENSIONAL one on a subset. *) +(* *) +(* NOTE: It's put here, so that RESTRICT in relationTheory can be defined *) +(* upon RESTRICTION. More theorems about RESTRICTION and EXTENSIONAL *) +(* are in pred_setTheory. *) +(* ------------------------------------------------------------------------- *) + +val RESTRICTION = new_definition + ("RESTRICTION", + “RESTRICTION s (f :'a->'b) x = if x IN s then f x else ARB”); + +Theorem RESTRICTION_THM : + !s (f :'a->'b). RESTRICTION s f = \x. if x IN s then f x else ARB +Proof + rpt GEN_TAC + >> REWRITE_TAC[FUN_EQ_THM, RESTRICTION] + >> BETA_TAC + >> REWRITE_TAC [] +QED + +Theorem RESTRICTION_DEFINED : + !s (f :'a->'b) x. x IN s ==> RESTRICTION s f x = f x +Proof + rpt GEN_TAC + >> REWRITE_TAC [RESTRICTION] + >> COND_CASES_TAC >> REWRITE_TAC [] +QED + +Theorem RESTRICTION_UNDEFINED : + !s (f :'a->'b) x. ~(x IN s) ==> RESTRICTION s f x = ARB +Proof + rpt GEN_TAC + >> REWRITE_TAC [RESTRICTION] + >> COND_CASES_TAC >> REWRITE_TAC [] +QED + +Theorem RESTRICTION_EQ : + !s (f :'a->'b) x y. x IN s /\ f x = y ==> RESTRICTION s f x = y +Proof + rpt STRIP_TAC + >> POP_ASSUM (fn th => (ONCE_REWRITE_TAC [SYM th])) + >> MATCH_MP_TAC RESTRICTION_DEFINED + >> ASM_REWRITE_TAC [] +QED + +(*---------------------------------------------------------------------------*) + val _ = adjoin_to_theory {sig_ps = NONE, struct_ps = SOME (fn _ => diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml index dea72b5418..6bf834aca7 100644 --- a/src/pred_set/src/pred_setScript.sml +++ b/src/pred_set/src/pred_setScript.sml @@ -7519,6 +7519,160 @@ val _ = export_rewrites "SUBSET_UNION" ]; +(* ------------------------------------------------------------------------- *) +(* More theorems about EXTENSIONAL and RESTRICTION *) +(* *) +(* (Ported from HOL-Light's sets.ml by Chun Tian) *) +(* ------------------------------------------------------------------------- *) + +Theorem EXTENSIONAL : + !s. EXTENSIONAL s = {f :'a->'b | !x. x NOTIN s ==> f x = ARB} +Proof + RW_TAC std_ss [IN_APP, EXTENSIONAL_def, Once EXTENSION, GSPECIFICATION] +QED + +Theorem EXTENSIONAL_EMPTY : + EXTENSIONAL {} = {\x:'a. ARB:'b} +Proof + RW_TAC std_ss [EXTENSION, IN_EXTENSIONAL, IN_SING, NOT_IN_EMPTY] THEN + REWRITE_TAC[FUN_EQ_THM] +QED + +Theorem EXTENSIONAL_UNIV : + !f. EXTENSIONAL univ(:'a) f +Proof + RW_TAC std_ss [EXTENSIONAL_def, IN_UNIV] +QED + +Theorem EXTENSIONAL_EQ : + !s f (g :'a->'b). + f IN EXTENSIONAL s /\ g IN EXTENSIONAL s /\ (!x. x IN s ==> f x = g x) + ==> f = g +Proof + REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN + ASM_CASES_TAC “(x :'a) IN s” THENL + [ASM_SIMP_TAC std_ss [], + ASM_MESON_TAC[IN_EXTENSIONAL_UNDEFINED]] +QED + +Theorem RESTRICTION_IN_EXTENSIONAL : + !s (f :'a->'b). RESTRICTION s f IN EXTENSIONAL s +Proof + SIMP_TAC std_ss [IN_EXTENSIONAL, RESTRICTION] +QED + +Theorem RESTRICTION_EXTENSION : + !s f (g :'a->'b). RESTRICTION s f = RESTRICTION s g <=> + (!x. x IN s ==> f x = g x) +Proof + REPEAT GEN_TAC THEN REWRITE_TAC [RESTRICTION, FUN_EQ_THM] THEN + EQ_TAC >> RW_TAC std_ss [] THEN + Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o (Q.SPEC ‘x’)) THEN + RW_TAC std_ss [] +QED + +Theorem RESTRICTION_FIXPOINT : + !s (f :'a->'b). RESTRICTION s f = f <=> f IN EXTENSIONAL s +Proof + REWRITE_TAC[IN_EXTENSIONAL, FUN_EQ_THM, RESTRICTION] + >> rpt GEN_TAC >> EQ_TAC >> RW_TAC std_ss [] + >- (Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o (Q.SPEC ‘x’)) \\ + RW_TAC std_ss []) + >> Cases_on ‘x IN s’ >> RW_TAC std_ss [] +QED + +Theorem RESTRICTION_RESTRICTION : + !s t (f :'a->'b). + s SUBSET t ==> RESTRICTION s (RESTRICTION t f) = RESTRICTION s f +Proof + REWRITE_TAC [FUN_EQ_THM, RESTRICTION] + >> RW_TAC std_ss [SUBSET_DEF] +QED + +Theorem RESTRICTION_IDEMP : + !s (f :'a->'b). RESTRICTION s (RESTRICTION s f) = RESTRICTION s f +Proof + REWRITE_TAC[RESTRICTION_FIXPOINT, RESTRICTION_IN_EXTENSIONAL] +QED + +Theorem IMAGE_RESTRICTION : + !(f :'a->'b) s t. s SUBSET t ==> IMAGE (RESTRICTION t f) s = IMAGE f s +Proof + RW_TAC std_ss [Once EXTENSION, IN_IMAGE, RESTRICTION, SUBSET_DEF] + >> EQ_TAC + >| [ (* goal 1 (of 2) *) + DISCH_THEN (X_CHOOSE_THEN “y :'a” MP_TAC) \\ + RW_TAC std_ss [] + >- (Q.EXISTS_TAC ‘y’ >> ASM_REWRITE_TAC []) \\ + Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o (Q.SPEC ‘y’)) \\ + ASM_REWRITE_TAC [], + (* goal 2 (of 2) *) + DISCH_THEN (X_CHOOSE_THEN “y :'a” MP_TAC) \\ + RW_TAC std_ss [] \\ + Q.EXISTS_TAC ‘y’ >> RW_TAC std_ss [] ] +QED + +Theorem RESTRICTION_COMPOSE_RIGHT : + !(f :'a->'b) (g :'b->'c) s. + RESTRICTION s (g o RESTRICTION s f) = + RESTRICTION s (g o f) +Proof + RW_TAC std_ss [FUN_EQ_THM, o_DEF, RESTRICTION] +QED + +Theorem RESTRICTION_COMPOSE_LEFT : + !(f :'a->'b) (g :'b->'c) s t. + IMAGE f s SUBSET t + ==> RESTRICTION s (RESTRICTION t g o f) = + RESTRICTION s (g o f) +Proof + RW_TAC std_ss [FUN_EQ_THM, o_DEF, RESTRICTION, IN_IMAGE, SUBSET_DEF] + >> Cases_on ‘x IN s’ + >> ASM_REWRITE_TAC [] + >> ‘f x IN t’ by (FIRST_X_ASSUM MATCH_MP_TAC \\ + Q.EXISTS_TAC ‘x’ >> ASM_REWRITE_TAC []) + >> ASM_SIMP_TAC std_ss [] +QED + +Theorem RESTRICTION_COMPOSE : + !(f :'a->'b) (g :'b->'c) s t. + IMAGE f s SUBSET t + ==> RESTRICTION s (RESTRICTION t g o RESTRICTION s f) = + RESTRICTION s (g o f) +Proof + SIMP_TAC std_ss [RESTRICTION_COMPOSE_LEFT, RESTRICTION_COMPOSE_RIGHT] +QED + +Theorem RESTRICTION_UNIQUE : + !s (f :'a->'b) g. + RESTRICTION s f = g <=> EXTENSIONAL s g /\ !x. x IN s ==> f x = g x +Proof + RW_TAC std_ss [FUN_EQ_THM, RESTRICTION, EXTENSIONAL_def] + >> EQ_TAC + >> RW_TAC std_ss [] + >| [ (* goal 1 (of 3) *) + Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o (Q.SPEC ‘x’)) \\ + RW_TAC std_ss [], + (* goal 2 (of 3) *) + Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o (Q.SPEC ‘x’)) \\ + RW_TAC std_ss [], + (* goal 3 (of 3) *) + Cases_on ‘x IN s’ >> RW_TAC std_ss [] ] +QED + +Theorem RESTRICTION_UNIQUE_ALT : + !s (f :'a->'b) g. + f = RESTRICTION s g <=> EXTENSIONAL s f /\ !x. x IN s ==> f x = g x +Proof + RW_TAC std_ss [FUN_EQ_THM, RESTRICTION, EXTENSIONAL_def] + >> EQ_TAC + >> RW_TAC std_ss [] + >> Cases_on ‘x IN s’ + >> RW_TAC std_ss [] +QED + +(*---------------------------------------------------------------------------*) + val _ = Theory.quote_adjoin_to_theory `val SET_SPEC_ss : simpLib.ssfrag` `local diff --git a/src/relation/relationScript.sml b/src/relation/relationScript.sml index 27c1c10176..d8d72bc891 100644 --- a/src/relation/relationScript.sml +++ b/src/relation/relationScript.sml @@ -5,13 +5,14 @@ * are also defined. * *---------------------------------------------------------------------------*) -open HolKernel Parse boolLib QLib tautLib mesonLib metisLib - simpLib boolSimps BasicProvers; +open HolKernel Parse boolLib BasicProvers; + +open QLib tautLib mesonLib metisLib simpLib boolSimps combinTheory; (* mention satTheory to work around dependency-analysis flaw in Holmake; satTheory is a dependency of BasicProvers, but without explicit mention here, Holmake will not rebuild relationTheory when satTheory changes. *) -local open combinTheory satTheory in end; +local open satTheory in end; val _ = new_theory "relation"; @@ -1218,11 +1219,19 @@ val _ = export_rewrites ["transitive_inv_image"] * Gordon's HOL development of the primitive recursion theorem. *---------------------------------------------------------------------------*) -val RESTRICT_DEF = -Q.new_definition -("RESTRICT_DEF", - `RESTRICT (f:'a->'b) R (x:'a) = \y:'a. if R y x then f y else ARB`); +(* NOTE: Now RESTRICT is based on the new combinTheory.RESTRICTION + + :('a -> 'b) -> ('a -> 'a -> bool) -> 'a -> 'a -> 'b + *) +val RESTRICT = new_definition + ("RESTRICT", “RESTRICT (f :'a->'b) R (x :'a) = RESTRICTION (\y. R y x) f”); +(* The old definition of RESTRICT now becomes a theorem *) +Theorem RESTRICT_DEF : + !(f :'a->'b) R x. RESTRICT f R x = \y. if R y x then f y else ARB +Proof + SRW_TAC[][RESTRICT, FUN_EQ_THM, RESTRICTION, IN_DEF] +QED (*--------------------------------------------------------------------------- * Obvious, but crucially useful. Unary case. Handling the n-ary case might From e3625f7e6cccb90bdb2f31f2971f4fd2e34fae6c Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Wed, 27 Mar 2024 14:28:02 +1100 Subject: [PATCH 2/2] [combin] Add one more theorem: EXTENSIONAL_RESTRICTION --- src/combin/combinScript.sml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/combin/combinScript.sml b/src/combin/combinScript.sml index 4a419a86ab..f5a67722b3 100644 --- a/src/combin/combinScript.sml +++ b/src/combin/combinScript.sml @@ -532,6 +532,18 @@ Proof >> ASM_REWRITE_TAC [] QED +(* NOTE: HOL-Light doesn't have this theorem. *) +Theorem EXTENSIONAL_RESTRICTION : + !s (f :'a->'b). EXTENSIONAL s (RESTRICTION s (f :'a -> 'b)) +Proof + REWRITE_TAC [EXTENSIONAL_def, RESTRICTION, IN_DEF] + >> BETA_TAC + >> rpt STRIP_TAC + >> reverse COND_CASES_TAC >- REFL_TAC + >> POP_ASSUM MP_TAC + >> ASM_REWRITE_TAC [] +QED + (*---------------------------------------------------------------------------*) val _ = adjoin_to_theory