EOD only ltree_finite_insert is left

src/coalgebras/ltreeScript.sml

@@ -1189,11 +1189,34 @@ QED
 
 Theorem ltree_el_ltree_delete :
     !f p t. ltree_el t p = SOME (a,SOME (SUC n)) ==>
-          ltree_el (ltree_delete f t p) p = SOME (a,SOME n)
+            ltree_el (ltree_delete f t p) p = SOME (f a,SOME n)
 Proof
-    cheat
+    Q.X_GEN_TAC ‘f’
+ >> Induct_on ‘p’
+ >- (rpt STRIP_TAC \\
+     Cases_on ‘t’ >> fs [ltree_el_def, ltree_delete_NIL] \\
+    ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
+     simp [ltree_el_def])
+ >> rpt STRIP_TAC
+ >> Cases_on ‘t’ >> fs [ltree_el_def]
+ >> Cases_on ‘LNTH h ts’ >> fs []
+ >> MP_TAC (Q.SPECL [‘f’, ‘a'’, ‘ts’, ‘h’, ‘p’, ‘x’] ltree_delete_CONS)
+ >> simp []
+ >> DISCH_THEN K_TAC
+ >> rw [ltree_el_def, LNTH_LGENLIST]
+ >> Cases_on ‘LLENGTH ts’ >> simp []
+ >> rename1 ‘LLENGTH ts = SOME N’
+ >> Know ‘IS_SOME (LNTH h ts)’ >- rw [IS_SOME_EXISTS]
+ >> rw [LNTH_IS_SOME, LFINITE_LLENGTH]
 QED
 
+(* |- !p t.
+        ltree_el t p = SOME (a,SOME (SUC n)) ==>
+        ltree_el (ltree_delete' t p) p = SOME (a,SOME n)
+ *)
+Theorem ltree_el_ltree_delete' =
+        ltree_el_ltree_delete |> Q.SPEC ‘I’ |> SRULE []
+
 (* NOTE: “ltree_el t p = SOME (a,SOME (SUC n)” indicates that “SNOC n p” is the
    subtree to be deleted.
  *)
@@ -1202,8 +1225,7 @@ Theorem ltree_delete_paths :
        ltree_el t p = SOME (a,SOME (SUC n)) ==>
        ltree_paths (ltree_delete f t p) =
        ltree_paths t DIFF
-         (IMAGE (\q. SNOC n p ++ q)
-                (ltree_paths (THE (ltree_lookup t (SNOC n p)))))
+         (IMAGE (\q. SNOC n p ++ q) (ltree_paths (THE (ltree_lookup t (SNOC n p)))))
 Proof
     Q.X_GEN_TAC ‘f’
  >> Induct_on ‘p’
@@ -1367,6 +1389,50 @@ Definition ltree_insert_def :
                        THE (ltree_el t0 (DROP (LENGTH p + 1) ns)))
 End
 
+Theorem ltree_insert_NIL :
+    !f a ts.
+         ltree_insert f (Branch a ts) [] t0 =
+         if LFINITE ts then
+            Branch (f a)
+               (LGENLIST (\i. if i < THE (LLENGTH ts) then THE (LNTH i ts)
+                              else t0)
+                         (SOME (THE (LLENGTH ts) + 1)))
+         else
+            Branch a ts
+Proof
+    rw [ltree_insert_def]
+ >- (rw [Once gen_ltree, ltree_el_def] >| (* 3 subgoals *)
+     [ (* goal 1 (of 3) *)
+       rw [LNTH_EQ, LNTH_LGENLIST] \\
+       gs [LFINITE_LLENGTH] \\
+       rename1 ‘LLENGTH ts = SOME N’ \\
+       Cases_on ‘n < N + 1’ >> simp [] \\
+      ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
+       Cases_on ‘LNTH n ts’ >> simp []
+       >- (Know ‘~IS_SOME (LNTH n ts)’ >- rw [] \\
+           POP_ASSUM K_TAC \\
+           ASM_SIMP_TAC bool_ss [LFINITE_LNTH_IS_SOME] \\
+           simp [] \\
+           rw [gen_ltree_unchanged]) \\
+       Know ‘IS_SOME (LNTH n ts)’ >- rw [] \\
+       rw [LFINITE_LNTH_IS_SOME] \\
+       simp [ltree_el_lemma] \\
+       rw [gen_ltree_unchanged_extra],
+       (* goal 2 (of 3) *)
+       gs [LFINITE_LLENGTH],
+       (* goal 3 (of 3) *)
+       gs [LFINITE_LLENGTH] ])
+ >> rw [Once gen_ltree, ltree_el_def]
+ >- (Cases_on ‘LLENGTH ts’ >> fs [LFINITE_LLENGTH])
+ >- (Cases_on ‘LLENGTH ts’ >> fs [LFINITE_LLENGTH])
+ >> rw [LNTH_EQ, LNTH_LGENLIST]
+ >> ‘!n. ?x. LNTH n ts = SOME x’ by METIS_TAC [infinite_lnth_some]
+ >> POP_ASSUM (MP_TAC o Q.SPEC ‘n’) >> rw []
+ >> simp []
+ >> simp [ltree_el_lemma]
+ >> rw [gen_ltree_unchanged_extra]
+QED
+
 Theorem ltree_insert_CONS :
     !f a ts h p t t0.
          LNTH h ts = SOME t /\ ltree_el t p <> NONE ==>
@@ -1409,13 +1475,12 @@ Proof
  >> rw [gen_ltree_unchanged_extra]
 QED
 
+(* ltree_finite_ind *)
 Theorem ltree_finite_insert :
-    !t. ltree_finite t ==>
-        !p d len. ltree_el t p = SOME (d,len) /\
-                  ltree_finite t0 ==> ltree_finite (ltree_insert f t p t0)
+    !p t d len. ltree_finite t /\ ltree_el t p = SOME (d,len) /\
+                ltree_finite t0 ==> ltree_finite (ltree_insert f t p t0)
 Proof
-    HO_MATCH_MP_TAC ltree_finite_ind
- >> cheat
+    cheat
 QED
 
 (* NOTE: These are simple versions not modifying ltree node data. *)
@@ -1768,7 +1833,7 @@ Proof
  >> irule ltree_finite_insert >> art []
  >> qexistsl_tac [‘a'’, ‘SOME i’]
  >> qunabbrev_tac ‘t'’
- >> MATCH_MP_TAC ltree_el_ltree_delete >> art []
+ >> MATCH_MP_TAC ltree_el_ltree_delete' >> art []
 QED
 
 Theorem finite_ltree_paths_imp_ltree_finite[local] :