Fixed agree_upto_lemma (and head_equivalent_def)

examples/lambda/basics/appFOLDLScript.sml

@@ -11,7 +11,7 @@ open HolKernel Parse boolLib bossLib;
 open arithmeticTheory listTheory rich_listTheory pred_setTheory finite_mapTheory
      hurdUtils listLib pairTheory;
 
-open termTheory binderLib;
+open termTheory binderLib basic_swapTheory;
 
 val _ = new_theory "appFOLDL"
 
@@ -403,14 +403,39 @@ Proof
     Induct_on ‘vs’ >> rw [LAM_eq_thm]
 QED
 
+fun RNEWS_TAC (vs, r, n) X :tactic =
+    qabbrev_tac ‘^vs = RNEWS ^r ^n ^X’
+ >> Know ‘ALL_DISTINCT ^vs /\ DISJOINT (set ^vs) ^X /\ LENGTH ^vs = ^n’
+ >- rw [RNEWS_def, Abbr ‘^vs’]
+ >> DISCH_THEN (STRIP_ASSUME_TAC o (REWRITE_RULE [DISJOINT_UNION']));
+
+Theorem LAMl_RNEWS_11 :
+    !X r n1 n2 y1 y2. FINITE X ==>
+       (LAMl (RNEWS r n1 X) (VAR y1) =
+        LAMl (RNEWS r n2 X) (VAR y2) <=> n1 = n2 /\ y1 = y2)
+Proof
+    rpt STRIP_TAC
+ >> reverse EQ_TAC >- (STRIP_TAC >> fs [])
+ >> Q_TAC (RNEWS_TAC (“vs1 :string list”, “r :num”, “n1 :num”)) ‘X’
+ >> Q_TAC (RNEWS_TAC (“vs2 :string list”, “r :num”, “n2 :num”)) ‘X’
+ >> DISCH_TAC
+ >> Know ‘size (LAMl vs1 (VAR y1)) = size (LAMl vs2 (VAR y2))’
+ >- (POP_ORW >> rw [])
+ >> simp [] (* n1 = n2 *)
+ >> DISCH_TAC
+ >> ‘vs1 = vs2’ by simp [Abbr ‘vs1’, Abbr ‘vs2’]
+ >> fs []
+QED
+
 (*---------------------------------------------------------------------------*
  *  funpow for lambda terms (using arithmeticTheory.FUNPOW)
  *---------------------------------------------------------------------------*)
 
 Overload funpow = “\f. FUNPOW (APP (f :term))”
 
 Theorem FV_FUNPOW :
-    !(f :term) x n. FV (FUNPOW (APP f) n x) = if n = 0 then FV x else FV f UNION FV x
+    !(f :term) x n. FV (FUNPOW (APP f) n x) =
+                    if n = 0 then FV x else FV f UNION FV x
 Proof
     rpt STRIP_TAC
  >> Q.SPEC_TAC (‘n’, ‘i’)

examples/lambda/basics/nomsetScript.sml

@@ -454,6 +454,26 @@ QED
 (* |- !p1 p2 x. lswapstr (p1 ++ p2) x = lswapstr p1 (lswapstr p2 x) *)
 Theorem lswapstr_append = ISPEC “string_pmact” pmact_append
 
+Theorem lswapstr_upperbound :
+    !xs ys v. LENGTH xs = LENGTH ys /\ DISJOINT (set xs) (set ys) /\
+              ALL_DISTINCT xs /\ ALL_DISTINCT ys ==>
+              lswapstr (ZIP (xs,ys)) v IN v INSERT set xs UNION set ys
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘pi = ZIP (xs,ys)’
+ >> Cases_on ‘~MEM v (MAP FST pi) /\ ~MEM v (MAP SND pi)’
+ >- (‘lswapstr pi v = v’ by PROVE_TAC [lswapstr_unchanged'] \\
+     simp [])
+ >> simp [IN_INSERT, IN_UNION] >> DISJ2_TAC
+ >> gs [Abbr ‘pi’, MAP_ZIP]
+ >| [ (* goal 1 (of 2) *)
+      DISJ2_TAC \\
+      MATCH_MP_TAC MEM_lswapstr >> art [],
+      (* goal 2 (of 2) *)
+      DISJ1_TAC \\
+      MATCH_MP_TAC MEM_lswapstr' >> art [] ]
+QED
+
 (*---------------------------------------------------------------------------*
  *  Permutation of a function call (fnpm)
  *---------------------------------------------------------------------------*)

examples/lambda/basics/termScript.sml

@@ -114,6 +114,12 @@ Theorem FINITE_FV[simp]: FINITE (FV t)
 Proof srw_tac [][supp_tpm, FINITE_GFV]
 QED
 
+Theorem FINITE_BIGUNION_IMAGE_FV[simp] :
+    FINITE (BIGUNION (IMAGE FV (set Ns)))
+Proof
+    rw [] >> rw [FINITE_FV]
+QED
+
 fun supp_clause {con_termP, con_def} = let
   val t = mk_comb(``supp ^t_pmact_t``, lhand (concl (SPEC_ALL con_def)))
 in

src/list/src/listScript.sml

@@ -2306,6 +2306,13 @@ val ALL_DISTINCT_APPEND = store_thm (
              (!e. MEM e l1 ==> ~(MEM e l2)))”,
   Induct THEN SRW_TAC [] [] THEN PROVE_TAC []);
 
+Theorem ALL_DISTINCT_APPEND' :
+    !l1 l2. ALL_DISTINCT (l1 ++ l2) <=>
+            ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\ DISJOINT (set l1) (set l2)
+Proof
+    RW_TAC std_ss [ALL_DISTINCT_APPEND, DISJOINT_ALT]
+QED
+
 val ALL_DISTINCT_SING = store_thm(
    "ALL_DISTINCT_SING",
    “!x. ALL_DISTINCT [x]”,

src/list/src/rich_listScript.sml

@@ -2713,6 +2713,13 @@ Proof
  >> rw [TAKE_LENGTH_TOO_LONG]
 QED
 
+Theorem IS_PREFIX_IMP_TAKE :
+    !l l1. l1 <<= l ==> l1 = TAKE (LENGTH l1) l
+Proof
+    rw [IS_PREFIX_EQ_TAKE]
+ >> rw [LENGTH_TAKE]
+QED
+
 (* NOTE: This theorem can also be proved by IS_PREFIX_LENGTH_ANTI and
    prefixes_is_prefix_total, but IS_PREFIX_EQ_TAKE is more natural.
  *)
@@ -3513,6 +3520,74 @@ QED
 end
 (* end CakeML lemmas *)
 
+(* BEGIN more lemmas of IS_SUFFIX *)
+Theorem IS_SUFFIX_EQ_DROP :
+    !l l1. IS_SUFFIX l l1 <=> ?n. n <= LENGTH l /\ l1 = DROP n l
+Proof
+    rw [GSYM IS_PREFIX_REVERSE, IS_PREFIX_EQ_TAKE]
+ >> EQ_TAC >> rpt STRIP_TAC
+ >| [ (* goal 1 (of 2) *)
+      Q.EXISTS_TAC ‘LENGTH l - n’ >> simp [] \\
+      ONCE_REWRITE_TAC [GSYM REVERSE_11] \\
+      POP_ASSUM (fn th => REWRITE_TAC [th]) \\
+      simp [TAKE_REVERSE, REVERSE_DROP],
+      (* goal 2 (of 2) *)
+      Q.EXISTS_TAC ‘LENGTH l - n’ >> simp [] \\
+      simp [TAKE_REVERSE, REVERSE_DROP] ]
+QED
+
+Theorem IS_SUFFIX_EQ_DROP' :
+    !l l1. IS_SUFFIX l l1 <=> ?n. l1 = DROP n l
+Proof
+    rpt GEN_TAC
+ >> EQ_TAC
+ >- (rw [IS_SUFFIX_EQ_DROP] \\
+     Q.EXISTS_TAC ‘n’ >> REWRITE_TAC [])
+ >> STRIP_TAC
+ >> Cases_on ‘n <= LENGTH l’
+ >- (rw [IS_SUFFIX_EQ_DROP] \\
+     Q.EXISTS_TAC ‘n’ >> ASM_REWRITE_TAC [])
+ >> ‘LENGTH l <= n’ by rw []
+ >> ‘l1 = []’ by rw [DROP_EQ_NIL]
+ >> simp [IS_SUFFIX]
+QED
+
+Theorem IS_SUFFIX_IMP_DROP :
+    !l l1. IS_SUFFIX l l1 ==> l1 = DROP (LENGTH l - LENGTH l1) l
+Proof
+    rw [IS_SUFFIX_EQ_DROP]
+ >> rw [LENGTH_DROP]
+QED
+
+Theorem IS_SUFFIX_IMP_LASTN :
+    !l l1. IS_SUFFIX l l1 ==> l1 = LASTN (LENGTH l1) l
+Proof
+    rw [IS_SUFFIX_EQ_DROP]
+ >> rw [DROP_LASTN]
+QED
+
+Theorem LIST_TO_SET_PREFIX :
+    !l l1. l1 <<= l ==> set l1 SUBSET set l
+Proof
+    rw [IS_PREFIX_EQ_TAKE']
+ >> rw [LIST_TO_SET_TAKE]
+QED
+
+Theorem LIST_TO_SET_SUFFIX :
+    !l l1. IS_SUFFIX l l1 ==> set l1 SUBSET set l
+Proof
+    rw [IS_SUFFIX_EQ_DROP']
+ >> rw [LIST_TO_SET_DROP]
+QED
+
+Theorem IS_SUFFIX_ALL_DISTINCT :
+    !l l1. IS_SUFFIX l l1 /\ ALL_DISTINCT l ==> ALL_DISTINCT l1
+Proof
+    rw [IS_SUFFIX_EQ_DROP']
+ >> MATCH_MP_TAC ALL_DISTINCT_DROP >> rw []
+QED
+(* END more lemmas of IS_SUFFIX *)
+
 Theorem nub_GENLIST:
   nub (GENLIST f n) =
     MAP f (FILTER (\i. !j. (i < j) /\ (j < n) ==> f i <> f j) (COUNT_LIST n))