Stage work on ltree_finite_BT_has_benf

examples/lambda/barendregt/lameta_completeScript.sml

@@ -1443,6 +1443,29 @@ Proof
  >> Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV M’ >> art []
 QED
 
+Theorem ltree_finite_BT_benf :
+    !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ benf M ==>
+            ltree_finite (BT' X M r)
+Proof
+    cheat
+QED
+
+(* NOTE: This proof relies on has_benf_thm and takahashi_3_5 *)
+Theorem ltree_finite_BT_has_benf :
+    !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ has_benf M ==>
+            ltree_finite (BT' X M r)
+Proof
+    rw [has_benf_thm]
+ >> ‘?P. M -b->* P /\ reduction eta P N’ by PROVE_TAC [takahashi_3_5]
+ >> ‘M == P’ by PROVE_TAC [betastar_lameq]
+ >> ‘FV P SUBSET FV M’ by PROVE_TAC [betastar_FV_SUBSET]
+ >> Know ‘BT' X M r = BT' X P r’
+ >- (MATCH_MP_TAC lameq_BT_cong >> art [] \\
+     Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV M’ >> art [])
+ >> Rewr
+ >> cheat
+QED
+
 (* NOTE: All bottoms ($\bot$) are translated to “Omega” (Omega_def). If a term
    is bnf (or has_bnf), then all terms are solvable, and there's no bottom in
    the resulting Boehm tree.
@@ -1455,26 +1478,27 @@ Definition rose_to_term_def :
 End
 
 (* NOTE: This assumes that the input Boehm tree is finite (ltree_finite). *)
-Definition BT_to_term :
-    BT_to_term = rose_to_term o to_rose
+Definition from_BT :
+    from_BT = rose_to_term o to_rose
 End
 
-(* |- !A. BT_to_term A =
+(* |- !t. from_BT t =
           rose_reduce
             (\x args.
                  case x of
                    NONE => Omega
-                 | SOME (vs,y) => LAMl vs (VAR y @* args)) (to_rose A)
+                 | SOME (vs,y) => LAMl vs (VAR y @* args)) (to_rose t)
  *)
-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
+Theorem from_BT_def =
+        from_BT |> SIMP_RULE std_ss [FUN_EQ_THM, rose_to_term_def, o_DEF]
+                |> Q.SPEC ‘t’ |> 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 /\
               has_benf M /\ has_benf N /\ ~lameta M N ==>
-              ?p. p IN BT_paths M INTER BT_paths N /\ ~subtree_equiv X M N p r
+              ?p. p IN BT_paths M /\ p IN BT_paths N /\
+                  ~subtree_equiv X M N p r
 Proof
     cheat
 QED

src/coalgebras/ltreeScript.sml

@@ -1004,6 +1004,10 @@ Theorem finite_ltree_paths_imp_ltree_finite_lemma[local] :
     !s. FINITE s ==> !t. ltree_paths t = s ==> ltree_finite t
 Proof
     HO_MATCH_MP_TAC FINITE_MAXIMAL_MEASURE_INDUCTION
+ (* TODO: how to define a measure taking into account (in lexicographic order):
+    1. LENGTH of list
+    2. LAST of list
+  *)
  >> Q.EXISTS_TAC ‘LENGTH’
  >> rw []
  >- (fs [ltree_paths_alt, Once EXTENSION] \\
@@ -1036,7 +1040,13 @@ Proof
      METIS_TAC [])
  (* “ltree_el t p” is the ltree node where t and t' (to be constructed) differ *)
  >> qabbrev_tac ‘p = FRONT a’
- (* construct t' by ltree_unfold of t *)
+ >> qabbrev_tac ‘n = LAST a’
+ (* construct t' by gen_ltree *)
+ >> qabbrev_tac ‘f = \ns. case (ltree_el t ns) of
+                            NONE => (ARB,SOME 0)
+                          | SOME (d,len) =>
+                            (d,if ns = p then OPTION_MAP PRE len else len)’
+ >> qabbrev_tac ‘t' = gen_ltree f’
  >> cheat
 QED