From 5b8fbcdb10deaa4df1422e584ea67d504df81901 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 4 Oct 2023 12:48:21 +0200
Subject: [PATCH 1/9] Move letrecs_distinct_def and Lets_def up

---
 .../proofs/pure_inline_cexpProofScript.sml    | 86 +++++++++----------
 .../passes/proofs/pure_letrecProofScript.sml  | 32 -------
 .../pure_letrec_spec_cexpProofScript.sml      | 24 +++---
 .../proofs/pure_to_thunkProofScript.sml       | 42 ++++-----
 language/pure_expScript.sml                   | 23 +++++
 meta-theory/pure_exp_lemmasScript.sml         | 12 +++
 6 files changed, 112 insertions(+), 107 deletions(-)

diff --git a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
index 38061514..18e93516 100644
--- a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
@@ -39,7 +39,7 @@ End
 Theorem Lets_append:
   ∀xs ys b. Lets (xs ++ ys) b = Lets xs (Lets ys b)
 Proof
-  Induct \\ fs [pure_letrecProofTheory.Lets_def,FORALL_PROD]
+  Induct \\ fs [pure_expTheory.Lets_def,FORALL_PROD]
 QED
 
 Theorem inline_list_empty:
@@ -378,7 +378,7 @@ Theorem exp_of_Lets:
     Lets (ZIP (MAP explode vs, MAP exp_of xs)) (exp_of b)
 Proof
   Induct \\ Cases_on ‘xs’
-  \\ gvs [pure_inline_cexpTheory.Lets_def,pure_letrecProofTheory.Lets_def]
+  \\ gvs [pure_inline_cexpTheory.Lets_def,pure_expTheory.Lets_def]
   \\ fs [exp_of_def]
 QED
 
@@ -392,9 +392,9 @@ Theorem subst_Lets:
 Proof
   Induct using SNOC_INDUCT
   \\ Cases_on ‘vs’ using SNOC_CASES
-  \\ fs [pure_letrecProofTheory.Lets_def]
+  \\ fs [pure_expTheory.Lets_def]
   \\ rw [] \\ gvs [ZIP_SNOC,MAP_SNOC]
-  \\ fs [SNOC_APPEND,Lets_append,pure_letrecProofTheory.Lets_def]
+  \\ fs [SNOC_APPEND,Lets_append,pure_expTheory.Lets_def]
   \\ last_x_assum $ DEP_REWRITE_TAC o single
   \\ fs [subst_def] \\ gvs [EVERY_MEM]
   \\ AP_TERM_TAC
@@ -412,10 +412,10 @@ Theorem eval_wh_Lets:
     eval_wh (subst (FEMPTY |++ xs) b)
 Proof
   Induct using SNOC_INDUCT
-  \\ fs [pure_letrecProofTheory.Lets_def,FUPDATE_LIST]
+  \\ fs [pure_expTheory.Lets_def,FUPDATE_LIST]
   \\ PairCases \\ fs [MAP_SNOC,EVERY_SNOC]
   \\ fs [SNOC_APPEND,Lets_append]
-  \\ fs [pure_letrecProofTheory.Lets_def,FUPDATE_LIST,subst_def]
+  \\ fs [pure_expTheory.Lets_def,FUPDATE_LIST,subst_def]
   \\ fs [eval_wh_App]
   \\ fs [eval_wh_Lam,bind_def,FLOOKUP_SIMP]
   \\ fs [FOLDL_APPEND] \\ rw []
@@ -465,9 +465,9 @@ Proof
   fs [freevars_Apps,freevars_Lams]
   \\ Induct using SNOC_INDUCT
   \\ Cases_on ‘vs’ using SNOC_CASES
-  \\ fs [pure_letrecProofTheory.Lets_def,EVERY_SNOC]
+  \\ fs [pure_expTheory.Lets_def,EVERY_SNOC]
   \\ gvs [ZIP_SNOC]
-  \\ fs [SNOC_APPEND,Lets_append,pure_letrecProofTheory.Lets_def] \\ rw []
+  \\ fs [SNOC_APPEND,Lets_append,pure_expTheory.Lets_def] \\ rw []
   \\ last_x_assum $ DEP_REWRITE_TAC o single \\ fs []
   \\ gvs [EVERY_MEM] \\ gvs [EXTENSION]
   \\ rw [] \\ eq_tac \\ rw [] \\ gvs [] \\ gvs [IN_DISJOINT]
@@ -483,9 +483,9 @@ Proof
   fs [boundvars_Apps,boundvars_Lams]
   \\ Induct using SNOC_INDUCT
   \\ Cases_on ‘vs’ using SNOC_CASES
-  \\ fs [pure_letrecProofTheory.Lets_def,EVERY_SNOC]
+  \\ fs [pure_expTheory.Lets_def,EVERY_SNOC]
   \\ gvs [ZIP_SNOC]
-  \\ fs [SNOC_APPEND,Lets_append,pure_letrecProofTheory.Lets_def] \\ rw []
+  \\ fs [SNOC_APPEND,Lets_append,pure_expTheory.Lets_def] \\ rw []
   \\ last_x_assum $ DEP_REWRITE_TAC o single \\ fs []
   \\ gvs [EVERY_MEM] \\ gvs [EXTENSION]
   \\ rw [] \\ eq_tac \\ rw [] \\ gvs [] \\ gvs [IN_DISJOINT]
@@ -533,7 +533,7 @@ Theorem letrecs_distinct_Apps[simp]:
       letrecs_distinct e ∧ EVERY letrecs_distinct es
 Proof
   Induct
-  \\ asm_rewrite_tac [Apps_def,EVERY_DEF,pure_letrecProofTheory.letrecs_distinct_def]
+  \\ asm_rewrite_tac [Apps_def,EVERY_DEF,pure_expTheory.letrecs_distinct_def]
   \\ rw [] \\ fs [] \\ eq_tac \\ rw [] \\ fs []
 QED
 
@@ -657,8 +657,8 @@ Theorem allvars_Lets:
                         BIGUNION (set (MAP allvars (MAP SND xs)))
 Proof
   Induct_on ‘xs’
-  \\ fs [pure_letrecProofTheory.Lets_def] \\ PairCases
-  \\ fs [pure_letrecProofTheory.Lets_def]
+  \\ fs [pure_expTheory.Lets_def] \\ PairCases
+  \\ fs [pure_expTheory.Lets_def]
   \\ gvs [EXTENSION] \\ rw [] \\ eq_tac \\ rw [] \\ gvs []
   \\ metis_tac []
 QED
@@ -1027,7 +1027,7 @@ Theorem letrecs_distinct_Lets:
 Proof
   Induct_on ‘xs’ \\ fs [Lets_def]
   \\ PairCases
-  \\ fs [Lets_def,pure_letrecProofTheory.letrecs_distinct_def,exp_of_def]
+  \\ fs [Lets_def,pure_expTheory.letrecs_distinct_def,exp_of_def]
   \\ gvs [AC CONJ_COMM CONJ_ASSOC]
 QED
 
@@ -1240,7 +1240,7 @@ Proof
        \\ rw [] \\ gvs []
        \\ gvs [AllCaseEqs()] \\ gvs []
        \\ gvs [cexp_wf_def,exp_of_def,
-               pure_letrecProofTheory.letrecs_distinct_def]
+               pure_expTheory.letrecs_distinct_def]
        \\ res_tac \\ fs []) >>
        drule $ cj 1 $ SRULE [fake_avoid_set_ok_def] inline_avoid_set_ok >> simp[] >>
        impl_tac >- metis_tac[wf_mem_IMP_mem_inv] >> strip_tac >>
@@ -1249,7 +1249,7 @@ Proof
        drule $ cj 1 inline_set_of >> impl_tac >- gvs[avoid_set_ok_def] >> strip_tac >>
        irule_at Any avoid_set_ok_subset >> rpt $ goal_assum $ drule_at Any
     \\ gvs [cexp_wf_def,exp_of_def,cns_arities_def,
-            pure_letrecProofTheory.letrecs_distinct_def]
+            pure_expTheory.letrecs_distinct_def]
     \\ gvs [SUBSET_DEF]
     \\ metis_tac []
     )
@@ -1263,7 +1263,7 @@ Proof
    (gvs [inline_def]
     \\ rpt (pairarg_tac \\ gvs [AllCaseEqs()])
     \\ gvs [SF ETA_ss,cexp_wf_def,exp_of_def,MAP_MAP_o,o_DEF,
-            pure_letrecProofTheory.letrecs_distinct_def,avoid_set_ok_Letrec]
+            pure_expTheory.letrecs_distinct_def,avoid_set_ok_Letrec]
     \\ gvs [LAMBDA_PROD,block_def]
     \\ dxrule LIST_REL_imp \\ strip_tac >>
     rev_drule $ cj 2 inline_set_of >> impl_tac >- gvs[avoid_set_ok_def] >> strip_tac
@@ -1321,7 +1321,7 @@ Proof
    (gvs [inline_def]
     \\ rpt (pairarg_tac \\ gvs [AllCaseEqs()])
     \\ gvs [block_def,cexp_wf_def,exp_of_def,SF ETA_ss,avoid_set_ok_Prim,
-            pure_letrecProofTheory.letrecs_distinct_def] >>
+            pure_expTheory.letrecs_distinct_def] >>
        drule $ cj 2 inline_set_of >> strip_tac >> simp[]
     \\ dxrule LIST_REL_imp \\ strip_tac
     \\ gvs [cns_arities_def]
@@ -1330,7 +1330,7 @@ Proof
    (gvs [inline_def]
     \\ rpt (pairarg_tac \\ gvs [])
     \\ gvs [block_def,cexp_wf_def,SF ETA_ss,exp_of_def,
-            pure_letrecProofTheory.letrecs_distinct_def]
+            pure_expTheory.letrecs_distinct_def]
     \\ ‘MAP (λ(v,vs,e). e) bs = MAP (SND ∘ SND) bs’ by
       (qid_spec_tac ‘bs’ \\ Induct \\ gvs [FORALL_PROD])
     \\ gvs []
@@ -1360,7 +1360,7 @@ Proof
        \\ rpt (pop_assum kall_tac)
        \\ Induct \\ Cases_on ‘bs2’ \\ gvs []
        \\ PairCases \\ gvs [])
