Stage work on ltree_finite_BT_bnf

examples/lambda/barendregt/head_reductionScript.sml

@@ -217,6 +217,14 @@ Proof
  >> Q.EXISTS_TAC ‘M0’ >> rw []
 QED
 
+Theorem hreduce_LAM :
+    !v M1 M2. LAM v M1 -h->* LAM v M2 <=> M1 -h->* M2
+Proof
+    rpt STRIP_TAC
+ >> MP_TAC (Q.SPECL [‘[v]’, ‘M1’, ‘M2’] hreduce_LAMl)
+ >> REWRITE_TAC [LAMl_thm]
+QED
+
 Theorem hreduce1_abs :
     !M N. M -h-> N ==> is_abs M ==> is_abs N
 Proof
@@ -1645,10 +1653,14 @@ Theorem hnf_head_hnf[simp] :
 Proof
     CONJ_TAC
  >- NTAC 2 (rw [Once hnf_head_def])
- >> MATCH_MP_TAC hnf_head_appstar
- >> rw []
+ >> MATCH_MP_TAC hnf_head_appstar >> rw []
 QED
 
+(* |- hnf_head (VAR y) = VAR y *)
+Theorem hnf_head_VAR[simp] =
+    (cj 2 hnf_head_hnf) |> Q.GEN ‘args’ |> Q.SPEC ‘[]’
+                        |> REWRITE_RULE [appstar_empty]
+
 Overload hnf_headvar = “\t. THE_VAR (hnf_head t)”
 
 (* hnf_children retrives the ‘args’ part of absfree hnf *)
@@ -1684,6 +1696,10 @@ Proof
  >> MATCH_MP_TAC hnf_children_appstar >> rw []
 QED
 
+(* |- hnf_children (VAR y) = [] *)
+Theorem hnf_children_VAR[simp] =
+        hnf_children_hnf |> Q.SPECL [‘y’, ‘[]’] |> REWRITE_RULE [appstar_empty]
+
 Theorem absfree_hnf_cases :
     !M. hnf M /\ ~is_abs M <=> ?y args. M = VAR y @* args
 Proof

examples/lambda/barendregt/lameta_completeScript.sml

@@ -1338,7 +1338,9 @@ QED
  *---------------------------------------------------------------------------*)
 
 (* 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).
+   All bottoms ($\bot$) are translated to “Omega” (see Omega_def). If a term is
+   bnf (or has_bnf), then all terms are solvable, and there's no bottom in the
+   tree.
  *)
 Definition rose_to_term_def :
     rose_to_term =
@@ -1369,10 +1371,66 @@ Theorem BT_to_term_def =
    by nc_INDUCTION2.
  *)
 Theorem ltree_finite_BT_bnf :
