EXTENSIONAL and RESTRICTION ported from HOL-Light

src/combin/combinScript.sml

@@ -450,6 +450,102 @@ 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
+
+(* 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
 {sig_ps = NONE,
  struct_ps = SOME (fn _ =>

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

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