From 8ae9192d8452e02e9793952daa8383ef7721cc72 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Wed, 22 Jan 2025 00:03:28 +1100 Subject: [PATCH] [lambda] agree_upto_thm --- examples/lambda/barendregt/boehmScript.sml | 411 +++--- examples/lambda/barendregt/chap2Script.sml | 42 + .../barendregt/head_reductionScript.sml | 33 + .../barendregt/lameta_completeScript.sml | 1151 +++++++++++++++-- examples/lambda/barendregt/solvableScript.sml | 22 + examples/lambda/basics/appFOLDLScript.sml | 27 +- examples/lambda/basics/basic_swapScript.sml | 46 +- examples/lambda/basics/termScript.sml | 12 + src/pred_set/src/pred_setScript.sml | 10 + 9 files changed, 1417 insertions(+), 337 deletions(-) diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml index 1221ec89d7..ec6bb2c7ba 100644 --- a/examples/lambda/barendregt/boehmScript.sml +++ b/examples/lambda/barendregt/boehmScript.sml @@ -10,8 +10,8 @@ open HolKernel Parse boolLib bossLib; (* core theories *) open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils - pairTheory finite_mapTheory topologyTheory listRangeTheory combinTheory - tautLib listLib string_numTheory numLib BasicProvers; + pairTheory finite_mapTheory topologyTheory combinTheory tautLib listLib + string_numTheory numLib BasicProvers; (* local theories *) open basic_swapTheory nomsetTheory termTheory appFOLDLTheory NEWLib chap2Theory @@ -23,7 +23,6 @@ open monadsyntax; val _ = enable_monadsyntax (); val _ = enable_monad "option"; -(* create the theory *) val _ = new_theory "boehm"; (* These theorems usually give unexpected results, should be applied manually *) @@ -39,13 +38,12 @@ val _ = hide "C"; val _ = hide "W"; val _ = hide "Y"; +(* some proofs here are large with too many assumptions *) val _ = set_trace "Goalstack.print_goal_at_top" 0; fun PRINT_TAC pfx g = (print (pfx ^ "\n"); ALL_TAC g); -(* Disable some conflicting overloads from labelledTermsTheory, by - repeating the desired overloads again (this prioritizes them). - *) +(* Disable some conflicting overloads from labelledTermsTheory *) Overload FV = “supp term_pmact” Overload VAR = “term$VAR” @@ -55,14 +53,12 @@ Overload VAR = “term$VAR” (* The type of Boehm trees: - For each ltree node, ‘NONE’ represents {\bot} (for unsolvable terms), while - ‘SOME (vs,y)’ represents ‘LAMl vs (VAR y)’. This separation of vs and y has - at least two advantages: + NOTE: For each ltree node, ‘NONE’ represents {\bot} for unsolvable terms, and + ‘SOME (vs,y)’ represents ‘LAMl vs (VAR y)’. There are at least two advantages: 1. ‘set vs’ is the set of binding variables at that ltree node. 2. ‘LAMl vs (VAR y)’ can easily "expand" (w.r.t. eta reduction) into terms - such as ‘LAMl (vs ++ [z0;z1]) t’ (with two extra children ‘z0’ and ‘z1’) - without changing the head variable (VAR y). + such as “LAMl (vs ++ [z0;z1]) t” without changing the head variable. *) Type BT_node[pp] = “:(string list # string) option” Type boehm_tree[pp] = “:BT_node ltree” @@ -119,7 +115,7 @@ Definition subterm_def : NONE End -(* NOTE: The use of ‘subterm' X M p r’ assumes that ‘subterm X M p r <> NONE’ *) +(* The use of ‘subterm' X M p r’ assumes that ‘subterm X M p r <> NONE’ *) Overload subterm' = “\X M p r. FST (THE (subterm X M p r))” (* |- subterm X M [] r = SOME (M,r) *) @@ -234,8 +230,8 @@ Proof >> qexistsl_tac [‘X’, ‘M’, ‘r’, ‘n’, ‘n’] >> simp [] QED -(* NOTE: Essentially, ‘hnf_children_size (principle_hnf M)’ is irrelevant with - the excluding list. This lemma shows the equivalence in defining ‘m’. +(* Essentially, ‘hnf_children_size (principle_hnf M)’ is irrelevant with + the excluding list. This lemma shows the equivalence in defining ‘m’. *) Theorem hnf_children_size_alt : !X M r M0 n vs M1 Ms. @@ -274,6 +270,14 @@ Proof rw [subterm_def] QED +Theorem subterm_of_unsolvables : + !X M p r. unsolvable M /\ p <> [] ==> subterm X M p r = NONE +Proof + rpt STRIP_TAC + >> Cases_on ‘p’ >> fs [] + >> rw [subterm_def] +QED + (* NOTE: With [hnf_children_size_alt] now we are ready to prove this alternative definition of ‘subterm’. *) @@ -360,6 +364,21 @@ Proof >> POP_ASSUM (rfs o wrap) QED +(* This proof without other antecedents is based on principle_hnf_hreduce *) +Theorem hreduce_BT_cong : + !X M N r. M -h->* N ==> BT' X M r = BT' X N r +Proof + rpt STRIP_TAC + >> ‘M == N’ by PROVE_TAC [hreduces_lameq] + >> reverse (Cases_on ‘solvable M’) + >- (‘unsolvable N’ by PROVE_TAC [lameq_solvable_cong] \\ + rw [BT_of_unsolvables]) + >> ‘solvable N’ by PROVE_TAC [lameq_solvable_cong] + >> ‘principle_hnf M = principle_hnf N’ by PROVE_TAC [principle_hnf_hreduce] + >> Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold]) ‘BT' X M r’ + >> Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold]) ‘BT' X N r’ +QED + Theorem BT_finite_branching : !X M r. finite_branching (BT' X M r) Proof @@ -729,108 +748,6 @@ Proof >> qexistsl_tac [‘X’, ‘r’, ‘M0’, ‘n’] >> simp [] QED -(* Proposition 10.1.6 [1, p.219] *) -Theorem lameq_BT_cong : - !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==> - BT' X M r = BT' X N r -Proof - RW_TAC std_ss [] - >> reverse (Cases_on ‘solvable M’) - >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\ - rw [BT_of_unsolvables]) - >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong] - (* applying ltree_bisimulation *) - >> rw [ltree_bisimulation] - (* NOTE: ‘solvable P /\ solvable Q’ cannot be added here *) - >> Q.EXISTS_TAC - ‘\x y. ?P Q r. FV P UNION FV Q SUBSET X UNION RANK r /\ - P == Q /\ x = BT' X P r /\ y = BT' X Q r’ - >> BETA_TAC - >> CONJ_TAC - >- (qexistsl_tac [‘M’, ‘N’, ‘r’] >> simp [] \\ - Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC \\ - Q.PAT_X_ASSUM ‘FINITE X’ MP_TAC \\ - SET_TAC []) - (* stage work *) - >> qx_genl_tac [‘a1’, ‘ts1’, ‘a2’, ‘ts2’] >> STRIP_TAC - >> qabbrev_tac ‘P0 = principle_hnf P’ - >> qabbrev_tac ‘Q0 = principle_hnf Q’ - >> qabbrev_tac ‘n = LAMl_size P0’ - >> qabbrev_tac ‘n' = LAMl_size Q0’ - >> qabbrev_tac ‘vs = RNEWS r n X’ - >> qabbrev_tac ‘vs'= RNEWS r n' X’ - >> qabbrev_tac ‘P1 = principle_hnf (P0 @* MAP VAR vs)’ - >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’ - >> qabbrev_tac ‘Ps = hnf_children P1’ - >> qabbrev_tac ‘Qs = hnf_children Q1’ - >> qabbrev_tac ‘y = hnf_head P1’ - >> qabbrev_tac ‘y' = hnf_head Q1’ - (* applying ltree_unfold *) - >> Q.PAT_X_ASSUM ‘_ = BT' X Q r’ MP_TAC - >> simp [BT_def, Once ltree_unfold, BT_generator_def] - >> Q.PAT_X_ASSUM ‘_ = BT' X P r’ MP_TAC - >> simp [BT_def, Once ltree_unfold, BT_generator_def] - >> NTAC 2 STRIP_TAC - (* easy case: unsolvable P (and Q) *) - >> reverse (Cases_on ‘solvable P’) - >- (‘unsolvable Q’ by PROVE_TAC [lameq_solvable_cong] >> fs [] \\ - rw [llist_rel_def, LLENGTH_MAP]) - (* now both P and Q are solvable *) - >> ‘solvable Q’ by PROVE_TAC [lameq_solvable_cong] - >> fs [] - (* applying lameq_principle_hnf_size_eq' *) - >> Know ‘n = n' /\ vs = vs'’ - >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\ - qunabbrevl_tac [‘n’, ‘n'’, ‘P0’, ‘Q0’] \\ - MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art []) - (* clean up now duplicated abbreviations: n' and vs' *) - >> qunabbrevl_tac [‘n'’, ‘vs'’] - >> DISCH_THEN (rfs o wrap o GSYM) - (* proving y = y' *) - >> STRONG_CONJ_TAC - >- (MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’] - lameq_principle_hnf_head_eq) \\ - simp [GSYM solvable_iff_has_hnf]) - >> DISCH_THEN (rfs o wrap o GSYM) - >> qunabbrevl_tac [‘y’, ‘y'’] - (* applying lameq_principle_hnf_thm' *) - >> MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’] - lameq_principle_hnf_thm) - >> simp [GSYM solvable_iff_has_hnf] - >> rw [llist_rel_def, LLENGTH_MAP, EL_MAP] - >> Cases_on ‘i < LENGTH Ps’ >> fs [LNTH_fromList, EL_MAP] - >> Q.PAT_X_ASSUM ‘(EL i Ps,SUC r) = z’ (ONCE_REWRITE_TAC o wrap o SYM) - >> Q.PAT_X_ASSUM ‘(EL i Qs,SUC r) = z'’ (ONCE_REWRITE_TAC o wrap o SYM) - >> qexistsl_tac [‘EL i Ps’, ‘EL i Qs’, ‘SUC r’] >> simp [] - >> qabbrev_tac ‘n = LAMl_size Q0’ - >> qabbrev_tac ‘m = LENGTH Qs’ - >> CONJ_TAC (* 2 symmetric subgoals *) - >| [ (* goal 1 (of 2) *) - MATCH_MP_TAC subterm_induction_lemma' \\ - qexistsl_tac [‘P’,‘P0’, ‘n’, ‘m’, ‘vs’, ‘P1’] >> simp [] \\ - qunabbrev_tac ‘vs’ \\ - Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\ - ‘DISJOINT (set vs) (FV P0)’ by METIS_TAC [subterm_disjoint_lemma'] \\ - Q_TAC (HNF_TAC (“P0 :term”, “vs :string list”, - “y :string”, “args :term list”)) ‘P1’ \\ - ‘TAKE (LAMl_size P0) vs = vs’ by rw [] \\ - POP_ASSUM (rfs o wrap) \\ - Q.PAT_X_ASSUM ‘LENGTH Ps = m’ (REWRITE_TAC o wrap o SYM) \\ - AP_TERM_TAC >> simp [Abbr ‘Ps’], - (* goal 2 (of 2) *) - MATCH_MP_TAC subterm_induction_lemma' \\ - qexistsl_tac [‘Q’,‘Q0’, ‘n’, ‘m’, ‘vs’, ‘Q1’] >> simp [] \\ - qunabbrev_tac ‘vs’ \\ - Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\ - ‘DISJOINT (set vs) (FV Q0)’ by METIS_TAC [subterm_disjoint_lemma'] \\ - Q_TAC (HNF_TAC (“Q0 :term”, “vs :string list”, - “y :string”, “args :term list”)) ‘Q1’ \\ - ‘TAKE (LAMl_size Q0) vs = vs’ by rw [] \\ - POP_ASSUM (rfs o wrap) \\ - qunabbrev_tac ‘m’ \\ - AP_TERM_TAC >> simp [Abbr ‘Qs’] ] -QED - (* NOTE: This theorem indicates that ‘m = LENGTH Ms’ is more natural. *) Theorem BT_ltree_el_NIL[local] : !X M r. ltree_el (BT' X M r) [] = @@ -985,6 +902,20 @@ Proof >> Q.PAT_X_ASSUM ‘Ms = Ms'’ (fs o wrap o SYM) QED +Theorem hreduce_subterm_cong : + !X M N p r. M -h->* N /\ p <> [] ==> subterm X M p r = subterm X N p r +Proof + rpt STRIP_TAC + >> ‘M == N’ by PROVE_TAC [hreduces_lameq] + >> reverse (Cases_on ‘solvable M’) + >- (‘unsolvable N’ by PROVE_TAC [lameq_solvable_cong] \\ + rw [subterm_of_unsolvables]) + >> ‘solvable N’ by PROVE_TAC [lameq_solvable_cong] + >> ‘principle_hnf M = principle_hnf N’ by PROVE_TAC [principle_hnf_hreduce] + >> Cases_on ‘p’ >> fs [] + >> rw [subterm_def] +QED + 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) @@ -1021,7 +952,7 @@ Proof >> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp [] QED -Theorem ltree_paths_valid_thm : +Theorem BT_ltree_paths_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 @@ -1030,10 +961,9 @@ 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) + subterm X M p r <> NONE ==> p IN ltree_paths (BT' X M r) Proof - PROVE_TAC [ltree_paths_valid_thm] + PROVE_TAC [BT_ltree_paths_thm] QED (* p <> [] is required because ‘[] IN ltree_paths (BT' X M r)’ always holds. *) @@ -1308,7 +1238,7 @@ Theorem subterm_valid_path_lemma : !q. q <<= FRONT p ==> subterm X M q r <> NONE Proof rpt GEN_TAC >> STRIP_TAC - >> ‘subterm X M p r <> NONE’ by PROVE_TAC [ltree_paths_valid_thm] + >> ‘subterm X M p r <> NONE’ by PROVE_TAC [BT_ltree_paths_thm] >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’, ‘r’] subterm_solvable_lemma) >> rw [] >> FIRST_X_ASSUM MATCH_MP_TAC @@ -1601,15 +1531,15 @@ QED (* NOTE: cf. subterm_fresh_tpm_cong for the easier case of fresh tpm *) Theorem subterm_tpm_lemma : - !X Y p M pi r r'. FINITE X /\ FINITE Y /\ - FV M SUBSET X UNION RANK r /\ - FV (tpm pi M) SUBSET Y UNION RANK r' /\ - set (MAP FST pi) SUBSET RANK r /\ - set (MAP SND pi) SUBSET RANK r' /\ r <= r' - ==> (subterm X M p r = NONE <=> - subterm Y (tpm pi M) p r' = NONE) /\ - (subterm X M p r <> NONE ==> - ?pi'. tpm pi' (subterm' X M p r) = subterm' Y (tpm pi M) p r') + !X Y p M pi r r'. + FINITE X /\ FINITE Y /\ FV M SUBSET X UNION RANK r /\ + FV (tpm pi M) SUBSET Y UNION RANK r' /\ + set (MAP FST pi) SUBSET RANK r /\ + set (MAP SND pi) SUBSET RANK r' /\ r <= r' ==> + (subterm X M p r = NONE <=> + subterm Y (tpm pi M) p r' = NONE) /\ + (subterm X M p r <> NONE ==> + ?pi'. tpm pi' (subterm' X M p r) = subterm' Y (tpm pi M) p r') Proof qx_genl_tac [‘X’, ‘Y’] >> Induct_on ‘p’ @@ -1672,11 +1602,11 @@ Proof >> qabbrev_tac ‘Z = X UNION Y UNION set vs UNION set vs1’ >> qabbrev_tac ‘z = SUC (string_width Z)’ (* NOTE: vs is in rank r; vs1 seems also in the same rank *) - >> qabbrev_tac ‘vs2 = alloc r z (z + n)’ + >> qabbrev_tac ‘vs2 = alloc r z n’ (* properties of vs2 *) >> Know ‘DISJOINT (set vs2) Z’ - >- (rw [Abbr ‘vs2’, Abbr ‘z’, DISJOINT_ALT', alloc_def, MEM_MAP] \\ - ONCE_REWRITE_TAC [TAUT ‘~P \/ Q \/ ~R <=> P /\ R ==> Q’] \\ + >- (rw [Abbr ‘vs2’, Abbr ‘z’, DISJOINT_ALT', alloc_def, MEM_GENLIST] \\ + ONCE_REWRITE_TAC [TAUT ‘~P \/ ~R <=> P /\ R ==> F’] \\ STRIP_TAC \\ ‘FINITE Z’ by rw [Abbr ‘Z’] \\ MP_TAC (Q.SPECL [‘x’, ‘Z’] string_width_thm) >> rw []) @@ -1694,7 +1624,7 @@ Proof Q.PAT_X_ASSUM ‘x IN RANK r’ MP_TAC \\ Suff ‘DISJOINT (RANK r) (set vs2)’ >- rw [DISJOINT_ALT] \\ qunabbrev_tac ‘vs2’ \\ - rw [DISJOINT_ALT, RANK, alloc_def, MEM_MAP] \\ + rw [DISJOINT_ALT, RANK, alloc_def, MEM_GENLIST] \\ rw [n2s_11]) >> DISCH_TAC >> ‘ALL_DISTINCT vs2 /\ LENGTH vs2 = n’ by rw [Abbr ‘vs2’, alloc_thm] @@ -2210,14 +2140,24 @@ Theorem subterm_solvable_cong : (solvable (subterm' X M p r) <=> solvable (subterm' Y M p r')) Proof rpt STRIP_TAC - >> MP_TAC (Q.SPECL [‘X’, ‘Y’, ‘M’, ‘p’, ‘r’, ‘r'’] subterm_tpm_cong) - >> rw [] + >> MP_TAC (Q.SPECL [‘X’, ‘Y’, ‘M’, ‘p’, ‘r’, ‘r'’] subterm_tpm_cong) >> rw [] + >> fs [tpm_rel_alt, solvable_tpm] +QED + +Theorem subterm_solvable_cong' : + !X Y M r r'. + FINITE X /\ FINITE Y /\ + FV M SUBSET X UNION RANK r /\ + FV M SUBSET Y UNION RANK r' ==> + !p. p IN ltree_paths (BT' X M r) ==> + (solvable (subterm' X M p r) <=> solvable (subterm' Y M p r')) +Proof + rpt STRIP_TAC + >> ‘subterm X M p r <> NONE’ by PROVE_TAC [BT_ltree_paths_thm] + >> MP_TAC (Q.SPECL [‘X’, ‘Y’, ‘M’, ‘p’, ‘r’, ‘r'’] subterm_tpm_cong) >> rw [] >> fs [tpm_rel_alt, solvable_tpm] QED -(* In this way, two such terms have the same ‘hnf_children_size o principle_hnf’, - because head reductions are congruence w.r.t. tpm. - *) Theorem subterm_hnf_children_size_cong : !X Y M p r r'. FINITE X /\ FINITE Y /\ FV M SUBSET X UNION RANK r /\ @@ -2400,6 +2340,16 @@ Proof RW_TAC std_ss [BT_tpm_thm, ltree_paths_map_cong] QED +Theorem BT_ltree_paths_cong : + !X Y M r r'. FINITE X /\ FINITE Y /\ + FV M SUBSET X UNION RANK r /\ + FV M SUBSET Y UNION RANK r' + ==> ltree_paths (BT' X M r) = ltree_paths (BT' Y M r') +Proof + rw [Once EXTENSION, BT_ltree_paths_thm] + >> MATCH_MP_TAC (cj 1 subterm_tpm_cong) >> art [] +QED + (*---------------------------------------------------------------------------* * Boehm transformations *---------------------------------------------------------------------------*) @@ -2474,13 +2424,15 @@ QED (* ‘apply pi M’ (applying a Boehm transformation) means "M^{pi}" or "pi(M)" - NOTE: ‘apply [f3;f2;f1] M = (f3 o f2 o f1) M = f3 (f2 (f1 M))’ + NOTE: ‘apply [f3;f2;f1] M = (f3 o f2 o f1) M = f3 (f2 (f1 M))’. [] = id. *) Definition apply_transform_def : apply_transform (pi :transform) = FOLDR $o I pi End Overload apply = “apply_transform” +Overload apply = “\pi (Ms :term list). MAP (apply pi) Ms” +Overload apply = “\pi (Ms :term set). IMAGE (apply pi) Ms” (* NOTE: either FOLDL or FOLDR is correct (due to combinTheory.o_ASSOC), but FOLDR seems more natural requiring natural list induction in @@ -2498,9 +2450,9 @@ Proof QED Theorem apply_transform_rwts[simp] : - (apply [] = I) /\ - (!f pi M. apply (f::pi) M = f (apply pi M)) /\ - (!f pi M. apply (SNOC f pi) M = apply pi (f M)) + (apply [] = (I :term -> term)) /\ + (!f pi M. apply (f::pi) (M :term) = f (apply pi M)) /\ + (!f pi M. apply (SNOC f pi) (M :term) = apply pi (f M)) Proof NTAC 2 (CONJ_TAC >- rw [apply_transform_def, o_DEF]) >> rw [apply_transform_alt, o_DEF, FOLDL_SNOC] @@ -2615,7 +2567,7 @@ Proof QED Theorem Boehm_apply_APPEND : - !p1 p2 M. apply (p1 ++ p2) M = apply p1 (apply p2 M) + !p1 p2 (M :term). apply (p1 ++ p2) M = apply p1 (apply p2 M) Proof Q.X_GEN_TAC ‘p1’ >> SNOC_INDUCT_TAC @@ -2649,11 +2601,10 @@ 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 : +Theorem unsolvable_apply : !pi M. Boehm_transform pi /\ unsolvable M ==> unsolvable (apply pi M) Proof - Induct_on ‘pi’ using SNOC_INDUCT - >- rw [] + Induct_on ‘pi’ using SNOC_INDUCT >- rw [] >> simp [FOLDR_SNOC, Boehm_transform_SNOC] >> qx_genl_tac [‘t’, ‘M’] >> reverse (rw [solving_transform_def]) @@ -2663,6 +2614,12 @@ Proof >> PROVE_TAC [solvable_APP_E] QED +Theorem solvable_apply_imp : + !pi M. Boehm_transform pi /\ solvable (apply pi M) ==> solvable M +Proof + METIS_TAC [unsolvable_apply] +QED + (* Definition 10.3.5 (ii) *) Definition head_original_def : head_original M0 = @@ -2684,6 +2641,11 @@ Definition is_ready_def : ?N. M -h->* N /\ hnf N /\ ~is_abs N /\ head_original N End +(* is_ready' is a more precise version for solvable terms *) +Definition is_ready' : + 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. *) @@ -2718,6 +2680,15 @@ Proof >> qexistsl_tac [‘y’, ‘args’] >> art [] QED +(* NOTE: this proof relies on the new [NOT_AND'] in boolSimps.BOOL_ss *) +Theorem is_ready_alt' : + !M. is_ready' M <=> solvable M /\ + ?y Ns. M -h->* VAR y @* Ns /\ EVERY (\e. y # e) Ns +Proof + rw [is_ready', 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. @@ -5006,20 +4977,12 @@ QED ?fm. apply pi M == fm ' M which is impossible if M is not already "is_ready". - - NOTE: Added ‘p IN ltree_paths (BT X (apply pi M))’ into conclusions for the - needs in the user theorem. - - NOTE: Extended the conclusion with ‘!q. q <<= p /\ q <> []’ - - NOTE: ‘FV (apply pi M) SUBSET X UNION RANK (SUC r)’ is added into the - conclusions for the needs of Boehm_out_lemma. *) 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 /\ - solvable (apply pi M) /\ is_ready (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 <> [] ==> @@ -5109,13 +5072,13 @@ Proof MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art []) >> DISCH_TAC >> qabbrev_tac ‘z = SUC (string_width Z)’ - >> qabbrev_tac ‘l = alloc r z (z + d - m + 1)’ + >> qabbrev_tac ‘l = alloc r z (d - m + 1)’ >> Know ‘ALL_DISTINCT l /\ LENGTH l = d - m + 1’ >- rw [Abbr ‘l’, alloc_thm] >> STRIP_TAC >> Know ‘DISJOINT (set l) Z’ - >- (rw [Abbr ‘l’, Abbr ‘z’, DISJOINT_ALT', alloc_def, MEM_MAP] \\ - ONCE_REWRITE_TAC [TAUT ‘~P \/ Q \/ ~R <=> P /\ R ==> Q’] \\ + >- (rw [Abbr ‘l’, Abbr ‘z’, DISJOINT_ALT', alloc_def, MEM_GENLIST] \\ + ONCE_REWRITE_TAC [TAUT ‘~P \/ ~R <=> P /\ R ==> F’] \\ STRIP_TAC \\ ‘FINITE Z’ by rw [Abbr ‘Z’] \\ MP_TAC (Q.SPECL [‘x’, ‘Z’] string_width_thm) >> rw []) @@ -5168,11 +5131,12 @@ Proof Q.EXISTS_TAC ‘apply p3 (P @* args')’ >> art [] \\ MATCH_MP_TAC Boehm_apply_lameq_cong >> rw []) >> DISCH_TAC - >> CONJ_ASM1_TAC + >> Know ‘solvable (apply pi M)’ >- (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]) + >> DISCH_TAC (* stage work *) >> Know ‘principle_hnf (apply pi M) = VAR b @* args' @* MAP VAR as’ >- (Q.PAT_X_ASSUM ‘Boehm_transform pi’ K_TAC \\ @@ -5264,9 +5228,9 @@ Proof *) MATCH_MP_TAC principle_hnf_denude_thm >> rw []) >> DISCH_TAC - (* applying is_ready_alt *) + (* applying is_ready_alt' *) >> CONJ_TAC - >- (simp [is_ready_alt, Abbr ‘pi’] \\ + >- (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’ @@ -5295,16 +5259,17 @@ Proof FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\ rw [SUBSET_DEF, IN_BIGUNION_IMAGE] \\ Q.EXISTS_TAC ‘e’ >> art []) - (* extra goal *) + (* extra goal: FV (apply pi M) SUBSET X UNION RANK (SUC r) *) >> CONJ_TAC >- (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 \\ + POP_ASSUM MP_TAC (* solvable (apply pi M) *) \\ 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) \\ + DISCH_TAC \\ reverse CONJ_TAC >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘ROW r’ \\ rw [Abbr ‘l’, alloc_SUBSET_ROW] \\ @@ -5483,10 +5448,6 @@ QED but this seems wrong, as ‘subterm X M p’ may not be defined if only ‘p’ is valid path (i.e. the subterm could be a bottom (\bot) as the result of un- solvable terms). - - NOTE: Can we enhance this lemma by using ‘-h->*’ instead of ‘==’? - - NOTE: Use subterm_imp_ltree_paths to prove ‘p IN ltree_paths (BT X M)’. *) Theorem Boehm_out_lemma : !X p M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ @@ -5513,7 +5474,7 @@ Proof >> POP_ASSUM (MP_TAC o (Q.SPEC ‘p’)) (* put q = p *) >> rw [] >> qabbrev_tac ‘M' = apply p0 M’ - >> Q.PAT_X_ASSUM ‘is_ready M'’ (MP_TAC o REWRITE_RULE [is_ready_alt]) + >> 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 *) @@ -5697,6 +5658,16 @@ Proof rw [subtree_equiv_def, Once ltree_equiv_comm] QED +Theorem hreduce_subtree_equiv_cong : + !X M M' N N' p r. M -h->* M' /\ N -h->* N' ==> + (subtree_equiv X M N p r <=> subtree_equiv X M' N' p r) +Proof + rw [subtree_equiv_def] + >> Suff ‘BT' X M r = BT' X M' r /\ BT' X N r = BT' X N' r’ + >- DISCH_THEN (fs o wrap) + >> rw [hreduce_BT_cong] +QED + (* NOTE: This is the explicit form of the Boehm transform constructed in the next lemma. It assumes (at least): @@ -5709,8 +5680,8 @@ Definition Boehm_construction_def : let n_max = MAX_LIST (MAP (\e. subterm_length e p) Ms); d_max = MAX_LIST (MAP (\e. subterm_width e p) Ms) + n_max; k = LENGTH Ms; - Y = BIGUNION (IMAGE FV (set Ms)); - vs0 = NEWS (n_max + SUC d_max + k) (X UNION Y); + X' = BIGUNION (IMAGE FV (set Ms)); + vs0 = NEWS (n_max + SUC d_max + k) (X UNION X'); vs = TAKE n_max vs0; xs = DROP n_max vs0; M i = EL i Ms; @@ -5759,6 +5730,13 @@ QED NOTE: This is the LAST theorem of the current theory, because this proof is so long. Further results (plus users of this lemma) are to be found in the next lameta_completeTheory. + + NOTE: Added the following conclusion for the need of [agree_upto_thm]: + + !q M. MEM M Ms /\ q <<= p ==> + (solvable (subterm' X M q r) <=> + solvable (subterm' X (apply pi M) q r)) + *) Theorem subtree_equiv_lemma_explicit : !X Ms p r. @@ -5767,11 +5745,14 @@ 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 (\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 <=> - subtree_equiv X (apply pi M) (apply pi N) q r) + EVERY is_ready' (apply pi Ms) /\ + EVERY (\M. p IN ltree_paths (BT' X M r)) (apply pi Ms) /\ + (!q M. MEM M Ms /\ q <<= p ==> + (solvable (subterm' X M q r) <=> + solvable (subterm' X (apply pi M) q r))) /\ + !q M N. 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) Proof rpt GEN_TAC >> simp [LET_DEF] >> STRIP_TAC @@ -6423,7 +6404,7 @@ Proof 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 @@ -7095,16 +7076,33 @@ Proof MATCH_MP_TAC ltree_paths_inclusive \\ Q.EXISTS_TAC ‘h::t’ >> simp []) >> DISCH_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L7111" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L7016" >> Suff ‘(!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) /\ + subtree_equiv X (apply pi M) (apply pi N) q r /\ + (solvable (subterm' X M q r) ==> + solvable (subterm' X (apply pi M) q r))) /\ (!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p /\ subtree_equiv X (apply pi M) (apply pi N) q r ==> - subtree_equiv X M N q r)’ - >- METIS_TAC [] + subtree_equiv X M N q r /\ + (solvable (subterm' X (apply pi M) q r) ==> + solvable (subterm' X M q r)))’ + >- (STRIP_TAC \\ + CONJ_TAC (* extra goal *) + >- (qx_genl_tac [‘q’, ‘t’] >> STRIP_TAC \\ + EQ_TAC >> STRIP_TAC >| (* 2 subgoals *) + [ (* goal 1 (of 2) *) + Q.PAT_X_ASSUM ‘!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p /\ + subtree_equiv X M N q r ==> _’ + (MP_TAC o Q.SPECL [‘t’, ‘t’, ‘q’]) >> simp [], + (* goal 2 (of 2) *) + Q.PAT_X_ASSUM + ‘!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p /\ + subtree_equiv X (apply pi M) (apply pi N) q r ==> _’ + (MP_TAC o Q.SPECL [‘t’, ‘t’, ‘q’]) >> simp [] ]) \\ + METIS_TAC []) (* stage work, next goal: !M N q. MEM M Ms /\ MEM N Ms /\ q <<= p /\ subtree_equiv X M N q r ==> @@ -7164,10 +7162,8 @@ Proof by (qunabbrev_tac ‘vs2’ \\ MATCH_MP_TAC LENGTH_TAKE >> art [] \\ FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\ - Q_TAC (RNEWS_TAC (“ys1 :string list”, “r :num”, - “(n :num -> num) j1”)) ‘X’ \\ - Q_TAC (RNEWS_TAC (“ys2 :string list”, “r :num”, - “(n :num -> num) j2”)) ‘X’ \\ + Q_TAC (RNEWS_TAC (“ys1 :string list”, “r :num”, “(n :num->num) j1”)) ‘X’ \\ + Q_TAC (RNEWS_TAC (“ys2 :string list”, “r :num”, “(n :num->num) j2”)) ‘X’ \\ Know ‘DISJOINT (set vs1) (set ys1)’ >- (MATCH_MP_TAC DISJOINT_SUBSET' \\ Q.EXISTS_TAC ‘set vs’ \\ @@ -7231,8 +7227,7 @@ Proof lswapstr (ZIP (vs2,ys2)) (y j2) = lswapstr (ZIP (vs, ys)) (y j2) ==> y j1 = y j2 - P (f j1) = VAR (y j1) ISUB ss = - VAR (y j2) ISUB ss = P (f j2) + P (f j1) = VAR (y j1) ISUB ss = VAR (y j2) ISUB ss = P (f j2) ==> permutator (d_max + f j1) = permutator (d_max + f j2) ==> d_max + f j1 = d_max + f j2 ==> f j1 = f j2 *) @@ -7522,8 +7517,17 @@ Proof Know ‘y i IN X UNION RANK r’ >- METIS_TAC [SUBSET_DEF] \\ Suff ‘RANK r SUBSET RANK r1’ >- SET_TAC [] \\ simp [Abbr ‘r1’, RANK_MONO] ]) >> STRIP_TAC \\ + (* extra goal *) + reverse CONJ_TAC + >- (Suff ‘subterm X (apply pi (M j1)) q r = subterm X (H j1) q r’ + >- (Rewr >> art []) \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> principle_hnf (apply pi (M i)) = H i’ + (MP_TAC o Q.SPEC ‘j1’) >> art [] \\ + DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\ + ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC subterm_of_principle_hnf >> simp []) \\ (* stage work *) - PRINT_TAC "stage work on subtree_equiv_lemma: L7539" \\ + PRINT_TAC "stage work on subtree_equiv_lemma: L7467" \\ 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) \\ @@ -7831,14 +7835,13 @@ Proof - vs1 = RNEWS r1 n1 X (NOTE: n1 <> n2) - vs2 = RNEWS r1 n2 X - vs3/vs4 = RNEWS r1 n3/n4 X - (SUC d_max) - ----- L -------------->| + + ----- L -------------->| (LENGTH = SUC d_max) zs1' = |<--- vs1 --->|<--- zs1 ------>|h| (ROW 0 & r1) vs3 = |<---(vs1)--- vs3 ----(xs1)----->| (ROW r1) (n3 = 1 + d_max + n1 - m1 > n1) - (SUC d_max) - ----- L -------------->| + ----- L -------------->| (LENGTH = SUC d_max) zs2' = |<--- vs2 ------>|<-- zs2 ---->|h| (ROW 0 & r1) vs3 = |<---(vs2)----- vs4 ---(xs2)---->| (ROW r1) (n4 = 1 + d_max + n2 - m2 > n2) @@ -8191,7 +8194,7 @@ 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: L8207" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L8134" >> rpt GEN_TAC >> STRIP_TAC >> POP_ASSUM MP_TAC >> ONCE_REWRITE_TAC [MONO_NOT_EQ] @@ -8435,15 +8438,25 @@ Proof ltree_el (BT' X (M j1) r) q = SOME bot’ >- (MATCH_MP_TAC BT_ltree_el_of_unsolvables >> rw []) \\ simp [] >> DISCH_THEN K_TAC \\ + Know ‘unsolvable (subterm' X (H j1) q r)’ + >- (ASM_SIMP_TAC std_ss [] \\ + MATCH_MP_TAC unsolvable_ISUB \\ + simp [solvable_tpm]) >> DISCH_TAC \\ + (* extra goal *) + Know ‘unsolvable (subterm' X (apply pi (M j1)) q r)’ + >- (Suff ‘subterm X (apply pi (M j1)) q r = subterm X (H j1) q r’ + >- (Rewr >> art []) \\ + FULL_SIMP_TAC std_ss [] \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> principle_hnf (apply pi (M i)) = H i’ + (MP_TAC o Q.SPEC ‘j1’) >> art [] \\ + DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\ + ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC subterm_of_principle_hnf >> simp []) >> Rewr \\ reverse (Cases_on ‘solvable (subterm' X (M j2) q r)’) >- (Know ‘unsolvable (subterm' X (M j2) q r) <=> ltree_el (BT' X (M j2) r) q = SOME bot’ >- (MATCH_MP_TAC BT_ltree_el_of_unsolvables >> rw []) \\ simp []) \\ - Know ‘unsolvable (subterm' X (H j1) q r)’ - >- (ASM_SIMP_TAC std_ss [] \\ - MATCH_MP_TAC unsolvable_ISUB \\ - simp [solvable_tpm]) >> DISCH_TAC \\ Know ‘unsolvable (subterm' X (H j1) q r) <=> ltree_el (BT' X (H j1) r) q = SOME bot’ >- (MATCH_MP_TAC BT_ltree_el_of_unsolvables >> simp []) \\ @@ -9889,7 +9902,7 @@ Proof rw [LAST_APPEND_NOT_NIL]) >> Rewr' \\ simp []) >> DISCH_TAC - >> PRINT_TAC "stage work on subtree_equiv_lemma: L9905" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L9842" >> 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) \\ @@ -9959,7 +9972,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: L9975" + >> PRINT_TAC "stage work on subtree_equiv_lemma: L9912" >> Cases_on ‘y1 = y2’ >> simp [] (* now: y1 <> y2 *) >> ‘y1' <> y2'’ by rw [Abbr ‘y1'’, Abbr ‘y2'’] diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 8bd9d214b7..af377fcb52 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -1454,6 +1454,48 @@ QED (* |- !i n. i < n ==> FV (selector i n) = {} *) Theorem FV_selector[simp] = REWRITE_RULE [closed_def] closed_selector +Theorem selector_alt : + !X i n. FINITE X /\ i < n ==> + ?vs v. LENGTH vs = n /\ ALL_DISTINCT vs /\ DISJOINT X (set vs) /\ + v = EL i vs /\ selector i n = LAMl vs (VAR v) +Proof + RW_TAC std_ss [selector_def] + >> qabbrev_tac ‘Z = GENLIST n2s n’ + >> ‘ALL_DISTINCT Z /\ LENGTH Z = n’ by rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST] + >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] + >> qabbrev_tac ‘z = EL i Z’ + >> ‘MEM z Z’ by rw [Abbr ‘z’, EL_MEM] + >> ‘n2s i = z’ by rw [Abbr ‘z’, Abbr ‘Z’, EL_GENLIST] + >> POP_ORW + (* preparing for LAMl_ALPHA_ssub *) + >> qabbrev_tac ‘Y = NEWS n (set Z UNION X)’ + >> ‘FINITE (set Z UNION X)’ by rw [] + >> ‘ALL_DISTINCT Y /\ DISJOINT (set Y) (set Z UNION X) /\ LENGTH Y = n’ + by rw [NEWS_def, Abbr ‘Y’] + >> fs [] + >> qabbrev_tac ‘M = VAR z’ + >> Know ‘LAMl Z M = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' M)’ + >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [Abbr ‘M’] \\ + Q.PAT_X_ASSUM ‘DISJOINT (set Z) (set Y)’ MP_TAC \\ + rw [DISJOINT_ALT]) + >> Rewr' + >> ‘Y <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] + >> REWRITE_TAC [GSYM fromPairs_def] + >> qabbrev_tac ‘fm = fromPairs Z (MAP VAR Y)’ + >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’] + >> qabbrev_tac ‘y = EL i Y’ + >> Know ‘fm ' M = VAR y’ + >- (simp [Abbr ‘M’, ssub_appstar] \\ + rw [Abbr ‘fm’, Abbr ‘z’] \\ + Know ‘fromPairs Z (MAP VAR Y) ' (EL i Z) = EL i (MAP VAR Y)’ + >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\ + rw [EL_MAP, Abbr ‘y’]) + >> Rewr' + >> Q.EXISTS_TAC ‘Y’ + >> rw [Abbr ‘y’] +QED + +(* TODO: rework this proof by (the new) selector_alt *) Theorem selector_thm : !i n Ns. i < n /\ LENGTH Ns = n ==> selector i n @* Ns == EL i Ns Proof diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml index 03a1473906..753b8747fc 100644 --- a/examples/lambda/barendregt/head_reductionScript.sml +++ b/examples/lambda/barendregt/head_reductionScript.sml @@ -639,6 +639,12 @@ Proof dsimp[SF CONJ_ss] >> metis_tac[] QED +Theorem hnf_absfree_hnf[simp] : + hnf (VAR y @* args) +Proof + rw [hnf_appstar] +QED + (* NOTE: ‘ALL_DISTINCT vs’ has been added to RHS. *) Theorem hnf_cases : !M : term. hnf M <=> ?vs args y. ALL_DISTINCT vs /\ (M = LAMl vs (VAR y @* args)) @@ -2546,6 +2552,33 @@ Proof >> simp [] QED +(* This theorem is more general than selector_thm *) +Theorem hreduce_selector : + !i n Ns. i < n /\ LENGTH Ns = n ==> selector i n @* Ns -h->* EL i Ns +Proof + rpt STRIP_TAC + >> qabbrev_tac ‘X = BIGUNION (IMAGE FV (set Ns))’ + >> ‘FINITE X’ by rw [Abbr ‘X’] + >> MP_TAC (Q.SPECL [‘X’, ‘i’, ‘n’] selector_alt) >> rw [] + >> POP_ORW + >> qabbrev_tac ‘t :term = VAR (EL i vs)’ + >> qabbrev_tac ‘fm = fromPairs vs Ns’ + >> ‘FDOM fm = set vs’ by rw [Abbr ‘fm’, FDOM_fromPairs] + >> Know ‘EL i Ns = fm ' t’ + >- (simp [ssub_thm, Abbr ‘t’, EL_MEM] \\ + simp [Abbr ‘fm’, Once EQ_SYM_EQ] \\ + MATCH_MP_TAC fromPairs_FAPPLY_EL >> art []) + >> Rewr' + >> qunabbrev_tac ‘fm’ + >> MATCH_MP_TAC hreduce_LAMl_appstar + >> rw [EVERY_MEM] + >> Q.PAT_X_ASSUM ‘DISJIONT X (set vs)’ MP_TAC + >> rw [DISJOINT_ALT, Abbr ‘X’] + >> FIRST_X_ASSUM irule + >> Q.EXISTS_TAC ‘FV e’ >> art [] + >> Q.EXISTS_TAC ‘e’ >> art [] +QED + val _ = export_theory() val _ = html_theory "head_reduction"; diff --git a/examples/lambda/barendregt/lameta_completeScript.sml b/examples/lambda/barendregt/lameta_completeScript.sml index c5ff4cc31f..2cede70748 100644 --- a/examples/lambda/barendregt/lameta_completeScript.sml +++ b/examples/lambda/barendregt/lameta_completeScript.sml @@ -2,17 +2,24 @@ (* FILE : lameta_completeScript.sml (chap10_4Script.sml) *) (* TITLE : Completeness of (Untyped) Lambda-Calculus [1, Chapter 10.4] *) (* *) -(* AUTHORS : 2024-2025 The Australian National University (Chun TIAN) *) +(* AUTHORS : 2024-2025 The Australian National University (Chun Tian) *) (* ========================================================================== *) open HolKernel Parse boolLib bossLib; open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory - ltreeTheory llistTheory relationTheory; + ltreeTheory llistTheory relationTheory tautLib topologyTheory; -open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory +open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory NEWLib horeductionTheory solvableTheory head_reductionTheory head_reductionLib - standardisationTheory boehmTheory; + nomsetTheory standardisationTheory boehmTheory takahashiS3Theory; + +(* enable basic monad support *) +open monadsyntax; +val _ = enable_monadsyntax (); +val _ = enable_monad "option"; + +val _ = new_theory "lameta_complete"; val _ = temp_delsimps [ "lift_disj_eq", "lift_imp_disj", @@ -29,33 +36,11 @@ val _ = hide "C"; val _ = hide "W"; 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 +(* some proofs here are large with too many assumptions *) +val _ = set_trace "Goalstack.print_goal_at_top" 0; (*---------------------------------------------------------------------------* - * Equivalent terms + * An equivalence relation of terms *---------------------------------------------------------------------------*) (* Definition 10.2.19 [1, p. 238] @@ -269,10 +254,566 @@ Proof rw [equivalent_def] QED +(* NOTE: ‘0 < r’ is not necessary but makes this proof much easier. *) +Theorem subtree_equiv_alt_equivalent : + !X M N r. FINITE X /\ 0 < r /\ + FV M SUBSET X UNION RANK r /\ + FV N SUBSET X UNION RANK r ==> + (subtree_equiv X M N [] r <=> equivalent M N) +Proof + rpt STRIP_TAC + (* special cases (unsolvable) *) + >> reverse (Cases_on ‘solvable M’) + >- (rw [subtree_equiv_def, equivalent_def, BT_of_unsolvables, ltree_el_def] \\ + reverse EQ_TAC + >- rw [BT_of_unsolvables, ltree_el_def] \\ + DISCH_TAC \\ + Know ‘ltree_el (BT' X N r) [] = SOME bot’ + >- (MATCH_MP_TAC ltree_equiv_some_bot_imp >> art []) \\ + simp [Once MONO_NOT_EQ] >> DISCH_TAC \\ + rw [BT_def, Once ltree_unfold, BT_generator_def, ltree_el_def]) + >> reverse (Cases_on ‘solvable N’) + >- (rw [subtree_equiv_def, equivalent_def, BT_of_unsolvables, ltree_el_def] \\ + CCONTR_TAC >> fs [] \\ + Know ‘ltree_el (BT' X M r) [] = SOME bot’ + >- (MATCH_MP_TAC ltree_equiv_some_bot_imp' >> art []) \\ + rw [BT_def, Once ltree_unfold, BT_generator_def, ltree_el_def]) + (* stage work, now both M and N are solvable *) + >> RW_TAC std_ss [subtree_equiv_def, equivalent_def] + >> qabbrev_tac ‘Y = FV M UNION FV N’ + >> Q_TAC (UNBETA_TAC [BT_def, Once ltree_unfold, BT_generator_def]) ‘BT' X M r’ + >> Q_TAC (UNBETA_TAC [BT_def, Once ltree_unfold, BT_generator_def]) ‘BT' X N r’ + >> simp [GSYM BT_def, LMAP_fromList] + >> rw [ltree_el_def, Abbr ‘l’, Abbr ‘l'’, head_equivalent_def] + (* renaming some abbreviations *) + >> rename1 ‘y3 = y4 /\ LENGTH vs1 + LENGTH Ms2 = LENGTH vs2 + LENGTH Ms1 <=> + y1 = y2 /\ m2 + n1 = m1 + n2’ + >> qunabbrev_tac ‘M0'’ + >> qabbrev_tac ‘N0 = principle_hnf N’ + >> qunabbrev_tac ‘n'''’ + >> qunabbrev_tac ‘M1''’ + >> qabbrev_tac ‘N1' = principle_hnf (N0 @* MAP VAR vs2)’ + >> rfs [Abbr ‘vs1’, Abbr ‘vs2’] + >> Q_TAC (RNEWS_TAC (“vs3 :string list”, “r :num”, “n1 :num”)) ‘X’ + >> Q_TAC (RNEWS_TAC (“vs4 :string list”, “r :num”, “n2 :num”)) ‘X’ + (* stage work *) + >> qabbrev_tac ‘n = MAX n1 n2’ + >> ‘n1 <= n /\ n2 <= n’ by rw [Abbr ‘n’, MAX_LE] + >> ‘FINITE Y’ by rw [Abbr ‘Y’] + >> qunabbrev_tac ‘vs’ + >> Q_TAC (NEWS_TAC (“vs :string list”, “n :num”)) ‘Y’ + (* vs0 includes both vs3 and vs4 *) + >> Q_TAC (RNEWS_TAC (“vs0 :string list”, “r :num”, “n :num”)) ‘X’ + >> ‘TAKE n1 vs0 = vs3’ by rw [Abbr ‘vs0’, Abbr ‘vs3’, TAKE_RNEWS] + >> ‘TAKE n2 vs0 = vs4’ by rw [Abbr ‘vs0’, Abbr ‘vs4’, TAKE_RNEWS] + >> Know ‘DISJOINT (set vs) (FV M0)’ + >- (MATCH_MP_TAC subterm_disjoint_lemma' \\ + qexistsl_tac [‘Y’, ‘M’, ‘0’, ‘n’] >> simp [Abbr ‘Y’]) + >> DISCH_TAC + >> Know ‘DISJOINT (set vs) (FV N0)’ + >- (MATCH_MP_TAC subterm_disjoint_lemma' \\ + qexistsl_tac [‘Y’, ‘N’, ‘0’, ‘n’] >> simp [Abbr ‘Y’]) + >> DISCH_TAC + >> Know ‘DISJOINT (set vs0) (FV M0)’ + >- (MATCH_MP_TAC subterm_disjoint_lemma' \\ + qexistsl_tac [‘X’, ‘M’, ‘r’, ‘n’] >> simp []) + >> DISCH_TAC + >> Know ‘DISJOINT (set vs0) (FV N0)’ + >- (MATCH_MP_TAC subterm_disjoint_lemma' \\ + qexistsl_tac [‘X’, ‘N’, ‘r’, ‘n’] >> simp []) + >> DISCH_TAC + >> qunabbrevl_tac [‘vsM’, ‘vsN’] + >> qabbrev_tac ‘vs1 = TAKE n1 vs’ + >> qabbrev_tac ‘vs2 = TAKE n2 vs’ + >> ‘LENGTH vs1 = n1 /\ LENGTH vs2 = n2 /\ + ALL_DISTINCT vs1 /\ ALL_DISTINCT vs2’ + by simp [Abbr ‘vs1’, Abbr ‘vs2’, ALL_DISTINCT_TAKE] + >> qunabbrev_tac ‘y1’ + >> Q_TAC (HNF_TAC (“M0 :term”, “vs :string list”, + “y1 :string”, “args1 :term list”)) ‘M1’ >> rfs [] + >> qunabbrev_tac ‘y2’ + >> Q_TAC (HNF_TAC (“N0 :term”, “vs :string list”, + “y2 :string”, “args2 :term list”)) ‘N1’ >> rfs [] + >> simp [Abbr ‘m1’, Abbr ‘m2’] + >> Q.PAT_X_ASSUM ‘M0 = _’ (ASSUME_TAC o SYM) + >> Q.PAT_X_ASSUM ‘M1 = _’ (ASSUME_TAC o SYM) + >> Q.PAT_X_ASSUM ‘N0 = _’ (ASSUME_TAC o SYM) + >> Q.PAT_X_ASSUM ‘N1 = _’ (ASSUME_TAC o SYM) + >> qunabbrev_tac ‘y3’ + >> Q_TAC (HNF_TAC (“M0 :term”, “vs0 :string list”, + “y3 :string”, “args3 :term list”)) ‘M1'’ >> rfs [] + >> qunabbrev_tac ‘y4’ + >> Q_TAC (HNF_TAC (“N0 :term”, “vs0 :string list”, + “y4 :string”, “args4 :term list”)) ‘N1'’ >> rfs [] + >> simp [Abbr ‘Ms1’, Abbr ‘Ms2’] + >> Q.PAT_X_ASSUM ‘M0 = _’ (ASSUME_TAC o SYM) + >> Q.PAT_X_ASSUM ‘M1' = _’ (ASSUME_TAC o SYM) + >> Q.PAT_X_ASSUM ‘N0 = _’ (ASSUME_TAC o SYM) + >> Q.PAT_X_ASSUM ‘N1' = _’ (ASSUME_TAC o SYM) + >> fs [] + >> Know ‘DISJOINT (set vs3) (set vs1)’ + >- (MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘set vs’ >> simp [Abbr ‘vs1’, LIST_TO_SET_TAKE] \\ + qunabbrevl_tac [‘vs’, ‘vs3’] \\ + MATCH_MP_TAC DISJOINT_RNEWS >> simp []) + >> DISCH_TAC + >> Know ‘DISJOINT (set vs4) (set vs2)’ + >- (MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘set vs’ >> simp [Abbr ‘vs2’, LIST_TO_SET_TAKE] \\ + qunabbrevl_tac [‘vs’, ‘vs4’] \\ + MATCH_MP_TAC DISJOINT_RNEWS >> simp []) + >> DISCH_TAC + (* NOTE: Two explicit HNFs for M0/N0 by vs1/vs2 and vs3/vs4 + + LAMl vs1 M1 = M0 = LAMl vs3 M1' + LAMl vs2 M2 = N0 = LAMl vs4 M2' + + vs1/vs2 is in ROW 0, while vs3/vs4 is in ROW r (0 < r). + + Now prove upper bounds of FV M1/N1 for disjointness with vs3/vs4 (ROW r) + *) + >> Know ‘FV M1 SUBSET FV (M0 @* MAP VAR vs1)’ + >- (qunabbrev_tac ‘M1’ \\ + MATCH_MP_TAC principle_hnf_FV_SUBSET \\ + simp [has_hnf_def] \\ + qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs1)’ \\ + Q.EXISTS_TAC ‘M1’ \\ + Q.PAT_X_ASSUM ‘LAMl vs1 M1 = M0’ (REWRITE_TAC o wrap o SYM) \\ + simp [] \\ + Q.PAT_X_ASSUM ‘_ = M1’ (REWRITE_TAC o wrap o SYM) \\ + simp [hnf_appstar]) + >> DISCH_TAC + >> Know ‘FV M1 SUBSET X UNION RANK r’ + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV (M0 @* MAP VAR vs1)’ >> simp [] \\ + CONJ_TAC + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV M’ >> art [] \\ + qunabbrev_tac ‘M0’ \\ + MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art []) \\ + Suff ‘set vs1 SUBSET RANK r’ >- SET_TAC [] \\ + Q_TAC (TRANS_TAC SUBSET_TRANS) ‘set vs’ \\ + simp [Abbr ‘vs1’, LIST_TO_SET_TAKE] \\ + qunabbrev_tac ‘vs’ \\ + MATCH_MP_TAC RNEWS_SUBSET_RANK >> art []) + >> DISCH_TAC + >> Know ‘FV N1 SUBSET FV (N0 @* MAP VAR vs2)’ + >- (qunabbrev_tac ‘N1’ \\ + MATCH_MP_TAC principle_hnf_FV_SUBSET \\ + simp [has_hnf_def] \\ + qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vs2)’ \\ + Q.EXISTS_TAC ‘N1’ \\ + Q.PAT_X_ASSUM ‘LAMl vs2 N1 = N0’ (REWRITE_TAC o wrap o SYM) \\ + simp [] \\ + Q.PAT_X_ASSUM ‘_ = N1’ (REWRITE_TAC o wrap o SYM) \\ + simp [hnf_appstar]) + >> DISCH_TAC + >> Know ‘FV N1 SUBSET X UNION RANK r’ + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV (N0 @* MAP VAR vs2)’ >> simp [] \\ + CONJ_TAC + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV N’ >> art [] \\ + qunabbrev_tac ‘N0’ \\ + MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art []) \\ + Suff ‘set vs2 SUBSET RANK r’ >- SET_TAC [] \\ + Q_TAC (TRANS_TAC SUBSET_TRANS) ‘set vs’ \\ + simp [Abbr ‘vs2’, LIST_TO_SET_TAKE] \\ + qunabbrev_tac ‘vs’ \\ + MATCH_MP_TAC RNEWS_SUBSET_RANK >> art []) + >> DISCH_TAC + (* preparing for LAMl_ALPHA *) + >> Know ‘DISJOINT (set vs3) (set vs1 UNION FV M1)’ + >- (simp [DISJOINT_UNION'] \\ + MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘X UNION RANK r’ >> art [] \\ + simp [DISJOINT_UNION'] \\ + qunabbrev_tac ‘vs3’ \\ + MATCH_MP_TAC DISJOINT_RNEWS_RANK >> simp []) + >> DISCH_TAC + >> Know ‘DISJOINT (set vs4) (set vs2 UNION FV N1)’ + >- (simp [DISJOINT_UNION'] \\ + MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘X UNION RANK r’ >> art [] \\ + simp [DISJOINT_UNION'] \\ + qunabbrev_tac ‘vs4’ \\ + MATCH_MP_TAC DISJOINT_RNEWS_RANK >> simp []) + >> DISCH_TAC + (* applying LAMl_ALPHA_tpm *) + >> Know ‘LAMl vs1 M1 = LAMl vs3 (tpm (ZIP (vs1,vs3)) M1)’ + >- (MATCH_MP_TAC LAMl_ALPHA_tpm >> art []) + >> DISCH_THEN (ASSUME_TAC o SYM) + >> Know ‘LAMl vs2 N1 = LAMl vs4 (tpm (ZIP (vs2,vs4)) N1)’ + >- (MATCH_MP_TAC LAMl_ALPHA_tpm >> art []) + >> DISCH_THEN (ASSUME_TAC o SYM) + >> qabbrev_tac ‘pm1 = ZIP (vs1,vs3)’ + >> qabbrev_tac ‘pm2 = ZIP (vs2,vs4)’ + >> Know ‘LAMl vs3 (tpm pm1 M1) = LAMl vs3 M1' /\ + LAMl vs4 (tpm pm2 N1) = LAMl vs4 N1'’ + >- PROVE_TAC [] + >> simp [] >> STRIP_TAC + >> qabbrev_tac ‘pm0 = ZIP (vs,vs0)’ + >> Suff ‘tpm pm1 M1 = tpm pm0 M1 /\ tpm pm2 N1 = tpm pm0 N1’ + >- (Q.PAT_X_ASSUM ‘tpm pm1 M1 = M1'’ (REWRITE_TAC o wrap) \\ + Q.PAT_X_ASSUM ‘tpm pm2 N1 = N1'’ (REWRITE_TAC o wrap) \\ + Q.PAT_X_ASSUM ‘_ = M1’ (REWRITE_TAC o wrap o SYM) \\ + Q.PAT_X_ASSUM ‘_ = N1’ (REWRITE_TAC o wrap o SYM) \\ + Q.PAT_X_ASSUM ‘_ = M1'’ (REWRITE_TAC o wrap o SYM) \\ + Q.PAT_X_ASSUM ‘_ = N1'’ (REWRITE_TAC o wrap o SYM) \\ + simp [tpm_appstar]) + (* clean useless assumptions (mostly about M1' and N1') *) + >> Q.PAT_X_ASSUM ‘tpm pm1 M1 = M1'’ K_TAC + >> Q.PAT_X_ASSUM ‘tpm pm2 N1 = N1'’ K_TAC + >> Q.PAT_X_ASSUM ‘LAMl vs3 _ = LAMl vs1 _’ K_TAC + >> Q.PAT_X_ASSUM ‘LAMl vs4 _ = LAMl vs2 _’ K_TAC + >> Q.PAT_X_ASSUM ‘LAMl vs3 M1' = M0’ K_TAC + >> Q.PAT_X_ASSUM ‘VAR y3 @* args3 = M1'’ K_TAC + >> Q.PAT_X_ASSUM ‘LAMl vs4 N1' = N0’ K_TAC + >> Q.PAT_X_ASSUM ‘VAR y4 @* args4 = N1'’ K_TAC + >> fs [Abbr ‘M1'’, Abbr ‘N1'’] + (* stage work, two ending symmetric subgoals *) + >> CONJ_TAC + >| [ (* goal 1 (of 2) *) + simp [Abbr ‘pm0’, Abbr ‘pm1’] \\ + qabbrev_tac ‘vs1' = DROP n1 vs’ \\ + qabbrev_tac ‘vs3' = DROP n1 vs0’ \\ + ‘vs = vs1 ++ vs1'’ by rw [TAKE_DROP, Abbr ‘vs1’, Abbr ‘vs1'’] \\ + Know ‘DISJOINT (set vs1) (set vs1')’ + >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\ + rw [Abbr ‘vs’, ALL_DISTINCT_APPEND']) >> DISCH_TAC \\ + ‘vs0 = vs3 ++ vs3'’ by rw [TAKE_DROP, Abbr ‘vs3'’] \\ + Q.PAT_X_ASSUM ‘vs = _’ (REWRITE_TAC o wrap) \\ + Q.PAT_X_ASSUM ‘vs0 = _’ (REWRITE_TAC o wrap) \\ + ‘LENGTH vs1' = n - n1’ by rw [Abbr ‘vs1'’, LENGTH_DROP] \\ + ‘LENGTH vs3' = n - n1’ by rw [Abbr ‘vs3'’, LENGTH_DROP] \\ + simp [GSYM ZIP_APPEND, pmact_decompose, Once EQ_SYM_EQ] \\ + MATCH_MP_TAC tpm_unchanged \\ + simp [MAP_ZIP] \\ + reverse CONJ_TAC + >- (MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘X UNION RANK r’ >> art [] \\ + MATCH_MP_TAC DISJOINT_SUBSET' \\ + Q.EXISTS_TAC ‘set vs0’ \\ + reverse CONJ_TAC >- simp [Abbr ‘vs3'’, LIST_TO_SET_DROP] \\ + rw [Once DISJOINT_SYM, Abbr ‘vs0’] \\ + MATCH_MP_TAC DISJOINT_RANK_RNEWS >> simp []) \\ + (* applying SET_TAC [] with sufficient conditions *) + Q.PAT_X_ASSUM ‘FV M1 SUBSET FV M0 UNION set vs1’ MP_TAC \\ + Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M0)’ MP_TAC \\ + Q.PAT_X_ASSUM ‘DISJOINT (set vs1) (set vs1')’ MP_TAC \\ + Know ‘set vs1' SUBSET set vs’ >- rw [Abbr ‘vs1'’, LIST_TO_SET_DROP] \\ + SET_TAC [], + (* goal 2 (of 2) *) + simp [Abbr ‘pm0’, Abbr ‘pm2’] \\ + qabbrev_tac ‘vs2' = DROP n2 vs’ \\ + qabbrev_tac ‘vs4' = DROP n2 vs0’ \\ + ‘vs = vs2 ++ vs2'’ by rw [TAKE_DROP, Abbr ‘vs2’, Abbr ‘vs2'’] \\ + Know ‘DISJOINT (set vs2) (set vs2')’ + >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\ + rw [Abbr ‘vs’, ALL_DISTINCT_APPEND']) >> DISCH_TAC \\ + ‘vs0 = vs4 ++ vs4'’ by rw [TAKE_DROP, Abbr ‘vs4'’] \\ + Q.PAT_X_ASSUM ‘vs = _’ (REWRITE_TAC o wrap) \\ + Q.PAT_X_ASSUM ‘vs0 = _’ (REWRITE_TAC o wrap) \\ + ‘LENGTH vs2' = n - n2’ by rw [Abbr ‘vs2'’, LENGTH_DROP] \\ + ‘LENGTH vs4' = n - n2’ by rw [Abbr ‘vs4'’, LENGTH_DROP] \\ + simp [GSYM ZIP_APPEND, pmact_decompose, Once EQ_SYM_EQ] \\ + MATCH_MP_TAC tpm_unchanged \\ + simp [MAP_ZIP] \\ + reverse CONJ_TAC + >- (MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘X UNION RANK r’ >> art [] \\ + MATCH_MP_TAC DISJOINT_SUBSET' \\ + Q.EXISTS_TAC ‘set vs0’ \\ + reverse CONJ_TAC >- simp [Abbr ‘vs4'’, LIST_TO_SET_DROP] \\ + rw [Once DISJOINT_SYM, Abbr ‘vs0’] \\ + MATCH_MP_TAC DISJOINT_RANK_RNEWS >> simp []) \\ + (* applying SET_TAC [] with sufficient conditions *) + Q.PAT_X_ASSUM ‘FV N1 SUBSET FV N0 UNION set vs2’ MP_TAC \\ + Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV N0)’ MP_TAC \\ + Q.PAT_X_ASSUM ‘DISJOINT (set vs2) (set vs2')’ MP_TAC \\ + Know ‘set vs2' SUBSET set vs’ >- rw [Abbr ‘vs2'’, LIST_TO_SET_DROP] \\ + SET_TAC [] ] +QED + +(*---------------------------------------------------------------------------* + * Boehm trees of beta/eta equivalent terms + *---------------------------------------------------------------------------*) + +(* Proposition 10.1.6 [1, p.219] + + M -h->* M0 + / \b* + == +---[lameq_CR] y1 = y2, n1 = n2, m1 = m2 + \ /b* + N -h->* Ns + *) +Theorem lameq_BT_cong : + !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==> + BT' X M r = BT' X N r +Proof + RW_TAC std_ss [] + >> reverse (Cases_on ‘solvable M’) + >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\ + rw [BT_of_unsolvables]) + >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong] + (* applying ltree_bisimulation *) + >> rw [ltree_bisimulation] + (* NOTE: ‘solvable P /\ solvable Q’ cannot be added here *) + >> Q.EXISTS_TAC + ‘\x y. ?P Q r. FV P UNION FV Q SUBSET X UNION RANK r /\ + P == Q /\ x = BT' X P r /\ y = BT' X Q r’ + >> BETA_TAC + >> CONJ_TAC + >- (qexistsl_tac [‘M’, ‘N’, ‘r’] >> simp [] \\ + Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC \\ + Q.PAT_X_ASSUM ‘FINITE X’ MP_TAC \\ + SET_TAC []) + (* stage work *) + >> qx_genl_tac [‘a1’, ‘ts1’, ‘a2’, ‘ts2’] >> STRIP_TAC + >> qabbrev_tac ‘P0 = principle_hnf P’ + >> qabbrev_tac ‘Q0 = principle_hnf Q’ + >> qabbrev_tac ‘n = LAMl_size P0’ + >> qabbrev_tac ‘n' = LAMl_size Q0’ + >> qabbrev_tac ‘vs = RNEWS r n X’ + >> qabbrev_tac ‘vs'= RNEWS r n' X’ + >> qabbrev_tac ‘P1 = principle_hnf (P0 @* MAP VAR vs)’ + >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’ + >> qabbrev_tac ‘Ps = hnf_children P1’ + >> qabbrev_tac ‘Qs = hnf_children Q1’ + >> qabbrev_tac ‘y = hnf_head P1’ + >> qabbrev_tac ‘y' = hnf_head Q1’ + (* applying ltree_unfold *) + >> Q.PAT_X_ASSUM ‘_ = BT' X Q r’ MP_TAC + >> simp [BT_def, Once ltree_unfold, BT_generator_def] + >> Q.PAT_X_ASSUM ‘_ = BT' X P r’ MP_TAC + >> simp [BT_def, Once ltree_unfold, BT_generator_def] + >> NTAC 2 STRIP_TAC + (* easy case: unsolvable P (and Q) *) + >> reverse (Cases_on ‘solvable P’) + >- (‘unsolvable Q’ by PROVE_TAC [lameq_solvable_cong] >> fs [] \\ + rw [llist_rel_def, LLENGTH_MAP]) + (* now both P and Q are solvable *) + >> ‘solvable Q’ by PROVE_TAC [lameq_solvable_cong] + >> fs [] + (* applying lameq_principle_hnf_size_eq' *) + >> Know ‘n = n' /\ vs = vs'’ + >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\ + qunabbrevl_tac [‘n’, ‘n'’, ‘P0’, ‘Q0’] \\ + MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art []) + (* clean up now duplicated abbreviations: n' and vs' *) + >> qunabbrevl_tac [‘n'’, ‘vs'’] + >> DISCH_THEN (rfs o wrap o GSYM) + (* proving y = y' *) + >> STRONG_CONJ_TAC + >- (MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’] + lameq_principle_hnf_head_eq) \\ + simp [GSYM solvable_iff_has_hnf]) + >> DISCH_THEN (rfs o wrap o GSYM) + >> qunabbrevl_tac [‘y’, ‘y'’] + (* applying lameq_principle_hnf_thm' *) + >> MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’] + lameq_principle_hnf_thm) + >> simp [GSYM solvable_iff_has_hnf] + >> rw [llist_rel_def, LLENGTH_MAP, EL_MAP] + >> Cases_on ‘i < LENGTH Ps’ >> fs [LNTH_fromList, EL_MAP] + >> Q.PAT_X_ASSUM ‘(EL i Ps,SUC r) = z’ (ONCE_REWRITE_TAC o wrap o SYM) + >> Q.PAT_X_ASSUM ‘(EL i Qs,SUC r) = z'’ (ONCE_REWRITE_TAC o wrap o SYM) + >> qexistsl_tac [‘EL i Ps’, ‘EL i Qs’, ‘SUC r’] >> simp [] + >> qabbrev_tac ‘n = LAMl_size Q0’ + >> qabbrev_tac ‘m = LENGTH Qs’ + >> CONJ_TAC (* 2 symmetric subgoals *) + >| [ (* goal 1 (of 2) *) + MATCH_MP_TAC subterm_induction_lemma' \\ + qexistsl_tac [‘P’,‘P0’, ‘n’, ‘m’, ‘vs’, ‘P1’] >> simp [] \\ + qunabbrev_tac ‘vs’ \\ + Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\ + ‘DISJOINT (set vs) (FV P0)’ by METIS_TAC [subterm_disjoint_lemma'] \\ + Q_TAC (HNF_TAC (“P0 :term”, “vs :string list”, + “y :string”, “args :term list”)) ‘P1’ \\ + ‘TAKE (LAMl_size P0) vs = vs’ by rw [] \\ + POP_ASSUM (rfs o wrap) \\ + Q.PAT_X_ASSUM ‘LENGTH Ps = m’ (REWRITE_TAC o wrap o SYM) \\ + AP_TERM_TAC >> simp [Abbr ‘Ps’], + (* goal 2 (of 2) *) + MATCH_MP_TAC subterm_induction_lemma' \\ + qexistsl_tac [‘Q’,‘Q0’, ‘n’, ‘m’, ‘vs’, ‘Q1’] >> simp [] \\ + qunabbrev_tac ‘vs’ \\ + Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\ + ‘DISJOINT (set vs) (FV Q0)’ by METIS_TAC [subterm_disjoint_lemma'] \\ + Q_TAC (HNF_TAC (“Q0 :term”, “vs :string list”, + “y :string”, “args :term list”)) ‘Q1’ \\ + ‘TAKE (LAMl_size Q0) vs = vs’ by rw [] \\ + POP_ASSUM (rfs o wrap) \\ + qunabbrev_tac ‘m’ \\ + AP_TERM_TAC >> simp [Abbr ‘Qs’] ] +QED + +(*---------------------------------------------------------------------------* + * BT_paths and BT_valid_paths + *---------------------------------------------------------------------------*) + +Definition BT_paths_def : + BT_paths M = ltree_paths (BT' (FV M) M 0) +End + +Theorem BT_paths_nil[simp] : + [] IN BT_paths M +Proof + rw [BT_paths_def] +QED + +Theorem BT_paths_thm : + !X M r. FINITE X /\ FV M SUBSET X UNION RANK r ==> + BT_paths M = ltree_paths (BT' X M r) +Proof + rw [BT_paths_def] + >> MATCH_MP_TAC BT_ltree_paths_cong >> simp [] +QED + +Theorem BT_paths_eq_subterm_not_none : + !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r ==> + (p IN BT_paths M <=> subterm X M p r <> NONE) +Proof + rw [GSYM BT_ltree_paths_thm, GSYM BT_paths_thm] +QED + +(* NOTE: "valid" paths are paths leading to non-bottom nodes. *) +Definition BT_valid_paths_def : + BT_valid_paths M = + {p | p IN BT_paths M /\ ltree_el (BT' (FV M) M 0) p <> SOME bot} +End + +Theorem BT_valid_paths_SUBSET_paths : + !M. BT_valid_paths M SUBSET BT_paths M +Proof + rw [SUBSET_DEF, BT_valid_paths_def] +QED + +Theorem BT_valid_paths_nil[simp] : + [] IN BT_valid_paths M <=> solvable M +Proof + rw [BT_valid_paths_def] + >> Suff ‘unsolvable (subterm' (FV M) M [] 0) <=> + ltree_el (BT' (FV M) M 0) [] = SOME bot’ + >- (simp [] >> PROVE_TAC []) + >> MATCH_MP_TAC BT_ltree_el_of_unsolvables >> simp [] +QED + +(* By subterm_tpm_cong and BT_ltree_el_of_unsolvables, etc. *) +Theorem BT_valid_paths_thm : + !X M r. FINITE X /\ FV M SUBSET X UNION RANK r ==> + BT_valid_paths M = + {p | p IN ltree_paths (BT' X M r) /\ + ltree_el (BT' X M r) p <> SOME bot} +Proof + rw [BT_valid_paths_def, Once EXTENSION] + >> simp [GSYM BT_paths_thm] + >> Cases_on ‘x IN BT_paths M’ >> rw [] + >> rename1 ‘p IN BT_paths M’ + >> Know ‘ltree_el (BT' X M r) p = SOME bot <=> unsolvable (subterm' X M p r)’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC BT_ltree_el_of_unsolvables >> art [] \\ + Know ‘subterm X M p r <> NONE <=> p IN ltree_paths (BT' X M r)’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC BT_ltree_paths_thm >> art []) >> Rewr' \\ + rw [GSYM BT_paths_thm]) + >> Rewr' + >> Know ‘ltree_el (BT' (FV M) M 0) p = SOME bot <=> + unsolvable (subterm' (FV M) M p 0)’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC BT_ltree_el_of_unsolvables >> simp [] \\ + Know ‘subterm (FV M) M p 0 <> NONE <=> p IN ltree_paths (BT' (FV M) M 0)’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC BT_ltree_paths_thm >> simp []) >> Rewr' \\ + rw [GSYM BT_paths_thm]) + >> Rewr' + >> Suff ‘tpm_rel (subterm' (FV M) M p 0) (subterm' X M p r)’ + >- (rw [tpm_rel_alt] >> POP_ORW \\ + rw [solvable_tpm]) + >> irule (cj 2 subterm_tpm_cong) >> simp [] + >> Know ‘subterm (FV M) M p 0 <> NONE <=> p IN ltree_paths (BT' (FV M) M 0)’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC BT_ltree_paths_thm >> simp []) + >> Rewr' + >> rw [GSYM BT_paths_thm] +QED + +(* By BT_ltree_paths_thm and BT_ltree_el_of_unsolvables, etc. *) +Theorem BT_valid_paths_thm' : + !X M r. FINITE X /\ FV M SUBSET X UNION RANK r ==> + BT_valid_paths M = + {p | subterm X M p r <> NONE /\ solvable (subterm' X M p r)} +Proof + rpt STRIP_TAC + >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘r’] BT_valid_paths_thm) >> rw [] + >> rw [Once EXTENSION] + >> simp [GSYM BT_ltree_paths_thm] + >> Cases_on ‘x IN ltree_paths (BT' X M r)’ >> rw [] + >> rename1 ‘p IN ltree_paths (BT' X M r)’ + >> Suff ‘unsolvable (subterm' X M p r) <=> ltree_el (BT' X M r) p = SOME bot’ + >- PROVE_TAC [] + >> MATCH_MP_TAC BT_ltree_el_of_unsolvables + >> rw [GSYM BT_ltree_paths_thm] +QED + (*---------------------------------------------------------------------------* * subtree_equiv_lemma *---------------------------------------------------------------------------*) +Theorem FV_apply_Boehm_construction : + !X Ms p r. + FINITE X /\ p <> [] /\ 0 < r /\ Ms <> [] /\ + BIGUNION (IMAGE FV (set Ms)) SUBSET X UNION RANK r ==> + !M. MEM M Ms ==> + FV (apply (Boehm_construction X Ms p) M) SUBSET X UNION RANK r +Proof + rpt GEN_TAC >> STRIP_TAC + >> Q.X_GEN_TAC ‘N’ + >> DISCH_TAC + >> UNBETA_TAC [Boehm_construction_def] “Boehm_construction X Ms p” + >> qunabbrev_tac ‘X'’ + >> qabbrev_tac ‘Y = BIGUNION (IMAGE FV (set Ms))’ + >> ‘FINITE Y’ by (rw [Abbr ‘Y’] >> rw []) + >> simp [Boehm_apply_APPEND] + (* eliminate p3 *) + >> simp [Abbr ‘p3’, Boehm_apply_MAP_rightctxt'] + >> reverse CONJ_TAC + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘set vs0’ \\ + rw [Abbr ‘xs’, LIST_TO_SET_DROP] \\ + Suff ‘set vs0 SUBSET RANK r’ >- SET_TAC [] \\ + Q_TAC (TRANS_TAC SUBSET_TRANS) ‘ROW 0’ >> rw [ROW_SUBSET_RANK] \\ + qunabbrev_tac ‘vs0’ \\ + MATCH_MP_TAC RNEWS_SUBSET_ROW >> rw []) + (* eliminate p2 *) + >> qabbrev_tac ‘sub = \k. GENLIST (\i. (P i,y i)) k’ + >> Know ‘!t. apply p2 t = t ISUB sub k’ + >- (simp [Abbr ‘p2’, Abbr ‘sub’] \\ + Q.SPEC_TAC (‘k’, ‘j’) \\ + Induct_on ‘j’ >- rw [] \\ + rw [GENLIST, REVERSE_SNOC, ISUB_SNOC]) + >> DISCH_TAC + >> simp [] + >> Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV (apply p1 N) UNION FVS (sub k)’ + >> CONJ_TAC >- rw [FV_ISUB_upperbound] + >> Know ‘!j. DOM (sub j) = IMAGE y (count j) /\ FVS (sub j) = {}’ + >- (simp [Abbr ‘sub’] \\ + Induct_on ‘j’ >- rw [DOM_DEF, FVS_DEF] \\ + rw [GENLIST, REVERSE_SNOC, DOM_DEF, FVS_DEF, COUNT_SUC, DOM_SNOC, FVS_SNOC] + >- SET_TAC [] \\ + rw [Abbr ‘P’, FV_permutator]) + >> DISCH_TAC + >> simp [] + (* eliminate p1 *) + >> simp [Abbr ‘p1’, Boehm_apply_MAP_rightctxt'] + >> reverse CONJ_TAC + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) ‘set vs0’ \\ + rw [Abbr ‘vs’, LIST_TO_SET_TAKE] \\ + Suff ‘set vs0 SUBSET RANK r’ >- SET_TAC [] \\ + Q_TAC (TRANS_TAC SUBSET_TRANS) ‘ROW 0’ >> rw [ROW_SUBSET_RANK] \\ + qunabbrev_tac ‘vs0’ \\ + MATCH_MP_TAC RNEWS_SUBSET_ROW >> rw []) + >> Q_TAC (TRANS_TAC SUBSET_TRANS) ‘Y’ >> art [] + >> rw [Abbr ‘Y’, SUBSET_DEF] + >> Q.EXISTS_TAC ‘FV N’ >> art [] + >> Q.EXISTS_TAC ‘N’ >> art [] +QED + Theorem subtree_equiv_lemma_explicit'[local] = subtree_equiv_lemma_explicit |> SIMP_RULE std_ss [LET_DEF] @@ -280,16 +821,37 @@ Theorem subtree_equiv_lemma : !X Ms p r. 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) /\ - 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 <=> - subtree_equiv X (apply pi M) (apply pi N) q r) + EVERY (\M. p IN ltree_paths (BT' X M r)) Ms ==> + ?pi. Boehm_transform pi /\ EVERY is_ready' (apply pi Ms) /\ + EVERY (\M. FV M SUBSET X UNION RANK r) (apply pi Ms) /\ + EVERY (\M. p IN ltree_paths (BT' X M r)) (apply pi Ms) /\ + (!q M. MEM M Ms /\ q <<= p ==> + (solvable (subterm' X M q r) <=> + solvable (subterm' X (apply pi M) q r))) /\ + (!q M N. 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)) Proof rpt STRIP_TAC + >> Know ‘EVERY (\M. subterm X M p r <> NONE) Ms’ + >- (POP_ASSUM MP_TAC \\ + rw [EVERY_MEM] \\ + Know ‘FV M SUBSET X UNION RANK r’ + >- (Q_TAC (TRANS_TAC SUBSET_TRANS) + ‘BIGUNION (IMAGE FV (set Ms))’ >> art [] \\ + rw [SUBSET_DEF] \\ + Q.EXISTS_TAC ‘FV M’ >> art [] \\ + Q.EXISTS_TAC ‘M’ >> art []) >> DISCH_TAC \\ + METIS_TAC [BT_ltree_paths_thm]) + >> DISCH_TAC >> Q.EXISTS_TAC ‘Boehm_construction X Ms p’ - >> MATCH_MP_TAC subtree_equiv_lemma_explicit' >> art [] + >> Suff ‘EVERY (\M. FV M SUBSET X UNION RANK r) + (MAP (apply (Boehm_construction X Ms p)) Ms)’ + >- (Rewr \\ + MATCH_MP_TAC subtree_equiv_lemma_explicit' >> art []) + >> simp [EVERY_MEM, MEM_MAP] + >> rw [] + >> irule FV_apply_Boehm_construction >> art [] QED (* Definition 10.3.10 (iii) and (iv) [1, p.251] @@ -299,7 +861,7 @@ QED *) Definition agree_upto_def : agree_upto X Ms p r <=> - !M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==> subtree_equiv X M N q r + !q M N. q <<= p /\ MEM M Ms /\ MEM N Ms ==> subtree_equiv X M N q r End (* NOTE: subtree_equiv_lemma and this theorem together implies the original @@ -307,9 +869,10 @@ 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 ==> + (!q M N. q <<= p /\ MEM M Ms /\ MEM N Ms /\ + 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 + agree_upto X Ms p r ==> agree_upto X (apply pi Ms) p r Proof RW_TAC std_ss [agree_upto_def, MEM_MAP] >> LAST_X_ASSUM MATCH_MP_TAC >> art [] @@ -319,88 +882,456 @@ QED (* Lemma 10.3.11 [1. p.251] *) Theorem agree_upto_lemma : !X Ms p r. - 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) /\ - (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 ==> - subtree_equiv X M N p r + FINITE X /\ Ms <> [] /\ p <> [] /\ 0 < r /\ + (!M. MEM M Ms ==> FV M SUBSET X UNION RANK r) /\ + (!M. MEM M Ms ==> p IN ltree_paths (BT' X M r)) ==> + ?pi. Boehm_transform pi /\ + (!M. MEM M Ms ==> is_ready' (apply pi M)) /\ + (!M. MEM M Ms ==> FV (apply pi M) SUBSET X UNION RANK r) /\ + (!M. MEM M Ms ==> p IN ltree_paths (BT' X (apply pi M) r)) /\ + (!q M. MEM M Ms /\ q <<= p ==> + (solvable (subterm' X M q r) <=> + solvable (subterm' X (apply pi M) q r))) /\ + (agree_upto X Ms p r ==> + agree_upto X (apply pi Ms) p r) /\ + !M N. MEM M Ms /\ MEM N Ms /\ + subtree_equiv X (apply pi M) (apply pi N) p r ==> + subtree_equiv X M N p r Proof - rpt GEN_TAC - >> DISCH_THEN (MP_TAC o (MATCH_MP subtree_equiv_lemma)) - >> rpt STRIP_TAC - >> Q.EXISTS_TAC ‘pi’ - >> RW_TAC std_ss [] - >- (MATCH_MP_TAC subtree_equiv_imp_agree_upto >> rw [] \\ - METIS_TAC []) - >> Q.PAT_X_ASSUM ‘!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==> _’ - (MP_TAC o Q.SPECL [‘M’, ‘N’, ‘p’]) - >> simp [] + rpt STRIP_TAC + >> MP_TAC (Q.SPECL [‘X’, ‘Ms’, ‘p’, ‘r’] subtree_equiv_lemma) + >> simp [BIGUNION_IMAGE_SUBSET, EVERY_MEM, MEM_MAP] + >> STRIP_TAC + >> Q.EXISTS_TAC ‘pi’ >> rw [] + >| [ (* goal 1 (of 4) *) + FIRST_X_ASSUM MATCH_MP_TAC \\ + Q.EXISTS_TAC ‘M’ >> art [], + (* goal 2 (of 4) *) + FIRST_X_ASSUM MATCH_MP_TAC \\ + Q.EXISTS_TAC ‘M’ >> art [], + (* goal 3 (of 4) *) + FIRST_X_ASSUM MATCH_MP_TAC \\ + Q.EXISTS_TAC ‘M’ >> art [], + (* goal 4 (of 4) *) + MATCH_MP_TAC subtree_equiv_imp_agree_upto >> rw [] \\ + METIS_TAC [] ] QED -(* Definition 10.3.10 (ii) [1, p.251] *) +(* Definition 10.3.10 (ii) [1, p.251] + + NOTE: This definition now assumes ’p IN ltree_paths (BT' X M r)’. + *) Definition is_faithful_def : is_faithful p X Ms pi r <=> - (!M. MEM M Ms ==> - (solvable (apply pi M) <=> p IN ltree_paths (BT' X M r))) /\ - !M N. MEM M Ms /\ MEM N Ms ==> - (subtree_equiv X M N p r <=> equivalent (apply pi M) (apply pi N)) + (!M. MEM M Ms ==> (p IN BT_valid_paths M <=> solvable (apply pi M))) /\ + !M N. MEM M Ms /\ MEM N Ms ==> + (subtree_equiv X M N p r <=> + equivalent (apply pi M) (apply pi N)) End Overload is_faithful' = “is_faithful []” 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) /\ - !M N. MEM M Ms /\ MEM N Ms ==> - (subtree_equiv X M N [] r <=> - equivalent (apply pi M) (apply pi N))) -Proof - rw [ltree_paths_def, is_faithful_def, EVERY_MEM] - >> reverse EQ_TAC - >- (rw [MEM_MAP] \\ - FIRST_X_ASSUM MATCH_MP_TAC \\ - Q.EXISTS_TAC ‘M’ >> art []) - >> simp [MEM_MAP] - >> STRIP_TAC - >> ONCE_REWRITE_TAC [CONJ_COMM] - >> CONJ_ASM1_TAC - >- (rw [] >> FIRST_X_ASSUM MATCH_MP_TAC >> art []) - >> Q.X_GEN_TAC ‘M’ - >> DISCH_TAC - >> Suff ‘solvable (apply pi M)’ - >- METIS_TAC [Boehm_transform_of_unsolvables] - >> FIRST_X_ASSUM MATCH_MP_TAC - >> Q.EXISTS_TAC ‘M’ >> art [] -QED - -Theorem is_faithful_two : - !p X M N pi r. - is_faithful p X [M; N] pi r <=> - (solvable (apply pi M) <=> p IN ltree_paths (BT' X M r)) /\ - (solvable (apply pi N) <=> p IN ltree_paths (BT' X N r)) /\ - (subtree_equiv X M N p r <=> equivalent (apply pi M) (apply pi N)) + !X Ms pi r. FINITE X /\ 0 < r /\ + (!M. MEM M Ms ==> FV M SUBSET X UNION RANK r) ==> + (is_faithful' X Ms pi r <=> + (!M. MEM M Ms ==> (solvable M <=> solvable (apply pi M))) /\ + !M N. MEM M Ms /\ MEM N Ms ==> + (equivalent M N <=> + equivalent (apply pi M) (apply pi N))) Proof rw [is_faithful_def] - >> EQ_TAC >> rw [] (* 6 subgoals here *) - >> rw [] (* only one subgoal is left *) - >> rw [Once subtree_equiv_comm, Once equivalent_comm] + >> Suff ‘!M N. MEM M Ms /\ MEM N Ms ==> + (subtree_equiv X M N [] r <=> equivalent M N)’ + >- METIS_TAC [] + >> rpt STRIP_TAC + >> MATCH_MP_TAC subtree_equiv_alt_equivalent >> rw [] QED -Theorem is_faithful_two' : - !p X M N pi r. - p IN ltree_paths (BT' X M r) /\ - p IN ltree_paths (BT' X N r) ==> - (is_faithful p X [M; N] pi r <=> - solvable (apply pi M) /\ - solvable (apply pi N) /\ - (subtree_equiv X M N p r <=> equivalent (apply pi M) (apply pi N))) +(* Proposition 10.3.13 [1, p.253] + + NOTE: In the base case ‘p = []’, terms in Ms are either all solvable or + all unsolvable. In the induction case, however, p IN BT_paths M, p <> [] + implies M solvable. + *) +Theorem agree_upto_thm : + !X p Ms r. FINITE X /\ Ms <> [] /\ 0 < r /\ + (!M. MEM M Ms ==> FV M SUBSET X UNION RANK r) /\ + (!M. MEM M Ms ==> p IN ltree_paths (BT' X M r)) /\ + agree_upto X Ms p r ==> + ?pi. Boehm_transform pi /\ is_faithful p X Ms pi r Proof - rw [is_faithful_two] + Q.X_GEN_TAC ‘X’ + >> Induct_on ‘p’ + >- (rpt STRIP_TAC >> Q.EXISTS_TAC ‘[]’ >> rw [is_faithful']) + (* stage work *) + >> rw [is_faithful_def] + (* trivial case: all unsolvable *) + >> Cases_on ‘!M. MEM M Ms ==> unsolvable M’ + >- (Q.EXISTS_TAC ‘[]’ \\ + reverse (rw []) + >- (fs [agree_upto_def] \\ + Know ‘equivalent M N <=> subtree_equiv X M N [] r’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC subtree_equiv_alt_equivalent >> art [] \\ + fs [BIGUNION_IMAGE_SUBSET]) >> Rewr' \\ + FIRST_X_ASSUM irule >> rw []) \\ + MP_TAC (Q.SPECL [‘X’, ‘M’, ‘r’] BT_valid_paths_thm') >> rw [] \\ + Know ‘subterm X M (h::p) r = NONE <=> h::p NOTIN ltree_paths (BT' X M r)’ + >- (Suff ‘h::p IN ltree_paths (BT' X M r) <=> subterm X M (h::p) r <> NONE’ + >- PROVE_TAC [] \\ + MATCH_MP_TAC BT_ltree_paths_thm >> simp []) >> Rewr' \\ + STRONG_DISJ_TAC \\ + Suff ‘solvable M’ >- METIS_TAC [] \\ + MATCH_MP_TAC ltree_paths_imp_solvable \\ + qexistsl_tac [‘h::p’, ‘X’, ‘r’] >> simp []) + (* one is solvable, all are solvable *) + >> Know ‘!M. MEM M Ms ==> solvable M’ + >- (rpt STRIP_TAC \\ + MATCH_MP_TAC ltree_paths_imp_solvable \\ + qexistsl_tac [‘h::p’, ‘X’, ‘r’] >> simp [GSYM BT_paths_thm]) + >> POP_ASSUM K_TAC >> DISCH_TAC + (* applying agree_upto_lemma *) + >> MP_TAC (Q.SPECL [‘X’, ‘Ms’, ‘h::p’, ‘r’] agree_upto_lemma) >> rw [] + (* p0 is asserted *) + >> rename1 ‘Boehm_transform p0’ + >> fs [is_ready_alt'] + (* decomposing Ms *) + >> qabbrev_tac ‘k = LENGTH Ms’ + >> ‘k <> 0’ by rw [Abbr ‘k’, LENGTH_NIL] + >> qabbrev_tac ‘M = \i. EL i Ms’ + >> Know ‘!P. (!N. MEM N Ms ==> P N) <=> !i. i < k ==> P (M i)’ + >- (Q.X_GEN_TAC ‘P’ \\ + reverse EQ_TAC >> rw [MEM_EL] >- simp [] \\ + FIRST_X_ASSUM MATCH_MP_TAC \\ + Q.EXISTS_TAC ‘i’ >> art []) + >> DISCH_THEN (fs o wrap) + >> qabbrev_tac ‘M1 = \i. principle_hnf (apply p0 (M i))’ + >> Know ‘!i. i < k ==> ?y Ns. M1 i = VAR y @* Ns /\ EVERY (\e. y # e) Ns’ + >- (rpt STRIP_TAC \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> solvable (apply p0 (M i)) /\ _’ drule \\ + rw [Abbr ‘M1’] \\ + qexistsl_tac [‘y’, ‘Ns’] >> art [] \\ + rw [principle_hnf_thm', hnf_appstar]) + >> DISCH_TAC + (* NOTE: take the head variable and children terms from ‘N 0’ *) + >> Know ‘?y Ns. M1 0 = VAR y @* Ns’ + >- (POP_ASSUM (MP_TAC o Q.SPEC ‘0’) >> rw [] \\ + qexistsl_tac [‘y’, ‘Ns’] >> art []) + >> STRIP_TAC + >> qabbrev_tac ‘m = LENGTH Ns’ + >> Know ‘!i. i < k ==> ?Ns. M1 i = VAR y @* Ns /\ EVERY (\e. y # e) Ns /\ + LENGTH Ns = m’ + >- (rpt STRIP_TAC \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> ?y Ns. P’ drule >> rw [] \\ + Q.EXISTS_TAC ‘Ns'’ \\ + Suff ‘y = y' /\ LENGTH Ns' = m’ >- rw [] \\ + Cases_on ‘i = 0’ >- fs [] \\ + FULL_SIMP_TAC std_ss [agree_upto_def] \\ + Q.PAT_X_ASSUM ‘!q M N. q <<= h::p /\ MEM M (apply p0 Ms) /\ _ ==> _’ + (MP_TAC o Q.SPECL [‘[]’, ‘apply p0 ((M :num -> term) 0)’, + ‘apply p0 ((M :num -> term) i)’]) \\ + simp [subtree_equiv_def, MEM_MAP] \\ + impl_tac + >- (CONJ_TAC >| (* 2 subgoals *) + [ (* goal 1 (of 2) *) + Q.EXISTS_TAC ‘M 0’ >> simp [MEM_EL] \\ + Q.EXISTS_TAC ‘0’ >> rw [], + (* goal 2 (of 2) *) + Q.EXISTS_TAC ‘M i’ >> simp [MEM_EL] \\ + Q.EXISTS_TAC ‘i’ >> rw [] ]) \\ + Know ‘BT' X (apply p0 (M 0)) r = BT' X (M1 0) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘M1’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + Know ‘BT' X (apply p0 (M i)) r = BT' X (M1 i) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘M1’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + REWRITE_TAC [BT_def] \\ + NTAC 2 (simp [Once ltree_unfold, BT_generator_def, LMAP_fromList, + ltree_el_def]) \\ + simp [head_equivalent_def]) + >> simp [EXT_SKOLEM_THM'] + >> STRIP_TAC (* this assert f as the children function of all Ms *) + >> Q.PAT_X_ASSUM ‘!i. i < k ==> ?y Ns. _’ K_TAC + >> Know ‘Ns = f 0’ (* eliminate Ns by f *) + >- (POP_ASSUM (MP_TAC o Q.SPEC ‘0’) >> rw []) + >> DISCH_THEN (FULL_SIMP_TAC std_ss o wrap) + >> ‘!i. i < k ==> solvable (apply p0 (M i))’ by PROVE_TAC [] + >> Q.PAT_X_ASSUM ‘!i. i < k ==> solvable (apply p0 (M i)) /\ _’ K_TAC + >> Know ‘!i. i < k ==> apply p0 (M i) -h->* VAR y @* f i’ + >- (rpt STRIP_TAC \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> M1 i = VAR y @* f i /\ _’ drule \\ + simp [Abbr ‘M1’, principle_hnf_thm']) + >> DISCH_TAC + (* Now we use ‘h::p IN BT_paths (apply p0 (M i))’ (and ‘M 0’) to show that + ‘h < m’, as otherwise p1 (the selector) cannot be properly defined. + *) + >> Know ‘h < m’ + >- (Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN ltree_paths (BT' X (apply p0 (M i)) r)’ + (MP_TAC o Q.SPEC ‘0’) >> simp [] \\ + MP_TAC (Q.SPECL [‘X’, ‘apply p0 ((M :num -> term) 0)’, ‘r’ ] BT_paths_thm) \\ + simp [] >> DISCH_THEN K_TAC \\ + Know ‘BT' X (apply p0 (M 0)) r = BT' X (M1 0) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘M1’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + Q.PAT_X_ASSUM ‘M1 0 = _’ (REWRITE_TAC o wrap) \\ + simp [BT_def, Once ltree_unfold, BT_generator_def, LMAP_fromList, + ltree_paths_alt, ltree_el_def] \\ + simp [GSYM BT_def, LNTH_fromList, MAP_MAP_o] \\ + Cases_on ‘h < m’ >> rw []) + >> DISCH_TAC + >> Q.PAT_X_ASSUM ‘M1 0 = _’ K_TAC + (* p1 is defined as a selector *) + >> qabbrev_tac ‘p1 = [[selector h m/y]]’ + >> ‘Boehm_transform p1’ by rw [Boehm_transform_def, Abbr ‘p1’] + >> Know ‘!i. i < k ==> apply (p1 ++ p0) (M i) -h->* EL h (f i)’ + >- (rw [Boehm_transform_APPEND, Abbr ‘p1’] \\ + MATCH_MP_TAC hreduce_TRANS \\ + Q.EXISTS_TAC ‘[selector h m/y] (VAR y @* f i)’ \\ + CONJ_TAC + >- (MATCH_MP_TAC hreduce_substitutive \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> M1 i = VAR y @* f i /\ _’ drule \\ + simp [Abbr ‘M1’, principle_hnf_thm']) \\ + simp [appstar_SUB] \\ + Know ‘MAP [selector h m/y] (f i) = f i’ + >- (rw [Once LIST_EQ_REWRITE, EL_MAP] \\ + MATCH_MP_TAC lemma14b \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> M1 i = VAR y @* f i /\ _’ drule \\ + rw [EVERY_MEM] \\ + POP_ASSUM MATCH_MP_TAC >> rw [EL_MEM]) >> Rewr' \\ + MATCH_MP_TAC hreduce_selector >> rw []) + >> DISCH_TAC + (* redefine Ns as the h-subterms of Ms + + NOTE: So far we don't know if any “EL h (f i)” is solvable, thus it's not + sure whether “principle_hnf (apply (p1 ++ p0) (M i)) = EL h (f i)”. + *) + >> qabbrev_tac ‘Ns = GENLIST (EL h o f) k’ + >> ‘LENGTH Ns = k’ by rw [Abbr ‘Ns’, LENGTH_GENLIST] + >> Know ‘!i. i < k ==> MEM (EL h (f i)) Ns’ + >- (rw [Abbr ‘Ns’, MEM_GENLIST] \\ + Q.EXISTS_TAC ‘i’ >> art []) + >> DISCH_TAC + (* proving one antecedent of IH *) + >> Know ‘agree_upto X Ns p (SUC r)’ + >- (fs [agree_upto_def] \\ + rw [Abbr ‘Ns’, MEM_GENLIST] \\ + NTAC 2 (POP_ASSUM MP_TAC) \\ + rename1 ‘a < k ==> b < k ==> _’ >> NTAC 2 STRIP_TAC \\ + Q.PAT_X_ASSUM ‘!q M N. q <<= h::p /\ MEM M (apply p0 Ms) /\ _ ==> _’ + (MP_TAC o Q.SPECL [‘h::q’, ‘apply p0 ((M :num -> term) a)’, + ‘apply p0 ((M :num -> term) b)’]) \\ + simp [MEM_MAP] \\ + impl_tac + >- (CONJ_TAC >| (* 2 subgoals *) + [ (* goal 1 (of 2) *) + Q.EXISTS_TAC ‘M a’ >> rw [EL_MEM, Abbr ‘M’], + (* goal 2 (of 2) *) + Q.EXISTS_TAC ‘M b’ >> rw [EL_MEM, Abbr ‘M’] ]) \\ + simp [subtree_equiv_def] \\ + Know ‘BT' X (apply p0 (M a)) r = BT' X (M1 a) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘M1’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + Know ‘BT' X (apply p0 (M b)) r = BT' X (M1 b) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘M1’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + simp [] \\ + ‘!i. solvable (VAR y @* f i)’ by rw [] \\ + ‘!i. principle_hnf (VAR y @* f i) = VAR y @* f i’ by rw [] \\ + Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold, + LMAP_fromList]) ‘BT' X (VAR y @* f a) r’ \\ + simp [Abbr ‘M0’, GSYM appstar_APPEND, LNTH_fromList, ltree_el_def, + GSYM BT_def, Abbr ‘y'’, Abbr ‘Ms'’, Abbr ‘n’, Abbr ‘l’, Abbr ‘M1'’, + Abbr ‘vs’, EL_MAP] \\ + Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold, + LMAP_fromList]) ‘BT' X (VAR y @* f b) r’ \\ + simp [Abbr ‘M0’, GSYM appstar_APPEND, LNTH_fromList, ltree_el_def, + GSYM BT_def, Abbr ‘y'’, Abbr ‘Ms'’, Abbr ‘n’, Abbr ‘l’, Abbr ‘M1'’, + Abbr ‘vs’, EL_MAP]) + >> DISCH_TAC + >> qabbrev_tac ‘pi' = p1 ++ p0’ + >> ‘Boehm_transform pi'’ by rw [Abbr ‘pi'’, Boehm_transform_APPEND] + >> Know ‘agree_upto X (apply pi' Ms) p (SUC r)’ + >- (Q.PAT_X_ASSUM ‘agree_upto X Ns p (SUC r)’ MP_TAC \\ + rw [agree_upto_def, MEM_MAP, Abbr ‘Ns’, MEM_GENLIST, MEM_EL] \\ + Know ‘subtree_equiv X (apply pi' (M n)) (apply pi' (M n')) q (SUC r) <=> + subtree_equiv X (EL h (f n)) (EL h (f n')) q (SUC r)’ + >- (MATCH_MP_TAC hreduce_subtree_equiv_cong >> simp []) >> Rewr' \\ + FIRST_X_ASSUM MATCH_MP_TAC >> rw [] >| (* 2 subgoals *) + [ (* goal 1 (of 2) *) + Q.EXISTS_TAC ‘n’ >> art [], + (* goal 2 (of 2) *) + Q.EXISTS_TAC ‘n'’ >> art [] ]) + >> DISCH_TAC + (* proving antecedents of IH *) + >> Know ‘!N. MEM N Ns ==> FV N SUBSET X UNION RANK (SUC r)’ + >- (simp [MEM_EL, Abbr ‘Ns’] \\ + NTAC 2 STRIP_TAC \\ + POP_ORW >> simp [EL_GENLIST] \\ + MATCH_MP_TAC subterm_induction_lemma' \\ + qexistsl_tac [‘apply p0 (M n)’, ‘M1 n’, ‘0’, ‘m’, ‘[]’, ‘M1 n’] \\ + simp []) + >> DISCH_TAC + >> Know ‘!N. MEM N Ns ==> p IN ltree_paths (BT' X N (SUC r))’ + >- (NTAC 2 STRIP_TAC \\ + Q.PAT_X_ASSUM ‘!N. MEM N Ns ==> FV N SUBSET X UNION RANK (SUC r)’ drule \\ + POP_ASSUM MP_TAC \\ + simp [MEM_EL, Abbr ‘Ns’] \\ + STRIP_TAC >> POP_ORW \\ + simp [EL_GENLIST] >> DISCH_TAC \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN ltree_paths (BT' X (apply p0 (M i)) r)’ + (MP_TAC o Q.SPEC ‘n’) >> simp [] \\ + MP_TAC (Q.SPECL [‘X’, ‘apply p0 ((M :num -> term) n)’, ‘r’] BT_paths_thm) \\ + simp [] >> DISCH_THEN K_TAC \\ + MP_TAC (Q.SPECL [‘X’, ‘EL h (f (n :num))’, ‘SUC r’] BT_paths_thm) \\ + simp [] >> DISCH_THEN K_TAC \\ + Know ‘BT' X (apply p0 (M n)) r = BT' X (M1 n) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘M1’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + ‘!i. solvable (VAR y @* f i)’ by rw [] \\ + ‘!i. principle_hnf (VAR y @* f i) = VAR y @* f i’ by rw [] \\ + Q_TAC (UNBETA_TAC [BT_def, Once ltree_unfold, BT_generator_def]) + ‘BT' X (M1 (n :num)) r’ \\ + simp [LMAP_fromList, ltree_paths_alt, ltree_el_def, GSYM BT_def] \\ + simp [Abbr ‘M0’, GSYM appstar_APPEND, LNTH_fromList, EL_MAP, + Abbr ‘y'’, Abbr ‘Ms'’, Abbr ‘n'’, Abbr ‘l’, Abbr ‘M1'’, Abbr ‘vs’]) + >> DISCH_TAC + >> Know ‘!N. MEM N (apply pi' Ms) ==> p IN ltree_paths (BT' X N (SUC r))’ + >- (rw [MEM_MAP, MEM_EL] \\ + Know ‘BT' X (apply pi' (M n)) (SUC r) = BT' X (EL h (f n)) (SUC r)’ + >- (MATCH_MP_TAC hreduce_BT_cong >> simp []) >> Rewr' \\ + FIRST_X_ASSUM MATCH_MP_TAC >> simp []) + >> DISCH_TAC + >> Know ‘!N. MEM N (apply pi' Ms) ==> FV N SUBSET X UNION RANK (SUC r)’ + >- (rw [MEM_MAP, MEM_EL, Abbr ‘pi'’, Boehm_apply_APPEND, Abbr ‘p1’] \\ + Q_TAC (TRANS_TAC SUBSET_TRANS) ‘FV (apply p0 (M n))’ \\ + CONJ_TAC >- (MATCH_MP_TAC FV_SUB_SUBSET >> simp [closed_def]) \\ + Q_TAC (TRANS_TAC SUBSET_TRANS) ‘X UNION RANK r’ >> simp [] \\ + Suff ‘RANK r SUBSET RANK (SUC r)’ >- SET_TAC [] \\ + simp [RANK_MONO]) + >> DISCH_TAC + (* using IH *) + >> Q.PAT_X_ASSUM + ‘!Ms' r'. Ms' <> [] /\ 0 < r' /\ _ /\ _ /\ agree_upto X Ms' p r' ==> + ?pi. Boehm_transform pi /\ is_faithful p X Ms' pi r'’ + (MP_TAC o Q.SPECL [‘apply pi' Ms’, ‘SUC r’]) + >> simp [is_faithful_def] + >> DISCH_THEN (Q.X_CHOOSE_THEN ‘p2’ STRIP_ASSUME_TAC) + >> qabbrev_tac ‘pi = p2 ++ p1 ++ p0’ + >> Q.EXISTS_TAC ‘pi’ + >> CONJ_TAC (* Boehm_transform pi *) + >- (qunabbrev_tac ‘pi’ \\ + MATCH_MP_TAC Boehm_transform_APPEND >> art [] \\ + MATCH_MP_TAC Boehm_transform_APPEND >> art []) + >> simp [Abbr ‘pi’, GSYM APPEND_ASSOC] + >> REWRITE_TAC [Boehm_apply_APPEND] + >> Know ‘!i. i < k ==> MEM (apply pi' (M i)) (apply pi' Ms)’ + >- (rw [MEM_MAP] \\ + Q.EXISTS_TAC ‘M i’ >> simp [EL_MEM, Abbr ‘M’]) + >> DISCH_TAC + (* stage work, the 2nd part is easier following textbook *) + >> reverse CONJ_TAC + >- (simp [MEM_EL] \\ + qx_genl_tac [‘t1’, ‘t2’] (* temporary names, to be consumed soon *) \\ + ONCE_REWRITE_TAC [TAUT ‘P /\ Q ==> R <=> P ==> Q ==> R’] \\ + DISCH_THEN (Q.X_CHOOSE_THEN ‘a’ STRIP_ASSUME_TAC) \\ + DISCH_THEN (Q.X_CHOOSE_THEN ‘b’ STRIP_ASSUME_TAC) \\ + Q.PAT_X_ASSUM ‘_ = M a’ (ONCE_REWRITE_TAC o wrap) \\ + Q.PAT_X_ASSUM ‘_ = M b’ (ONCE_REWRITE_TAC o wrap) \\ + qabbrev_tac ‘t1 = apply pi' (M a)’ \\ + qabbrev_tac ‘t2 = apply pi' (M b)’ \\ + Q.PAT_X_ASSUM ‘!M N. _ ==> (subtree_equiv X M N p (SUC r) <=> + equivalent (apply p2 M) (apply p2 N))’ + (MP_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ] o + Q.SPECL [‘t1’, ‘t2’]) \\ + simp [Abbr ‘t1’, Abbr ‘t2’] >> DISCH_THEN K_TAC \\ + (* now “equivalent” is elimianted *) + Know ‘subtree_equiv X (M a) (M b) (h::p) r’ + >- (Q.PAT_X_ASSUM ‘agree_upto X Ms (h::p) r’ MP_TAC \\ + rw [agree_upto_def] \\ + POP_ASSUM MATCH_MP_TAC >> simp [EL_MEM, Abbr ‘M’]) >> Rewr \\ + qabbrev_tac ‘t1 = apply p0 (M a)’ \\ + qabbrev_tac ‘t2 = apply p0 (M b)’ \\ + Q.PAT_X_ASSUM ‘agree_upto X (apply p0 Ms) (h::p) r’ MP_TAC \\ + rw [agree_upto_def] \\ + POP_ASSUM (MP_TAC o Q.SPECL [‘h::p’, ‘t1’, ‘t2’]) \\ + simp [Abbr ‘t1’, Abbr ‘t2’] \\ + impl_tac + >- (rw [MEM_MAP] >| (* 2 subgoals *) + [ Q.EXISTS_TAC ‘M a’ >> simp [EL_MEM, Abbr ‘M’], + Q.EXISTS_TAC ‘M b’ >> simp [EL_MEM, Abbr ‘M’] ]) \\ + (* applying hreduce_subtree_equiv_cong *) + Know ‘subtree_equiv X (apply p0 (M a)) (apply p0 (M b)) (h::p) r <=> + subtree_equiv X (VAR y @* f a) (VAR y @* f b) (h::p) r’ + >- (MATCH_MP_TAC hreduce_subtree_equiv_cong >> simp []) >> Rewr' \\ + Know ‘subtree_equiv X (apply pi' (M a)) (apply pi' (M b)) p (SUC r) <=> + subtree_equiv X (EL h (f a)) (EL h (f b)) p (SUC r)’ + >- (MATCH_MP_TAC hreduce_subtree_equiv_cong >> simp []) >> Rewr' \\ + simp [subtree_equiv_def] \\ + ‘!i. solvable (VAR y @* f i)’ by rw [] \\ + ‘!i. principle_hnf (VAR y @* f i) = VAR y @* f i’ by rw [] \\ + Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold, + LMAP_fromList, LET_DEF]) ‘BT' X (VAR y @* f a) r’ \\ + simp [GSYM BT_def, LMAP_fromList, ltree_el_def, LNTH_fromList, EL_MAP] \\ + Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold, + LMAP_fromList, LET_DEF]) ‘BT' X (VAR y @* f b) r’ \\ + simp [GSYM BT_def, LMAP_fromList, ltree_el_def, LNTH_fromList, EL_MAP]) + (* final goal *) + >> rpt STRIP_TAC + (* clean up all assumptions involving term equivalences *) + >> Q.PAT_X_ASSUM ‘!M N. _ ==> (subtree_equiv X M N p (SUC r) <=> _)’ K_TAC + >> Q.PAT_X_ASSUM ‘!M N. _ ==> subtree_equiv X M N (h::p) r’ K_TAC + >> rpt (Q.PAT_X_ASSUM ‘agree_upto X _ _ _’ K_TAC) + >> qabbrev_tac ‘N = apply pi' (M i)’ + >> Q.PAT_X_ASSUM ‘!M. MEM M (apply pi' Ms) ==> + (p IN BT_valid_paths M <=> solvable (apply p2 M))’ + (MP_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ] o Q.SPEC ‘N’) + >> simp [Abbr ‘N’] + >> DISCH_THEN K_TAC + >> qabbrev_tac ‘N = apply pi' (M i)’ + (* applying BT_valid_paths_thm' to turn the goal to subterm arguments *) + >> Know ‘BT_valid_paths N = {p | subterm X N p (SUC r) <> NONE /\ + solvable (subterm' X N p (SUC r))}’ + >- (MATCH_MP_TAC BT_valid_paths_thm' >> simp [Abbr ‘N’]) + >> Rewr' + >> Know ‘BT_valid_paths (M i) = {p | subterm X (M i) p r <> NONE /\ + solvable (subterm' X (M i) p r)}’ + >- (MATCH_MP_TAC BT_valid_paths_thm' >> simp []) + >> Rewr' + >> simp [Abbr ‘N’] + (* applying BT_ltree_paths_thm *) + >> ‘subterm X (M i) (h::p) r <> NONE’ by simp [GSYM BT_ltree_paths_thm] + >> ‘subterm X (apply pi' (M i)) p (SUC r) <> NONE’ + by simp [GSYM BT_ltree_paths_thm] + >> simp [] + >> Q.PAT_X_ASSUM ‘!q M. MEM M Ms /\ q <<= h::p ==> _’ + (MP_TAC o Q.SPECL [‘h::p’, ‘M (i :num)’]) + >> impl_tac >- simp [EL_MEM, Abbr ‘M’] + >> Rewr' + (* applying hreduce_subterm_cong *) + >> Know ‘subterm X (apply p0 (M i)) (h::p) r = + subterm X (VAR y @* f i) (h::p) r’ + >- (MATCH_MP_TAC hreduce_subterm_cong >> simp []) + >> Rewr' + (* NOTE: To apply hreduce_subterm_cong to “subterm' X (apply pi' (M i)”, + ‘p <> []’ is required. The case ‘p = []’ is trivial. + *) + >> Cases_on ‘p = []’ + >- (simp [] \\ + Know ‘solvable (apply pi' (M i)) <=> solvable (EL h (f i))’ + >- (MATCH_MP_TAC hreduce_solvable_cong >> simp []) >> Rewr' \\ + Suff ‘subterm' X (VAR y @* f i) [h] r = EL h (f i)’ >- rw [] \\ + rw [subterm_def]) + >> Know ‘subterm X (apply pi' (M i)) p (SUC r) = + subterm X (EL h (f i)) p (SUC r)’ + >- (MATCH_MP_TAC hreduce_subterm_cong >> simp []) + >> Rewr' + >> Suff ‘subterm' X (VAR y @* f i) (h::p) r = + subterm' X (EL h (f i)) p (SUC r)’ >- rw [] + >> ‘!i. solvable (VAR y @* f i)’ by rw [] + >> ‘!i. principle_hnf (VAR y @* f i) = VAR y @* f i’ by rw [] + >> Q_TAC (UNBETA_TAC [subterm_def]) ‘subterm X (VAR y @* f i) (h::p) r’ + >> simp [] QED Theorem is_faithful_swap : @@ -885,16 +1816,16 @@ Proof (* stage work *) >> ‘?M0. M == M0 /\ hnf M0’ by METIS_TAC [has_hnf_def, solvable_iff_has_hnf] >> ‘?vs args y. ALL_DISTINCT vs /\ M0 = LAMl vs (VAR y @* args)’ - by METIS_TAC [hnf_cases] + by METIS_TAC [hnf_cases] >> qabbrev_tac ‘as = NEWS (LENGTH args) (FV P)’ >> qabbrev_tac ‘pi = [LAMl as P/y]::MAP rightctxt (MAP VAR (REVERSE vs))’ >> Q.EXISTS_TAC ‘pi’ >> STRONG_CONJ_TAC >- rw [Abbr ‘pi’, Boehm_transform_def, EVERY_SNOC, EVERY_MAP] >> DISCH_TAC - (* applying Boehm_transform_of_unsolvables *) + (* applying unsolvable_apply *) >> reverse CONJ_TAC - >- (MATCH_MP_TAC Boehm_transform_of_unsolvables >> art []) + >- (MATCH_MP_TAC unsolvable_apply >> art []) (* stage work *) >> MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘apply pi M0’ @@ -915,7 +1846,7 @@ Proof >- (irule lameq_sub_cong >> rw [lameq_LAMl_appstar_VAR]) >> rw [Abbr ‘t’, appstar_SUB] >> ‘DISJOINT (set as) (FV P) /\ LENGTH as = LENGTH args’ - by rw [NEWS_def, Abbr ‘as’] + by rw [NEWS_def, Abbr ‘as’] >> MATCH_MP_TAC lameq_LAMl_appstar_reduce >> rw [] QED diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml index 933a377e98..60914169c9 100644 --- a/examples/lambda/barendregt/solvableScript.sml +++ b/examples/lambda/barendregt/solvableScript.sml @@ -659,6 +659,20 @@ Proof >> MATCH_MP_TAC unsolvable_subst >> art [] QED +Theorem solvable_hnf[simp] : + solvable (LAMl vs (VAR y @* args)) +Proof + REWRITE_TAC [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 + (*---------------------------------------------------------------------------* * Principle Head Normal Forms (principle_hnf) *---------------------------------------------------------------------------*) @@ -1148,6 +1162,14 @@ Proof >> MATCH_MP_TAC lameq_solvable_cong_lemma >> art [] QED +Theorem hreduce_solvable_cong : + !M N. M -h->* N ==> (solvable M <=> solvable N) +Proof + rpt STRIP_TAC + >> MATCH_MP_TAC lameq_solvable_cong + >> MATCH_MP_TAC hreduces_lameq >> art [] +QED + Theorem lameq_principle_hnf : !M. has_hnf M ==> principle_hnf M == M Proof diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml index 940719825c..ccbb1342d6 100644 --- a/examples/lambda/basics/appFOLDLScript.sml +++ b/examples/lambda/basics/appFOLDLScript.sml @@ -308,11 +308,19 @@ Proof QED Theorem tpm_LAMl: - tpm π (LAMl vs M) = LAMl (listpm string_pmact π vs) (tpm π M) + !vs pi M. tpm pi (LAMl vs M) = LAMl (listpm string_pmact pi vs) (tpm pi M) Proof - Induct_on ‘vs’ >> simp[] + Induct_on ‘vs’ >> simp[] QED +(* |- !vs pi M. + LAMl vs (tpm pi M) = + tpm pi (LAMl (listpm string_pmact (REVERSE pi) vs) M) + *) +Theorem LAMl_tpm = tpm_LAMl |> Q.SPECL [‘vs’, ‘REVERSE pi’, ‘tpm pi M’] + |> SRULE [tpm_eql] + |> Q.GENL [‘vs’, ‘pi’, ‘M’] + Theorem tpm_appstar: tpm π (M ·· Ms) = tpm π M ·· listpm term_pmact π Ms Proof @@ -375,10 +383,23 @@ Proof ] QED +Theorem LAMl_ALPHA_tpm : + !xs ys M. LENGTH xs = LENGTH ys /\ ALL_DISTINCT xs /\ ALL_DISTINCT ys /\ + DISJOINT (set ys) (set xs UNION FV M) ==> + LAMl xs M = LAMl ys (tpm (ZIP (xs,ys)) M) +Proof + rpt STRIP_TAC + >> Know ‘LAMl xs M = LAMl ys (M ISUB REVERSE (ZIP (MAP VAR ys, xs)))’ + >- (MATCH_MP_TAC LAMl_ALPHA >> art []) + >> Rewr' + >> fs [DISJOINT_UNION'] + >> simp [fresh_tpm_isub, REVERSE_ZIP, MAP_REVERSE] +QED + Theorem LAMl_ALPHA_ssub : !vs vs' M. LENGTH vs = LENGTH vs' /\ ALL_DISTINCT vs /\ ALL_DISTINCT vs' /\ - DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==> + DISJOINT (set vs') (set vs UNION FV M) ==> LAMl vs M = LAMl vs' ((FEMPTY |++ ZIP (vs, MAP VAR vs')) ' M) Proof rpt STRIP_TAC diff --git a/examples/lambda/basics/basic_swapScript.sml b/examples/lambda/basics/basic_swapScript.sml index c9d0ea8b32..dcdbcee5eb 100644 --- a/examples/lambda/basics/basic_swapScript.sml +++ b/examples/lambda/basics/basic_swapScript.sml @@ -9,8 +9,7 @@ open HolKernel Parse boolLib bossLib; open boolSimps arithmeticTheory stringTheory pred_setTheory numLib hurdUtils - listTheory rich_listTheory pairTheory numpairTheory - string_numTheory listRangeTheory; + listTheory rich_listTheory pairTheory numpairTheory string_numTheory; val _ = new_theory "basic_swap"; @@ -164,28 +163,25 @@ QED (* The primitive ‘alloc’ allocates a ranged list of variables in the row *) Definition alloc_def : - alloc r m n = MAP (n2s o npair r) [m ..< n] + alloc r z n = GENLIST (\i. n2s (npair r (z + i))) n End -Theorem alloc_NIL[simp] : - alloc r n n = [] +Theorem alloc_0[simp] : + alloc r z 0 = [] Proof rw [alloc_def] QED Theorem alloc_thm : - !r m n. ALL_DISTINCT (alloc r m n) /\ LENGTH (alloc r m n) = n - m + !r z n. ALL_DISTINCT (alloc r z n) /\ LENGTH (alloc r z n) = n Proof - rw [alloc_def] - >> MATCH_MP_TAC ALL_DISTINCT_MAP_INJ >> rw [] + rw [alloc_def, ALL_DISTINCT_GENLIST] QED Theorem alloc_prefix : !r m n n'. n <= n' ==> alloc r m n <<= alloc r m n' Proof - rw [alloc_def] - >> MATCH_MP_TAC isPREFIX_MAP - >> MATCH_MP_TAC isPREFIX_listRangeLHI >> art [] + rw [alloc_def, isPREFIX_GENLIST] QED (* ---------------------------------------------------------------------- @@ -193,7 +189,7 @@ QED ---------------------------------------------------------------------- *) Definition RNEWS : - RNEWS r n s = let d = SUC (string_width s) in alloc r d (d + n) + RNEWS r n s = let z = SUC (string_width s) in alloc r z n End Theorem RNEWS_0[simp] : @@ -204,16 +200,15 @@ QED Theorem RNEWS_def : !r n s. - FINITE s ==> - ALL_DISTINCT (RNEWS r n s) /\ DISJOINT (set (RNEWS r n s)) s /\ - LENGTH (RNEWS r n s) = n + FINITE s ==> + ALL_DISTINCT (RNEWS r n s) /\ DISJOINT (set (RNEWS r n s)) s /\ + LENGTH (RNEWS r n s) = n Proof rw [RNEWS, alloc_thm] - >> rw [DISJOINT_ALT', alloc_def, MEM_MAP] - >> rw [Once DISJ_COMM] - >> STRONG_DISJ_TAC - >> MP_TAC (Q.SPECL [‘n2s (r *, y)’, ‘s’] string_width_thm) - >> rw [] + >> rw [DISJOINT_ALT', alloc_def, MEM_MAP, MEM_GENLIST] + >> qabbrev_tac ‘x = n2s (r *, (i + SUC (string_width s)))’ + >> MP_TAC (Q.SPECL [‘x’, ‘s’] string_width_thm) + >> simp [Abbr ‘x’] QED Theorem RNEWS_prefix : @@ -227,7 +222,7 @@ Theorem TAKE_RNEWS : Proof rw [RNEWS, alloc_def] >> qabbrev_tac ‘z = string_width s’ - >> simp [Once LIST_EQ_REWRITE, listRangeLHI_def] + >> simp [Once LIST_EQ_REWRITE] >> Q.X_GEN_TAC ‘i’ >> DISCH_TAC >> simp [EL_TAKE, EL_MAP] QED @@ -238,9 +233,10 @@ Theorem RNEWS_set : string_width s < j /\ j <= string_width s + n} Proof rw [RNEWS, alloc_def, Once EXTENSION, MEM_GENLIST, MEM_MAP] + >> qabbrev_tac ‘z = string_width s’ >> EQ_TAC >> rw [] - >- (Q.EXISTS_TAC ‘y’ >> rw []) - >> Q.EXISTS_TAC ‘j’ >> rw [] + >- (Q.EXISTS_TAC ‘i + SUC z’ >> rw []) + >> Q.EXISTS_TAC ‘j - SUC z’ >> rw [] QED Theorem RNEWS_11 : @@ -298,8 +294,8 @@ QED Theorem alloc_SUBSET_ROW : !r m n. set (alloc r m n) SUBSET ROW r Proof - rw [alloc_def, ROW, SUBSET_DEF, MEM_MAP] - >> Q.EXISTS_TAC ‘y’ >> rw [] + rw [alloc_def, ROW, SUBSET_DEF, MEM_GENLIST] + >> Q.EXISTS_TAC ‘i + m’ >> art [] QED Theorem ROW_DISJOINT : diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml index 9f5b65af63..ac1a25cae0 100644 --- a/examples/lambda/basics/termScript.sml +++ b/examples/lambda/basics/termScript.sml @@ -494,6 +494,7 @@ Theorem tpm_subst_out: Proof SRW_TAC [][tpm_subst] QED +(* Lemma 1.15 (a) [2, p.8] (NOTE: It was Lemma 1.14 (a) of 1st edition of [2]) *) Theorem lemma14a[simp]: !t. [VAR v/v] t = t Proof @@ -501,6 +502,7 @@ Proof SRW_TAC [][SUB_THM, SUB_VAR] QED +(* Lemma 1.15 (b) [2, p.8] *) Theorem lemma14b: !M. ~(v IN FV M) ==> ([N/v] M = M) Proof @@ -605,6 +607,7 @@ Proof >> ASM_SET_TAC [] QED +(* Lemma 1.16 (a) [2, p.9] *) Theorem lemma15a: !M. v ∉ FV M ==> [N/v]([VAR v/x]M) = [N/x]M Proof @@ -612,6 +615,7 @@ Proof SRW_TAC [][SUB_THM, SUB_VAR] QED +(* Lemma 1.16 (b) [2, p.9] *) Theorem lemma15b: v ∉ FV M ==> [VAR u/v]([VAR v/u] M) = M Proof SRW_TAC [][lemma15a] @@ -1928,3 +1932,11 @@ val _ = adjoin_after_completion (fn _ => PP.add_string term_info_string) val _ = export_theory() val _ = html_theory "term"; + +(* References: + + [1] Barendregt, H.P.: The lambda calculus, its syntax and semantics. + College Publications, London (1984). + [2] Hindley, J.R., Seldin, J.P.: Lambda-calculus and combinators, an introduction. + Second Edition. Cambridge University Press, Cambridge (2008). + *) diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml index a282504e79..efd37db982 100644 --- a/src/pred_set/src/pred_setScript.sml +++ b/src/pred_set/src/pred_setScript.sml @@ -4669,6 +4669,16 @@ Proof PROVE_TAC [] QED +Theorem BIGUNION_IMAGE_SUBSET : + !f s t. BIGUNION (IMAGE f s) SUBSET t <=> !x. x IN s ==> f x SUBSET t +Proof + RW_TAC std_ss [BIGUNION_SUBSET, IN_IMAGE] + >> reverse EQ_TAC >> rw [] + >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) + >> FIRST_X_ASSUM MATCH_MP_TAC + >> Q.EXISTS_TAC ‘x’ >> art [] +QED + val BIGUNION_IMAGE_UNIV = store_thm (* from util_prob *) ("BIGUNION_IMAGE_UNIV", ``!f N.