-    !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ bnf M ==>
+    !M X r. FINITE X /\ FV M SUBSET X UNION RANK r /\ bnf M ==>
             ltree_finite (BT' X M r)
 Proof
-    cheat
+    HO_MATCH_MP_TAC nc_INDUCTION2
+ >> Q.EXISTS_TAC ‘{}’ >> rw [] (* 3 subgoals *)
+ (* goal 1 (of 3): VAR s *)
+ >- (simp [BT_def, BT_generator_def, Once ltree_unfold, principle_hnf_reduce] \\
+     rw [ltree_finite])
+ (* goal 2 (of 3): M @@ M' *)
+ >- (MP_TAC (Q.SPEC ‘M’ bnf_characterisation) >> rw [] \\
+     gs [is_abs_LAMl, is_abs_appstar, FV_appstar, BIGUNION_IMAGE_SUBSET] \\
+     REWRITE_TAC [GSYM appstar_SNOC] \\
+     qabbrev_tac ‘Ms' = SNOC M' Ms’ \\
+     simp [BT_def, BT_generator_def, Once ltree_unfold, principle_hnf_reduce] \\
+     simp [GSYM BT_def, LMAP_fromList, MAP_MAP_o, o_DEF] \\
+     rw [ltree_finite, MEM_MAP, Abbr ‘Ms'’]
+     >- (FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\
+         Q_TAC (TRANS_TAC SUBSET_TRANS) ‘X UNION RANK r’ >> art [] \\
+         Suff ‘RANK r SUBSET RANK (SUC r)’ >- SET_TAC [] \\
+         rw [RANK_MONO]) \\
+     Q.PAT_X_ASSUM ‘!X r. FINITE X /\ v IN X UNION RANK r /\ _ ==> ltree_finite _’
+       (MP_TAC o Q.SPECL [‘X’, ‘r’]) >> simp [] \\
+    ‘solvable (VAR v @* Ms)’ by rw [] \\
+     Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold])
+           ‘BT' X (VAR v @* Ms) r’ \\
+     gs [principle_hnf_reduce, Abbr ‘M0’, Abbr ‘n’, Abbr ‘vs’, Abbr ‘M1’,
+         Abbr ‘y’, Abbr ‘Ms'’, Abbr ‘l’, GSYM BT_def, LMAP_fromList,
+         MAP_MAP_o, o_DEF] \\
+     DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE [ltree_finite]) >> rw [MEM_MAP] \\
+     POP_ASSUM MATCH_MP_TAC \\
+     Q.EXISTS_TAC ‘e’ >> art [])
+ (* goal 3 (of 3): LAM y M *)
+ >> reverse (rw [BT_def, BT_generator_def, Once ltree_unfold])
+ >- rw [ltree_finite]
+ >> simp [GSYM BT_def, LMAP_fromList, MAP_MAP_o, o_DEF]
+ (* NOTE: “principle_hnf M” vs “principle_hnf (LAM y M)”
+
+    1. M -h->* M0 = LAMl vs (VAR y @* args) (hnf)
+    2. LAM y M -h->* LAM y M0 = LAMl (y::vs) (VAR y @* args) (hnf)
+
+    But it's possible that ‘MEM y vs’. In this case, we can safely allocate
+    another name and replace it with y, without changing inner terms.
+
+    Otherwise, if y is not in ROW r, we need to allocate another fresh name
+    in ROW r and replace it with ‘y’, and this case tpm of children terms.
+  *)
+ >> qabbrev_tac ‘M0  = principle_hnf M’
+ >> qabbrev_tac ‘M0' = principle_hnf (LAM y M)’
+ >> qabbrev_tac ‘n   = LAMl_size M0’
+ >> qabbrev_tac ‘n'  = LAMl_size M0'’
+ >> Q_TAC (RNEWS_TAC (“vs' :string list”, “r :num”, “n' :num”)) ‘X’
+ >> cheat
+QED
+
+Theorem ltree_finite_BT_has_bnf :
+    !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ has_bnf M ==>
+            ltree_finite (BT' X M r)
+Proof
+    rw [has_bnf_def] >> rename1 ‘bnf M'’
+ >> cheat
 QED
 
 (* Exercise 10.6.9 [1, p.272] *)
@@ -1385,7 +1443,7 @@ Proof
 QED
 
 (*---------------------------------------------------------------------------*
- *  Separability of lambda terms
+ *  Separability of (two) lambda terms
  *---------------------------------------------------------------------------*)
 
 Theorem separability_lemma0_case2[local] :

examples/lambda/barendregt/solvableScript.sml

@@ -659,19 +659,21 @@ Proof
  >> MATCH_MP_TAC unsolvable_subst >> art []
 QED
 
-Theorem solvable_hnf[simp] :
-    solvable (LAMl vs (VAR y @* args))
+Theorem solvable_hnf :
+    !vs y args. solvable (LAMl vs (VAR y @* args))
 Proof
-    REWRITE_TAC [solvable_iff_has_hnf]
+    rw [solvable_iff_has_hnf]
  >> MATCH_MP_TAC hnf_has_hnf >> rw []
 QED
 
-Theorem solvable_absfree_hnf[simp] :
-    solvable (VAR y @* args)
-Proof
-    REWRITE_TAC [solvable_iff_has_hnf]
- >> MATCH_MP_TAC hnf_has_hnf >> rw []
-QED
+(* |- solvable (VAR y @* args) *)
+Theorem solvable_absfree_hnf[simp] =
+        solvable_hnf |> Q.SPECL [‘[]’, ‘y’, ‘args’] |> REWRITE_RULE [LAMl_thm]
+
+(* |- solvable (VAR y) *)
+Theorem solvable_VAR[simp] =
+        solvable_hnf |> Q.SPECL [‘[]’, ‘y’, ‘[]’]
+                     |> REWRITE_RULE [LAMl_thm, appstar_empty]
 
 (*---------------------------------------------------------------------------*
  *  Principle Head Normal Forms (principle_hnf)

src/coalgebras/llistScript.sml

@@ -1118,10 +1118,11 @@ val LTL_fromList = Q.store_thm(
   `LTL (fromList l) = if NULL l then NONE else SOME (fromList (TL l))`,
   Cases_on `l` >> simp[]);
 
-val LFINITE_fromList = store_thm(
-  "LFINITE_fromList",
-  ``!l. LFINITE (fromList l)``,
-  Induct THEN ASM_SIMP_TAC (srw_ss()) []);
+Theorem LFINITE_fromList[simp] :
+    !l. LFINITE (fromList l)
+Proof
+  Induct THEN ASM_SIMP_TAC (srw_ss()) []
+QED
 
 val LLENGTH_fromList = store_thm(
   "LLENGTH_fromList[simp]",
@@ -2966,6 +2967,12 @@ Definition LSET_def:
   LSET l x = ?n. LNTH n l = SOME x
 End
 
+Theorem IN_LSET :
+    !x l. x IN LSET l <=> ?n. LNTH n l = SOME x
+Proof
+    rw [IN_APP, LSET_def]
+QED
+
 Theorem LSET[simp]:
   LSET LNIL = {} /\
   LSET (x:::xs) = x INSERT LSET xs
@@ -2977,6 +2984,13 @@ Proof
   THEN1 (qexists_tac `SUC n` \\ fs [])
 QED
 
+Theorem LSET_fromList[simp] :
+    LSET (fromList l) = set l
+Proof
+    rw [Once EXTENSION, IN_LSET, LNTH_fromList, MEM_EL]
+ >> METIS_TAC []
+QED
+
 Definition llist_rel_def:
   llist_rel R l1 l2 <=>
     LLENGTH l1 = LLENGTH l2 /\