-    \\ gvs [pure_letrecProofTheory.letrecs_distinct_def,freevars_rows_of] >>
+    \\ gvs [pure_expTheory.letrecs_distinct_def,freevars_rows_of] >>
        `wf_mem ns1 m ∧ wf_mem ns2 m` by (
           irule_at Any wf_mem_subset >> rpt $ goal_assum $ drule_at Any >>
           irule_at Any wf_mem_subset >> rpt $ goal_assum $ drule_at Any >>
@@ -1513,8 +1513,8 @@ Theorem boundvars_Lets:
   boundvars (Lets binds e) =
     set (MAP FST binds) ∪ BIGUNION (set $ MAP (boundvars o SND) binds) ∪ boundvars e
 Proof
-  Induct_on `binds` >> rw[pure_letrecProofTheory.Lets_def] >>
-  PairCases_on `h` >> gvs[pure_letrecProofTheory.Lets_def] >>
+  Induct_on `binds` >> rw[pure_expTheory.Lets_def] >>
+  PairCases_on `h` >> gvs[pure_expTheory.Lets_def] >>
   rw[EXTENSION] >> metis_tac[]
 QED
 
@@ -1522,8 +1522,8 @@ Theorem allvars_Lets:
   allvars (Lets binds e) =
     set (MAP FST binds) ∪ BIGUNION (set $ MAP (allvars o SND) binds) ∪ allvars e
 Proof
-  Induct_on `binds` >> rw[pure_letrecProofTheory.Lets_def] >>
-  PairCases_on `h` >> gvs[pure_letrecProofTheory.Lets_def] >>
+  Induct_on `binds` >> rw[pure_expTheory.Lets_def] >>
+  PairCases_on `h` >> gvs[pure_expTheory.Lets_def] >>
   rw[EXTENSION] >> metis_tac[]
 QED
 
@@ -1534,8 +1534,8 @@ Theorem unique_boundvars_Lets:
     ALL_DISTINCT (MAP FST binds) ∧
     list_disjoint (set (MAP FST binds) :: boundvars e :: MAP (boundvars o SND) binds)
 Proof
-  Induct_on `binds` >> rw[unique_boundvars_def, pure_letrecProofTheory.Lets_def] >>
-  PairCases_on `h` >> gvs[pure_letrecProofTheory.Lets_def] >>
+  Induct_on `binds` >> rw[unique_boundvars_def, pure_expTheory.Lets_def] >>
+  PairCases_on `h` >> gvs[pure_expTheory.Lets_def] >>
   simp[unique_boundvars_def, list_disjoint_cons, boundvars_Lets] >>
   eq_tac >> rw[] >> gvs[]
   >- (gvs[EVERY_MEM] >> metis_tac[DISJOINT_SYM])
@@ -1550,8 +1550,8 @@ Theorem freevars_Lets_SUBSET:
     (freevars e DIFF set (MAP FST binds)) ∪
       BIGUNION (set $ MAP (freevars o SND) binds)
 Proof
-  Induct_on `binds` >> rw[pure_letrecProofTheory.Lets_def] >>
-  PairCases_on `h` >> gvs[pure_letrecProofTheory.Lets_def] >>
+  Induct_on `binds` >> rw[pure_expTheory.Lets_def] >>
+  PairCases_on `h` >> gvs[pure_expTheory.Lets_def] >>
   gvs[SUBSET_DEF] >> metis_tac[]
 QED
 
@@ -1672,8 +1672,8 @@ Theorem letrecs_distinct_Lets:
     letrecs_distinct (Lets (ZIP (vs,xs)) x)
 Proof
   Induct \\ Cases_on ‘xs’
-  \\ fs [pure_letrecProofTheory.Lets_def] \\ rw []
-  \\ fs [pure_letrecProofTheory.letrecs_distinct_def]
+  \\ fs [pure_expTheory.Lets_def] \\ rw []
+  \\ fs [pure_expTheory.letrecs_distinct_def]
 QED
 
 Theorem NestedCase_free_SmartApp:
@@ -1801,7 +1801,7 @@ Triviality if_lemma:
   letrecs_distinct (if b then Seq Fail x else x) = letrecs_distinct x
 Proof
   Cases_on ‘b’ \\ gvs []
-  \\ gvs [pure_letrecProofTheory.letrecs_distinct_def] \\ rw []
+  \\ gvs [pure_expTheory.letrecs_distinct_def] \\ rw []
 QED
 
 Theorem list_subst_rel_if_lemma:
@@ -1894,7 +1894,7 @@ Proof
       \\ last_x_assum $ irule_at Any
       \\ last_x_assum $ irule_at Any
       \\ fs [EVERY_MAP,DISJOINT_SYM,cexp_wf_def]
-      \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def]
+      \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def]
       \\ imp_res_tac avoid_set_ok_imp_vars_ok \\ fs []
       \\ imp_res_tac inline_set_of \\ fs []
       \\ irule_at Any avoid_set_ok_subset \\ fs []
@@ -1912,7 +1912,7 @@ Proof
       \\ last_x_assum $ irule_at Any
       \\ gvs [memory_inv_def,DISJOINT_SYM]
       \\ fs [EVERY_MAP,DISJOINT_SYM,cexp_wf_def]
-      \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def,FORALL_PROD]
+      \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def,FORALL_PROD]
       \\ imp_res_tac avoid_set_ok_imp_vars_ok \\ fs []
       \\ imp_res_tac inline_set_of \\ fs []
       \\ irule_at Any avoid_set_ok_subset \\ fs []
@@ -1934,7 +1934,7 @@ Proof
       \\ last_x_assum $ irule_at Any
       \\ gvs [memory_inv_def,DISJOINT_SYM]
       \\ fs [EVERY_MAP,DISJOINT_SYM,cexp_wf_def]
-      \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def]
+      \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def]
       \\ imp_res_tac avoid_set_ok_imp_vars_ok \\ fs []
       \\ imp_res_tac inline_set_of \\ fs []
       \\ irule_at Any avoid_set_ok_subset \\ fs []
@@ -1957,7 +1957,7 @@ Proof
       \\ fs [EVERY_MAP,DISJOINT_SYM]
       \\ irule_at Any list_subst_rel_refl
       \\ fs [EVERY_MAP,DISJOINT_SYM,cexp_wf_def]
-      \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def]
+      \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def]
     )
     \\ gvs []
     \\ rename [`inline _ _ _ _ _ = (q_inline, r_inline)`]
@@ -1971,7 +1971,7 @@ Proof
       \\ fs [EVERY_MAP,DISJOINT_SYM]
       \\ irule_at Any list_subst_rel_refl
       \\ fs [EVERY_MAP,DISJOINT_SYM,cexp_wf_def]
-      \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def]
+      \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def]
     )
     \\ gvs []
     \\ Cases_on ‘e’ \\ gvs [get_Var_name_def,exp_of_def]
@@ -2115,7 +2115,7 @@ Proof
     gvs [inline_def]
     \\ rpt (pairarg_tac \\ gvs [])
     \\ gvs [exp_of_def]
-    \\ fs [cexp_wf_def,pure_letrecProofTheory.letrecs_distinct_def]
+    \\ fs [cexp_wf_def,pure_expTheory.letrecs_distinct_def]
     \\ ‘avoid_set_ok ns e1 ∧ avoid_set_ok ns e2’ by
           (fs [avoid_set_ok_def,exp_of_def] \\ metis_tac [])
     \\ fs [heuristic_insert_def]
@@ -2125,7 +2125,7 @@ Proof
       \\ conj_tac
       >- (
         last_x_assum irule
-        \\ fs [cexp_wf_def,pure_letrecProofTheory.letrecs_distinct_def]
+        \\ fs [cexp_wf_def,pure_expTheory.letrecs_distinct_def]
         \\ fs [DISJOINT_SYM,memory_inv_def]
       )
       \\ last_x_assum irule
@@ -2166,7 +2166,7 @@ Proof
     gvs [inline_def]
     \\ rpt (pairarg_tac \\ gvs [])
     \\ gvs [list_subst_rel_refl,exp_of_def]
-    \\ fs [pure_letrecProofTheory.letrecs_distinct_def]
+    \\ fs [pure_expTheory.letrecs_distinct_def]
     \\ ‘avoid_set_ok ns e ∧ EVERY (avoid_set_ok ns o SND) vbs’ by
       (fs [avoid_set_ok_def,EVERY_MEM,exp_of_def,MEM_MAP,PULL_EXISTS,
            FORALL_PROD,EXISTS_PROD] \\ metis_tac [])
@@ -2272,7 +2272,7 @@ Proof
     \\ fs [LIST_REL_MAP,o_DEF,FORALL_PROD,LIST_REL_MAP2,PULL_EXISTS]
     \\ last_x_assum irule
     \\ fs [EVERY_MEM,cexp_wf_def,
-           pure_letrecProofTheory.letrecs_distinct_def,MEM_MAP,PULL_EXISTS]
+           pure_expTheory.letrecs_distinct_def,MEM_MAP,PULL_EXISTS]
     \\ rw []
     \\ fs [avoid_set_ok_def,exp_of_def,MEM_MAP,PULL_EXISTS]
     \\ metis_tac []
