[ltree] More supporting theorems for rose trees

src/coalgebras/llistScript.sml

@@ -1,7 +1,11 @@
+(* ===================================================================== *)
+(* FILE          : llistScript.sml                                       *)
+(* DESCRIPTION   : Possibly infinite sequences (llist)                   *)
+(* ===================================================================== *)
 
 open HolKernel boolLib Parse bossLib
 
-open BasicProvers boolSimps markerLib optionTheory ;
+open BasicProvers boolSimps markerLib optionTheory hurdUtils;
 
 val _ = new_theory "llist";
 
@@ -3222,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

src/coalgebras/ltreeScript.sml

@@ -960,6 +960,14 @@ Datatype:
   rose_tree = Rose 'a (rose_tree list)
 End
 
+Definition rose_node_def[simp] :
+    rose_node (Rose a ts) = a
+End
+
+Definition rose_children_def[simp] :
+    rose_children (Rose a ts) = ts
+End
+
 Definition from_rose_def:
   from_rose (Rose a ts) = Branch a (fromList (MAP from_rose ts))
 Termination
@@ -968,6 +976,24 @@ End
 
 Theorem rose_tree_induction[allow_rebind] = from_rose_ind;
 
+Theorem from_rose_11 :
+    !r1 r2. from_rose r1 = from_rose r2 <=> r1 = r2
+Proof
+    rpt GEN_TAC
+ >> reverse EQ_TAC >- simp []
+ >> qid_spec_tac ‘r2’
+ >> qid_spec_tac ‘r1’
+ >> HO_MATCH_MP_TAC rose_tree_induction
+ >> rpt STRIP_TAC
+ >> Cases_on ‘r2’
+ >> fs [from_rose_def]
+ >> POP_ASSUM MP_TAC
+ >> rw [LIST_EQ_REWRITE, EL_MAP]
+ >> rename1 ‘n < LENGTH l’
+ >> Q.PAT_X_ASSUM ‘!r1. MEM r1 ts ==> P’ (MP_TAC o Q.SPEC ‘EL n ts’)
+ >> rw [EL_MEM, EL_MAP]
+QED
+
 Theorem ltree_finite_from_rose:
   ltree_finite t <=> ?r. from_rose r = t
 Proof
@@ -987,6 +1013,71 @@ Proof
   \\ fs [EVERY_MEM,MEM_MAP,PULL_EXISTS]
 QED
 
+(* The previous theorem induces a new constant “to_rose” for finite ltrees *)
+local
+  val thm = Q.prove (‘!t. ltree_finite t ==> ?r. from_rose r = t’,
+                     METIS_TAC [ltree_finite_from_rose]);
+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);
+end;
+
+Theorem to_rose_thm :
+    !r. to_rose (from_rose r) = r
+Proof
+    Q.X_GEN_TAC ‘r’
+ >> qabbrev_tac ‘t = from_rose r’
+ >> ‘ltree_finite t’ by METIS_TAC [ltree_finite_from_rose]
+ >> rw [GSYM from_rose_11, to_rose_def]
+QED
+
+Theorem rose_node_to_rose :
+    !t. ltree_finite t ==> rose_node (to_rose t) = ltree_node t
+Proof
+    rw [ltree_finite_from_rose]
+ >> rw [to_rose_thm]
+ >> Cases_on ‘r’
+ >> rw [rose_node_def, from_rose_def, ltree_node_def]
+QED
+
+Theorem rose_children_to_rose :
+    !t. ltree_finite t ==>
+        rose_children (to_rose t) = MAP to_rose (THE (toList (ltree_children t)))
+Proof
+    rw [ltree_finite_from_rose]
+ >> rw [to_rose_thm]
+ >> Cases_on ‘r’
+ >> rw [rose_node_def, from_rose_def, ltree_node_def]
+ >> simp [from_toList, MAP_MAP_o]
+ >> simp [o_DEF, to_rose_thm]
+QED
+
+Theorem rose_children_to_rose' :
+    !t. ltree_finite t ==>
+        rose_children (to_rose t) = THE (toList (LMAP to_rose (ltree_children t)))
+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_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]
+QED
+
+(* This is a general recursive reduction function for rose trees. The type of
+   f is “:'a -> 'b list -> 'b”, where 'b is the type of reductions of trees.
+
+   See examples/lambda/barendregt/lameta_complateTheory.rose_to_term_def for
+   an application.
+ *)
+Definition rose_reduce_def :
+    rose_reduce f ((Rose a ts) :'a rose_tree) = f a (MAP (rose_reduce f) ts)
+Termination
+    WF_REL_TAC ‘measure (rose_tree_size (K 0) o SND)’
+End
 
 (* tidy up theory exports *)
 

src/list/src/listScript.sml

@@ -1767,6 +1767,13 @@ val MEM_EL = store_thm(
     ASM_MESON_TAC []
   ]);
 
+Theorem EL_MEM :
+    !n l. n < LENGTH l ==> MEM (EL n l) l
+Proof
+    RW_TAC std_ss [MEM_EL]
+ >> Q.EXISTS_TAC ‘n’ >> ASM_REWRITE_TAC []
+QED
+
 val SUM_MAP_PLUS_ZIP = store_thm(
   "SUM_MAP_PLUS_ZIP",
   “!ls1 ls2.

src/list/src/rich_listScript.sml

@@ -2302,14 +2302,7 @@ val TAKE_SEG_DROP = Q.store_thm("TAKE_SEG_DROP",
   first_x_assum (Q.SPECL_THEN [‘SUC n’, ‘m’] mp_tac) >>
   SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [ADD1]);
 
-val EL_MEM = Q.store_thm ("EL_MEM",
-   `!n l. n < LENGTH l ==> (MEM (EL n l) l)`,
-   INDUCT_TAC
-   THEN LIST_INDUCT_TAC
-   THEN ASM_REWRITE_TAC [LENGTH, EL, HD, TL, NOT_LESS_0, LESS_MONO_EQ, MEM]
-   THEN REPEAT STRIP_TAC
-   THEN DISJ2_TAC
-   THEN RES_TAC);
+Theorem EL_MEM = listTheory.EL_MEM
 
 val TL_SNOC = Q.store_thm ("TL_SNOC",
    `!x l. TL (SNOC x l) = if NULL l then [] else SNOC x (TL l)`,
@@ -4425,6 +4418,13 @@ Proof
   simp[]
 QED
 
+Theorem HD_APPEND_NOT_NIL :
+  !l1 l2. l1 <> [] ==> HD (l1 ++ l2) = HD l1
+Proof
+    rpt GEN_TAC
+ >> Cases_on ‘l1’ >> rw [HD_APPEND]
+QED
+
 (* Theorem: 0 <> n ==> (EL (n-1) t = EL n (h::t)) *)
 (* Proof:
    Note n = SUC k for some k         by num_CASES