FTBFS

binghe · Jan 23, 2025 · 2c510b1 · 2c510b1
1 parent ec6bb0a
commit 2c510b1
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 13 deletions.
diff --git a/src/coalgebras/llistScript.sml b/src/coalgebras/llistScript.sml
@@ -1156,15 +1156,6 @@ val to_fromList = store_thm(
   SIMP_TAC (srw_ss()) [toList_THM] THEN REPEAT STRIP_TAC THEN
   IMP_RES_TAC LFINITE_toList THEN FULL_SIMP_TAC (srw_ss()) []);
 
-Theorem MAP_THE_toList :
-    !ll f. LFINITE ll ==> MAP f (THE (toList ll)) = THE (toList (LMAP f ll))
-Proof
-    rpt STRIP_TAC
- >> ‘ll = fromList (THE (toList ll))’ by METIS_TAC [to_fromList]
- >> POP_ORW
- >> simp [LMAP_fromList, to_fromList, from_toList]
-QED
-
 Theorem LTAKE_LAPPEND2:
   !n l1 l2.
     LTAKE n l1 = NONE ==>
@@ -3235,6 +3226,15 @@ Proof
   Induct_on `l` >> fs[]
 QED
 
+Theorem MAP_toList :
+    !ll f. LFINITE ll ==> MAP f (THE (toList ll)) = THE (toList (LMAP f ll))
+Proof
+    rpt STRIP_TAC
+ >> ‘ll = fromList (THE (toList ll))’ by METIS_TAC [to_fromList]
+ >> POP_ORW
+ >> simp [LMAP_fromList, to_fromList, from_toList]
+QED
+
 Theorem exists_fromSeq[simp]:
   !p f. exists p (fromSeq f) = ?i. p (f i)
 Proof

diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
@@ -1021,7 +1021,7 @@ in
   (* |- !t. ltree_finite t ==> from_rose (to_rose t) = t *)
   val to_rose_def = new_specification
     ("to_rose_def", ["to_rose"],
-     SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] thm);
+      SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] thm);
 end;
 
 Theorem to_rose_thm :
@@ -1042,7 +1042,6 @@ Proof
  >> rw [rose_node_def, from_rose_def, ltree_node_def]
 QED
 
-(* cf. MAP_THE_toList *)
 Theorem rose_children_to_rose :
     !t. ltree_finite t ==>
         rose_children (to_rose t) = MAP to_rose (THE (toList (ltree_children t)))
@@ -1062,8 +1061,7 @@ Proof
     rpt STRIP_TAC
  >> ‘finite_branching t’ by PROVE_TAC [ltree_finite_imp_finite_branching]
  >> Suff ‘LFINITE (ltree_children t)’
- >- (DISCH_TAC \\
-     simp [GSYM MAP_THE_toList] \\
+ >- (DISCH_TAC >> simp [GSYM MAP_toList] \\
      MATCH_MP_TAC rose_children_to_rose >> art [])
  >> Suff ‘finite_branching (Branch (ltree_node t) (ltree_children t))’ >- rw []
  >> ASM_REWRITE_TAC [ltree_node_children_reduce]