@@ -2425,7 +2425,7 @@ Proof
     \\ reverse conj_tac
     >-
      (first_x_assum irule \\ fs []
-      \\ gvs [cexp_wf_def,pure_letrecProofTheory.letrecs_distinct_def]
+      \\ gvs [cexp_wf_def,pure_expTheory.letrecs_distinct_def]
       \\ simp [DISJOINT_SYM]
       \\ first_x_assum (fn th => mp_tac th \\ match_mp_tac avoid_set_ok_subset_exp)
       \\ gvs [allvars_def,exp_of_def]
@@ -2456,7 +2456,7 @@ Proof
       \\ irule_at Any list_subst_rel_Prim \\ fs []
       \\ pairarg_tac \\ gvs [list_subst_rel_refl]
       \\ last_x_assum irule \\ fs []
-      \\ gvs [pure_letrecProofTheory.letrecs_distinct_def,
+      \\ gvs [pure_expTheory.letrecs_distinct_def,
               letrecs_distinct_rows_of,cexp_wf_def]
       \\ simp [DISJOINT_SYM]
       \\ ‘avoid_set_ok ns x1’ by
@@ -2494,7 +2494,7 @@ Proof
     \\ simp [LAMBDA_PROD] \\ gvs []
     \\ gvs [EVERY_MEM,FORALL_PROD]
     \\ simp [DISJOINT_SYM,SF SFY_ss]
-    \\ gvs [pure_letrecProofTheory.letrecs_distinct_def,
+    \\ gvs [pure_expTheory.letrecs_distinct_def,
             letrecs_distinct_rows_of,cexp_wf_def]
     \\ conj_tac >- metis_tac [avoid_set_ok_subset,SUBSET_DEF]
     \\ reverse conj_tac >- metis_tac [avoid_set_ok_subset,SUBSET_DEF]
diff --git a/compiler/backend/passes/proofs/pure_letrecProofScript.sml b/compiler/backend/passes/proofs/pure_letrecProofScript.sml
index 1fe0becc..943311ac 100644
--- a/compiler/backend/passes/proofs/pure_letrecProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrecProofScript.sml
@@ -65,33 +65,6 @@ Proof
   gvs[Once (GSYM MEM_MAP_FST_make_distinct)]
 QED
 
-Definition letrecs_distinct_def:
-  (letrecs_distinct (pure_exp$Letrec xs y) ⇔
-    ALL_DISTINCT (MAP FST xs) ∧
-    EVERY letrecs_distinct (MAP SND xs) ∧
-    letrecs_distinct y) ∧
-  (letrecs_distinct (Lam n x) ⇔ letrecs_distinct x) ∧
-  (letrecs_distinct (Prim p xs) ⇔ EVERY letrecs_distinct xs) ∧
-  (letrecs_distinct (App x y) ⇔ letrecs_distinct x ∧ letrecs_distinct y) ∧
-  (letrecs_distinct _ ⇔ T)
-Termination
-  WF_REL_TAC `measure (λe. exp_size e)` >> rw[exp_size_def] >>
-  Induct_on `xs` >> rw[] >> gvs[exp_size_def] >>
-  PairCases_on `h` >> gvs[exp_size_def]
-End
-
-Theorem letrecs_distinct_Apps:
-  ∀l e. letrecs_distinct (Apps e l) ⇔ letrecs_distinct e ∧ EVERY letrecs_distinct l
-Proof
-  Induct \\ gs [letrecs_distinct_def, Apps_def, GSYM CONJ_ASSOC]
-QED
-
-Theorem letrecs_distinct_Lams:
-  ∀l e. letrecs_distinct (Lams l e) ⇔ letrecs_distinct e
-Proof
-  Induct \\ gs [letrecs_distinct_def, Lams_def]
-QED
-
 Theorem letrecs_distinct_lets_for:
   ∀l m n e. letrecs_distinct (lets_for m n l e) ⇔ letrecs_distinct e
 Proof
@@ -193,11 +166,6 @@ Definition valid_split_def:
     DISJOINT (set (MAP FST xs2)) (BIGUNION (set (MAP (λ(_,e). freevars e) xs1)))
 End
 
-Definition Lets_def:
-  Lets [] b = b ∧
-  Lets ((v,x)::xs) b = Let v x (Lets xs b)
-End
-
 Inductive letrec_rel:
   (∀n.
     letrec_rel c (Var n) (Var n))
diff --git a/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml
index 81c9fcb4..d830fc09 100644
--- a/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrec_spec_cexpProofScript.sml
@@ -47,7 +47,7 @@ Theorem letrecs_distinct_Lams:
   ∀vs e. letrecs_distinct (Lams vs e) ⇔ letrecs_distinct e
 Proof
   Induct \\ fs [Lams_def]
-  \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def]
+  \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def]
 QED
 
 Theorem letrecs_distinct_Apps:
@@ -55,7 +55,7 @@ Theorem letrecs_distinct_Apps:
          letrecs_distinct e ∧ EVERY letrecs_distinct es
 Proof
   Induct \\ fs [Apps_def]
-  \\ fs [EVERY_MEM,pure_letrecProofTheory.letrecs_distinct_def]
+  \\ fs [EVERY_MEM,pure_expTheory.letrecs_distinct_def]
   \\ metis_tac []
 QED
 
@@ -476,7 +476,7 @@ QED
 Theorem letrecs_distinct_if:
   letrecs_distinct (if b then Seq Fail x else x) = letrecs_distinct x
 Proof
-  rw [pure_letrecProofTheory.letrecs_distinct_def]
+  rw [pure_expTheory.letrecs_distinct_def]
 QED
 
 Triviality UNCURRY_lemma:
@@ -501,7 +501,7 @@ Proof
   \\ gen_tac \\ strip_tac \\ first_x_assum drule \\ strip_tac \\ gvs []
   \\ Cases_on ‘h’ \\ gvs [eq_Var_def,exp_of_def]
   \\ gvs [cns_arities_def]
-  \\ gvs [pure_letrecProofTheory.letrecs_distinct_def]
+  \\ gvs [pure_expTheory.letrecs_distinct_def]
 QED
 
 Theorem spec_one_vars:
@@ -619,7 +619,7 @@ Proof
       \\ gvs [SUBSET_DEF])
     \\ gvs [cns_arities_def,cexp_wf_def,SF ETA_ss,
             letrecs_distinct_Lams,letrecs_distinct_Apps,
-            pure_letrecProofTheory.letrecs_distinct_def]
+            pure_expTheory.letrecs_distinct_def]
     \\ gvs [SF SFY_ss,delete_with_wf]
     \\ gvs [EVERY_MAP])
   >~ [‘Apps’] >-
@@ -632,14 +632,14 @@ Proof
     \\ gvs [cns_arities_def,SF ETA_ss,letrecs_distinct_Lams])
   >~ [‘Let’] >-
    (gvs [SUBSET_DEF,cexp_wf_def,cns_arities_def,
-         pure_letrecProofTheory.letrecs_distinct_def])
+         pure_expTheory.letrecs_distinct_def])
   >~ [‘Prim’] >-
    (gvs [SUBSET_DEF,cexp_wf_def,cns_arities_def,EVERY_MAP,SF ETA_ss,
-         pure_letrecProofTheory.letrecs_distinct_def])
+         pure_expTheory.letrecs_distinct_def])
   >~ [‘Letrec’] >-
    (fs [MAP_MAP_o,combinTheory.o_DEF] \\ fs [LAMBDA_PROD]
     \\ gvs [SUBSET_DEF,cexp_wf_def,cns_arities_def,EVERY_MAP,SF ETA_ss,
-            pure_letrecProofTheory.letrecs_distinct_def]
+            pure_expTheory.letrecs_distinct_def]
     \\ rpt (pop_assum mp_tac)
     \\ rewrite_tac [EXTENSION,SUBSET_DEF]
     \\ rpt strip_tac
@@ -664,7 +664,7 @@ Proof
         \\ DISJ2_TAC
         \\ first_x_assum irule
         \\ metis_tac [])
-    \\ gvs [pure_letrecProofTheory.letrecs_distinct_def,
+    \\ gvs [pure_expTheory.letrecs_distinct_def,
             letrecs_distinct_rows_of,EVERY_MAP]
     \\ gvs [UNCURRY_lemma]
     \\ gvs [LAMBDA_PROD]
@@ -673,7 +673,7 @@ Proof
   >- fs [SUBSET_DEF]
   >- fs [SUBSET_DEF,rows_of_def]
   >- (fs [IfDisj_def] \\ fs [SUBSET_DEF]
-      \\ gvs [pure_letrecProofTheory.letrecs_distinct_def])
+      \\ gvs [pure_expTheory.letrecs_distinct_def])
 QED
 
 Triviality can_spec_arg_map:
@@ -969,8 +969,8 @@ Proof
   \\ drule specialise_each_vars \\ strip_tac \\ gvs [cexp_wf_def]
   \\ drule drop_common_suffix_thm \\ strip_tac \\ gvs [exp_of_def]
   \\ gvs [letrecs_distinct_Lams,set_map_empty,letrecs_distinct_Apps,
-          pure_letrecProofTheory.letrecs_distinct_def]
-  \\ gvs [EVERY_MAP,pure_letrecProofTheory.letrecs_distinct_def,
+          pure_expTheory.letrecs_distinct_def]
+  \\ gvs [EVERY_MAP,pure_expTheory.letrecs_distinct_def,
           set_sing_lemma,boundvars_Lams]
   \\ imp_res_tac specialise_each_subset \\ fs []
   \\ rewrite_tac [GSYM DIFF_UNION]
diff --git a/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
index ee62d9ee..761b1802 100644
--- a/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunkProofScript.sml
@@ -6,7 +6,7 @@ open HolKernel Parse boolLib bossLib term_tactic monadsyntax dep_rewrite;
 open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
      finite_mapTheory pred_setTheory rich_listTheory arithmeticTheory combinTheory
      pure_semanticsTheory thunkLangTheory thunk_semanticsTheory pure_evalTheory
-     thunkLang_primitivesTheory pure_exp_lemmasTheory pure_miscTheory
+     thunkLang_primitivesTheory pure_exp_lemmasTheory pure_miscTheory pure_expTheory
      pure_to_thunk_2ProofTheory pure_cexpTheory pureLangTheory thunk_cexpTheory
      var_setTheory pure_namesTheory pure_namesProofTheory pure_to_thunkTheory
      thunk_split_Delay_LamTheory thunk_split_Delay_LamProofTheory pure_letrecProofTheory;
@@ -44,10 +44,12 @@ Proof
 QED
 
 Theorem boundvars_lets_for:
-  ∀list constr len w e. boundvars (lets_for len constr w list e)
-                                  ⊆ {w} ∪ (set (MAP SND list)) ∪ boundvars e
+  ∀list constr len w e.
+    thunkLang$boundvars (lets_for len constr w list e)
+    ⊆ {w} ∪ (set (MAP SND list)) ∪ boundvars e
 Proof
-  Induct \\ gs [thunk_exp_ofTheory.lets_for_def, FORALL_PROD, boundvars_def]
+  Induct
+  \\ gs [thunk_exp_ofTheory.lets_for_def, FORALL_PROD, thunkLangTheory.boundvars_def]
   \\ rw []
   \\ irule SUBSET_TRANS
   \\ last_x_assum $ irule_at Any
@@ -58,7 +60,8 @@ Theorem boundvars_rows_of_NONE:
   ∀rows w. boundvars (thunk_exp_of$rows_of w rows NONE) ⊆ {w} ∪ BIGUNION (set (MAP (set o FST o SND) rows))
                      ∪ BIGUNION (set (MAP (boundvars o SND o SND) rows))
 Proof
