ltree_finite_BT_has_benf and ltree_finite_BT_benf

examples/lambda/barendregt/lameta_completeScript.sml

@@ -1443,27 +1443,22 @@ 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 ==>
+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
-    cheat
+    rw [has_benf_has_bnf]
+ >> MATCH_MP_TAC ltree_finite_BT_has_bnf >> art []
 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 ==>
+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
-    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
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC ltree_finite_BT_has_benf
+ >> rw [has_benf_def]
+ >> Q.EXISTS_TAC ‘M’ >> rw [lameta_REFL]
 QED
 
 (* NOTE: All bottoms ($\bot$) are translated to “Omega” (Omega_def). If a term

src/coalgebras/ltreeScript.sml

@@ -969,6 +969,28 @@ Proof
  >> Cases_on ‘LNTH h ts’ >> rw []
 QED
 
+(*---------------------------------------------------------------------------*
+ *  ltree_delete: delete the rightmost children at a subtree
+ *---------------------------------------------------------------------------*)
+
+(* NOTE: p is the path arriving at the parent node whose rightmost children
+   is going to be deleted. f is the modifier function for the parent node in
+   case it needs changes after losing one children.
+ *)
+Definition ltree_delete_def :
+    ltree_delete f t p =
+    gen_ltree (\ns. THE do (d,len) <- ltree_el t ns;
+                                   m <- len;
+                           return
+                             if ns = p /\ len <> NONE /\ 0 < m then
+                               (f d,SOME (m - 1))
+                             else
+                               (d,len)
+                        od)
+End
+
+Overload ltree_delete' = “ltree_delete I”
+
 (*---------------------------------------------------------------------------*
  *  ltree_finite and (finite) ltree_paths
  *---------------------------------------------------------------------------*)
@@ -1041,12 +1063,7 @@ Proof
  (* “ltree_el t p” is the ltree node where t and t' (to be constructed) differ *)
  >> qabbrev_tac ‘p = FRONT a’
  >> 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’
+ >> qabbrev_tac ‘t' = ltree_delete' t p’
  >> cheat
 QED