Done rose_children_to_rose, etc.

examples/lambda/barendregt/lameta_completeScript.sml

@@ -7,8 +7,8 @@
 
 open HolKernel Parse boolLib bossLib;
 
-open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory
-     ltreeTheory llistTheory relationTheory tautLib topologyTheory;
+open hurdUtils combinTheory tautLib arithmeticTheory pred_setTheory listTheory
+     rich_listTheory llistTheory ltreeTheory relationTheory topologyTheory;
 
 open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory NEWLib
      horeductionTheory solvableTheory head_reductionTheory head_reductionLib
@@ -1333,6 +1333,7 @@ Proof
  >> simp []
 QED
 
+(* NOTE: useless, to be removed *)
 Theorem is_faithful_swap :
     !p X M N pi r. is_faithful p X [M; N] pi r <=> is_faithful p X [N; M] pi r
 Proof
@@ -1344,23 +1345,31 @@ QED
  * Distinct beta-eta-NFs are not everywhere (subtree) equivalent
  *---------------------------------------------------------------------------*)
 
-(* NOTE: This definition is impossible for ltree because ltree has no "size",
-   all bottom (\bot) leaves are treated as the “Omega” term. For terms having
-   benf, there should be no bottoms in their Boehm trees.
+(* NOTE: Here the input is a rose tree corresponding to a Boehm tree as ltree.
+   All bottoms (\bot) are translated to “Omega” (see Omega_def).
  *)
-Definition fromRose_def :
-    fromRose (t :BT_node rose_tree) =
-      case (rose_node t) of
-        SOME (vs,y) => LAMl vs (VAR y @* MAP fromRose (rose_children t))
-      | NONE => Omega
-Termination
-    WF_REL_TAC ‘measure (rose_tree_size (\x. 0))’ >> rw []
- >> MP_TAC (ISPEC “t :BT_node rose_tree” rose_tree_nchotomy)
- >> STRIP_TAC
- >> fs [rose_tree_size_def, rose_tree_size_eq, Once MEM_SPLIT_APPEND_first]
- >> simp [list_size_append, list_size_def]
+Definition rose_to_term_def :
+    rose_to_term =
+    rose_reduce (\x args. case x of
+                            SOME (vs,y) => LAMl vs (VAR y @* args)
+                          | NONE => Omega)
+End
+
+Definition BT_to_term :
+    BT_to_term = rose_to_term o to_rose
 End
 
+(* |- !A. BT_to_term A =
+          rose_reduce
+            (\x args.
+                 case x of
+                   NONE => Omega
+                 | SOME (vs,y) => LAMl vs (VAR y @* args)) (to_rose A)
+ *)
+Theorem BT_to_term_def =
+        BT_to_term |> SIMP_RULE std_ss [FUN_EQ_THM, rose_to_term_def, o_DEF]
+                   |> Q.SPEC ‘A’ |> GEN_ALL
+
 (* Exercise 10.6.9 [1, p.272] *)
 Theorem distinct_benf_imp_not_subtree_equiv :
     !X M N r. FINITE X /\ X SUBSET FV M UNION FV N /\

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";
 
@@ -1152,6 +1156,15 @@ 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 ==>

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,7 @@ 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]);
@@ -997,19 +1024,61 @@ in
      SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] thm);
 end;
 
-Definition rose_node_def[simp] :
-    rose_node (Rose a ts) = a
-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
 
-Definition rose_children_def[simp] :
-    rose_children (Rose a ts) = ts
-End
+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
 
-(* This is a general recursive reduction function for rose trees *)
+(* 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)))
+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_THE_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 (\x. 0) o SND)’
+    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)`,