Complete a round of moves / clean up

Author: myreen

language/pure_expScript.sml

@@ -47,6 +47,11 @@ Definition Lams_def:
   Lams (v::vs) b = Lam v (Lams vs b)
 End
 
+Definition Seqs_def[simp]: (* TODO: move *)
+  Seqs [] x = x /\
+  Seqs (y::ys) x = Seq y (Seqs ys x)
+End
+
 Definition Bottom_def:
   Bottom = Letrec [("bot",Var "bot")] (Var "bot")
 End

meta-theory/pure_beta_equivScript.sml

@@ -614,7 +614,7 @@ Definition iidd_def:
   iidd = Lam "y" (App id (Var "y"))
 End
 
-(*TODO: a tactic that, given a goal like:
+(* Would be nice to have a tactic that, given a goal like:
 
         exp_alpha (Lam "y" (Var "y")) (Lam "x" (Var "x"))
 
@@ -642,4 +642,3 @@ Theorem id_iidd_equivalence_expanded =
    id_iidd_equivalence |> REWRITE_RULE [iidd_def,id_def]
 
 val _ = export_theory();
-

meta-theory/pure_congruenceScript.sml

@@ -2973,13 +2973,6 @@ Proof
   simp [bind_def, SF SFY_ss]
 QED
 
-Triviality ignore_FDIFF: (* TODO: move *)
-  DISJOINT f (FDOM m) ⇒ FDIFF m f = m
-Proof
-  fs [fmap_eq_flookup,FLOOKUP_DEF,FDIFF_def,DRESTRICT_DEF,IN_DISJOINT]
-  \\ metis_tac []
-QED
-
 Theorem Lams_cong:
   ∀vs x y. (x ≅? y) b ⇒ (Lams vs x ≅? Lams vs y) b
 Proof

meta-theory/pure_exp_lemmasScript.sml

@@ -913,4 +913,37 @@ Proof
   rw[closed_def, freevars_Lams] >> simp[SUBSET_DIFF_EMPTY]
 QED
 
+Theorem Apps_append:
+  ∀xs ys x. Apps x (xs ++ ys) = Apps (Apps x xs) ys
+Proof
+  Induct \\ fs [Apps_def]
+QED
+
+Theorem Apps_11:
+  ∀xs ys x y. Apps x xs = Apps y ys ∧ LENGTH xs = LENGTH ys ⇒ x = y ∧ xs = ys
+Proof
+  Induct \\ fs [Apps_def]
+  \\ Cases_on ‘ys’ \\ fs [Apps_def]
+  \\ rw [] \\ res_tac \\ fs []
+QED
+
+Theorem subst_Seqs:
+  ∀xs y. subst m (Seqs xs y) = Seqs (MAP (subst m) xs) (subst m y)
+Proof
+  Induct \\ fs [subst_def]
+QED
+
+Theorem subst_Apps:
+  ∀xs m f. subst m (Apps f xs) = Apps (subst m f) (MAP (subst m) xs)
+Proof
+  Induct \\ fs [Apps_def,subst_def]
+QED
+
+Theorem ignore_FDIFF:
+  DISJOINT f (FDOM m) ⇒ FDIFF m f = m
+Proof
+  fs [fmap_eq_flookup,FLOOKUP_DEF,FDIFF_def,DRESTRICT_DEF,IN_DISJOINT]
+  \\ metis_tac []
+QED
+
 val _ = export_theory();

meta-theory/pure_letrec_congScript.sml

@@ -52,20 +52,14 @@ Proof
   \\ rw [] \\ res_tac \\ fs []
 QED
 
-Triviality LIST_REL_opp: (* TODO: move *)
-  ∀xs ys. LIST_REL R xs ys ⇒ LIST_REL (λx y. R y x) ys xs
-Proof
-  Induct \\ fs [PULL_EXISTS]
-QED
-
 Theorem letrec_binds_opp:
   letrec_binds binds2 binds1 = (λx y. letrec_binds binds1 binds2 y x)
 Proof
   qsuff_tac ‘∀b2 b1 x y. letrec_binds b2 b1 x y ⇒ letrec_binds b1 b2 y x’
   >- (rw [FUN_EQ_THM] \\ eq_tac \\ fs [])
   \\ ho_match_mp_tac letrec_binds_ind \\ rw []
   \\ simp [Once letrec_binds_cases]
-  \\ imp_res_tac LIST_REL_opp \\ fs [SF ETA_ss]
+  \\ once_rewrite_tac [LIST_REL_SWAP] \\ fs [SF ETA_ss]
 QED
 
 Theorem letrec_binds_freevars:
@@ -145,12 +139,6 @@ Proof
   \\ metis_tac []
 QED
 
-Triviality MAP_ID: (* TODO: move *)
-  ∀xs f. (MAP f xs = xs) ⇔ ∀x. MEM x xs ⇒ f x = x
-Proof
-  Induct \\ fs [] \\ metis_tac []
-QED
-
 Theorem subst_letrec_binds:
   ∀b1 b2 x y m1 m2.
     letrec_binds b1 b2 x y ∧
@@ -165,7 +153,7 @@ Proof
    (fs [subst_def]
     \\ simp [Once letrec_binds_cases]
     \\ disj1_tac
-    \\ fs [MAP_ID,FORALL_PROD]
+    \\ fs [MAP_ID_EQ,FORALL_PROD]
     \\ reverse (rw [])
     >-
      (last_x_assum irule \\ fs [FDOM_FDIFF,EXTENSION,SUBSET_DEF]
@@ -235,21 +223,6 @@ Proof
   fs [FDOM_FUPDATE_LIST,MAP_MAP_o,combinTheory.o_DEF,UNCURRY,SF ETA_ss]
 QED
 
-Triviality FORALL_FRANGE: (* TODO: move *)
-  (∀v. v ∈ FRANGE m ⇒ P v) ⇔ ∀k v. FLOOKUP m k = SOME v ⇒ P v
-Proof
-  fs [FRANGE_DEF,FLOOKUP_DEF,PULL_EXISTS]
-QED
-
-Triviality MEM_IMP_EQ: (* TODO: move *)
-  ∀b1 k p1 p2.
-    MEM (k,p1) b1 ∧ MEM (k,p2) b1 ∧ ALL_DISTINCT (MAP FST b1) ⇒ p1 = p2
-Proof
-  Induct \\ fs [FORALL_PROD] \\ rw []
-  \\ fs [MEM_MAP,EXISTS_PROD]
-  \\ res_tac \\ fs []
-QED
-
 Triviality EVERY_FLOOKUP_closed_lemma:
   EVERY (λe. freevars e ⊆ set (MAP FST ys)) (MAP SND ys) ⇒
   (∀n v.
@@ -262,12 +235,6 @@ Proof
   \\ res_tac \\ fs []
 QED
 
-Triviality FORALL_FRANGE: (* TODO: move *)
-  (∀x. x IN FRANGE v ⇒ p x) ⇔ ∀k x. FLOOKUP v k = SOME x ⇒ p x
-Proof
-  fs [FRANGE_DEF,FLOOKUP_DEF,PULL_EXISTS]
-QED
-
 Theorem ALOOKUP_REVERSE_LIST_REL:
   ∀bs ys.
     LIST_REL p (MAP SND bs) (MAP SND ys) ∧
@@ -285,42 +252,21 @@ Proof
   \\ metis_tac []
 QED
 
-Theorem MEM_LIST_REL: (* TODO: move *)
+Theorem MEM_LIST_REL[local]:
   ∀xs ys P y. LIST_REL P xs ys ∧ MEM y ys ⇒ ∃x. MEM x xs ∧ P x y
 Proof
-  Induct \\ fs [PULL_EXISTS]
-  \\ rw [] \\ fs [] \\ res_tac \\ fs []
-  \\ metis_tac []
+  metis_tac [LIST_REL_MEM_ALT]
 QED
 
-Theorem MEM_LIST_REL1: (* TODO: move *)
+Theorem MEM_LIST_REL1:
   ∀xs ys P x. LIST_REL P xs ys ∧ MEM x xs ⇒ ∃y. MEM y ys ∧ P x y
 Proof
-  Induct \\ fs [PULL_EXISTS]
-  \\ rw [] \\ fs [] \\ res_tac \\ fs []
-  \\ metis_tac []
-QED
-
-Theorem LIST_REL_COMP: (* TODO: move *)
-  ∀xs ys zs.
-    LIST_REL f xs ys ∧ LIST_REL g ys zs ⇒
-    LIST_REL (λx z. ∃y. f x y ∧ g y z) xs zs
-Proof
-  Induct \\ fs [PULL_EXISTS]
-  \\ metis_tac []
+  metis_tac [LIST_REL_MEM]
 QED
 
 Triviality eval_wh_Constructor_NIL_bisim =
   eval_wh_Constructor_bisim |> Q.GEN ‘xs’ |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) [];
 
-Triviality LIST_REL_IMP_MAP_EQ: (* TODO: move *)
-  ∀xs ys P f g.
-    (∀x y. MEM x xs ∧ MEM y ys ∧ P x y ⇒ f x = g y) ⇒
-    LIST_REL P xs ys ⇒ MAP g ys = MAP f xs
-Proof
-  Induct \\ fs [PULL_EXISTS,SF DNF_ss] \\ metis_tac []
-QED
-
 Theorem eval_forward_letrec_binds:
   ALL_DISTINCT (MAP FST binds2) ∧
   MAP FST binds1 = MAP FST binds2 ∧
@@ -811,27 +757,13 @@ Proof
   \\ irule_at Any eval_forward_letrec_binds
   \\ fs []
   \\ pop_assum kall_tac
-  \\ drule LIST_REL_opp \\ fs []
+  \\ pop_assum mp_tac \\ simp [Once LIST_REL_SWAP] \\ fs []
   \\ fs [UNCURRY,LAMBDA_PROD]
   \\ match_mp_tac LIST_REL_mono
   \\ fs [FORALL_PROD]
   \\ metis_tac [app_bisimilarity_sym]
 QED
 
-Triviality FST_LAM: (* TODO: move *)
-  FST = λ(p1,p2). p1
-Proof
-  fs [FUN_EQ_THM,FORALL_PROD]
-QED
-
-Triviality LIST_REL_MAP_CONG: (* TODO: move *)
-  ∀xs ys R Q f.
-    (∀x y. R x y ∧ MEM x xs ∧ MEM y ys ⇒ Q (f x) (f y)) ∧ LIST_REL R xs ys ⇒
-    LIST_REL Q (MAP f xs) (MAP f ys)
-Proof
-  Induct \\ fs [PULL_EXISTS] \\ metis_tac []
-QED
-
 Triviality LIST_REL_IMP_same_keys:
   ∀binds1 binds2.
     LIST_REL (λ(v1,e1) (v2,e2). v1 = v2) binds1 binds2 ⇒
@@ -860,7 +792,7 @@ Proof
    (rw [] \\ irule pure_exp_lemmasTheory.IMP_closed_bind \\ fs [])
   \\ rw [bind_def] \\ fs [subst_def,bind_def] \\ fs [SF SFY_ss]
   \\ irule exp_eq_Letrec_change_lemma
-  \\ gs [MAP_MAP_o,combinTheory.o_DEF,LAMBDA_PROD,GSYM FST_LAM]
+  \\ gs [MAP_MAP_o,combinTheory.o_DEF,LAMBDA_PROD,FST_INTRO]
   \\ conj_tac
   >-
    (irule LIST_REL_MAP_CONG \\ fs []