-  Induct \\ gs [FORALL_PROD, thunk_exp_ofTheory.rows_of_def, boundvars_def]
+  Induct
+  \\ gs [FORALL_PROD, thunk_exp_ofTheory.rows_of_def, thunkLangTheory.boundvars_def]
   \\ rw []
   >- (irule SUBSET_TRANS
       \\ irule_at Any boundvars_lets_for
@@ -76,7 +79,9 @@ Theorem boundvars_rows_of_SOME:
                      ∪ BIGUNION (set (MAP (boundvars o SND o SND) rows))
                      ∪ boundvars e
 Proof
-  Induct \\ gs [FORALL_PROD, thunk_exp_ofTheory.rows_of_def, boundvars_def, boundvars_Disj]
+  Induct
+  \\ gs [FORALL_PROD, thunk_exp_ofTheory.rows_of_def,
+         thunkLangTheory.boundvars_def, boundvars_Disj]
   \\ rw []
   >- (irule SUBSET_TRANS
       \\ irule_at Any boundvars_lets_for
@@ -122,9 +127,9 @@ QED
 Theorem boundvars_exp_of_mk_delay:
   ∀e flag. boundvars (exp_of (mk_delay flag e)) = boundvars (exp_of e)
 Proof
-  Cases \\ simp [mk_delay_def, Once exp_of_def, boundvars_def]
-  \\ CASE_TAC \\ simp [exp_of_def, boundvars_def]
-  \\ Cases \\ simp[exp_of_def, boundvars_def]
+  Cases \\ simp [mk_delay_def, Once exp_of_def, thunkLangTheory.boundvars_def]
+  \\ CASE_TAC \\ simp [exp_of_def, thunkLangTheory.boundvars_def]
+  \\ Cases \\ simp[exp_of_def, thunkLangTheory.boundvars_def]
 QED
 
 Theorem cexp_wf_mk_delay:
@@ -187,7 +192,7 @@ Proof
   \\ rpt (pairarg_tac \\ fs [])
   \\ TRY strip_tac
   \\ rpt BasicProvers.var_eq_tac
-  \\ fs [cexp_wf_def, boundvars_def, thunk_exp_ofTheory.cexp_wf_def,
+  \\ fs [cexp_wf_def, thunkLangTheory.boundvars_def, thunk_exp_ofTheory.cexp_wf_def,
          exp_of_def, letrecs_distinct_def, letrecs_distinct_Lams, letrecs_distinct_Apps,
          thunk_cexpTheory.cns_arities_def, pure_cexpTheory.cns_arities_def]
   >~ [‘exp_rel (Var _ _)’] >-
@@ -253,7 +258,7 @@ Proof
     \\ irule_at (Pos hd) SUBSET_TRANS
     \\ first_assum $ irule_at $ Pos hd \\ fs []
     \\ conj_tac
-    \\ simp [SUBSET_DEF, PULL_EXISTS, boundvars_def, MEM_EL]
+    \\ simp [SUBSET_DEF, PULL_EXISTS, thunkLangTheory.boundvars_def, MEM_EL]
     \\ rpt $ gen_tac \\ strip_tac
     \\ gs [EVERY_EL, EL_MAP2, SUBSET_DEF]
     >- first_x_assum $ dxrule_all_then irule
@@ -321,7 +326,7 @@ Proof
           \\ drule freevars_IMP_allvars
           \\ strip_tac
           \\ metis_tac [])
-      \\ simp [boundvars_def, boundvars_exp_of_mk_delay, GSYM CONJ_ASSOC]
+      \\ simp [thunkLangTheory.boundvars_def, boundvars_exp_of_mk_delay, GSYM CONJ_ASSOC]
       \\ conj_tac
       >- gs [SUBSET_DEF]
       \\ conj_tac
@@ -432,7 +437,7 @@ Proof
         \\ imp_res_tac freevars_IMP_allvars \\ fs []
         \\ fs [SUBSET_DEF]
         \\ metis_tac [])
-    \\ simp [boundvars_def, boundvars_exp_of_mk_delay]
+    \\ simp [thunkLangTheory.boundvars_def, boundvars_exp_of_mk_delay]
     \\ conj_tac
     >- (simp [GSYM CONJ_ASSOC]
         \\ conj_tac
@@ -529,10 +534,8 @@ Proof
     \\ simp [cns_arities_mk_delay]
     \\ gs [SUBSET_DEF])
   >~ [‘Prim c p xs’] >-
-
    (Cases_on ‘p’
     >~ [‘Cons m’] >-
-
      (gvs []
       \\ Cases_on ‘mop_of_mlstring m’ \\ gvs []
       >-
@@ -540,8 +543,8 @@ Proof
         \\ irule_at Any exp_rel_Cons \\ gvs []
         \\ qpat_x_assum ‘_ ⇒ _’ mp_tac \\ impl_tac
         >- fs [EVERY_MEM,SUBSET_DEF,PULL_EXISTS,MEM_MAP,PULL_FORALL,SF SFY_ss]
-        \\ strip_tac \\ fs [boundvars_def]
-        \\ fs [BIGUNION_SUBSET, EVERY_MEM, MEM_MAP, PULL_EXISTS, boundvars_def]
+        \\ strip_tac \\ fs [thunkLangTheory.boundvars_def]
+        \\ fs [BIGUNION_SUBSET, EVERY_MEM, MEM_MAP, PULL_EXISTS, thunkLangTheory.boundvars_def]
         \\ conj_tac
         >-
          (gvs [LIST_REL_MAP_ALT, SF ETA_ss]
@@ -569,7 +572,6 @@ Proof
       \\ qpat_x_assum ‘mop_of_mlstring m = SOME x’ mp_tac
       \\ simp [mop_of_mlstring_def,AllCaseEqs()]
       \\ strip_tac \\ gvs [pure_configTheory.num_monad_args_def]
-
       \\ gvs [LENGTH_EQ_NUM_compute,monad_to_thunk_def,cns_arities_def,
               thunkLangTheory.boundvars_def,cexp_wf_mk_delay,cns_arities_mk_delay,
               thunk_exp_ofTheory.cexp_wf_def,pure_configTheory.num_mop_args_def,
@@ -591,7 +593,7 @@ Proof
       \\ qpat_x_assum ‘_ ⇒ _’ mp_tac \\ impl_tac
       >- fs [EVERY_MEM,SUBSET_DEF,PULL_EXISTS,MEM_MAP,PULL_FORALL,SF SFY_ss]
       \\ strip_tac \\ fs [thunk_exp_ofTheory.cexp_wf_def, SF ETA_ss]
-      \\ fs [BIGUNION_SUBSET, EVERY_MEM, MEM_MAP, PULL_EXISTS, boundvars_def]
+      \\ fs [BIGUNION_SUBSET, EVERY_MEM, MEM_MAP, PULL_EXISTS, thunkLangTheory.boundvars_def]
       \\ conj_tac
       >- (drule_then assume_tac LIST_REL_LENGTH
           \\ Cases_on ‘a’
@@ -625,7 +627,7 @@ Proof
         \\ strip_tac
         \\ metis_tac [])
     \\ conj_tac
-    >- (simp [boundvars_def]
+    >- (simp [thunkLangTheory.boundvars_def]
         \\ rw [] \\ gs [])
     \\ simp [thunk_cexpTheory.cns_arities_def]
     \\ rw []
diff --git a/language/pure_expScript.sml b/language/pure_expScript.sml
index 1f4943f5..5019b534 100644
--- a/language/pure_expScript.sml
+++ b/language/pure_expScript.sml
@@ -26,7 +26,10 @@ Datatype:
       | Letrec ((vname # exp) list) exp   (* mutually recursive exps  *)
 End
 
+val exp_size_def = fetch "-" "exp_size_def";
+
 (* some abbreviations *)
+
 Overload Let  = “λs x y. App (Lam s y) x”         (* let-expression    *)
 Overload If   = “λx y z. Prim If [x; y; z]”       (* If   at exp level *)
 Overload Cons = “λs. Prim (Cons s)”               (* Cons at exp level *)
@@ -52,6 +55,11 @@ Definition Seqs_def[simp]: (* TODO: move *)
   Seqs (y::ys) x = Seq y (Seqs ys x)
 End
 
+Definition Lets_def:
+  Lets [] b = b ∧
+  Lets ((v,x)::xs) b = Let v x (Lets xs b)
+End
+
 Definition Bottom_def:
   Bottom = Letrec [("bot",Var "bot")] (Var "bot")
 End
@@ -182,4 +190,19 @@ End
 
 Overload Case = “λx nm css. expandCases x nm css”
 
+Definition letrecs_distinct_def:
+  (letrecs_distinct (pure_exp$Letrec xs y) ⇔
+    ALL_DISTINCT (MAP FST xs) ∧
+    EVERY letrecs_distinct (MAP SND xs) ∧
+    letrecs_distinct y) ∧
+  (letrecs_distinct (Lam n x) ⇔ letrecs_distinct x) ∧
+  (letrecs_distinct (Prim p xs) ⇔ EVERY letrecs_distinct xs) ∧
+  (letrecs_distinct (App x y) ⇔ letrecs_distinct x ∧ letrecs_distinct y) ∧
+  (letrecs_distinct _ ⇔ T)
+Termination
+  WF_REL_TAC `measure (λe. exp_size e)` >> rw[exp_size_def] >>
+  Induct_on `xs` >> rw[] >> gvs[exp_size_def] >>
+  PairCases_on `h` >> gvs[exp_size_def]
+End
+
 val _ = export_theory ();
diff --git a/meta-theory/pure_exp_lemmasScript.sml b/meta-theory/pure_exp_lemmasScript.sml
index 15c274b6..3885d359 100644
--- a/meta-theory/pure_exp_lemmasScript.sml
+++ b/meta-theory/pure_exp_lemmasScript.sml
@@ -975,6 +975,18 @@ Proof
   Induct \\ fs [Apps_def,subst_def]
 QED
 
+Theorem letrecs_distinct_Apps:
+  ∀l e. letrecs_distinct (Apps e l) ⇔ letrecs_distinct e ∧ EVERY letrecs_distinct l
+Proof
+  Induct \\ gs [letrecs_distinct_def, Apps_def, GSYM CONJ_ASSOC]
+QED
+
+Theorem letrecs_distinct_Lams:
+  ∀l e. letrecs_distinct (Lams l e) ⇔ letrecs_distinct e
+Proof
+  Induct \\ gs [letrecs_distinct_def, Lams_def]
+QED
+
 Theorem ignore_FDIFF:
   DISJOINT f (FDOM m) ⇒ FDIFF m f = m
 Proof

From a25d9b63345f653ef25dd2f196391b84d450a0d2 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 4 Oct 2023 15:45:06 +0200
Subject: [PATCH 2/9] Make letrecs_distinct_def into an automatic simp

---
 .../pure_demands_analysisProofScript.sml      | 82 +++++++++----------
 .../passes/proofs/pure_letrecProofScript.sml  | 11 +--
 language/pure_expScript.sml                   |  2 +-
 3 files changed, 47 insertions(+), 48 deletions(-)

diff --git a/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml b/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
index 380884b2..14273235 100644
--- a/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_demands_analysisProofScript.sml
@@ -3384,27 +3384,27 @@ Proof
           \\ unabbrev_all_tac \\ gvs [ctxt_trans_def, FOLDL_delete_ok]
           \\ rpt $ last_x_assum $ drule_then assume_tac \\ gs [])
       >- (rw [letrecs_distinct_def]
-          >- (gs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
-              \\ irule ALL_DISTINCT_IMP
-              \\ gs [MAP_ZIP, ALL_DISTINCT_IMP2])
-          >- (gs [EVERY_EL, EL_MAP, EL_ZIP] \\ rw [FST_THM, SND_THM]
-              \\ pairarg_tac \\ gs []
-              \\ pairarg_tac \\ gs []
-              \\ pairarg_tac \\ gs []
-              \\ rename1 ‘i < _’
-              \\ last_x_assum $ qspecl_then [‘cexp_size f (SND (EL i binds))’] assume_tac
-              \\ ‘cexp_size f (SND (EL i binds)) < cexp7_size f binds’
-                by (assume_tac cexp_size_lemma \\ gvs [] \\ first_x_assum irule
+          \\ gs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
+          \\ irule ALL_DISTINCT_IMP
+          \\ gs [MAP_ZIP, ALL_DISTINCT_IMP2])
+      >- (gs [EVERY_EL, EL_MAP, EL_ZIP] \\ rw [FST_THM, SND_THM]
+          \\ pairarg_tac \\ gs []
+          \\ pairarg_tac \\ gs []
+          \\ pairarg_tac \\ gs []
+          \\ rename1 ‘i < _’
+          \\ last_x_assum $ qspecl_then [‘cexp_size f (SND (EL i binds))’] assume_tac
+          \\ ‘cexp_size f (SND (EL i binds)) < cexp7_size f binds’
+            by (assume_tac cexp_size_lemma \\ gvs [] \\ first_x_assum irule
                 \\ gvs [MEM_EL] \\ first_assum $ irule_at Any
-                    \\ simp [])
-              \\ gvs [] \\ pop_assum kall_tac
-              \\ first_x_assum $ resolve_then (Pos hd) (drule_then assume_tac) EQ_REFL
-              \\ gs [FOLDL_delete_ok]
-              \\ last_x_assum $ drule_then assume_tac
-              \\ last_x_assum $ drule_then assume_tac
-              \\ last_x_assum $ drule_then assume_tac
-              \\ gs [])
-          >- gs [letrecs_distinct_adds_demands])
+                \\ simp [])
+          \\ gvs [] \\ pop_assum kall_tac
+          \\ first_x_assum $ resolve_then (Pos hd) (drule_then assume_tac) EQ_REFL
+          \\ gs [FOLDL_delete_ok]
+          \\ last_x_assum $ drule_then assume_tac
+          \\ last_x_assum $ drule_then assume_tac
+          \\ last_x_assum $ drule_then assume_tac
+          \\ gs [])
+      >- gs [letrecs_distinct_adds_demands]
       >- (last_x_assum $ qspecl_then [‘cexp_size f (SND (EL i binds))’] assume_tac
           \\ ‘cexp_size f (SND (EL i binds)) < cexp7_size f binds’
             by (assume_tac cexp_size_lemma \\ gvs [] \\ first_x_assum irule
@@ -3439,30 +3439,28 @@ Proof
           \\ qabbrev_tac ‘pair = EL i binds’ \\ PairCases_on ‘pair’ \\ gvs []
           \\ unabbrev_all_tac \\ gvs [ctxt_trans_def, FOLDL_delete_ok]
           \\ rpt $ last_x_assum $ drule_then assume_tac \\ gs [])
-      >- (rw [letrecs_distinct_def]
-          >- (gs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
-              \\ irule ALL_DISTINCT_IMP
-              \\ gs [MAP_ZIP, ALL_DISTINCT_IMP2])
-          >- (gs [EVERY_EL, EL_MAP, EL_ZIP] \\ rw [FST_THM, SND_THM]
-              \\ pairarg_tac \\ gs []
-              \\ pairarg_tac \\ gs []
-              \\ pairarg_tac \\ gs []
-              \\ rename1 ‘i < _’
-              \\ last_x_assum $ qspecl_then [‘cexp_size f (SND (EL i binds))’] assume_tac
-              \\ ‘cexp_size f (SND (EL i binds)) < cexp7_size f binds’
-                by (assume_tac cexp_size_lemma \\ gvs [] \\ first_x_assum irule
+      >- (gs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
+          \\ irule ALL_DISTINCT_IMP
+          \\ gs [MAP_ZIP, ALL_DISTINCT_IMP2])
+      >- (gs [EVERY_EL, EL_MAP, EL_ZIP] \\ rw [FST_THM, SND_THM]
+          \\ pairarg_tac \\ gs []
+          \\ pairarg_tac \\ gs []
+          \\ pairarg_tac \\ gs []
+          \\ rename1 ‘i < _’
+          \\ last_x_assum $ qspecl_then [‘cexp_size f (SND (EL i binds))’] assume_tac
+          \\ ‘cexp_size f (SND (EL i binds)) < cexp7_size f binds’
+            by (assume_tac cexp_size_lemma \\ gvs [] \\ first_x_assum irule
                 \\ gvs [MEM_EL] \\ first_assum $ irule_at Any
-                    \\ simp [])
-              \\ gvs [] \\ pop_assum kall_tac
-              \\ first_x_assum $ resolve_then (Pos hd) (drule_then assume_tac) EQ_REFL
-              \\ gs [FOLDL_delete_ok]
-              \\ last_x_assum $ drule_then assume_tac
-              \\ last_x_assum $ drule_then assume_tac
-              \\ last_x_assum $ drule_then assume_tac
-              \\ gs [])
-          >- gs [letrecs_distinct_adds_demands]))
+                \\ simp [])
+          \\ gvs [] \\ pop_assum kall_tac
+          \\ first_x_assum $ resolve_then (Pos hd) (drule_then assume_tac) EQ_REFL
+          \\ gs [FOLDL_delete_ok]
+          \\ last_x_assum $ drule_then assume_tac
+          \\ last_x_assum $ drule_then assume_tac
+          \\ last_x_assum $ drule_then assume_tac
+          \\ gs [])
+      >- gs [letrecs_distinct_adds_demands])
   >~ [‘Case a case_exp s l opt’]
-
   >- (gen_tac \\ gen_tac
       \\ rename1 ‘Bind _ _ c’
       \\ rpt $ gen_tac
diff --git a/compiler/backend/passes/proofs/pure_letrecProofScript.sml b/compiler/backend/passes/proofs/pure_letrecProofScript.sml
index 943311ac..1a4253fe 100644
--- a/compiler/backend/passes/proofs/pure_letrecProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_letrecProofScript.sml
@@ -1764,17 +1764,18 @@ Proof
   recInduct freevars_ind >> rw[letrecs_distinct_def, letrec_recurse_def] >>
   gvs[EVERY_MAP, EVERY_MEM] >>
   simp[clean_one_def] >> IF_CASES_TAC >> gvs[] >>
-  pop_assum kall_tac >> Cases_on `lcs` >> gvs[] >- simp[letrecs_distinct_def] >>
+  pop_assum kall_tac >> Cases_on `lcs` >> gvs[] >>
   Cases_on `t` >> gvs[]
   >- (
     pairarg_tac >> gvs[] >> IF_CASES_TAC >> gvs[] >> simp[letrecs_distinct_def]
     ) >>
-  ntac 2 $ once_rewrite_tac[GSYM MAP] >>
-  qpat_abbrev_tac `foo = _ :: _ :: _` >>
-  `ALL_DISTINCT (MAP FST foo)` by (unabbrev_all_tac >> gvs[]) >>
+  gvs [SF DNF_ss] >>
+  rename [‘FST h1 ≠ FST h2’] >>
+  PairCases_on ‘h1’ >> PairCases_on ‘h2’ >> gvs [] >>
+  gvs [MEM_MAP,FORALL_PROD,PULL_EXISTS,EVERY_MEM] >>
   simp[letrecs_distinct_def, MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD] >>
   simp[GSYM FST_THM, EVERY_MAP, LAMBDA_PROD] >>
-  gvs[EVERY_MEM, FORALL_PROD] >> unabbrev_all_tac >> gvs[] >> metis_tac[]
+  metis_tac []
 QED
 
 
diff --git a/language/pure_expScript.sml b/language/pure_expScript.sml
index 5019b534..0b438059 100644
--- a/language/pure_expScript.sml
+++ b/language/pure_expScript.sml
@@ -190,7 +190,7 @@ End
 
 Overload Case = “λx nm css. expandCases x nm css”
 
-Definition letrecs_distinct_def:
+Definition letrecs_distinct_def[simp]:
   (letrecs_distinct (pure_exp$Letrec xs y) ⇔
     ALL_DISTINCT (MAP FST xs) ∧
     EVERY letrecs_distinct (MAP SND xs) ∧

From 393c7d4f62f74e2268b3668d43a0ec5d69f0c84b Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 4 Oct 2023 17:15:23 +0200
Subject: [PATCH 3/9] Move some definitions upwards

---
 compiler/backend/languages/env_cexpScript.sml | 20 +++++++++++++++++
 .../backend/languages/pure_cexpScript.sml     | 22 ++++++++++++++++++-
 .../backend/languages/state_cexpScript.sml    |  5 +++++
 .../backend/languages/thunk_cexpScript.sml    | 10 +++++++++
 .../backend/passes/env_to_stateScript.sml     | 20 -----------------
 .../proofs/pure_inline_cexpProofScript.sml    |  2 +-
 .../passes/proofs/thunk_to_envProofScript.sml | 15 +++++++------
 .../backend/passes/pure_inline_cexpScript.sml | 15 -------------
 .../passes/pure_letrec_spec_cexpScript.sml    |  5 -----
 .../passes/thunk_split_Delay_LamScript.sml    | 10 ---------
 .../backend/passes/thunk_to_envScript.sml     | 10 ---------
 language/pure_configScript.sml                |  5 +++++
 12 files changed, 70 insertions(+), 69 deletions(-)

diff --git a/compiler/backend/languages/env_cexpScript.sml b/compiler/backend/languages/env_cexpScript.sml
index 2653ae30..7b30469e 100644
--- a/compiler/backend/languages/env_cexpScript.sml
+++ b/compiler/backend/languages/env_cexpScript.sml
@@ -80,4 +80,24 @@ Termination
   WF_REL_TAC `measure cexp_size`
 End
 
+Definition Lams_def:
+  Lams [] x = x ∧
+  Lams (y::ys) x = Lam y (Lams ys x)
+End
+
+Definition Apps_def:
+  Apps x [] = x ∧
+  Apps x (y::ys) = Apps (App x y) ys
+End
+
+Definition dest_Delay_def:
+  dest_Delay (Delay x) = SOME x ∧
+  dest_Delay _ = NONE
+End
+
+Definition dest_Lam_def:
+  dest_Lam (Lam v x) = SOME (v,x) ∧
+  dest_Lam _ = NONE
+End
+
 val _ = export_theory();
diff --git a/compiler/backend/languages/pure_cexpScript.sml b/compiler/backend/languages/pure_cexpScript.sml
index 310f3c37..27fec654 100644
--- a/compiler/backend/languages/pure_cexpScript.sml
+++ b/compiler/backend/languages/pure_cexpScript.sml
@@ -105,11 +105,31 @@ Theorem better_cexp_induction =
 
 val _ = TypeBase.update_induction better_cexp_induction
 
-Definition dest_var_def[simp]:
+Definition is_Lam_def:
+  is_Lam (Lam a vs e) = T ∧
+  is_Lam _ = F
+End
+
+Definition Lets_def:
+  Lets a ((v,e)::xs) e1 = Let a v e (Lets a xs e1) ∧
+  Lets a _ e = e
+End
+
+Definition dest_var_def[simp]: (* TODO: uppercase var *)
   dest_var (Var _ vnm) = SOME vnm ∧
   dest_var _ = NONE
 End
 
+Definition get_Var_name_def: (* TODO: replace by dest_var *)
+  get_Var_name (Var a v) = (SOME v) ∧
+  get_Var_name _ = NONE
+End
+
+Definition eq_Var_def:
+  eq_Var f (Var a v) = (f = v:mlstring) ∧
+  eq_Var f _ = F
+End
+
 Definition dest_nestedcase_def[simp]:
   dest_nestedcase (NestedCase _ g gv p e pes) = SOME (g, gv, (p,e)::pes) ∧
   dest_nestedcase _ = NONE
diff --git a/compiler/backend/languages/state_cexpScript.sml b/compiler/backend/languages/state_cexpScript.sml
index 8c660dc9..d830c352 100644
--- a/compiler/backend/languages/state_cexpScript.sml
+++ b/compiler/backend/languages/state_cexpScript.sml
@@ -53,6 +53,11 @@ Overload IntLit = “λi. App (AtomOp (Lit (Int i))) []”
 Overload StrLit = “λs. App (AtomOp (Lit (Str s))) []”
 Overload Eq = “λx y. App (AtomOp Eq) [x; y]”
 
+Definition Lets_def:
+  Lets [] x = (x:state_cexp$cexp) ∧
+  Lets ((v,y)::ys) x = Let v y (Lets ys x)
+End
+
 (* We require the correct number of arguments to be passed to the following.
    We could specify this for all operations, but it isn't necessary *)
 Definition op_args_ok_def:
diff --git a/compiler/backend/languages/thunk_cexpScript.sml b/compiler/backend/languages/thunk_cexpScript.sml
index ab209297..bb23a23e 100644
--- a/compiler/backend/languages/thunk_cexpScript.sml
+++ b/compiler/backend/languages/thunk_cexpScript.sml
@@ -65,4 +65,14 @@ Termination
   WF_REL_TAC `measure cexp_size`
 End
 
+Definition is_Lam_def:
+  is_Lam (Lam s e) = T ∧
+  is_Lam _ = F
+End
+
+Definition dest_Var_def:
+  dest_Var (Var v) = SOME v ∧
+  dest_Var _ = NONE
+End
+
 val _ = export_theory();
diff --git a/compiler/backend/passes/env_to_stateScript.sml b/compiler/backend/passes/env_to_stateScript.sml
index 4820460b..d6f59144 100644
--- a/compiler/backend/passes/env_to_stateScript.sml
+++ b/compiler/backend/passes/env_to_stateScript.sml
@@ -14,32 +14,12 @@ val _ = new_theory "env_to_state";
 
 val _ = set_grammar_ancestry ["env_cexp", "state_cexp", "pure_comp_conf"];
 
-Definition dest_Message_def:
-  dest_Message (Message s) = SOME s ∧
-  dest_Message _ = NONE
-End
-
-Definition Lets_def:
-  Lets [] x = (x:state_cexp$cexp) ∧
-  Lets ((v,y)::ys) x = Let v y (Lets ys x)
-End
-
 Definition Letrec_imm_def:
   (Letrec_imm vs ((Var v):env_cexp$cexp) ⇔ MEM v vs) ∧
   (Letrec_imm vs (Lam _ _) ⇔ T) ∧
   (Letrec_imm vs _ ⇔ F)
 End
 
-Definition dest_Delay_def:
-  dest_Delay (Delay x) = SOME (x:env_cexp$cexp) ∧
-  dest_Delay _ = NONE
-End
-
-Definition dest_Lam_def:
-  dest_Lam (Lam v x) = SOME (v,x:env_cexp$cexp) ∧
-  dest_Lam _ = NONE
-End
-
 Definition Letrec_split_def:
   Letrec_split vs [] = ([],[]) ∧
   Letrec_split vs ((v:mlstring,x)::fns) =
diff --git a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
index 18e93516..eb606ff8 100644
--- a/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_inline_cexpProofScript.sml
@@ -378,7 +378,7 @@ Theorem exp_of_Lets:
     Lets (ZIP (MAP explode vs, MAP exp_of xs)) (exp_of b)
 Proof
   Induct \\ Cases_on ‘xs’
-  \\ gvs [pure_inline_cexpTheory.Lets_def,pure_expTheory.Lets_def]
+  \\ gvs [pure_cexpTheory.Lets_def,pure_expTheory.Lets_def]
   \\ fs [exp_of_def]
 QED
 
diff --git a/compiler/backend/passes/proofs/thunk_to_envProofScript.sml b/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
index 5ce88233..fac8a5af 100644
--- a/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_to_envProofScript.sml
@@ -43,7 +43,7 @@ Proof
   >~ [‘Lam’] >-
    (last_x_assum mp_tac \\ fs [to_env_def]
     \\ qid_spec_tac ‘vs’ \\ Induct
-    \\ fs [Lams_def] \\ rw [] \\ fs []
+    \\ fs [env_cexpTheory.Lams_def] \\ rw [] \\ fs []
     \\ irule exp_rel_Lam \\ fs [])
   >~ [‘App’] >-
    (fs [to_env_def]
@@ -54,10 +54,10 @@ Proof
     \\ qid_spec_tac ‘x’
     \\ qid_spec_tac ‘xs’
     \\ Induct
-    \\ fs [Apps_def] \\ rw [] \\ fs [SF DNF_ss]
+    \\ fs [env_cexpTheory.Apps_def] \\ rw [] \\ fs [SF DNF_ss]
     \\ ‘cexp_wf (App x [h])’ by fs [cexp_wf_def]
     \\ last_x_assum drule
-    \\ fs [to_env_def,Apps_def]
+    \\ fs [to_env_def,env_cexpTheory.Apps_def]
     \\ disch_then irule
     \\ irule exp_rel_App
     \\ gs [])
@@ -144,7 +144,7 @@ Proof
   >~ [‘Lams’] >-
    (strip_tac
     \\ strip_tac \\ pop_assum kall_tac
-    \\ Induct_on ‘vs’ \\ fs [Lams_def,cexp_wf_def]
+    \\ Induct_on ‘vs’ \\ fs [env_cexpTheory.Lams_def,cexp_wf_def]
     \\ fs [to_env_def,cexp_wf_def,
            thunk_cexpTheory.cns_arities_def,
            env_cexpTheory.cns_arities_def])
@@ -153,13 +153,13 @@ Proof
     \\ strip_tac \\ pop_assum kall_tac \\ fs [SF ETA_ss]
     \\ rpt $ pop_assum mp_tac
     \\ qid_spec_tac ‘x’
-    \\ Induct_on ‘xs’ \\ fs [Apps_def,cexp_wf_def]
+    \\ Induct_on ‘xs’ \\ fs [env_cexpTheory.Apps_def,cexp_wf_def]
     \\ fs [to_env_def,cexp_wf_def,SF DNF_ss,
            thunk_cexpTheory.cns_arities_def,
            env_cexpTheory.cns_arities_def]
     \\ rw [] \\ fs []
     \\ rpt $ last_x_assum $ qspec_then ‘App x [h]’ mp_tac
-    \\ fs [to_env_def,Apps_def]
+    \\ fs [to_env_def,env_cexpTheory.Apps_def]
     \\ fs [to_env_def,cexp_wf_def,SF DNF_ss,
            thunk_cexpTheory.cns_arities_def,
            env_cexpTheory.cns_arities_def]
@@ -176,7 +176,8 @@ Proof
     >-
      (rename [‘cexp_ok_bind pp’] \\ Cases_on ‘pp’ \\ fs [cexp_ok_bind_def]
       \\ fs [to_env_def]
-      \\ fs [cexp_wf_def] \\ rename [‘Lams l’] \\ Cases_on ‘l’ \\ fs [Lams_def])
+      \\ fs [cexp_wf_def] \\ rename [‘Lams l’] \\ Cases_on ‘l’
+      \\ fs [env_cexpTheory.Lams_def])
     >- metis_tac [])
   >- (strip_tac \\ strip_tac \\ fs []
       \\ rpt $ conj_tac
diff --git a/compiler/backend/passes/pure_inline_cexpScript.sml b/compiler/backend/passes/pure_inline_cexpScript.sml
index 735681f4..ae43eb06 100644
--- a/compiler/backend/passes/pure_inline_cexpScript.sml
+++ b/compiler/backend/passes/pure_inline_cexpScript.sml
@@ -62,16 +62,6 @@ Definition heuristic_insert_Rec_def:
       | _ => m
 End
 
-Definition is_Lam_def:
-  is_Lam (Lam a vs e) = T ∧
-  is_Lam _ = F
-End
-
-Definition get_Var_name_def:
-  get_Var_name (Var a v) = (SOME v) ∧
-  get_Var_name _ = NONE
-End
-
 Triviality size_lemma:
   ∀bs.
     list_size (cexp_size (K 0)) (MAP (λ(v,vs,e). e) bs) ≤
@@ -93,11 +83,6 @@ by inlining in the App case. The problem now is that
 And so goint further won't do anything
 *)
 
-Definition Lets_def:
-  Lets a ((v,e)::xs) e1 = Let a v e (Lets a xs e1) ∧
-  Lets a _ e = e
-End
-
 Definition App_Lam_to_Lets_def:
   App_Lam_to_Lets (App a (Lam _ vs b) es) =
     (if LENGTH es < LENGTH vs (* not fully applied *) then NONE else
diff --git a/compiler/backend/passes/pure_letrec_spec_cexpScript.sml b/compiler/backend/passes/pure_letrec_spec_cexpScript.sml
index 5b31aca9..7da84278 100644
--- a/compiler/backend/passes/pure_letrec_spec_cexpScript.sml
+++ b/compiler/backend/passes/pure_letrec_spec_cexpScript.sml
@@ -7,11 +7,6 @@ open pure_cexpTheory pure_varsTheory balanced_mapTheory;
 
 val _ = new_theory "pure_letrec_spec_cexp";
 
-Definition eq_Var_def:
-  eq_Var f (Var a v) = (f = v:mlstring) ∧
-  eq_Var f _ = F
-End
-
 (*
   For every elemen in xs, if y is a variable reference to the corresponding
   element from xs, then return (SOME x). Otherwise NONE.
diff --git a/compiler/backend/passes/thunk_split_Delay_LamScript.sml b/compiler/backend/passes/thunk_split_Delay_LamScript.sml
index c7166276..05e0f915 100644
--- a/compiler/backend/passes/thunk_split_Delay_LamScript.sml
+++ b/compiler/backend/passes/thunk_split_Delay_LamScript.sml
@@ -7,21 +7,11 @@ open thunk_cexpTheory mlmapTheory mlstringTheory pred_setTheory var_setTheory;
 
 val _ = new_theory "thunk_split_Delay_Lam";
 
-Definition is_Lam_def:
-  is_Lam (Lam s e) = T ∧
-  is_Lam _ = F
-End
-
 Definition dest_Delay_Lam_def:
     (dest_Delay_Lam (Delay (Lam v e)) = SOME (Lam v e)) /\
     (dest_Delay_Lam _ = NONE)
 End
 
-Definition dest_Var_def:
-    (dest_Var (Var v) = SOME v) /\
-    (dest_Var _ = NONE)
-End
-
 Definition letrec_split_def:
     (letrec_split [] var_creator maps = ([], var_creator, maps)) /\
     (letrec_split ((name, expr)::list) var_creator maps =
diff --git a/compiler/backend/passes/thunk_to_envScript.sml b/compiler/backend/passes/thunk_to_envScript.sml
index dc3212aa..653168f5 100644
--- a/compiler/backend/passes/thunk_to_envScript.sml
+++ b/compiler/backend/passes/thunk_to_envScript.sml
@@ -10,16 +10,6 @@ val _ = new_theory "thunk_to_env";
 
 val _ = set_grammar_ancestry ["thunk_cexp", "env_cexp"]
 
-Definition Lams_def:
-  Lams [] x = x ∧
-  Lams (y::ys) x = env_cexp$Lam y (Lams ys x)
-End
-
-Definition Apps_def:
-  Apps x [] = x ∧
-  Apps x (y::ys) = Apps (env_cexp$App x y) ys
-End
-
 Definition get_arg_def:
   get_arg n [] = env_cexp$Prim (Cons (strlit "")) [] ∧
   get_arg n (x::xs) = if n = 0:num then x else get_arg (n-1) xs
diff --git a/language/pure_configScript.sml b/language/pure_configScript.sml
index 2201d6ed..54db3665 100644
--- a/language/pure_configScript.sml
+++ b/language/pure_configScript.sml
@@ -226,4 +226,9 @@ Proof
   simp[monad_cns_def]
 QED
 
+Definition dest_Message_def:
+  dest_Message (Message s) = SOME s ∧
+  dest_Message _ = NONE
+End
+
 val _ = export_theory ();

From c5a9fc68af4b6695b8e8e6db35dc49f81eb6927d Mon Sep 17 00:00:00 2001
From: Hrutvik Kanabar <hrutvikkanabar@yahoo.co.uk>
Date: Wed, 4 Oct 2023 16:39:19 +0100
Subject: [PATCH 4/9] Delete some unnecessary dependencies in
 `pure_tcexpTheory`

---
 typing/pure_tcexpScript.sml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/typing/pure_tcexpScript.sml b/typing/pure_tcexpScript.sml
index d8df93d1..11e37ef4 100644
--- a/typing/pure_tcexpScript.sml
+++ b/typing/pure_tcexpScript.sml
@@ -2,10 +2,9 @@
    This file defines expressions for pure_lang as the type system sees them.
 *)
 open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite;
-open arithmeticTheory listTheory rich_listTheory alistTheory stringTheory
+open arithmeticTheory listTheory alistTheory stringTheory
      optionTheory pairTheory pred_setTheory finite_mapTheory;
-open pure_cexpTheory pure_cexp_lemmasTheory pure_expTheory pure_evalTheory
-     pure_exp_lemmasTheory pure_exp_relTheory pure_congruenceTheory;
+open pure_cexpTheory pureLangTheory pure_expTheory;
 
 val _ = new_theory "pure_tcexp";
 

From 4a41122817c876ea4c0ea72b85cc3de81b1fb951 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 4 Oct 2023 17:51:53 +0200
Subject: [PATCH 5/9] Update translation for moves

---
 compiler/binary/pure_backendProgScript.sml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/compiler/binary/pure_backendProgScript.sml b/compiler/binary/pure_backendProgScript.sml
index b45e0682..094100ea 100644
--- a/compiler/binary/pure_backendProgScript.sml
+++ b/compiler/binary/pure_backendProgScript.sml
@@ -24,6 +24,8 @@ val r = translate pure_cexpTheory.dest_Lam_def;
 val r = translate pure_cexpTheory.dest_App_def;
 val r = translate pure_cexpTheory.SmartLam_def;
 val r = translate pure_cexpTheory.SmartApp_def;
+val r = translate pure_cexpTheory.is_Lam_def;
+val r = translate pure_cexpTheory.Lets_def;
 
 val r = translate var_setTheory.insert_var_def;
 val r = translate var_setTheory.insert_vars_def;
@@ -54,7 +56,7 @@ val r = translate pure_namesTheory.pure_names_def;
 
 val r = translate FOLDL;
 val r = translate FOLDR;
-val r = translate thunk_split_Delay_LamTheory.dest_Var_def;
+val r = translate thunk_cexpTheory.dest_Var_def;
 val r = translate thunk_split_Delay_LamTheory.dest_Delay_Lam_def;
 val r = translate thunk_split_Delay_LamTheory.letrec_split_def;
 val r = translate_no_ind thunk_split_Delay_LamTheory.split_Delayed_Lam_def;
@@ -95,8 +97,8 @@ val r = translate compile_to_thunk_def;
 
 (* thunk_to_env *)
 
-val r = translate thunk_to_envTheory.Lams_def;
-val r = translate thunk_to_envTheory.Apps_def;
+val r = translate env_cexpTheory.Lams_def;
+val r = translate env_cexpTheory.Apps_def;
 val r = translate thunk_to_envTheory.get_arg_def;
 val r = translate thunk_to_envTheory.remove_Delay_def;
 val r = translate thunk_to_envTheory.op_to_env_def;
@@ -104,10 +106,10 @@ val r = translate thunk_to_envTheory.to_env_def;
 
 (* env_to_state *)
 
-val r = translate env_to_stateTheory.dest_Message_def;
-val r = translate env_to_stateTheory.dest_Delay_def;
-val r = translate env_to_stateTheory.dest_Lam_def;
-val r = translate env_to_stateTheory.Lets_def;
+val r = translate pure_configTheory.dest_Message_def;
+val r = translate env_cexpTheory.dest_Delay_def;
+val r = translate env_cexpTheory.dest_Lam_def;
+val r = translate state_cexpTheory.Lets_def;
 val r = translate env_to_stateTheory.Bool_def;
 val r = translate env_to_stateTheory.some_ref_bool_def;
 val r = translate env_to_stateTheory.unsafe_update_def;

From 6ee88c7de53bb27865a53cbea4371f0d9118410b Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 4 Oct 2023 18:27:25 +0200
Subject: [PATCH 6/9] Tweak pure_pres

---
 .../backend/languages/relations/pure_presScript.sml   | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

diff --git a/compiler/backend/languages/relations/pure_presScript.sml b/compiler/backend/languages/relations/pure_presScript.sml
index fadd4646..f7ebea55 100644
--- a/compiler/backend/languages/relations/pure_presScript.sml
+++ b/compiler/backend/languages/relations/pure_presScript.sml
@@ -678,15 +678,6 @@ Proof
                   pure_demandTheory.Letrec_unfold \\ fs []
     \\ gvs [EL_MAP] \\ disch_then drule \\ fs []
     \\ disch_then $ qspec_then ‘T’ mp_tac
-    \\ impl_tac
-    >-
-     (gvs [MAP_MAP_o,o_DEF,LAMBDA_PROD]
-      \\ qpat_x_assum `ALL_DISTINCT _` mp_tac
-      \\ qmatch_goalsub_abbrev_tac ‘_ xs ⇒ _ ys’
-      \\ qsuff_tac ‘xs = MAP implode ys’ \\ gvs []
-      >- metis_tac [ALL_DISTINCT_MAP]
-      \\ unabbrev_all_tac \\ rpt $ pop_assum kall_tac
-      \\ Induct_on ‘l’ \\ gvs [] \\ PairCases \\ fs [])
     \\ qpat_x_assum ‘_ = EL _ _’ $ assume_tac o GSYM
     \\ simp [])
   >~ [‘spec_arg’] >-
@@ -826,6 +817,7 @@ Proof
   IF_CASES_TAC >> gvs[]
 QED
 
+(*
 Theorem bidir_preserves_typing:
   ∀x y ns db st env t.
     (x <--> y) ∧ namespace_ok ns
@@ -1253,6 +1245,7 @@ Proof
       )
     )
 QED
+*)
 
 (**********)
 

From 09dad9266a8a76f590560c3daadb4360c21047e2 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 4 Oct 2023 18:27:46 +0200
Subject: [PATCH 7/9] Tidy up some thunkLang files

---
 .../backend/languages/semantics/thunkLangScript.sml   | 11 +++++++++++
 .../passes/proofs/pure_to_thunk_2ProofScript.sml      |  6 +++---
 .../passes/proofs/thunk_case_inlProofScript.sml       |  6 ------
 .../passes/proofs/thunk_case_projProofScript.sml      |  6 ------
 .../backend/passes/proofs/thunk_tickProofScript.sml   |  6 ------
 .../passes/proofs/thunk_unthunkProofScript.sml        |  5 -----
 6 files changed, 14 insertions(+), 26 deletions(-)

diff --git a/compiler/backend/languages/semantics/thunkLangScript.sml b/compiler/backend/languages/semantics/thunkLangScript.sml
index ef87a6cc..ea795e65 100644
--- a/compiler/backend/languages/semantics/thunkLangScript.sml
+++ b/compiler/backend/languages/semantics/thunkLangScript.sml
@@ -568,6 +568,11 @@ Definition is_Delay_def[simp]:
   (is_Delay _ = F)
 End
 
+Definition is_delay_def[simp]: (* TODO: delete, replace by above *)
+  is_delay (Delay x) = T ∧
+  is_delay _ = F
+End
+
 Definition ok_bind_def[simp]:
   (ok_bind (Lam _ _) = T) ∧
   (ok_bind (Delay _) = T) ∧
@@ -606,4 +611,10 @@ Proof
   \\ simp [SET_EQ_SUBSET, SUBSET_DEF]
 QED
 
+Definition ok_binder_def[simp]:
+  ok_binder (Lam s x) = T ∧
+  ok_binder (Delay x) = T ∧
+  ok_binder _ = F
+End
+
 val _ = export_theory ();
diff --git a/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml b/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
index c7539fa2..2d37530a 100644
--- a/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
+++ b/compiler/backend/passes/proofs/pure_to_thunk_2ProofScript.sml
@@ -492,7 +492,7 @@ Proof
     \\ qid_spec_tac ‘xs’
     \\ Induct \\ fs [PULL_EXISTS]
     \\ rw [] \\ gvs []
-    \\ fs [thunk_unthunkProofTheory.is_delay_def]
+    \\ fs []
     \\ rpt $ first_assum $ irule_at Any
     \\ last_x_assum drule \\ strip_tac
     \\ rpt $ first_assum $ irule_at Any
@@ -508,7 +508,7 @@ Proof
       \\ qpat_x_assum ‘force_rel NONE y2 _’ $ irule_at Any
       \\ irule_at Any thunk_case_projProofTheory.compile_rel_Delay
       \\ first_x_assum $ irule_at $ Pos hd
-      \\ fs [thunk_unthunkProofTheory.is_delay_def]
+      \\ fs []
       \\ irule_at Any thunk_unthunkProofTheory.delay_force_Delay \\ fs [])
     \\ fs [cexp_wf_def,SF SFY_ss,exp_of'_def]
     \\ irule_at Any pure_to_thunk_1ProofTheory.compile_rel_Var
@@ -522,7 +522,7 @@ Proof
     \\ irule_at Any thunk_case_projProofTheory.compile_rel_Force
     \\ irule_at Any thunk_case_projProofTheory.compile_rel_Var
     \\ irule_at Any thunk_unthunkProofTheory.delay_force_Delat_Force_Var
-    \\ fs [thunk_unthunkProofTheory.is_delay_def])
+    \\ fs [])
   >~ [‘Apps’] >-
    (pop_assum kall_tac
     \\ rpt $ pop_assum mp_tac
diff --git a/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml b/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
index 020715e8..161b25d3 100644
--- a/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_inlProofScript.sml
@@ -26,12 +26,6 @@ Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
 Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
-Definition ok_binder_def[simp]:
-  ok_binder (Lam s x) = T ∧
-  ok_binder (Delay x) = T ∧
-  ok_binder _ = F
-End
-
 Inductive exp_rel:
 (* Inlining *)
 [exp_rel_Inline:]
diff --git a/compiler/backend/passes/proofs/thunk_case_projProofScript.sml b/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
index 7780bf23..29de4067 100644
--- a/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_case_projProofScript.sml
@@ -27,12 +27,6 @@ Theorem SUM_REL_THM[local,simp] = sumTheory.SUM_REL_THM;
 
 Theorem PAIR_REL_def[local,simp] = pairTheory.PAIR_REL;
 
-Definition ok_binder_def[simp]:
-  ok_binder (Lam s x) = T ∧
-  ok_binder (Delay x) = T ∧
-  ok_binder _ = F
-End
-
 Inductive exp_rel:
 (* Proj *)
 [exp_rel_Proj:]
diff --git a/compiler/backend/passes/proofs/thunk_tickProofScript.sml b/compiler/backend/passes/proofs/thunk_tickProofScript.sml
index 1a921b6a..77a2f864 100644
--- a/compiler/backend/passes/proofs/thunk_tickProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_tickProofScript.sml
@@ -20,12 +20,6 @@ Theorem PAIR_REL_THM[local,simp] = pairTheory.PAIR_REL_THM;
 
 val _ = numLib.prefer_num ();
 
-Definition ok_bind_def[simp]:
-  ok_bind (Delay x) = T ∧
-  ok_bind (Lam s x) = T ∧
-  ok_bind _ = F
-End
-
 Inductive exp_rel:
 [~Var:]
   (∀n. exp_rel (Var n) (Var n)) ∧
diff --git a/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml b/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
index 1de0dd66..043c0782 100644
--- a/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
+++ b/compiler/backend/passes/proofs/thunk_unthunkProofScript.sml
@@ -185,11 +185,6 @@ QED
 
  *)
 
-Definition is_delay_def[simp]:
-  is_delay (Delay x) = T ∧
-  is_delay _ = F
-End
-
 Inductive exp_rel:
 [exp_rel_Delay_Force_Var:]
   (∀v.

From 05de3cc45831112c0cf746b09294d2ae263f125c Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Thu, 5 Oct 2023 22:06:33 +0200
Subject: [PATCH 8/9] Fix App_Lam rule in bidir

---
 .../languages/relations/pure_presScript.sml   | 11 ++-
 .../relations/pure_pres_lemmasScript.sml      | 96 ++++++++++---------
 2 files changed, 58 insertions(+), 49 deletions(-)

diff --git a/compiler/backend/languages/relations/pure_presScript.sml b/compiler/backend/languages/relations/pure_presScript.sml
index f7ebea55..0a5fdc4d 100644
--- a/compiler/backend/languages/relations/pure_presScript.sml
+++ b/compiler/backend/languages/relations/pure_presScript.sml
@@ -16,7 +16,6 @@ open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
      pure_tcexpTheory pure_tcexp_lemmasTheory
      pure_typingTheory pure_typingPropsTheory;
 
-
 val exp_of_def = pureLangTheory.exp_of_def;
 val rows_of_def = pureLangTheory.rows_of_def;
 val lets_for_def = pureLangTheory.lets_for_def;
@@ -155,9 +154,11 @@ Inductive bidir:
   (* typing: => direction proved
              <= direction has mismatching free variables *)
 [~App_Lam:]
-  (∀a b c vs x.
-    bidir (App a (Lam b vs x) (MAP (Var c) vs))
-          x) ∧
+  (∀a b c vs x ws.
+    set vs ⊆ set ws ∧ vs ≠ []
+    ⇒
+    bidir (Lam a ws (App b (Lam c vs x) (MAP (Var d) vs)))
+          (Lam a ws x)) ∧
 [~Letrec_Lam:]
   (∀a b c d vs l e.
     EVERY (λ(v,e). DISJOINT (IMAGE explode (set vs)) (freevars (exp_of e)) ∧
@@ -361,7 +362,6 @@ Proof
   >~ [`spec_arg`]
   >- cheat (* TODO specialisation *) >>
   rw[] >> eq_tac >> rw[] >> gvs[EVERY_MEM, FORALL_PROD] >> res_tac
-  >- cheat (* App_Lam - not true due to potentially empty `vs` *)
 QED
 
 Theorem pres_imp_wf_preserved:
@@ -638,6 +638,7 @@ Proof
     \\ irule Letrec_eq_Let_Letrec)
   >-
    (fs [exp_of_def,MAP_MAP_o,o_DEF]
+    \\ irule exp_eq_Lams_cong
     \\ ‘MAP (λx. Var (explode x) : exp) vs = MAP Var (MAP explode vs)’ by
           fs [MAP_MAP_o,o_DEF]
     \\ simp [Apps_Lams_Vars])
diff --git a/compiler/backend/languages/relations/pure_pres_lemmasScript.sml b/compiler/backend/languages/relations/pure_pres_lemmasScript.sml
index 355a0f7a..0d9f2625 100644
--- a/compiler/backend/languages/relations/pure_pres_lemmasScript.sml
+++ b/compiler/backend/languages/relations/pure_pres_lemmasScript.sml
@@ -15,7 +15,7 @@ open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
 val _ = new_theory "pure_pres_lemmas";
 
 Theorem bidir_letrec_eta:
-  MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧
+  MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧ vs ≠ [] ∧
   EVERY (λ(v,e).
            DISJOINT (IMAGE explode (set vs)) (freevars (exp_of e)) ∧
            ~MEM v vs) l ∧
@@ -34,7 +34,8 @@ Proof
   \\ conj_tac
   >-
    (irule bidir_Letrec \\ fs [LIST_REL_same]
-    \\ irule bidir_Lam \\ simp [Once bidir_sym,bidir_App_Lam])
+    \\ simp [Once bidir_sym]
+    \\ irule bidir_App_Lam \\ fs [])
   \\ irule_at Any bidir_trans
   \\ irule_at (Pos hd) bidir_Letrec_Lam \\ fs []
   \\ simp [Once bidir_sym]
@@ -55,7 +56,7 @@ Proof
 QED
 
 Theorem bidir_letrec_eta_1:
-  ¬MEM f vs
+  ¬MEM f vs ∧ vs ≠ []
   ⇒
   (Letrec a [(f,Lam a vs x)] (Var a f))
   <-->
@@ -67,7 +68,7 @@ Proof
 QED
 
 Theorem bidir_letrec_expand_1:
-  ¬MEM f vs
+  ¬MEM f vs ∧ vs ≠ []
   ⇒
   (Letrec a [(f,Lam a vs x)] x)
   <-->
@@ -91,7 +92,7 @@ Proof
 QED
 
 Theorem bidir_contract_1:
-  ~MEM f ps ∧ ~MEM f ws ∧ vs ≠ [] ∧ ws ≠ []
+  ~MEM f ps ∧ ~MEM f ws ∧ vs ≠ [] ∧ ws ≠ [] ∧ set ws ⊆ set vs
   ⇒
   (Lam a (vs ++ ps)
      (Letrec a [(f,Lam a (ws ++ ps) x)]
@@ -103,53 +104,60 @@ Theorem bidir_contract_1:
 Proof
   Cases_on ‘ps = []’ >- fs []
   \\ rw []
-  \\ irule bidir_trans
-  \\ irule_at Any bidir_Lam_append \\ fs []
-  \\ irule bidir_Lam
-  \\ irule bidir_trans
-  \\ qabbrev_tac ‘y = Letrec a [(f,Lam a (ws ++ ps) x)] x’
-  \\ qexists_tac ‘Lam a ps
-                   (App a (Lam a (ws ++ ps) y) (MAP (Var a) ws ++ MAP (Var a) ps))’
-  \\ conj_tac >-
-   (irule bidir_Lam
-    \\ irule bidir_trans
-    \\ irule_at Any bidir_Letrec_App_forget
-    \\ irule_at Any bidir_App
-    \\ fs [LIST_REL_same,EVERY_MAP,exp_of_def]
-    \\ gvs [EVERY_MEM]
-    \\ irule bidir_trans
-    \\ irule_at (Pos hd) bidir_Letrec_unroll \\ fs []
-    \\ unabbrev_all_tac
-    \\ irule bidir_Letrec_Lam
-    \\ fs [exp_of_def,IN_DISJOINT,MEM_MAP]
-    \\ metis_tac [])
-  \\ simp [Once bidir_sym]
-  \\ irule bidir_trans
-  \\ qexists_tac ‘App a (Lam a (ws ++ ps) y) (MAP (Var a) ws)’
-  \\ conj_tac >-
+  \\ qabbrev_tac ‘z = Letrec a [(f,Lam a (ws ++ ps) x)] x’
+  \\ ‘Letrec a [(f,Lam a (ws ++ ps) x)] (Var a f) <--> Lam a (ws ++ ps) z’ by
    (irule bidir_trans
-    \\ irule_at Any bidir_Letrec_App_forget
-    \\ irule_at Any bidir_App
-    \\ fs [LIST_REL_same,EVERY_MAP,exp_of_def]
-    \\ gvs [EVERY_MEM]
-    \\ irule bidir_trans
     \\ irule_at (Pos hd) bidir_Letrec_unroll \\ fs []
     \\ unabbrev_all_tac
-    \\ irule bidir_Letrec_Lam
-    \\ fs [exp_of_def,IN_DISJOINT,MEM_MAP]
+    \\ irule_at (Pos hd) bidir_Letrec_Lam \\ gvs []
+    \\ gvs [exp_of_def,IN_DISJOINT,MEM_MAP]
     \\ metis_tac [])
-  \\ irule bidir_trans
-  \\ qexists_tac ‘Lam a ps y’
-  \\ conj_tac >-
-   (irule bidir_trans
+  \\ qsuff_tac ‘
+      Lam a (vs ++ ps)
+        (App a (Lam a (ws ++ ps) z) (MAP (Var a) ws ++ MAP (Var a) ps)) <-->
+      Lam a vs
+        (App a (Lam a (ws ++ ps) z) (MAP (Var a) ws))’
+  >-
+   (strip_tac
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at (Pos last) bidir_trans
+    \\ pop_assum $ irule_at $ Pos hd
+    \\ irule_at Any bidir_Lam
+    \\ irule_at Any bidir_Lam
+    \\ unabbrev_all_tac
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at Any bidir_Letrec_App_forget
+    \\ gvs [EVERY_MAP,exp_of_def] \\ gvs [EVERY_MEM]
+    \\ irule_at (Pos hd) bidir_App
+    \\ gvs [LIST_REL_same]
+    \\ simp [Once bidir_sym]
+    \\ irule_at (Pos hd) bidir_trans
+    \\ irule_at Any bidir_Letrec_App_forget
+    \\ gvs [EVERY_MAP,exp_of_def] \\ gvs [EVERY_MEM]
     \\ irule_at (Pos hd) bidir_App
+    \\ gvs [LIST_REL_same])
+  \\ irule_at Any bidir_trans
+  \\ qexists_tac ‘Lam a (vs ++ ps) z’
+  \\ conj_tac >-
+   (rewrite_tac [GSYM MAP_APPEND]
+    \\ irule bidir_App_Lam \\ fs []
+    \\ gvs [SUBSET_DEF])
+  \\ qsuff_tac ‘
+      Lam a vs (Lam a ps z) <-->
+      Lam a vs (App a (Lam a ws (Lam a ps z)) (MAP (Var a) ws))’
+  >-
+   (strip_tac
+    \\ irule bidir_trans
     \\ irule_at (Pos hd) bidir_Lam_append \\ fs []
-    \\ qexists_tac ‘MAP (Var a) ws’ \\ fs []
+    \\ irule bidir_trans
+    \\ pop_assum $ irule_at $ Pos hd
+    \\ irule bidir_Lam
+    \\ irule bidir_App
     \\ gvs [LIST_REL_same]
-    \\ metis_tac [bidir_App_Lam])
-  \\ irule bidir_Lam
+    \\ simp [Once bidir_sym]
+    \\ irule_at (Pos hd) bidir_Lam_append \\ fs [])
   \\ simp [Once bidir_sym]
-  \\ rewrite_tac [GSYM MAP_APPEND,bidir_App_Lam]
+  \\ irule bidir_App_Lam \\ fs []
 QED
 
 val _ = export_theory ();

From da03bc717dc2221701868b4ff367f22f2799d722 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Sat, 7 Oct 2023 18:08:27 +0200
Subject: [PATCH 9/9] Fix a broken proof (in an unused file)

---
 .../backend/languages/properties/env_cexp_lemmasScript.sml     | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
index 853edf92..9b2c90a8 100644
--- a/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
+++ b/compiler/backend/languages/properties/env_cexp_lemmasScript.sml
@@ -7,6 +7,8 @@ open pure_miscTheory env_cexpTheory ;
 val _ = new_theory "env_cexp_lemmas";
 
 val freevars_def = envLangTheory.freevars_def;
+val Lams_def = envLangTheory.Lams_def;
+val Apps_def = envLangTheory.Apps_def;
 
 Theorem freevars_Lams[simp]:
   ∀vs e. freevars (Lams vs e) = freevars e DIFF set vs
@@ -106,4 +108,3 @@ QED
  *)
 
 val _ = export_theory();
-