From da2d9a2a629882b62a5342f3460d211aaaeebe60 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Wed, 1 Jan 2025 22:31:11 +1100 Subject: [PATCH] [lambda] remove non-standard is_ready'; move equivalent_def, etc. out of boehmTheory --- examples/lambda/barendregt/boehmScript.sml | 523 +++++------------- .../barendregt/lameta_completeScript.sml | 278 +++++++++- src/coalgebras/ltreeScript.sml | 2 +- 3 files changed, 384 insertions(+), 419 deletions(-) diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml index 7dcd680aed..1221ec89d7 100644 --- a/examples/lambda/barendregt/boehmScript.sml +++ b/examples/lambda/barendregt/boehmScript.sml @@ -49,29 +49,6 @@ fun PRINT_TAC pfx g = (print (pfx ^ "\n"); ALL_TAC g); Overload FV = “supp term_pmact” Overload VAR = “term$VAR” -(*---------------------------------------------------------------------------* - * ltreeTheory extras - *---------------------------------------------------------------------------*) - -(* ltree_subset A B <=> A results from B by "cutting off" some subtrees. Thus, - - 1) The paths of A is a subset of paths of B - 2) The node contents for all paths of A is identical to those of B, but the number - of successors at those nodes of B may be different (B may have more successors) - - NOTE: Simply defining ‘ltree_subset A B <=> subtrees A SUBSET subtrees B’ is wrong, - as A may appear as a non-root subtree of B, i.e. ‘A IN subtrees B’ but there's - no way to "cut off" B to get A, the resulting subtree in B always have some - more path prefixes. - *) -Definition ltree_subset_def : - ltree_subset A B <=> - (ltree_paths A) SUBSET (ltree_paths B) /\ - !p. p IN ltree_paths A ==> - ltree_node (THE (ltree_lookup A p)) = - ltree_node (THE (ltree_lookup B p)) -End - (*---------------------------------------------------------------------------* * Boehm Trees (and subterms) - name after Corrado_Böhm [2] UOK * *---------------------------------------------------------------------------*) @@ -1008,51 +985,68 @@ Proof >> Q.PAT_X_ASSUM ‘Ms = Ms'’ (fs o wrap o SYM) QED -(* NOTE: When subterm X M p = NONE, either 1) M or its subterm is unsolvable, - or 2) p runs out of ltree_paths (BT X M). If we knew subterm X M p <> NONE - a priori, then p IN ltree_paths (BT X M) must hold. - *) -Theorem subterm_imp_ltree_paths : - !p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ - subterm X M p r <> NONE ==> - p IN ltree_paths (BT' X M r) +Theorem BT_ltree_el_eq_none : + !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r ==> + (ltree_el (BT' X M r) p = NONE <=> subterm X M p r = NONE) Proof - Induct_on ‘p’ >- rw [] - >> rpt GEN_TAC - >> STRIP_TAC - >> POP_ASSUM MP_TAC (* subterm X M (h::p) r <> NONE *) + Suff ‘!X. FINITE X ==> + !p M r. FV M SUBSET X UNION RANK r ==> + (ltree_el (BT' X M r) p = NONE <=> + subterm X M p r = NONE)’ + >- METIS_TAC [] + >> Q.X_GEN_TAC ‘X’ >> DISCH_TAC + >> Induct_on ‘p’ + >- rw [BT_ltree_el_NIL] + >> rpt STRIP_TAC >> reverse (Cases_on ‘solvable M’) - >- simp [subterm_def, ltree_paths_def, ltree_lookup] - >> UNBETA_TAC [subterm_alt] “subterm X M (h::p) r” - >> UNBETA_TAC [BT_def, Once ltree_unfold, BT_generator_def] “BT' X M r” - >> simp [LMAP_fromList, EL_MAP, Abbr ‘l’] - >> ‘n = n'’ by rw [Abbr ‘n’, Abbr ‘n'’] - >> POP_ASSUM (fs o wrap o SYM) - >> Q.PAT_X_ASSUM ‘vs = vs'’ (fs o wrap o SYM) - >> Q.PAT_X_ASSUM ‘M1 = M1'’ (fs o wrap o SYM) - >> Q.PAT_X_ASSUM ‘Ms = Ms'’ (fs o wrap o SYM) - >> qunabbrev_tac ‘vs’ + >- rw [subterm_def, BT_of_unsolvables, ltree_el_def] + (* stage work *) + >> rw [subterm_def, BT_def, BT_generator_def, Once ltree_unfold, ltree_el_def] + >> qabbrev_tac ‘M0 = principle_hnf M’ + >> qabbrev_tac ‘n = LAMl_size M0’ >> Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ >> ‘DISJOINT (set vs) (FV M0)’ by METIS_TAC [subterm_disjoint_lemma'] - (* extra work *) - >> qunabbrev_tac ‘y’ + >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’ >> Q_TAC (HNF_TAC (“M0 :term”, “vs :string list”, “y :string”, “args :term list”)) ‘M1’ >> ‘TAKE n vs = vs’ by rw [] >> POP_ASSUM (rfs o wrap) + >> qabbrev_tac ‘m = LENGTH args’ + >> simp [LNTH_fromList, GSYM BT_def, EL_MAP] >> Cases_on ‘h < m’ >> simp [] - >> ‘Ms = args’ by rw [Abbr ‘Ms’] - >> POP_ASSUM (fs o wrap) - >> DISCH_TAC - >> simp [GSYM BT_def] - >> fs [ltree_paths_def, ltree_lookup_def, LNTH_fromList, EL_MAP] - >> T_TAC - (* extra work *) - >> FIRST_X_ASSUM MATCH_MP_TAC >> art [] + >> qabbrev_tac ‘N = EL h args’ + >> FIRST_X_ASSUM MATCH_MP_TAC + >> qunabbrev_tac ‘N’ >> MATCH_MP_TAC subterm_induction_lemma' >> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp [] QED +Theorem ltree_paths_valid_thm : + !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r ==> + (p IN ltree_paths (BT' X M r) <=> subterm X M p r <> NONE) +Proof + rw [ltree_paths_alt, BT_ltree_el_eq_none] +QED + +Theorem subterm_imp_ltree_paths : + !p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ + subterm X M p r <> NONE ==> + p IN ltree_paths (BT' X M r) +Proof + PROVE_TAC [ltree_paths_valid_thm] +QED + +(* p <> [] is required because ‘[] IN ltree_paths (BT' X M r)’ always holds. *) +Theorem ltree_paths_imp_solvable : + !p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ p <> [] /\ + p IN ltree_paths (BT' X M r) ==> solvable M +Proof + rw [ltree_paths_def] + >> Cases_on ‘p’ >> fs [] + >> CCONTR_TAC + >> fs [BT_of_unsolvables, ltree_lookup_def] +QED + (* ltree_lookup returns more information (the entire subtree), thus can be used to construct the return value of ltree_el. @@ -1177,14 +1171,6 @@ Proof >> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp [] QED -Theorem subterm_is_none_exclusive : - !p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ - p IN ltree_paths (BT' X M r) /\ - subterm X M p r = NONE ==> subterm X M (FRONT p) r <> NONE -Proof - METIS_TAC [subterm_is_none_iff_parent_unsolvable] -QED - (* NOTE: for whatever reasons such that ‘subterm X M p = NONE’, even when ‘p NOTIN ltree_paths (BT X M)’, the conclusion (rhs) always holds. *) @@ -1322,12 +1308,7 @@ Theorem subterm_valid_path_lemma : !q. q <<= FRONT p ==> subterm X M q r <> NONE Proof rpt GEN_TAC >> STRIP_TAC - >> Cases_on ‘subterm X M p r = NONE’ - >- (POP_ASSUM MP_TAC \\ - rw [subterm_is_none_iff_parent_unsolvable] \\ - Cases_on ‘FRONT p = []’ >- fs [] \\ - MP_TAC (Q.SPECL [‘X’, ‘M’, ‘FRONT p’, ‘r’] subterm_solvable_lemma) \\ - rw []) + >> ‘subterm X M p r <> NONE’ by PROVE_TAC [ltree_paths_valid_thm] >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’, ‘r’] subterm_solvable_lemma) >> rw [] >> FIRST_X_ASSUM MATCH_MP_TAC @@ -2419,221 +2400,6 @@ Proof RW_TAC std_ss [BT_tpm_thm, ltree_paths_map_cong] QED -(*---------------------------------------------------------------------------* - * Equivalent terms - *---------------------------------------------------------------------------*) - -(* Definition 10.2.19 [1, p. 238] - - M = LAMl v1 (y @* Ms) @@ (MAP VAR v1) == y @* Ms' - N = LAMl v2 (y' @* Ns) @@ (MAP VAR v2) == y' @* Ns' - - LENGTH Ms = n /\ LENGTH Ns = n' - LENGTH Ms' = m /\ LENGTH Ns' = m' - - y = y' - n - m = n' - m' (possibly negative) <=> n + m' = n' + m (non-negative) - *) -Definition equivalent_def : - equivalent (M :term) (N :term) = - if solvable M /\ solvable N then - let M0 = principle_hnf M; - N0 = principle_hnf N; - n = LAMl_size M0; - n' = LAMl_size N0; - vs = NEWS (MAX n n') (FV M UNION FV N); - vsM = TAKE n vs; - vsN = TAKE n' vs; - M1 = principle_hnf (M0 @* MAP VAR vsM); - N1 = principle_hnf (N0 @* MAP VAR vsN); - y = hnf_head M1; - y' = hnf_head N1; - m = LENGTH (hnf_children M1); - m' = LENGTH (hnf_children N1); - in - y = y' /\ n + m' = n' + m - else - ~solvable M /\ ~solvable N -End - -Theorem equivalent_reflexive : - reflexive equivalent -Proof - rw [reflexive_def, equivalent_def] -QED - -(* |- equivalent x x *) -Theorem equivalent_refl[simp] = - SPEC_ALL (REWRITE_RULE [reflexive_def] equivalent_reflexive) - -Theorem equivalent_symmetric : - symmetric equivalent -Proof - RW_TAC std_ss [symmetric_def, equivalent_def, Once MAX_COMM, Once UNION_COMM] - >> reverse (Cases_on ‘solvable x /\ solvable y’) >- fs [] - >> simp [] - >> rename1 ‘y1 = y2 /\ m1 + n = m + n1 <=> y3 = y4 /\ m3 + n1 = m2 + n3’ - >> ‘n3 = n’ by rw [Abbr ‘n3’, Abbr ‘n’] >> gs [] - >> EQ_TAC >> rw [] -QED - -(* |- !x y. equivalent x y <=> equivalent y x *) -Theorem equivalent_comm = REWRITE_RULE [symmetric_def] equivalent_symmetric - -Theorem equivalent_of_solvables : - !M N. solvable M /\ solvable N ==> - (equivalent M N <=> - let M0 = principle_hnf M; - N0 = principle_hnf N; - n = LAMl_size M0; - n' = LAMl_size N0; - vs = NEWS (MAX n n') (FV M UNION FV N); - vsM = TAKE n vs; - vsN = TAKE n' vs; - M1 = principle_hnf (M0 @* MAP VAR vsM); - N1 = principle_hnf (N0 @* MAP VAR vsN); - y = hnf_head M1; - y' = hnf_head N1; - m = LENGTH (hnf_children M1); - m' = LENGTH (hnf_children N1); - in - y = y' /\ n + m' = n' + m) -Proof - RW_TAC std_ss [equivalent_def] -QED - -(* beta-equivalent terms are also equivalent here *) -Theorem lameq_imp_equivalent : - !M N. M == N ==> equivalent M N -Proof - rpt STRIP_TAC - >> reverse (Cases_on ‘solvable M’) - >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\ - rw [equivalent_def]) - >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong] - >> qabbrev_tac ‘X = FV M UNION FV N’ - >> ‘FINITE X’ by rw [Abbr ‘X’] - >> ‘LAMl_size (principle_hnf M) = LAMl_size (principle_hnf N)’ - by METIS_TAC [lameq_principle_hnf_size_eq'] - (* stage work *) - >> RW_TAC std_ss [equivalent_of_solvables] (* 2 subgoals, same tactics *) - >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) X /\ LENGTH vs = n’ - by (rw [Abbr ‘vs’, NEWS_def]) - >> ‘vsM = vs’ by rw [Abbr ‘vsM’, TAKE_LENGTH_ID_rwt] - >> POP_ASSUM (fs o wrap) - >> Q.PAT_X_ASSUM ‘vs = vsN’ (fs o wrap o SYM) - >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘N0’, ‘n’, ‘vs’, ‘M1’, ‘N1’] - lameq_principle_hnf_thm_simple) - >> simp [Abbr ‘X’, GSYM solvable_iff_has_hnf] -QED - -(* NOTE: the initial calls of ‘principle_hnf’ get eliminated if the involved - terms are already in head normal forms. - *) -Theorem equivalent_of_hnf : - !M N. hnf M /\ hnf N ==> - (equivalent M N <=> - let n = LAMl_size M; - n' = LAMl_size N; - vs = NEWS (MAX n n') (FV M UNION FV N); - vsM = TAKE n vs; - vsN = TAKE n' vs; - M1 = principle_hnf (M @* MAP VAR vsM); - N1 = principle_hnf (N @* MAP VAR vsN); - y = hnf_head M1; - y' = hnf_head N1; - m = LENGTH (hnf_children M1); - m' = LENGTH (hnf_children N1) - in - y = y' /\ n + m' = n' + m) -Proof - rpt STRIP_TAC - >> ‘solvable M /\ solvable N’ by PROVE_TAC [hnf_has_hnf, solvable_iff_has_hnf] - >> RW_TAC std_ss [equivalent_def, principle_hnf_reduce] - >> METIS_TAC [] -QED - -(* From [1, p.238]. This concerte example shows that dB encoding is not easy in - defining this "concept": the literal encoding of inner head variables are not - the same for equivalent terms. - *) -Theorem not_equivalent_example : - !x y. x <> y ==> ~equivalent (LAM x (VAR y @@ t)) (LAM y (VAR y @@ t)) -Proof - qx_genl_tac [‘x’, ‘v’] >> DISCH_TAC - >> ‘hnf (LAM x (VAR v @@ t)) /\ hnf (LAM v (VAR v @@ t))’ by rw [] - >> ‘solvable (LAM x (VAR v @@ t)) /\ solvable (LAM v (VAR v @@ t))’ - by rw [solvable_iff_has_hnf, hnf_has_hnf] - >> RW_TAC std_ss [equivalent_of_solvables, principle_hnf_reduce] - (* fix M0 *) - >> qunabbrev_tac ‘M0’ >> qabbrev_tac ‘M0 = LAM x (VAR v @@ t)’ - >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0 UNION FV N0) /\ - LENGTH vs = MAX n n'’ by rw [Abbr ‘vs’, NEWS_def] - >> ‘DISJOINT (set vs) (FV M0) /\ DISJOINT (set vs) (FV N0)’ - by METIS_TAC [DISJOINT_SYM, DISJOINT_UNION] - >> Q_TAC (HNF_TAC (“M0 :term”, “vs :string list”, - “y1 :string”, “args1 :term list”)) ‘M1’ - >> Q_TAC (HNF_TAC (“N0 :term”, “vs :string list”, - “y2 :string”, “args2 :term list”)) ‘N1’ - >> ‘TAKE (LAMl_size M0) vs = vsM’ by rw [Abbr ‘vsM’, Abbr ‘n’] - >> ‘TAKE (LAMl_size N0) vs = vsN’ by rw [Abbr ‘vsN’, Abbr ‘n'’] - >> NTAC 2 (POP_ASSUM (rfs o wrap)) - (* reshaping and reordering assumptions *) - >> qunabbrev_tac ‘M1’ - >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vsM)’ - >> qunabbrev_tac ‘N1’ - >> qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vsN)’ - >> Q.PAT_X_ASSUM ‘M0 = _’ ASSUME_TAC - >> Q.PAT_X_ASSUM ‘N0 = _’ ASSUME_TAC - >> Q.PAT_X_ASSUM ‘M1 = _’ ASSUME_TAC - >> Q.PAT_X_ASSUM ‘N1 = _’ ASSUME_TAC - >> ‘VAR y1 = y’ by rw [Abbr ‘y’ , absfree_hnf_head] - >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, absfree_hnf_head] - >> qunabbrevl_tac [‘n’, ‘n'’] - >> Know ‘LAMl_size M0 = 1 /\ LAMl_size N0 = 1’ - >- (rw [Abbr ‘M0’, Abbr ‘N0’, LAMl_size_def]) - >> DISCH_THEN (rfs o wrap) - >> ‘vsN = vs’ by rw [Abbr ‘vsN’, TAKE_LENGTH_ID_rwt] - >> POP_ASSUM (rfs o wrap) - >> Q.PAT_X_ASSUM ‘vs = vsM’ (rfs o wrap o SYM) - >> qunabbrev_tac ‘vsN’ - (* stage work *) - >> qabbrev_tac ‘z = HD vs’ - >> ‘vs = [z]’ by METIS_TAC [SING_HD] - >> POP_ASSUM (rfs o wrap) - >> qunabbrevl_tac [‘M0’, ‘N0’] - >> DISJ1_TAC - >> qunabbrevl_tac [‘y’, ‘y'’] - >> Q.PAT_X_ASSUM ‘VAR y1 = hnf_head M1’ (rfs o wrap o SYM) - >> Q.PAT_X_ASSUM ‘_ = LAM z (VAR y1 @* args1)’ (rfs o wrap o SYM) - >> Q.PAT_X_ASSUM ‘_ = LAM z (VAR y2 @* args2)’ (rfs o wrap o SYM) - (* now the goal is ‘y1 <> y2’ *) - >> qabbrev_tac ‘u = VAR v @@ t’ - >> ‘hnf u’ by rw [Abbr ‘u’] - >> Know ‘M1 = [VAR z/x] u’ - >- (qunabbrev_tac ‘M1’ \\ - Cases_on ‘z = x’ >- (POP_ASSUM (gs o wrap) \\ - fs [principle_hnf_beta_reduce1]) \\ - MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘u’] \\ - rfs [FV_thm]) - >> DISCH_THEN (rfs o wrap) - >> Know ‘N1 = [VAR z/v] u’ - >- (qunabbrev_tac ‘N1’ \\ - Cases_on ‘z = v’ >- (POP_ASSUM (rfs o wrap)) \\ - MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘u’] \\ - rfs [FV_thm]) - >> DISCH_THEN (rfs o wrap) - >> qunabbrevl_tac [‘M1’, ‘N1’] - >> rfs [Abbr ‘u’, app_eq_appstar] - >> METIS_TAC [] -QED - -Theorem equivalent_of_unsolvables : - !M N. unsolvable M /\ unsolvable N ==> equivalent M N -Proof - rw [equivalent_def] -QED - (*---------------------------------------------------------------------------* * Boehm transformations *---------------------------------------------------------------------------*) @@ -2878,19 +2644,23 @@ Proof >> rw [Boehm_apply_MAP_rightctxt] QED -(* NOTE: if M is solvable, ‘apply pi M’ may not be solvable. *) -Theorem Boehm_apply_unsolvable : +(* |- !M N. solvable (M @@ N) ==> solvable M *) +Theorem solvable_APP_E[local] = + has_hnf_APP_E |> REWRITE_RULE [GSYM solvable_iff_has_hnf] + |> Q.GENL [‘M’, ‘N’] + +Theorem Boehm_transform_of_unsolvables : !pi M. Boehm_transform pi /\ unsolvable M ==> unsolvable (apply pi M) Proof - SNOC_INDUCT_TAC >> rw [] - >> FIRST_X_ASSUM MATCH_MP_TAC >> art [] - >> fs [solving_transform_def, solvable_iff_has_hnf] (* 2 subgaols *) - >| [ (* goal 1 (of 2) *) - CCONTR_TAC >> fs [] \\ - METIS_TAC [has_hnf_APP_E], - (* goal 2 (of 2) *) - CCONTR_TAC >> fs [] \\ - METIS_TAC [has_hnf_SUB_E] ] + Induct_on ‘pi’ using SNOC_INDUCT + >- rw [] + >> simp [FOLDR_SNOC, Boehm_transform_SNOC] + >> qx_genl_tac [‘t’, ‘M’] + >> reverse (rw [solving_transform_def]) + >- (FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\ + MATCH_MP_TAC unsolvable_subst >> art []) + >> FIRST_X_ASSUM MATCH_MP_TAC >> simp [] + >> PROVE_TAC [solvable_APP_E] QED (* Definition 10.3.5 (ii) *) @@ -2914,10 +2684,6 @@ Definition is_ready_def : ?N. M -h->* N /\ hnf N /\ ~is_abs N /\ head_original N End -Definition is_ready'_def : - is_ready' M <=> is_ready M /\ solvable M -End - (* NOTE: This alternative definition of ‘is_ready’ consumes ‘head_original’ and eliminated the ‘principle_hnf’ inside it. *) @@ -2952,15 +2718,6 @@ Proof >> qexistsl_tac [‘y’, ‘args’] >> art [] QED -Theorem is_ready_alt' : - !M. is_ready' M <=> solvable M /\ - ?y Ns. M -h->* VAR y @* Ns /\ EVERY (\e. y # e) Ns -Proof - (* NOTE: this proof relies on the new [NOT_AND'] in boolSimps.BOOL_ss *) - rw [is_ready'_def, is_ready_alt, RIGHT_AND_OVER_OR] - >> REWRITE_TAC [Once CONJ_COMM] -QED - (* ‘subterm_width M p’ is the maximal number of children of all subterms of form ‘subterm X M q r’ such that ‘q <<= p’, irrelevant with particular X and r. @@ -5261,7 +5018,8 @@ QED Theorem Boehm_transform_exists_lemma : !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r /\ p <> [] /\ subterm X M p r <> NONE ==> - ?pi. Boehm_transform pi /\ is_ready' (apply pi M) /\ + ?pi. Boehm_transform pi /\ + solvable (apply pi M) /\ is_ready (apply pi M) /\ FV (apply pi M) SUBSET X UNION RANK (SUC r) /\ ?v P. closed P /\ !q. q <<= p /\ q <> [] ==> @@ -5391,15 +5149,16 @@ Proof >> CONJ_ASM1_TAC >- (MATCH_MP_TAC Boehm_transform_APPEND >> art [] \\ MATCH_MP_TAC Boehm_transform_APPEND >> art []) - >> Know ‘apply (p3 ++ p2 ++ p1) M == VAR b @* args' @* MAP VAR as’ + >> qabbrev_tac ‘pi = p3 ++ p2 ++ p1’ + >> Know ‘apply pi M == VAR b @* args' @* MAP VAR as’ >- (MATCH_MP_TAC lameq_TRANS \\ - Q.EXISTS_TAC ‘apply (p3 ++ p2 ++ p1) M0’ \\ + Q.EXISTS_TAC ‘apply pi M0’ \\ CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong \\ CONJ_TAC >- art [] \\ qunabbrev_tac ‘M0’ \\ MATCH_MP_TAC lameq_SYM \\ MATCH_MP_TAC lameq_principle_hnf' >> art []) \\ - ONCE_REWRITE_TAC [Boehm_apply_APPEND] \\ + SIMP_TAC std_ss [Once Boehm_apply_APPEND, Abbr ‘pi’] \\ MATCH_MP_TAC lameq_TRANS \\ Q.EXISTS_TAC ‘apply (p3 ++ p2) M1’ \\ CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> art [] \\ @@ -5409,18 +5168,23 @@ Proof Q.EXISTS_TAC ‘apply p3 (P @* args')’ >> art [] \\ MATCH_MP_TAC Boehm_apply_lameq_cong >> rw []) >> DISCH_TAC + >> CONJ_ASM1_TAC + >- (Suff ‘solvable (VAR b @* args' @* MAP VAR as)’ + >- METIS_TAC [lameq_solvable_cong] \\ + simp [solvable_iff_has_hnf, GSYM appstar_APPEND] \\ + MATCH_MP_TAC hnf_has_hnf >> simp [hnf_appstar]) (* stage work *) - >> Know ‘principle_hnf (apply (p3 ++ p2 ++ p1) M) = VAR b @* args' @* MAP VAR as’ - >- (Q.PAT_X_ASSUM ‘Boehm_transform (p3 ++ p2 ++ p1)’ K_TAC \\ - Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC \\ - Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC \\ - Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\ + >> Know ‘principle_hnf (apply pi M) = VAR b @* args' @* MAP VAR as’ + >- (Q.PAT_X_ASSUM ‘Boehm_transform pi’ K_TAC \\ + Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC \\ + Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC \\ + Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC \\ + Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC \\ + Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC \\ + Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\ (* preparing for principle_hnf_denude_thm *) - Q.PAT_X_ASSUM ‘apply (p3 ++ p2 ++ p1) M == _’ MP_TAC \\ - simp [Boehm_apply_APPEND, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’, + Q.PAT_X_ASSUM ‘apply pi M == _’ MP_TAC \\ + simp [Boehm_apply_APPEND, Abbr ‘pi’, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’, Boehm_apply_MAP_rightctxt'] \\ Know ‘[P/y] (M @* MAP VAR vs) @* MAP VAR (SNOC b as) = [P/y] (M @* MAP VAR vs @* MAP VAR (SNOC b as))’ @@ -5500,17 +5264,9 @@ Proof *) MATCH_MP_TAC principle_hnf_denude_thm >> rw []) >> DISCH_TAC - >> simp [is_ready'_def, GSYM CONJ_ASSOC] - (* extra subgoal: solvable (apply (p3 ++ p2 ++ p1) M) *) - >> ONCE_REWRITE_TAC [TAUT ‘P /\ Q /\ R <=> Q /\ P /\ R’] - >> CONJ_ASM1_TAC - >- (Suff ‘solvable (VAR b @* args' @* MAP VAR as)’ - >- PROVE_TAC [lameq_solvable_cong] \\ - REWRITE_TAC [solvable_iff_has_hnf] \\ - MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]) (* applying is_ready_alt *) >> CONJ_TAC - >- (simp [is_ready_alt] \\ + >- (simp [is_ready_alt, Abbr ‘pi’] \\ qexistsl_tac [‘b’, ‘args' ++ MAP VAR as’] \\ CONJ_TAC >- (MP_TAC (Q.SPEC ‘VAR b @* args' @* MAP VAR as’ @@ -5541,12 +5297,12 @@ Proof Q.EXISTS_TAC ‘e’ >> art []) (* extra goal *) >> CONJ_TAC - >- (Q.PAT_X_ASSUM ‘apply (p3 ++ p2 ++ p1) M == _’ K_TAC \\ - Q.PAT_X_ASSUM ‘principle_hnf (apply (p3 ++ p2 ++ p1) M) = _’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\ - rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\ - Q.PAT_X_ASSUM ‘solvable (apply (p3 ++ p2 ++ p1) M)’ K_TAC \\ - simp [Boehm_apply_APPEND, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’, + >- (Q.PAT_X_ASSUM ‘apply pi M == _’ K_TAC \\ + Q.PAT_X_ASSUM ‘principle_hnf (apply pi M) = _’ K_TAC \\ + Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\ + rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\ + Q.PAT_X_ASSUM ‘solvable (apply pi M)’ K_TAC \\ + simp [Boehm_apply_APPEND, Abbr ‘pi’, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’, Boehm_apply_MAP_rightctxt'] \\ POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ reverse CONJ_TAC @@ -5567,7 +5323,6 @@ Proof Suff ‘RANK r SUBSET RANK (SUC r)’ >- SET_TAC [] \\ rw [RANK_MONO]) (* stage work, there's the textbook choice of y and P *) - >> qabbrev_tac ‘pi = p3 ++ p2 ++ p1’ >> qexistsl_tac [‘y’, ‘P’] >> art [] >> NTAC 2 STRIP_TAC (* push ‘q <<= p’ to assumptions *) (* RHS rewriting from M to M0 *) @@ -5758,17 +5513,17 @@ Proof >> POP_ASSUM (MP_TAC o (Q.SPEC ‘p’)) (* put q = p *) >> rw [] >> qabbrev_tac ‘M' = apply p0 M’ - >> ‘solvable M' /\ ?y Ms. M' -h->* VAR y @* Ms /\ EVERY (\e. y # e) Ms’ - by METIS_TAC [is_ready_alt'] - >> ‘principle_hnf M' = VAR y @* Ms’ by rw [principle_hnf_thm', hnf_appstar] + >> Q.PAT_X_ASSUM ‘is_ready M'’ (MP_TAC o REWRITE_RULE [is_ready_alt]) + >> STRIP_TAC + >> ‘principle_hnf M' = VAR y @* Ns’ by rw [principle_hnf_thm', hnf_appstar] (* stage work *) >> qunabbrev_tac ‘p’ - >> Know ‘h < LENGTH Ms’ + >> Know ‘h < LENGTH Ns’ >- (Q.PAT_X_ASSUM ‘subterm X M' (h::t) r <> NONE’ MP_TAC \\ RW_TAC std_ss [subterm_of_solvables] >> fs []) >> DISCH_TAC - >> qabbrev_tac ‘m = LENGTH Ms’ - >> qabbrev_tac ‘N = EL h Ms’ + >> qabbrev_tac ‘m = LENGTH Ns’ + >> qabbrev_tac ‘N = EL h Ns’ (* stage work *) >> Know ‘subterm X N t (SUC r) <> NONE /\ subterm' X M' (h::t) r = subterm' X N t (SUC r)’ @@ -5795,10 +5550,10 @@ Proof MATCH_MP_TAC lameq_SYM \\ MATCH_MP_TAC lameq_principle_hnf' >> art []) \\ rw [Abbr ‘p1’, appstar_SUB] \\ - Know ‘MAP [U/y] Ms = Ms’ + Know ‘MAP [U/y] Ns = Ns’ >- (rw [LIST_EQ_REWRITE, EL_MAP] \\ MATCH_MP_TAC lemma14b \\ - Q.PAT_X_ASSUM ‘EVERY (\e. y # e) Ms’ MP_TAC \\ + Q.PAT_X_ASSUM ‘EVERY (\e. y # e) Ns’ MP_TAC \\ rw [EVERY_MEM, MEM_EL] \\ POP_ASSUM MATCH_MP_TAC >> rename1 ‘i < m’ \\ Q.EXISTS_TAC ‘i’ >> art []) >> Rewr' \\ @@ -5812,12 +5567,12 @@ Proof MATCH_MP_TAC SUBSET_TRANS \\ Q.EXISTS_TAC ‘FV (apply p0 M)’ >> art [] \\ MATCH_MP_TAC SUBSET_TRANS \\ - Q.EXISTS_TAC ‘FV (VAR y @* Ms)’ \\ + Q.EXISTS_TAC ‘FV (VAR y @* Ns)’ \\ reverse CONJ_TAC >- (MATCH_MP_TAC hreduce_FV_SUBSET >> art []) \\ rw [SUBSET_DEF, FV_appstar, IN_UNION] \\ DISJ2_TAC \\ - Q.EXISTS_TAC ‘FV (EL h Ms)’ >> art [] \\ - Q.EXISTS_TAC ‘EL h Ms’ >> rw [EL_MEM]) + Q.EXISTS_TAC ‘FV (EL h Ns)’ >> art [] \\ + Q.EXISTS_TAC ‘EL h Ns’ >> rw [EL_MEM]) >> RW_TAC std_ss [] >> rename1 ‘apply p2 N == _ ISUB ss'’ >> qabbrev_tac ‘N' = subterm' X M (h::t) r’ @@ -6012,7 +5767,7 @@ Theorem subtree_equiv_lemma_explicit : EVERY (\M. subterm X M p r <> NONE) Ms ==> let pi = Boehm_construction X Ms p in Boehm_transform pi /\ - EVERY is_ready' (MAP (apply pi) Ms) /\ + EVERY is_ready (MAP (apply pi) Ms) /\ EVERY (\M. p IN ltree_paths (BT' X M r)) (MAP (apply pi) Ms) /\ !M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==> (subtree_equiv X M N q r <=> @@ -6662,13 +6417,13 @@ Proof REWRITE_TAC [solvable_iff_has_hnf] \\ MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar, GSYM appstar_APPEND]) >> DISCH_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L6560" - >> CONJ_TAC (* EVERY is_ready' ... *) + >> PRINT_TAC "stage work on subtree_equiv_lemma: L6433" + >> CONJ_TAC (* EVERY is_ready ... *) >- (rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\ simp [EVERY_EL, EL_MAP] \\ Q.X_GEN_TAC ‘i’ >> DISCH_TAC \\ (* now expanding ‘is_ready’ using [is_ready_alt] *) - ASM_SIMP_TAC std_ss [is_ready_alt'] \\ + ASM_SIMP_TAC std_ss [is_ready_alt] \\ qexistsl_tac [‘b i’, ‘Ns i ++ tl i’] \\ (* subgoal: apply pi (M i) -h->* VAR (b i) @* (Ns i ++ tl i) *) CONJ_TAC @@ -6822,7 +6577,7 @@ Proof Suff ‘EL (j i) xs = EL a' xs <=> j i = a'’ >- rw [] \\ MATCH_MP_TAC ALL_DISTINCT_EL_IMP >> rw []) (* cleanup *) - >> PRINT_TAC "stage work on subtree_equiv_lemma: L6720" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L6593" >> Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC >> Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC >> Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC @@ -7122,7 +6877,8 @@ Proof qunabbrev_tac ‘ys’ \\ MATCH_MP_TAC DISJOINT_RNEWS >> simp []) >> DISCH_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L7111" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L6893" + (* Now ‘subterm X (M i) q r <> NONE’ is added into antecedents of the subgoal *) >> Know ‘!q. q <<= p /\ q <> [] ==> !i. i < k ==> subterm X (H i) q r <> NONE /\ subterm' X (H i) q r = @@ -7142,8 +6898,8 @@ Proof ‘LAMl_size (H i) = 0’ by rw [Abbr ‘H’, LAMl_size_appstar, GSYM appstar_APPEND] \\ simp [] \\ - NTAC 2 (POP_ASSUM K_TAC) \\ - DISCH_TAC \\ + NTAC 2 (POP_ASSUM K_TAC) (* principle_hnf (H i), LAMl_size (H i) *) \\ + DISCH_TAC (* subterm_width (M i) (h::t) <= d *) \\ Q_TAC (RNEWS_TAC (“ys' :string list”, “r :num”, “(n :num -> num) i”)) ‘X’ \\ qabbrev_tac ‘vs' = TAKE (n i) vs’ \\ ‘ALL_DISTINCT vs' /\ LENGTH vs' = n i’ @@ -7339,7 +7095,7 @@ Proof MATCH_MP_TAC ltree_paths_inclusive \\ Q.EXISTS_TAC ‘h::t’ >> simp []) >> DISCH_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L7328" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L7111" >> Suff ‘(!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p /\ subtree_equiv X M N q r ==> @@ -7480,7 +7236,7 @@ Proof ==> permutator (d_max + f j1) = permutator (d_max + f j2) ==> d_max + f j1 = d_max + f j2 ==> f j1 = f j2 *) - PRINT_TAC "stage work on subtree_equiv_lemma: L7381" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L7252" \\ Suff ‘y j1 = y j2’ >- (DISCH_TAC \\ Know ‘VAR (y j1) ISUB ss = VAR (y j2) ISUB ss’ @@ -7767,7 +7523,7 @@ Proof Suff ‘RANK r SUBSET RANK r1’ >- SET_TAC [] \\ simp [Abbr ‘r1’, RANK_MONO] ]) >> STRIP_TAC \\ (* stage work *) - PRINT_TAC "stage work on subtree_equiv_lemma: L7760" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L7539" \\ Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’ ASSUME_TAC \\ (* applying BT_subterm_thm on ‘H j1’ *) MP_TAC (Q.SPECL [‘q’, ‘X’, ‘H (j1 :num)’, ‘r’] BT_subterm_thm) \\ @@ -7940,7 +7696,7 @@ Proof Q.PAT_X_ASSUM ‘_ = W0'’ (REWRITE_TAC o wrap o SYM) \\ simp [Abbr ‘Ns1'’, Abbr ‘Ns2'’, Abbr ‘Ns1''’, Abbr ‘Ns2''’]) \\ (* hard case *) - PRINT_TAC "stage work on subtree_equiv_lemma: L7933" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L7712" \\ POP_ASSUM MP_TAC >> simp [] \\ DISCH_THEN (Q.X_CHOOSE_THEN ‘j3’ STRIP_ASSUME_TAC) \\ ‘(LEAST j. y j = y1') = f j3’ by rw [] >> POP_ORW \\ @@ -8089,7 +7845,7 @@ Proof now applying RNEWS_prefix first: *) - PRINT_TAC "stage work on subtree_equiv_lemma: L7986" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L7861" \\ Know ‘vs1 <<= vs3’ >- (qunabbrevl_tac [‘vs1’, ‘vs3’] \\ MATCH_MP_TAC RNEWS_prefix >> simp []) \\ @@ -8207,22 +7963,13 @@ Proof reverse CONJ_TAC >- (MP_TAC (Q.SPECL [‘ss’, ‘EL i Ns1'’] FV_ISUB_upperbound) \\ simp [EL_MAP, Abbr ‘Ns1'’]) \\ - (* Ns1' is tpm (REVERSE pm) of Ns1 - pm = ZIP (vs,ys), vs is in ROW 0, ys s in ROW r - vsx (part of vs4) is in ROW r1 > r - - The key is to prove DISJOINT (set vsx) (FV (EL i Ns1)). - *) + (* The key is to prove DISJOINT (set vsx) (FV (EL i Ns1)) *) POP_ASSUM MP_TAC \\ simp [Abbr ‘Ns1'’, EL_listpm, Abbr ‘pm’, REVERSE_ZIP] >> DISCH_TAC \\ (* applying FV_tpm_disjoint *) MATCH_MP_TAC FV_tpm_disjoint \\ simp [ALL_DISTINCT_REVERSE] \\ - (* goal: DISJOINT (set ys1) (FV (EL i Ns1)), given: - - principle_hnf (N0 @* MAP VAR vs1) = VAR y1 @* Ns1 - FV N0 SUBSET FV N SUBSET X UNION RANK r1 - *) + (* goal: DISJOINT (set ys1) (FV (EL i Ns1)) *) Know ‘FV N0 SUBSET X UNION RANK r1’ >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV N’ >> art [] \\ qunabbrev_tac ‘N0’ \\ @@ -8343,7 +8090,7 @@ Proof qabbrev_tac ‘pm3 = ZIP (ls,vs3)’ \\ (* applying IS_SUFFIX_IMP_LASTN *) Know ‘DROP n1 ls = xs1 /\ DROP n2 ls = xs2’ - >- (PRINT_TAC "stage work on subtree_equiv_lemma: L8238" \\ + >- (PRINT_TAC "stage work on subtree_equiv_lemma: L8106" \\ ‘xs1 = LASTN (LENGTH xs1) L’ by simp [IS_SUFFIX_IMP_LASTN] \\ POP_ORW \\ ‘xs2 = LASTN (LENGTH xs2) L’ by simp [IS_SUFFIX_IMP_LASTN] \\ @@ -8358,7 +8105,7 @@ Proof >- (irule LASTN_LASTN >> simp []) >> Rewr' \\ Suff ‘LENGTH ys1 = n3 - n1 /\ LENGTH ys2 = n3 - n2’ >- Rewr \\ simp [Abbr ‘ys1’, Abbr ‘ys2’, LENGTH_DROP]) >> STRIP_TAC \\ - PRINT_TAC "stage work on subtree_equiv_lemma: L8351" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L8121" \\ (* preparing for lswapstr_unchanged' *) qabbrev_tac ‘xs1' = TAKE n1 ls’ \\ qabbrev_tac ‘xs2' = TAKE n2 ls’ \\ @@ -8444,15 +8191,13 @@ Proof subtree_equiv X (apply pi M) (apply pi N) p r ==> subtree_equiv' X M N p r *) - >> PRINT_TAC "stage work on subtree_equiv_lemma: L8437" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L8207" >> rpt GEN_TAC >> STRIP_TAC >> POP_ASSUM MP_TAC >> ONCE_REWRITE_TAC [MONO_NOT_EQ] (* NOTE: The antecedent “~subtree_equiv' X t1 t2 q r” makes sure that ‘n1 + m2 <> n1 + m1’ is always assumed (instead of ‘y1 <> y2’). And - the goal is to prove ‘y3 <> y4 \/ n3 + m3 <> n4 + m4’ - - The original proof assumes q = p, but the proof also work for q <<= p. + the goal is to prove ‘y3 <> y4 \/ n3 + m3 <> n4 + m4’. *) >> NTAC 2 (Q.PAT_X_ASSUM ‘MEM _ Ms’ MP_TAC) >> simp [MEM_EL] @@ -8542,13 +8287,12 @@ Proof Q.EXISTS_TAC ‘Z’ >> art [] \\ rw [Abbr ‘t2’, FV_appstar]) >> Rewr' \\ simp [Abbr ‘t1’, Abbr ‘t2’, tpm_appstar] \\ - PRINT_TAC "stage work on subtree_equiv_lemma: L8535" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L8303" \\ qabbrev_tac ‘pm1 = ZIP (vs1,ys1)’ \\ qabbrev_tac ‘pm2 = ZIP (vs2,ys2)’ \\ qabbrev_tac ‘vs1' = DROP (n j1) vs’ \\ qabbrev_tac ‘vs2' = DROP (n j2) vs’ \\ (* current situation: - |<--------- vs (n_max) --------->| |<--- vs1 ----->|<---- vs1'----->| y j1 ---+ |<------ vs2 ------->|<--vs2'--->| y j2 ---|--+ @@ -8860,7 +8604,7 @@ Proof (* stage work, now “subterm' X (M j1) p r)” and “subterm' X (M j2) p r)” are both solvable. *) - >> PRINT_TAC "stage work on subtree_equiv_lemma: L8853" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L8620" >> MP_TAC (Q.SPECL [‘q’, ‘X’, ‘M (j1 :num)’, ‘r’] BT_subterm_thm) >> simp [] >> STRIP_TAC (* this asserts ‘x’ *) >> NTAC 3 (Cases_on ‘x’ >> fs []) @@ -8990,7 +8734,7 @@ Proof rw [SUBSET_DEF] \\ POP_ASSUM MATCH_MP_TAC >> Q.EXISTS_TAC ‘i’ >> art [] ]) >> STRIP_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L8983" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L8750" >> Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’ ASSUME_TAC >> MP_TAC (Q.SPECL [‘q’, ‘X’, ‘H (j1 :num)’, ‘r’] BT_subterm_thm) >> simp [] >> STRIP_TAC (* this asserts ‘x’ *) @@ -9220,11 +8964,8 @@ Proof LAMl |<----------- zs2' ----------->| VAR h LAMl |<----vs2----->|<----zs2---->|h| VAR h n4 = n2 + d_max - m2 +1 - - It seems that y4 is ‘LAST vs4’ while y1' (at most in vs1/vs3, which is - strictly shorter than vs4), thus cannot be the same (ALL_DISTINCT vs4). *) - >- (PRINT_TAC "stage work on subtree_equiv_lemma: L9111" \\ + >- (PRINT_TAC "stage work on subtree_equiv_lemma: L8981" \\ POP_ASSUM MP_TAC >> simp [ISUB_VAR_FRESH'] \\ DISCH_THEN (Q.X_CHOOSE_THEN ‘j3’ STRIP_ASSUME_TAC) \\ ‘(LEAST j. y j = y2') = f j3’ by rw [] >> POP_ORW \\ @@ -9529,7 +9270,7 @@ Proof simp [ALL_DISTINCT_APPEND] \\ DISJ2_TAC >> Q.EXISTS_TAC ‘y1'’ >> art [] ]) (* Case 3 (of 4): (almost) symmetric with previous Case 2 *) - >- (PRINT_TAC "stage work on subtree_equiv_lemma: L9414" \\ + >- (PRINT_TAC "stage work on subtree_equiv_lemma: L9286" \\ Q.PAT_X_ASSUM ‘~(y1' NOTIN DOM ss)’ MP_TAC >> simp [ISUB_VAR_FRESH'] \\ DISCH_THEN (Q.X_CHOOSE_THEN ‘j3’ STRIP_ASSUME_TAC) \\ ‘(LEAST j. y j = y1') = f j3’ by rw [] >> POP_ORW \\ @@ -9802,7 +9543,7 @@ Proof simp [ALL_DISTINCT_APPEND] \\ DISJ2_TAC >> Q.EXISTS_TAC ‘y2'’ >> art [] ]) (* Case 4 (of 4): hardest *) - >> PRINT_TAC "stage work on subtree_equiv_lemma: L9795" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L9559" >> NTAC 2 (POP_ASSUM (MP_TAC o REWRITE_RULE [])) >> simp [] >> DISCH_THEN (Q.X_CHOOSE_THEN ‘j3’ STRIP_ASSUME_TAC) @@ -10148,7 +9889,7 @@ Proof rw [LAST_APPEND_NOT_NIL]) >> Rewr' \\ simp []) >> DISCH_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L10141" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L9905" >> Know ‘y3 = y4 <=> n3 = n4’ >- (Q.PAT_X_ASSUM ‘LAST vs3 = y3’ (REWRITE_TAC o wrap o SYM) \\ Q.PAT_X_ASSUM ‘LAST vs4 = y4’ (REWRITE_TAC o wrap o SYM) \\ @@ -10218,7 +9959,7 @@ Proof n4 = n2 + d_max' j4 - m2 + 1 (m4 = m2 + d_max' j4 - m2 = d_max' j4) *) - >> PRINT_TAC "stage work on subtree_equiv_lemma: L10211" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L9975" >> Cases_on ‘y1 = y2’ >> simp [] (* now: y1 <> y2 *) >> ‘y1' <> y2'’ by rw [Abbr ‘y1'’, Abbr ‘y2'’] diff --git a/examples/lambda/barendregt/lameta_completeScript.sml b/examples/lambda/barendregt/lameta_completeScript.sml index b749b44b8c..c5ff4cc31f 100644 --- a/examples/lambda/barendregt/lameta_completeScript.sml +++ b/examples/lambda/barendregt/lameta_completeScript.sml @@ -8,7 +8,7 @@ open HolKernel Parse boolLib bossLib; open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory - ltreeTheory llistTheory; + ltreeTheory llistTheory relationTheory; open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory horeductionTheory solvableTheory head_reductionTheory head_reductionLib @@ -31,6 +31,248 @@ val _ = hide "Y"; val _ = new_theory "lameta_complete"; +(*---------------------------------------------------------------------------* + * ltreeTheory extras + *---------------------------------------------------------------------------*) + +(* ltree_subset A B <=> A results from B by "cutting off" some subtrees. Thus, + + 1) The paths of A is a subset of paths of B + 2) The node contents for all paths of A is identical to those of B, but the number + of successors at those nodes of B may be different (B may have more successors) + + NOTE: Simply defining ‘ltree_subset A B <=> subtrees A SUBSET subtrees B’ is wrong, + as A may appear as a non-root subtree of B, i.e. ‘A IN subtrees B’ but there's + no way to "cut off" B to get A, the resulting subtree in B always have some + more path prefixes. + *) +Definition ltree_subset_def : + ltree_subset A B <=> + (ltree_paths A) SUBSET (ltree_paths B) /\ + !p. p IN ltree_paths A ==> + ltree_node (THE (ltree_lookup A p)) = + ltree_node (THE (ltree_lookup B p)) +End + +(*---------------------------------------------------------------------------* + * Equivalent terms + *---------------------------------------------------------------------------*) + +(* Definition 10.2.19 [1, p. 238] + + M = LAMl v1 (y @* Ms) @@ (MAP VAR v1) == y @* Ms' + N = LAMl v2 (y' @* Ns) @@ (MAP VAR v2) == y' @* Ns' + + LENGTH Ms = n /\ LENGTH Ns = n' + LENGTH Ms' = m /\ LENGTH Ns' = m' + + y = y' + n - m = n' - m' (possibly negative) <=> n + m' = n' + m (non-negative) + *) +Definition equivalent_def : + equivalent (M :term) (N :term) = + if solvable M /\ solvable N then + let M0 = principle_hnf M; + N0 = principle_hnf N; + n = LAMl_size M0; + n' = LAMl_size N0; + vs = NEWS (MAX n n') (FV M UNION FV N); + vsM = TAKE n vs; + vsN = TAKE n' vs; + M1 = principle_hnf (M0 @* MAP VAR vsM); + N1 = principle_hnf (N0 @* MAP VAR vsN); + y = hnf_head M1; + y' = hnf_head N1; + m = LENGTH (hnf_children M1); + m' = LENGTH (hnf_children N1); + in + y = y' /\ n + m' = n' + m + else + ~solvable M /\ ~solvable N +End + +Theorem equivalent_reflexive : + reflexive equivalent +Proof + rw [reflexive_def, equivalent_def] +QED + +(* |- equivalent x x *) +Theorem equivalent_refl[simp] = + SPEC_ALL (REWRITE_RULE [reflexive_def] equivalent_reflexive) + +Theorem equivalent_symmetric : + symmetric equivalent +Proof + RW_TAC std_ss [symmetric_def, equivalent_def, Once MAX_COMM, Once UNION_COMM] + >> reverse (Cases_on ‘solvable x /\ solvable y’) >- fs [] + >> simp [] + >> rename1 ‘y1 = y2 /\ m1 + n = m + n1 <=> y3 = y4 /\ m3 + n1 = m2 + n3’ + >> ‘n3 = n’ by rw [Abbr ‘n3’, Abbr ‘n’] >> gs [] + >> EQ_TAC >> rw [] +QED + +(* |- !x y. equivalent x y <=> equivalent y x *) +Theorem equivalent_comm = REWRITE_RULE [symmetric_def] equivalent_symmetric + +Theorem equivalent_of_solvables : + !M N. solvable M /\ solvable N ==> + (equivalent M N <=> + let M0 = principle_hnf M; + N0 = principle_hnf N; + n = LAMl_size M0; + n' = LAMl_size N0; + vs = NEWS (MAX n n') (FV M UNION FV N); + vsM = TAKE n vs; + vsN = TAKE n' vs; + M1 = principle_hnf (M0 @* MAP VAR vsM); + N1 = principle_hnf (N0 @* MAP VAR vsN); + y = hnf_head M1; + y' = hnf_head N1; + m = LENGTH (hnf_children M1); + m' = LENGTH (hnf_children N1); + in + y = y' /\ n + m' = n' + m) +Proof + RW_TAC std_ss [equivalent_def] +QED + +(* beta-equivalent terms are also equivalent here *) +Theorem lameq_imp_equivalent : + !M N. M == N ==> equivalent M N +Proof + rpt STRIP_TAC + >> reverse (Cases_on ‘solvable M’) + >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\ + rw [equivalent_def]) + >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong] + >> qabbrev_tac ‘X = FV M UNION FV N’ + >> ‘FINITE X’ by rw [Abbr ‘X’] + >> ‘LAMl_size (principle_hnf M) = LAMl_size (principle_hnf N)’ + by METIS_TAC [lameq_principle_hnf_size_eq'] + (* stage work *) + >> RW_TAC std_ss [equivalent_of_solvables] (* 2 subgoals, same tactics *) + >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) X /\ LENGTH vs = n’ + by (rw [Abbr ‘vs’, NEWS_def]) + >> ‘vsM = vs’ by rw [Abbr ‘vsM’, TAKE_LENGTH_ID_rwt] + >> POP_ASSUM (fs o wrap) + >> Q.PAT_X_ASSUM ‘vs = vsN’ (fs o wrap o SYM) + >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘N0’, ‘n’, ‘vs’, ‘M1’, ‘N1’] + lameq_principle_hnf_thm_simple) + >> simp [Abbr ‘X’, GSYM solvable_iff_has_hnf] +QED + +(* NOTE: the initial calls of ‘principle_hnf’ get eliminated if the involved + terms are already in head normal forms. + *) +Theorem equivalent_of_hnf : + !M N. hnf M /\ hnf N ==> + (equivalent M N <=> + let n = LAMl_size M; + n' = LAMl_size N; + vs = NEWS (MAX n n') (FV M UNION FV N); + vsM = TAKE n vs; + vsN = TAKE n' vs; + M1 = principle_hnf (M @* MAP VAR vsM); + N1 = principle_hnf (N @* MAP VAR vsN); + y = hnf_head M1; + y' = hnf_head N1; + m = LENGTH (hnf_children M1); + m' = LENGTH (hnf_children N1) + in + y = y' /\ n + m' = n' + m) +Proof + rpt STRIP_TAC + >> ‘solvable M /\ solvable N’ by PROVE_TAC [hnf_has_hnf, solvable_iff_has_hnf] + >> RW_TAC std_ss [equivalent_def, principle_hnf_reduce] + >> METIS_TAC [] +QED + +(* From [1, p.238]. This concerte example shows that dB encoding is not easy in + defining this "concept": the literal encoding of inner head variables are not + the same for equivalent terms. + *) +Theorem not_equivalent_example : + !x y. x <> y ==> ~equivalent (LAM x (VAR y @@ t)) (LAM y (VAR y @@ t)) +Proof + qx_genl_tac [‘x’, ‘v’] >> DISCH_TAC + >> ‘hnf (LAM x (VAR v @@ t)) /\ hnf (LAM v (VAR v @@ t))’ by rw [] + >> ‘solvable (LAM x (VAR v @@ t)) /\ solvable (LAM v (VAR v @@ t))’ + by rw [solvable_iff_has_hnf, hnf_has_hnf] + >> RW_TAC std_ss [equivalent_of_solvables, principle_hnf_reduce] + (* fix M0 *) + >> qunabbrev_tac ‘M0’ >> qabbrev_tac ‘M0 = LAM x (VAR v @@ t)’ + >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0 UNION FV N0) /\ + LENGTH vs = MAX n n'’ by rw [Abbr ‘vs’, NEWS_def] + >> ‘DISJOINT (set vs) (FV M0) /\ DISJOINT (set vs) (FV N0)’ + by METIS_TAC [DISJOINT_SYM, DISJOINT_UNION] + >> Q_TAC (HNF_TAC (“M0 :term”, “vs :string list”, + “y1 :string”, “args1 :term list”)) ‘M1’ + >> Q_TAC (HNF_TAC (“N0 :term”, “vs :string list”, + “y2 :string”, “args2 :term list”)) ‘N1’ + >> ‘TAKE (LAMl_size M0) vs = vsM’ by rw [Abbr ‘vsM’, Abbr ‘n’] + >> ‘TAKE (LAMl_size N0) vs = vsN’ by rw [Abbr ‘vsN’, Abbr ‘n'’] + >> NTAC 2 (POP_ASSUM (rfs o wrap)) + (* reshaping and reordering assumptions *) + >> qunabbrev_tac ‘M1’ + >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vsM)’ + >> qunabbrev_tac ‘N1’ + >> qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vsN)’ + >> Q.PAT_X_ASSUM ‘M0 = _’ ASSUME_TAC + >> Q.PAT_X_ASSUM ‘N0 = _’ ASSUME_TAC + >> Q.PAT_X_ASSUM ‘M1 = _’ ASSUME_TAC + >> Q.PAT_X_ASSUM ‘N1 = _’ ASSUME_TAC + >> ‘VAR y1 = y’ by rw [Abbr ‘y’ , absfree_hnf_head] + >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, absfree_hnf_head] + >> qunabbrevl_tac [‘n’, ‘n'’] + >> Know ‘LAMl_size M0 = 1 /\ LAMl_size N0 = 1’ + >- (rw [Abbr ‘M0’, Abbr ‘N0’, LAMl_size_def]) + >> DISCH_THEN (rfs o wrap) + >> ‘vsN = vs’ by rw [Abbr ‘vsN’, TAKE_LENGTH_ID_rwt] + >> POP_ASSUM (rfs o wrap) + >> Q.PAT_X_ASSUM ‘vs = vsM’ (rfs o wrap o SYM) + >> qunabbrev_tac ‘vsN’ + (* stage work *) + >> qabbrev_tac ‘z = HD vs’ + >> ‘vs = [z]’ by METIS_TAC [SING_HD] + >> POP_ASSUM (rfs o wrap) + >> qunabbrevl_tac [‘M0’, ‘N0’] + >> DISJ1_TAC + >> qunabbrevl_tac [‘y’, ‘y'’] + >> Q.PAT_X_ASSUM ‘VAR y1 = hnf_head M1’ (rfs o wrap o SYM) + >> Q.PAT_X_ASSUM ‘_ = LAM z (VAR y1 @* args1)’ (rfs o wrap o SYM) + >> Q.PAT_X_ASSUM ‘_ = LAM z (VAR y2 @* args2)’ (rfs o wrap o SYM) + (* now the goal is ‘y1 <> y2’ *) + >> qabbrev_tac ‘u = VAR v @@ t’ + >> ‘hnf u’ by rw [Abbr ‘u’] + >> Know ‘M1 = [VAR z/x] u’ + >- (qunabbrev_tac ‘M1’ \\ + Cases_on ‘z = x’ >- (POP_ASSUM (gs o wrap) \\ + fs [principle_hnf_beta_reduce1]) \\ + MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘u’] \\ + rfs [FV_thm]) + >> DISCH_THEN (rfs o wrap) + >> Know ‘N1 = [VAR z/v] u’ + >- (qunabbrev_tac ‘N1’ \\ + Cases_on ‘z = v’ >- (POP_ASSUM (rfs o wrap)) \\ + MATCH_MP_TAC principle_hnf_beta >> simp [Abbr ‘u’] \\ + rfs [FV_thm]) + >> DISCH_THEN (rfs o wrap) + >> qunabbrevl_tac [‘M1’, ‘N1’] + >> rfs [Abbr ‘u’, app_eq_appstar] + >> METIS_TAC [] +QED + +Theorem equivalent_of_unsolvables : + !M N. unsolvable M /\ unsolvable N ==> equivalent M N +Proof + rw [equivalent_def] +QED + +(*---------------------------------------------------------------------------* + * subtree_equiv_lemma + *---------------------------------------------------------------------------*) + Theorem subtree_equiv_lemma_explicit'[local] = subtree_equiv_lemma_explicit |> SIMP_RULE std_ss [LET_DEF] @@ -39,7 +281,7 @@ Theorem subtree_equiv_lemma : FINITE X /\ p <> [] /\ 0 < r /\ Ms <> [] /\ BIGUNION (IMAGE FV (set Ms)) SUBSET X UNION RANK r /\ EVERY (\M. subterm X M p r <> NONE) Ms ==> - ?pi. Boehm_transform pi /\ EVERY is_ready' (MAP (apply pi) Ms) /\ + ?pi. Boehm_transform pi /\ EVERY is_ready (MAP (apply pi) Ms) /\ EVERY (\M. p IN ltree_paths (BT' X M r)) (MAP (apply pi) Ms) /\ !M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==> (subtree_equiv X M N q r <=> @@ -65,9 +307,8 @@ End *) Theorem subtree_equiv_imp_agree_upto : !X Ms p r pi. - (!M N q. - MEM M Ms /\ MEM N Ms /\ q <<= p /\ subtree_equiv X M N q r ==> - subtree_equiv X (apply pi M) (apply pi N) q r) /\ + (!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p /\ subtree_equiv X M N q r ==> + subtree_equiv X (apply pi M) (apply pi N) q r) /\ agree_upto X Ms p r ==> agree_upto X (MAP (apply pi) Ms) p r Proof RW_TAC std_ss [agree_upto_def, MEM_MAP] @@ -81,7 +322,7 @@ Theorem agree_upto_lemma : FINITE X /\ p <> [] /\ 0 < r /\ Ms <> [] /\ BIGUNION (IMAGE FV (set Ms)) SUBSET X UNION RANK r /\ EVERY (\M. subterm X M p r <> NONE) Ms ==> - ?pi. Boehm_transform pi /\ EVERY is_ready' (MAP (apply pi) Ms) /\ + ?pi. Boehm_transform pi /\ EVERY is_ready (MAP (apply pi) Ms) /\ (agree_upto X Ms p r ==> agree_upto X (MAP (apply pi) Ms) p r) /\ !M N. MEM M Ms /\ MEM N Ms /\ subtree_equiv X (apply pi M) (apply pi N) p r ==> @@ -110,28 +351,11 @@ End Overload is_faithful' = “is_faithful []” -(* |- !N M. solvable (M @@ N) ==> solvable M *) -Theorem solvable_APP_E[local] = - has_hnf_APP_E |> REWRITE_RULE [GSYM solvable_iff_has_hnf] |> GEN_ALL - -Theorem Boehm_transform_of_unsolvables : - !pi M. Boehm_transform pi /\ unsolvable M ==> unsolvable (apply pi M) -Proof - Induct_on ‘pi’ using SNOC_INDUCT - >- rw [] - >> simp [FOLDR_SNOC, Boehm_transform_SNOC] - >> qx_genl_tac [‘t’, ‘M’] - >> reverse (rw [solving_transform_def]) - >- (FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\ - MATCH_MP_TAC unsolvable_subst >> art []) - >> FIRST_X_ASSUM MATCH_MP_TAC >> simp [] - >> PROVE_TAC [solvable_APP_E] -QED - Theorem is_faithful' : !X Ms pi r. Boehm_transform pi ==> (is_faithful' X Ms pi r <=> - EVERY solvable Ms /\ EVERY solvable (MAP (apply pi) Ms) /\ + EVERY solvable Ms /\ + EVERY solvable (MAP (apply pi) Ms) /\ !M N. MEM M Ms /\ MEM N Ms ==> (subtree_equiv X M N [] r <=> equivalent (apply pi M) (apply pi N))) @@ -668,9 +892,9 @@ Proof >> STRONG_CONJ_TAC >- rw [Abbr ‘pi’, Boehm_transform_def, EVERY_SNOC, EVERY_MAP] >> DISCH_TAC - (* applying Boehm_apply_unsolvable *) + (* applying Boehm_transform_of_unsolvables *) >> reverse CONJ_TAC - >- (MATCH_MP_TAC Boehm_apply_unsolvable >> art []) + >- (MATCH_MP_TAC Boehm_transform_of_unsolvables >> art []) (* stage work *) >> MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘apply pi M0’ diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml index 5179b3264e..9f10b18439 100644 --- a/src/coalgebras/ltreeScript.sml +++ b/src/coalgebras/ltreeScript.sml @@ -879,7 +879,7 @@ Proof QED Theorem ltree_paths_alt : - !t. ltree_paths A = {p | ltree_el A p <> NONE} + !t. ltree_paths t = {p | ltree_el t p <> NONE} Proof rw [ltree_paths_def, Once EXTENSION, ltree_lookup_iff_ltree_el] QED