diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml index 160d44dbf4..dc87f6d27c 100644 --- a/examples/lambda/barendregt/boehmScript.sml +++ b/examples/lambda/barendregt/boehmScript.sml @@ -2,119 +2,54 @@ * boehmScript.sml: (Effective) Boehm Trees (Chapter 10 of [1]) * *---------------------------------------------------------------------------*) -open HolKernel boolLib Parse bossLib BasicProvers; +open HolKernel Parse boolLib bossLib; (* core theories *) open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils - finite_mapTheory; + finite_mapTheory topologyTheory listRangeTheory tautLib; open binderLib termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory head_reductionTheory standardisationTheory solvableTheory reductionEval; open basic_swapTheory horeductionTheory takahashiS3Theory; +open monadsyntax; +val _ = enable_monadsyntax (); +val _ = enable_monad "option"; + val _ = new_theory "boehm"; val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]; val o_DEF = combinTheory.o_DEF; + +val _ = hide "B"; +val _ = hide "C"; val _ = hide "Y"; (*---------------------------------------------------------------------------* - * ‘tpm’ as an equivalence relation between terms + * ltreeTheory extras *---------------------------------------------------------------------------*) -Definition tpm_rel_def : - tpm_rel M N = ?pi. tpm pi M = N -End - -Theorem tpm_rel_alt : - !M N. tpm_rel M N <=> ?pi. M = tpm pi N -Proof - rw [tpm_rel_def] - >> EQ_TAC >> rpt STRIP_TAC - >| [ (* goal 1 (of 2) *) - fs [tpm_eql] >> Q.EXISTS_TAC ‘REVERSE pi’ >> rw [], - (* goal 2 (of 2) *) - fs [tpm_eqr] >> Q.EXISTS_TAC ‘REVERSE pi’ >> rw [] ] -QED - -Theorem equivalence_tpm_rel : - equivalence tpm_rel -Proof - rw [equivalence_def, reflexive_def, symmetric_def, transitive_def] - >| [ (* goal 1 (of 3) *) - rw [tpm_rel_def] >> Q.EXISTS_TAC ‘[]’ >> rw [], - (* goal 2 (of 3) *) - rw [tpm_rel_def] >> EQ_TAC >> rpt STRIP_TAC >| (* 2 subgoals *) - [ (* goal 2.1 (of 2) *) - ONCE_REWRITE_TAC [EQ_SYM_EQ] >> fs [tpm_eql] \\ - Q.EXISTS_TAC ‘REVERSE pi’ >> rw [], - (* goal 2.2 (of 2) *) - ONCE_REWRITE_TAC [EQ_SYM_EQ] >> fs [tpm_eql] \\ - Q.EXISTS_TAC ‘REVERSE pi’ >> rw [] ], - (* goal 3 (of 3) *) - fs [tpm_rel_def] \\ - POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ - POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ - Q.EXISTS_TAC ‘pi' ++ pi’ \\ - rw [pmact_decompose] ] -QED - -val tpm_rel_thm = equivalence_tpm_rel |> - REWRITE_RULE [equivalence_def, reflexive_def, symmetric_def, transitive_def]; +(* ltree_subset A B <=> A results from B by "cutting off" some subtrees. Thus, -(* below are easy-to-use forms of [equivalence_tpm_rel] *) -Theorem tpm_rel_REFL[simp] : - tpm_rel M M -Proof - rw [tpm_rel_thm] -QED + 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) -Theorem tpm_rel_SYM : - !M N. tpm_rel M N ==> tpm_rel N M -Proof - rw [tpm_rel_thm] -QED - -Theorem tpm_rel_SYM_EQ : - !M N. tpm_rel M N <=> tpm_rel N M -Proof - rw [tpm_rel_thm] -QED - -Theorem tpm_rel_TRANS : - !M1 M2 M3. tpm_rel M1 M2 /\ tpm_rel M2 M3 ==> tpm_rel M1 M3 -Proof - rpt STRIP_TAC - >> MATCH_MP_TAC (cj 3 tpm_rel_thm) - >> Q.EXISTS_TAC ‘M2’ >> art [] -QED - -Theorem tpm_rel_tpm[simp] : - tpm_rel (tpm pi M) M /\ tpm_rel M (tpm pi M) -Proof - CONJ_ASM1_TAC - >- (REWRITE_TAC [tpm_rel_alt] \\ - Q.EXISTS_TAC ‘pi’ >> REWRITE_TAC []) - >> MATCH_MP_TAC tpm_rel_SYM >> art [] -QED - -Theorem tpm_rel_cong : - !M M' N N'. tpm_rel M M' /\ tpm_rel N N' ==> (tpm_rel M N <=> tpm_rel M' N') -Proof - rpt STRIP_TAC - >> EQ_TAC >> STRIP_TAC - >| [ (* goal 1 (of 2) *) - MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\ - MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘M’ >> art [] \\ - MATCH_MP_TAC tpm_rel_SYM >> art [], - (* goal 2 (of 2) *) - MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘M'’ >> art [] \\ - MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘N'’ >> art [] \\ - MATCH_MP_TAC tpm_rel_SYM >> art [] ] -QED + 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 (*---------------------------------------------------------------------------* * Canonical binding list of a term w.r.t. excluded variables @@ -162,7 +97,11 @@ QED such as ‘LAMl (vs ++ [z0;z1]) t’ (with two extra children ‘z0’ and ‘z1’) without changing the head variable (VAR y). *) -Type boehm_tree[pp] = “:(string list # string) option ltree” + +(* The type of each Boehm tree node (the type variable 'a of general ltree) *) +Type BT_node[pp] = “:(string list # string) option” + +Type boehm_tree[pp] = “:BT_node ltree” (* Definition 10.1.9 [1, p.221] (Effective Boehm Tree) @@ -228,8 +167,8 @@ End *) Overload bot = “Branch NONE (LNIL :boehm_tree llist)” -(* Another form of ‘bot’, usually returned by “THE (ltree_el A p)”. *) -Overload bot = “(NONE :(string list # string) option, SOME 0)” +(* Another form of ‘bot’, usually returned by “THE (ltree_el A p)” *) +Overload bot = “(NONE, SOME 0) :(BT_node # num option)” (* Unicode name: "base" *) val _ = Unicode.unicode_version {u = UTF8.chr 0x22A5, tmnm = "bot"}; @@ -458,6 +397,27 @@ Proof qunabbrev_tac ‘Q0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [] ] QED +Theorem BT_ltree_el_top : + !X M. ltree_el (BTe X M) [] = + if solvable M then + let + M0 = principle_hnf M; + n = LAMl_size M0; + vs = NEWS n (X UNION FV M0); + M1 = principle_hnf (M0 @* MAP VAR vs); + y = hnf_headvar M1; + Ms = hnf_children M1; + m = LENGTH Ms; + in + SOME (SOME (vs,y),SOME m) + else + SOME (NONE,SOME 0) +Proof + rw [BT_def, Once ltree_unfold, BT_generator_def, ltree_el_def] + (* one goal is left *) + >> simp [LMAP_fromList] +QED + (*---------------------------------------------------------------------------* * subterm *---------------------------------------------------------------------------*) @@ -476,7 +436,8 @@ QED *) Definition subterm_def : subterm X M [] = SOME (X,M :term) /\ - subterm X M (x::xs) = if solvable M then + subterm X M (x::xs) = + if solvable M then let M0 = principle_hnf M; n = LAMl_size M0; m = hnf_children_size M0; @@ -485,7 +446,7 @@ Definition subterm_def : Ms = hnf_children M1 in if x < m then subterm (X UNION set vs) (EL x Ms) xs else NONE - else + else NONE End @@ -528,7 +489,7 @@ QED definition of subterm can be greatly simplified. *) Theorem subterm_of_absfree_hnf : - !X M x xs. FINITE X /\ hnf M /\ ~is_abs M ==> + !X M x xs. hnf M /\ ~is_abs M ==> subterm X M (x::xs) = let m = hnf_children_size M; Ms = hnf_children M @@ -545,6 +506,18 @@ Proof >> gs [Abbr ‘Ms'’, Abbr ‘M1’, hnf_children_hnf] QED +Theorem subterm_of_absfree_hnf' : + subterm X (VAR y @* Ms) (x::xs) = + if x < LENGTH Ms then + subterm X (EL x Ms) xs + else + NONE +Proof + MP_TAC (Q.SPECL [‘X’, ‘VAR y @* Ms’, ‘x’, ‘xs’] + subterm_of_absfree_hnf) + >> rw [hnf_appstar, is_abs_appstar] +QED + (* NOTE: The uses of ‘subterm' X M p’ assumes ‘subterm X M p <> NONE’ *) Overload subterm' = “\X M p. SND (THE (subterm X M p))” @@ -624,12 +597,34 @@ Proof >> fs [ltree_paths_def] QED -(* Lemma 10.1.15 [1, p.222] *) -Theorem BT_subterm_thm_old[local] : - !p X M. p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> +(* ltree_lookup returns more information (the entire subtree), thus can be + used to construct the return value of ltree_el. + + NOTE: This theorem connects ‘ltree_el’ and ‘ltree_lookup’ for Boehm trees + + |- !p X M. + p IN ltree_paths (BTe X M) ==> + ltree_el (BTe X M) p = + do t' <- ltree_lookup (BTe X M) p; + SOME (ltree_node t',LLENGTH (ltree_children t')) + od + *) +Theorem BT_ltree_el_thm = + ltree_el_alt_ltree_lookup |> INST_TYPE [“:'a” |-> “:BT_node”] + |> Q.SPECL [‘p’, ‘BTe X M’] |> GEN_ALL + +(* Lemma 10.1.15 [1, p.222] (subterm and ltree_lookup) *) +Theorem BT_subterm_lemma : + !p X M. FINITE X /\ subterm X M p <> NONE ==> BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p) Proof - Induct_on ‘p’ + Suff ‘!p X M. p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> + BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p)’ + >- (rpt STRIP_TAC \\ + FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\ + MATCH_MP_TAC subterm_imp_ltree_paths >> art []) + (* now the old proof *) + >> Induct_on ‘p’ >- rw [subterm_def, ltree_lookup_def] >> rw [subterm_def, ltree_lookup] >> qabbrev_tac ‘M0 = principle_hnf M’ @@ -646,13 +641,76 @@ Proof >> rw [ltree_paths_def, ltree_lookup_def, LNTH_fromList, GSYM BT_def, EL_MAP] QED +Theorem subterm_finite_lemma : + !p X M Y N. FINITE X /\ subterm X M p = SOME (Y,N) ==> FINITE Y +Proof + Induct_on ‘p’ >- simp [] + >> rpt GEN_TAC + >> simp [subterm_def] + >> qabbrev_tac ‘M0 = principle_hnf M’ + >> qabbrev_tac ‘n = LAMl_size M0’ + >> qabbrev_tac ‘vs = NEWS n (X UNION FV M0)’ + >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’ + >> rpt STRIP_TAC + >> FIRST_X_ASSUM MATCH_MP_TAC + >> qexistsl_tac [‘X UNION set vs’, ‘EL h (hnf_children M1)’, ‘N’] + >> rw [] +QED + +(* Lemma 10.1.15 (related) [1, p.222] (subterm and ltree_el) + + Assuming all involved terms are solvable: + + - “ltree_el (BTe X M) p” returns ‘SOME (SOME (vs,y),SOME k)’ (ltree node), + - “subterm X M p” returns ‘(Z,N)’ where N is the actual subterm. + + Then M0 := principle_hnf N has the explicit form: ‘LAMl vs (VAR y @* Ms)’, + and ‘LENGTH Ms = k’ (NOTE: vs, y and k come from ‘ltree_el (BTe X M) p’. + + Needs: subterm_solvable_lemma, BT_subterm_lemma, BT_ltree_el_thm, + subterm_imp_ltree_paths, subterm_finite_lemma, etc. + *) Theorem BT_subterm_thm : - !p X M. FINITE X /\ subterm X M p <> NONE ==> - BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p) + !p X M. FINITE X /\ subterm X M p <> NONE /\ solvable (subterm' X M p) ==> + do (t,m) <- ltree_el (BTe X M) p; + (Z,N) <- subterm X M p; + (xs,y) <- t; + M0 <<- principle_hnf N; + n <<- LAMl_size M0; + vs <<- NEWS n (Z UNION FV M0); + M1 <<- principle_hnf (M0 @* MAP VAR vs); + return (vs = xs /\ hnf_headvar M1 = y /\ + hnf_children_size M1 = THE m) + od = SOME T Proof rpt STRIP_TAC - >> MATCH_MP_TAC BT_subterm_thm_old >> art [] - >> MATCH_MP_TAC subterm_imp_ltree_paths >> art [] + >> ‘p IN ltree_paths (BTe X M)’ by PROVE_TAC [subterm_imp_ltree_paths] + >> ‘ltree_lookup (BTe X M) p <> NONE’ by rw [GSYM ltree_lookup_valid] + >> Know ‘BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p)’ + >- (MATCH_MP_TAC BT_subterm_lemma >> art []) + >> gs [GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS] + >> Cases_on ‘x’ >> fs [] + >> rename1 ‘subterm X M p = SOME (Y,N)’ + >> rw [BT_ltree_el_thm] + >> Know ‘BTe Y N = ltree_unfold BT_generator (Y,N)’ >- rw [BT_def] + >> Rewr' + >> NTAC 2 (simp [Once ltree_unfold, BT_generator_def]) + >> simp [LMAP_fromList] +(* stage work *) + >> qabbrev_tac ‘N0 = principle_hnf N’ + >> qabbrev_tac ‘n = LAMl_size N0’ + >> qabbrev_tac ‘vs = NEWS n (Y UNION FV N0)’ + >> qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vs)’ + >> ‘FINITE Y’ by PROVE_TAC [subterm_finite_lemma] + >> Know ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (Y UNION FV N0) /\ LENGTH vs = n’ + >- rw [Abbr ‘vs’, NEWS_def] + >> DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [DISJOINT_UNION']) + >> qunabbrev_tac ‘N1’ + >> ‘hnf N0’ by rw [Abbr ‘N0’, hnf_principle_hnf'] + >> hnf_tac (“N0 :term”, “vs :string list”, + “N1 :term”, “y :string”, “args :term list”) + >> ‘TAKE n vs = vs’ by rw [TAKE_LENGTH_ID_rwt] + >> POP_ASSUM (rfs o wrap) QED (* NOTE: This proof shares a lot of tactics with [subterm_tpm_lemma] *) @@ -762,13 +820,12 @@ Proof >- (qunabbrev_tac ‘M1'’ \\ MATCH_MP_TAC principle_hnf_tpm >> art [] \\ REWRITE_TAC [has_hnf_thm] \\ - Q.EXISTS_TAC ‘(FEMPTY |++ ZIP (vs2,MAP VAR vs1p)) ' (VAR y @* args)’ \\ + Q.EXISTS_TAC ‘fromPairs vs2 (MAP VAR vs1p) ' (VAR y @* args)’ \\ CONJ_TAC >- (MATCH_MP_TAC hreduce_LAMl_appstar \\ rw [EVERY_MEM, MEM_MAP] >> rw [] \\ Q.PAT_X_ASSUM ‘DISJOINT (set vs2) (set vs1p)’ MP_TAC \\ rw [DISJOINT_ALT']) \\ - REWRITE_TAC [GSYM fromPairs_def] \\ ‘FDOM (fromPairs vs2 (MAP VAR vs1p)) = set vs2’ by rw [FDOM_fromPairs] \\ Cases_on ‘MEM y vs2’ >- (simp [ssub_thm, ssub_appstar, hnf_appstar] \\ @@ -915,7 +972,7 @@ QED ‘p NOTIN ltree_paths (BTe X M)’, the conclusion (rhs) always holds. *) Theorem subterm_is_none_iff_children : - !X M p. subterm X M p = NONE <=> !p'. p <<= p' ==> subterm X M p' = NONE + !X M p. subterm X M p = NONE <=> !q. p <<= q ==> subterm X M q = NONE Proof rpt GEN_TAC >> reverse EQ_TAC @@ -925,16 +982,16 @@ Proof >> Q.ID_SPEC_TAC ‘p’ >> Induct_on ‘p’ >- rw [subterm_NIL] >> rw [subterm_def] - >> Cases_on ‘p'’ >> fs [subterm_def] + >> Cases_on ‘q’ >> fs [subterm_def] QED Theorem subterm_solvable_lemma : - !X M p. FINITE X /\ p <> [] /\ - p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> + !X M p. FINITE X /\ p <> [] /\ subterm X M p <> NONE ==> (!q. q <<= p ==> subterm X M q <> NONE) /\ (!q. q <<= FRONT p ==> solvable (subterm' X M q)) Proof rpt GEN_TAC >> STRIP_TAC + >> ‘p IN ltree_paths (BTe X M)’ by PROVE_TAC [subterm_imp_ltree_paths] >> CONJ_ASM1_TAC >- (Q.X_GEN_TAC ‘q’ >> DISCH_TAC \\ CCONTR_TAC \\ @@ -1211,12 +1268,12 @@ Proof >- (‘unsolvable (tpm pi M)’ by PROVE_TAC [solvable_tpm] \\ simp [subterm_def]) >> ‘solvable (tpm pi M)’ by PROVE_TAC [solvable_tpm] - (* BEGIN Michael Norrish's tactics *) + (* BEGIN Norrish's advanced tactics *) >> CONV_TAC (UNBETA_CONV “subterm X M (h::p)”) >> qmatch_abbrev_tac ‘P _’ >> RW_TAC bool_ss [subterm_of_solvables] >> simp [Abbr ‘P’] - (* END Michael Norrish's tactics. + (* END Norrish's advanced tactics. preparing for expanding ‘subterm' Y (tpm pi M) (h::p)’ *) >> qabbrev_tac ‘M0' = principle_hnf (tpm pi M)’ >> Know ‘M0' = tpm pi M0’ @@ -1234,12 +1291,12 @@ Proof >- (rw [] >> rw [subterm_of_solvables]) (* stage work, now h < m *) >> simp [] (* eliminate ‘h < m’ in the goal *) - (* BEGIN Michael Norrish's tactics, again *) + (* BEGIN Norrish's advanced tactics, again *) >> CONV_TAC (UNBETA_CONV “subterm Y (tpm pi M) (h::p)”) >> qmatch_abbrev_tac ‘P _’ >> RW_TAC bool_ss [subterm_of_solvables] >> simp [Abbr ‘P’] - (* END Michael Norrish's tactics. *) + (* END Norrish's advanced tactics. *) >> Q.PAT_X_ASSUM ‘tpm pi M0 = principle_hnf (tpm pi M)’ (rfs o wrap o SYM) >> Q.PAT_X_ASSUM ‘n = n'’ (fs o wrap o SYM) >> Q.PAT_X_ASSUM ‘n = n''’ (fs o wrap o SYM) @@ -1323,13 +1380,12 @@ Proof >- (qunabbrev_tac ‘M1'’ \\ MATCH_MP_TAC principle_hnf_tpm >> art [] \\ REWRITE_TAC [has_hnf_thm] \\ - Q.EXISTS_TAC ‘(FEMPTY |++ ZIP (vs2,MAP VAR vs1p)) ' (VAR y @* args)’ \\ + Q.EXISTS_TAC ‘fromPairs vs2 (MAP VAR vs1p) ' (VAR y @* args)’ \\ CONJ_TAC >- (MATCH_MP_TAC hreduce_LAMl_appstar \\ rw [EVERY_MEM, MEM_MAP] >> rw [] \\ Q.PAT_X_ASSUM ‘DISJOINT (set vs2) (set vs1p)’ MP_TAC \\ rw [DISJOINT_ALT']) \\ - REWRITE_TAC [GSYM fromPairs_def] \\ ‘FDOM (fromPairs vs2 (MAP VAR vs1p)) = set vs2’ by rw [FDOM_fromPairs] \\ Cases_on ‘MEM y vs2’ >- (simp [ssub_thm, ssub_appstar, hnf_appstar] \\ @@ -1452,6 +1508,16 @@ Definition equivalent_def : ~solvable M /\ ~solvable N End +Theorem equivalent_reflexive : + reflexive equivalent +Proof + rw [reflexive_def, equivalent_def] +QED + +(* |- !x. equivalent x x *) +Theorem equivalent_refl[simp] = + REWRITE_RULE [reflexive_def] equivalent_reflexive + Theorem equivalent_symmetric : symmetric equivalent Proof @@ -1843,6 +1909,12 @@ Proof >> rw [APPEND_SNOC] QED +Theorem Boehm_apply_SNOC_SUB : + !(N :term) v p M. apply (SNOC [N/v] p) M = apply p ([N/v] M) +Proof + rw [apply_def, FOLDR_SNOC] +QED + Theorem Boehm_apply_MAP_rightctxt : !Ns t. apply (MAP rightctxt Ns) t = t @* (REVERSE Ns) Proof @@ -1915,14 +1987,7 @@ Proof >> reverse EQ_TAC >- (rw [is_ready_def] >- art [] \\ DISJ2_TAC >> Q.EXISTS_TAC ‘VAR y @* Ns’ >> art [] \\ - CONJ_ASM1_TAC >- (rw [hnf_appstar]) >> simp [] \\ - RW_TAC std_ss [head_original_def, LAMl_size_hnf_absfree] \\ - qunabbrev_tac ‘n’ \\ - ‘vs = []’ by METIS_TAC [LENGTH_NIL, NEWS_def, FINITE_FV] \\ - POP_ASSUM (fs o wrap) >> qunabbrev_tac ‘vs’ \\ - ‘M1 = VAR y @* Ns’ by rw [principle_hnf_reduce, Abbr ‘M1’] \\ - POP_ORW >> qunabbrev_tac ‘M1’ \\ - simp [hnf_head_hnf, hnf_children_hnf]) + rw [head_original_def, hnf_appstar]) (* stage work *) >> rw [is_ready_def] >- art [] >> DISJ2_TAC @@ -2095,12 +2160,12 @@ Proof >> DISCH_TAC >> Know ‘subterm X M (h::l) <> NONE’ >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw []) - (* BEGIN Michael Norrish's tactics *) + (* BEGIN Norrish's advanced tactics *) >> CONV_TAC (UNBETA_CONV “subterm X M (h::l)”) >> qmatch_abbrev_tac ‘f _’ >> RW_TAC bool_ss [subterm_of_solvables] >> simp [Abbr ‘f’] - (* END Michael Norrish's tactics. *) + (* END Norrish's advanced tactics. *) >> STRIP_TAC (* getting explicit representation of M0 *) >> Know ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (X UNION FV M0) /\ LENGTH vs = n’ @@ -2184,7 +2249,7 @@ Proof ‘FRONT (h::t) <> []’ by rw [] \\ Know ‘h::p' <<= FRONT (h::t)’ >- (simp [] >> Cases_on ‘t’ >> fs []) >> Rewr \\ - (* Michael Norrish's tactics *) + (* Norrish's advanced tactics *) CONV_TAC (UNBETA_CONV “subterm X M (h::p')”) \\ qmatch_abbrev_tac ‘f _’ \\ RW_TAC bool_ss [subterm_of_solvables] \\ @@ -2314,7 +2379,7 @@ Proof >> CONV_TAC (UNBETA_CONV “subterm X ([P/v] M) (h::l)”) >> qmatch_abbrev_tac ‘f _’ >> ASM_SIMP_TAC std_ss [subterm_of_solvables] - >> LET_ELIM_TAC + >> BasicProvers.LET_ELIM_TAC >> Q.PAT_X_ASSUM ‘subterm _ (EL h (hnf_children M1)) l <> NONE’ MP_TAC >> simp [Abbr ‘f’, hnf_children_hnf] >> DISCH_TAC (* subterm (X UNION set vs) (EL h args) l <> NONE *) @@ -2449,13 +2514,12 @@ Proof (* applying hreduce_LAMl_appstar *) >> qabbrev_tac ‘xs' = SNOC z xs’ >> qabbrev_tac ‘t' = VAR z @* args' @* MAP VAR xs’ - >> Know ‘LAMl xs' t' @* MAP VAR ys -h->* (FEMPTY |++ ZIP (xs',MAP VAR ys)) ' t'’ + >> Know ‘LAMl xs' t' @* MAP VAR ys -h->* fromPairs xs' (MAP VAR ys) ' t'’ >- (MATCH_MP_TAC hreduce_LAMl_appstar >> simp [Abbr ‘xs'’] \\ rw [EVERY_MEM, MEM_MAP] >> REWRITE_TAC [FV_thm] \\ MATCH_MP_TAC DISJOINT_SUBSET' \\ Q.EXISTS_TAC ‘set ys’ >> art [] \\ rw [SUBSET_DEF]) - >> REWRITE_TAC [GSYM fromPairs_def] >> ‘FDOM (fromPairs xs' (MAP VAR ys)) = set xs'’ by rw [FDOM_fromPairs, Abbr ‘xs'’] >> ASM_SIMP_TAC std_ss [Abbr ‘t'’, ssub_appstar, Abbr ‘xs'’] @@ -2584,7 +2648,7 @@ Proof Q.EXISTS_TAC ‘FRONT l’ >> rw [] \\ MATCH_MP_TAC IS_PREFIX_FRONT_MONO >> rw []) >> Rewr - (* Michael Norrish's tactics *) + (* Norrish's advanced tactics *) >> CONV_TAC (UNBETA_CONV “subterm X M (h::p')”) >> qmatch_abbrev_tac ‘f _’ >> RW_TAC bool_ss [subterm_of_solvables] @@ -2650,15 +2714,17 @@ QED NOTE4: Added ‘p IN ltree_paths (BTe X (apply pi M))’ into conclusions for the needs in the user theorem. + + NOTE5: Extended the conclusion with ‘!q. q <<= p’ *) Theorem Boehm_transform_exists_lemma : !X M p. FINITE X /\ p <> [] /\ subterm X M p <> NONE ==> - ?pi. Boehm_transform pi /\ - solvable (apply pi M) /\ is_ready (apply pi M) /\ - ?Z v P. Z = X UNION FV M /\ closed P /\ - subterm Z (apply pi M) p <> NONE /\ - tpm_rel (subterm' Z (apply pi M) p) - ([P/v] (subterm' Z M p)) + ?pi. Boehm_transform pi /\ + solvable (apply pi M) /\ is_ready (apply pi M) /\ + ?Z v P. Z = X UNION FV M /\ closed P /\ + !q. q <> [] /\ q <<= p ==> + subterm Z (apply pi M) q <> NONE /\ + tpm_rel (subterm' Z (apply pi M) q) ([P/v] (subterm' Z M q)) Proof rpt STRIP_TAC >> ‘p IN ltree_paths (BTe X M)’ by PROVE_TAC [subterm_imp_ltree_paths] @@ -2681,7 +2747,6 @@ Proof >- (rw [Abbr ‘vs’, NEWS_def]) >> DISCH_THEN (STRIP_ASSUME_TAC o (REWRITE_RULE [DISJOINT_UNION'])) (* applying the shared hnf_tac to decompose M0 *) - >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR (TAKE n vs))’ >> Know ‘?y args. M0 = LAMl (TAKE n vs) (VAR y @* args)’ >- (qunabbrev_tac ‘n’ >> irule (iffLR hnf_cases_shared) >> rw [] \\ MATCH_MP_TAC DISJOINT_SUBSET \\ @@ -2691,6 +2756,7 @@ Proof (* eliminate ‘TAKE n vs’ *) >> ‘TAKE n vs = vs’ by rw [] >> POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap) + >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’ >> Know ‘M1 = VAR y @* args’ >- (qunabbrev_tac ‘M1’ >> POP_ORW \\ MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar]) @@ -2768,7 +2834,8 @@ Proof >> ‘Boehm_transform p3’ by rw [Abbr ‘p3’, MAP_MAP_o, GSYM MAP_REVERSE] (* applying permutator_thm *) >> Know ‘apply p3 (P @* args') == VAR b @* args' @* MAP VAR as’ - >- (simp [Abbr ‘p3’, Abbr ‘P’, rightctxt_thm, MAP_SNOC, Boehm_apply_MAP_rightctxt'] \\ + >- (simp [Abbr ‘p3’, Abbr ‘P’, rightctxt_thm, MAP_SNOC, + Boehm_apply_MAP_rightctxt'] \\ REWRITE_TAC [GSYM appstar_APPEND, APPEND_ASSOC] \\ MATCH_MP_TAC permutator_thm >> rw []) >> DISCH_TAC @@ -2797,18 +2864,17 @@ Proof >> DISCH_TAC (* stage work *) >> Know ‘principle_hnf (apply (p3 ++ p2 ++ p1) M) = VAR b @* args' @* MAP VAR as’ - >- (Q.PAT_X_ASSUM ‘apply (p3 ++ p2 ++ p1) M == _’ MP_TAC \\ - simp [Boehm_apply_APPEND] \\ - Q.PAT_X_ASSUM ‘Boehm_transform (p3 ++ p2 ++ p1)’ K_TAC \\ - Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC \\ - simp [Abbr ‘p1’, Boehm_apply_MAP_rightctxt'] \\ - Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC \\ - simp [Abbr ‘p2’] \\ - Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC \\ - Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\ - simp [Abbr ‘p3’, Boehm_apply_MAP_rightctxt'] \\ + >- (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 \\ + (* 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’, + 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))’ >- (simp [appstar_SUB] \\ @@ -2836,8 +2902,8 @@ Proof >- (MATCH_MP_TAC lemma14b >> fs [MEM_SNOC]) >> Rewr' \\ simp [Abbr ‘P’, GSYM appstar_APPEND] \\ MATCH_MP_TAC principle_hnf_permutator >> rw []) >> Rewr' \\ - (* applying principle_hnf_substitutive *) - MATCH_MP_TAC principle_hnf_substitutive \\ + (* applying principle_hnf_SUB_cong *) + MATCH_MP_TAC principle_hnf_SUB_cong \\ CONJ_TAC (* has_hnf #1 *) >- (simp [GSYM solvable_iff_has_hnf, GSYM appstar_APPEND] \\ ‘M0 == M’ by rw [lameq_principle_hnf', Abbr ‘M0’] \\ @@ -2925,21 +2991,24 @@ Proof FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\ rw [SUBSET_DEF, IN_BIGUNION_IMAGE] \\ Q.EXISTS_TAC ‘e’ >> art []) - (* NOTE: for rewriting M to M0 in the goal, Z can be anything. *) + (* stage work, there's the textbook choice *) + >> qexistsl_tac [‘y’, ‘P’] >> art [] + >> NTAC 2 STRIP_TAC (* push ‘q <<= p’ to assumptions *) + (* NOTE: for rewriting M to M0 in the goal, Y can be anything. *) >> Q.ABBREV_TAC ‘Y = X UNION FV M’ >> ‘FINITE Y’ by rw [Abbr ‘Y’] (* RHS rewriting from M to M0 *) - >> Know ‘subterm Y M0 p = subterm Y M p’ + >> Know ‘subterm Y M0 q = subterm Y M q’ >- (qunabbrev_tac ‘M0’ \\ MATCH_MP_TAC subterm_of_principle_hnf >> art []) >> DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) (* LHS rewriting from M to M0 *) - >> Know ‘subterm Y (apply (p3 ++ p2 ++ p1) M) p = - subterm Y (VAR b @* args' @* MAP VAR as) p’ + >> Know ‘subterm Y (apply (p3 ++ p2 ++ p1) M) q = + subterm Y (VAR b @* args' @* MAP VAR as) q’ >- (Q.PAT_X_ASSUM ‘_ = VAR b @* args' @* MAP VAR as’ (ONCE_REWRITE_TAC o wrap o SYM) \\ qabbrev_tac ‘t = apply (p3 ++ p2 ++ p1) M’ \\ - Suff ‘subterm Y (principle_hnf t) p = subterm Y t p’ >- rw [] \\ + Suff ‘subterm Y (principle_hnf t) q = subterm Y t q’ >- rw [] \\ MATCH_MP_TAC subterm_of_principle_hnf >> art []) >> Rewr' (* stage cleanups *) @@ -2948,9 +3017,12 @@ Proof >> Q.PAT_X_ASSUM ‘apply (p3 ++ p2 ++ p1) M == _’ K_TAC >> Q.PAT_X_ASSUM ‘Boehm_transform (p3 ++ p2 ++ p1)’ K_TAC (* stage work, now ‘M’ is eliminated from both sides! *) - >> Cases_on ‘p’ >- FULL_SIMP_TAC std_ss [] + >> Cases_on ‘q’ >- FULL_SIMP_TAC std_ss [] >> Know ‘h < m’ - >- (Q.PAT_X_ASSUM ‘subterm X M (h::t) <> NONE’ MP_TAC \\ + >- (Cases_on ‘p’ >> fs [] \\ + Q.PAT_X_ASSUM ‘h = h'’ (fs o wrap o SYM) \\ + Know ‘subterm X M (h::t) <> NONE’ + >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw []) \\ RW_TAC std_ss [subterm_of_solvables] >> fs []) >> DISCH_TAC (* applying subterm_of_absfree_hnf *) @@ -3027,9 +3099,6 @@ Proof qunabbrev_tac ‘M0’ \\ MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art []) >> DISCH_TAC - (* stage work, there's the textbook choice *) - >> qexistsl_tac [‘y’, ‘P’] >> art [] - >> REWRITE_TAC [GSYM SUB_ISUB_SINGLETON] (* preparing for subterm_subst_cong *) >> Suff ‘subterm Z ([P/y] N) t <> NONE /\ tpm_rel (subterm' Z ([P/y] N) t) ([P/y] (subterm' Z N t))’ @@ -3051,7 +3120,9 @@ Proof to convert ‘subterm X M (h::t) <> NONE’ to ‘subterm Z M (h::t) <> NONE’. *) >> Know ‘t IN ltree_paths (BTe Z N)’ - >- (Q.PAT_X_ASSUM ‘h::t IN ltree_paths (BTe X M)’ MP_TAC \\ + >- (Know ‘h::t IN ltree_paths (BTe X M)’ + >- (MATCH_MP_TAC ltree_paths_inclusive \\ + Q.EXISTS_TAC ‘p’ >> art []) \\ ‘ltree_paths (BTe X M) = ltree_paths (BTe Y M)’ by PROVE_TAC [BT_ltree_paths_cong] >> POP_ORW \\ simp [ltree_paths_def, ltree_lookup] \\ @@ -3066,7 +3137,8 @@ Proof >> DISCH_TAC (* stage work *) >> CONJ_ASM1_TAC (* subterm Z N t <> NONE *) - >- (Q.PAT_X_ASSUM ‘subterm X M (h::t) <> NONE’ MP_TAC \\ + >- (Know ‘subterm X M (h::t) <> NONE’ + >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\ ‘subterm X M (h::t) <> NONE <=> subterm Y M (h::t) <> NONE’ by PROVE_TAC [subterm_tpm_cong] >> POP_ORW \\ Q.PAT_X_ASSUM ‘M0 = _’ K_TAC \\ @@ -3078,23 +3150,19 @@ Proof (* final goal: subterm_width (EL h args) t <= d *) >> qunabbrev_tac ‘d’ (* applying subterm_width_alt *) - >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘h::t’] subterm_width_alt) + >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’] subterm_width_alt) >> simp [] >> DISCH_THEN K_TAC - >> qabbrev_tac ‘p = h::t’ >> Know ‘IMAGE (hnf_children_size o principle_hnf) {subterm' X M p' | p' <<= FRONT p} = {hnf_children_size (principle_hnf (subterm' X M p')) | p' <<= FRONT p}’ >- (rw [Once EXTENSION] \\ EQ_TAC >> rw [] >| (* 2 subgoals *) [ (* goal 1 (of 2) *) - rename1 ‘q <<= FRONT p’ \\ - Q.EXISTS_TAC ‘q’ >> rw [], + Q.EXISTS_TAC ‘p'’ >> rw [], (* goal 2 (of 2) *) - rename1 ‘q <<= FRONT p’ \\ - Q.EXISTS_TAC ‘subterm' X M q’ >> art [] \\ - Q.EXISTS_TAC ‘q’ >> art [] ]) + Q.EXISTS_TAC ‘subterm' X M p'’ >> art [] \\ + Q.EXISTS_TAC ‘p'’ >> art [] ]) >> Rewr' - >> qunabbrev_tac ‘p’ >> Cases_on ‘t = []’ >- rw [] (* applying subterm_width_alt again *) >> MP_TAC (Q.SPECL [‘Z’, ‘N’, ‘t’] subterm_width_alt) @@ -3109,19 +3177,23 @@ Proof MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix]) >> CONJ_TAC >- (‘{hnf_children_size (principle_hnf (subterm' X M p')) | - p' <<= FRONT (h::t)} = + p' <<= FRONT p} = IMAGE (\p'. hnf_children_size (principle_hnf (subterm' X M p'))) - {p' | p' <<= FRONT (h::t)}’ + {p' | p' <<= FRONT p}’ by rw [Once EXTENSION] >> POP_ORW \\ MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix]) >> ‘hnf_children_size M0 = m’ by rw [Abbr ‘m’] >> Q.PAT_X_ASSUM ‘M0 = _’ K_TAC >> rw [SUBSET_DEF] (* this asserts ‘p' <<= FRONT t’ *) >> Q.EXISTS_TAC ‘h::p'’ - >> ‘FRONT (h::t) <> []’ by rw [] - >> Know ‘h::p' <<= FRONT (h::t)’ - >- (simp [] >> Cases_on ‘t’ >> fs []) - >> Rewr + >> ONCE_REWRITE_TAC [CONJ_COMM] + >> STRONG_CONJ_TAC + >- (Cases_on ‘p’ >> fs [] \\ + Cases_on ‘t'’ >> fs [] \\ + MATCH_MP_TAC IS_PREFIX_TRANS \\ + Q.EXISTS_TAC ‘FRONT t’ >> art [] \\ + MATCH_MP_TAC IS_PREFIX_FRONT_MONO >> rw []) + >> DISCH_TAC >> Suff ‘hnf_children_size (principle_hnf (subterm' X M (h::p'))) = hnf_children_size (principle_hnf (subterm' Y M (h::p')))’ >- (Rewr' \\ @@ -3140,33 +3212,40 @@ Proof >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [] \\ Cases_on ‘t’ >> fs []) (* final goal: subterm X M (h::p') <> NONE *) - >> FIRST_X_ASSUM MATCH_MP_TAC >> rw [] + >> FIRST_X_ASSUM MATCH_MP_TAC >> MATCH_MP_TAC IS_PREFIX_TRANS - >> Q.EXISTS_TAC ‘FRONT t’ >> art [] + >> Q.EXISTS_TAC ‘FRONT p’ >> art [] >> MATCH_MP_TAC IS_PREFIX_BUTLAST' >> art [] QED -(* Another version with ‘tpm_rel’ but with ‘ISUB’ +(* Another version with ‘ISUB’ instead of ‘tpm_rel’ NOTE: there's also ‘p IN ltree_paths (BTe Z (apply pi M))’ added into the conclusion, which has to be proved. *) Theorem Boehm_transform_exists_lemma' : !X M p. FINITE X /\ p <> [] /\ subterm X M p <> NONE ==> - ?pi. Boehm_transform pi /\ - solvable (apply pi M) /\ is_ready (apply pi M) /\ - ?Z ss. Z = X UNION FV M /\ - subterm Z (apply pi M) p <> NONE /\ - p IN ltree_paths (BTe Z (apply pi M)) /\ - subterm' Z (apply pi M) p = (subterm' Z M p) ISUB ss + ?pi Z. Boehm_transform pi /\ + solvable (apply pi M) /\ is_ready (apply pi M) /\ + Z = X UNION FV M /\ + !q. q <<= p /\ q <> [] ==> + subterm Z (apply pi M) q <> NONE /\ + q IN ltree_paths (BTe Z (apply pi M)) /\ + ?ss. subterm' Z (apply pi M) q = (subterm' Z M q) ISUB ss Proof rpt STRIP_TAC >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’] Boehm_transform_exists_lemma) >> RW_TAC std_ss [] - >> Q.EXISTS_TAC ‘pi’ >> rw [] + >> Q.EXISTS_TAC ‘pi’ + >> RW_TAC std_ss [] + >- (qabbrev_tac ‘N = apply pi M’ \\ + qabbrev_tac ‘Z = X UNION FV M’ \\ + MATCH_MP_TAC subterm_imp_ltree_paths >> rw [Abbr ‘Z’]) + >> Q.PAT_X_ASSUM ‘!q. q <> [] /\ q <<= p ==> _’ (MP_TAC o (Q.SPEC ‘q’)) + >> RW_TAC std_ss [] >> POP_ASSUM MP_TAC (* tpm_rel ... *) - >> qabbrev_tac ‘t = [P/v] (subterm' (X UNION FV M) M p)’ - >> rw [tpm_rel_alt] + >> qabbrev_tac ‘t = [P/v] (subterm' (X UNION FV M) M q)’ + >> RW_TAC std_ss [tpm_rel_alt] >> POP_ORW (* applying tpm_ISUB_exists *) >> STRIP_ASSUME_TAC (Q.SPECL [‘pi'’, ‘t’] tpm_ISUB_exists) @@ -3174,22 +3253,33 @@ Proof >> qunabbrev_tac ‘t’ >> Q.EXISTS_TAC ‘[(P,v)] ++ ss’ >> rw [GSYM ISUB_APPEND] - (* final goal: p IN ltree_paths (BTe (X UNION FV M) (apply pi M)) *) - >> qabbrev_tac ‘N = apply pi M’ - >> qabbrev_tac ‘Z = X UNION FV M’ - >> MATCH_MP_TAC subterm_imp_ltree_paths >> art [] - >> rw [Abbr ‘Z’] QED (* Proposition 10.3.7 (i) [1, p.248] (Boehm out lemma) NOTE: this time the case ‘p = []’ is included, but it's a trvial case. + + NOTE2: The original lemma in textbook requires ‘p IN ltree_paths (BTe X M)’, + 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). + + NOTE3: This theorem doesn't use the feature of Boehm_transform_exists_lemma + with generalizations: ‘!q. q <<= p /\ q <> [] ==> _’. *) -Theorem Boehm_out_lemma_old[local] : - !p X M. FINITE X /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> +Theorem Boehm_out_lemma : + !p X M. FINITE X /\ subterm X M p <> NONE ==> ?pi ss. Boehm_transform pi /\ apply pi M == subterm' X M p ISUB ss Proof - Induct_on ‘p’ + Suff ‘!p X M. FINITE X /\ p IN ltree_paths (BTe X M) /\ + subterm X M p <> NONE ==> + ?pi ss. Boehm_transform pi /\ + apply pi M == subterm' X M p ISUB ss’ + >- (rpt STRIP_TAC \\ + FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\ + MATCH_MP_TAC subterm_imp_ltree_paths >> art []) + (* now the old proof *) + >> Induct_on ‘p’ >- (rw [] >> qexistsl_tac [‘[]’, ‘[]’] >> rw []) >> rpt STRIP_TAC >> rename1 ‘subterm X M (h::t) <> NONE’ @@ -3200,6 +3290,8 @@ Proof by METIS_TAC [subterm_solvable_lemma] >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘h::t’] Boehm_transform_exists_lemma') >> rw [] (* this asserts pi and [P/v] *) + >> POP_ASSUM (MP_TAC o (Q.SPEC ‘p’)) + >> rw [] >> rename1 ‘Boehm_transform p0’ >> qabbrev_tac ‘Z = X UNION FV M’ (* Z is now unique *) >> ‘FINITE Z’ by rw [Abbr ‘Z’] diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 9b383a7bd2..5d532e5e58 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -1197,6 +1197,80 @@ QED (* |- !n. FV (permutator n) = {} *) Theorem FV_permutator[simp] = REWRITE_RULE [closed_def] closed_permutator +(* NOTE: the default permutator binding variables can be exchanged to another + fresh list excluding any given set X. + *) +Theorem permutator_cases : + !X n. FINITE X ==> + ?vs v. LENGTH vs = n /\ ALL_DISTINCT (SNOC v vs) /\ + DISJOINT X (set (SNOC v vs)) /\ + permutator n = LAMl vs (LAM v (VAR v @* MAP VAR vs)) +Proof + RW_TAC std_ss [permutator_def] + >> qabbrev_tac ‘Z = GENLIST n2s (n + 1)’ + >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’ + by (rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST]) + >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] + >> qabbrev_tac ‘z = LAST Z’ + >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL] + >> qabbrev_tac ‘M = VAR z @* MAP VAR (FRONT Z)’ + (* preparing for LAMl_ALPHA_ssub *) + >> qabbrev_tac ‘Y = NEWS (n + 1) (set Z UNION X)’ + >> ‘FINITE (set Z UNION X)’ by rw [] + >> ‘ALL_DISTINCT Y /\ DISJOINT (set Y) (set Z UNION X) /\ + LENGTH Y = n + 1’ by rw [NEWS_def, Abbr ‘Y’] + >> fs [] + >> Know ‘LAMl Z M = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' M)’ + >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\ + Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\ + rw [Abbr ‘M’, FV_appstar] \\ + ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\ + POP_ORW \\ + simp [LIST_TO_SET_SNOC] \\ + rw [Once EXTENSION, MEM_MAP]) + >> 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 = LAST Y’ + (* postfix for LAMl_ALPHA_ssub *) + >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’ + by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW + >> REWRITE_TAC [LAMl_SNOC] + >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’ + >- (simp [Abbr ‘M’, ssub_appstar] \\ + Know ‘fm ' z = VAR y’ + >- (rw [Abbr ‘fm’, Abbr ‘z’, LAST_EL] \\ + Know ‘fromPairs Z (MAP VAR Y) ' (EL (PRE (n + 1)) Z) = + EL (PRE (n + 1)) (MAP VAR Y)’ + >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\ + rw [EL_MAP, Abbr ‘y’, LAST_EL]) >> Rewr' \\ + Suff ‘MAP ($' fm) (MAP VAR (FRONT Z)) = MAP VAR (FRONT Y)’ >- rw [] \\ + rw [LIST_EQ_REWRITE, LENGTH_FRONT] \\ + ‘PRE (n + 1) = n’ by rw [] >> POP_ASSUM (fs o wrap) \\ + rename1 ‘i < n’ \\ + simp [EL_MAP, LENGTH_FRONT] \\ + Know ‘MEM (EL i (FRONT Z)) Z’ + >- (rw [MEM_EL] \\ + Q.EXISTS_TAC ‘i’ >> rw [] \\ + MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) \\ + rw [Abbr ‘fm’] \\ + Know ‘EL i (FRONT Z) = EL i Z’ + >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\ + Know ‘EL i (FRONT Y) = EL i Y’ + >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\ + 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]) + >> Rewr' + >> qexistsl_tac [‘FRONT Y’, ‘y’] + >> rw [LENGTH_FRONT, ALL_DISTINCT_SNOC, SNOC_LAST_FRONT, Abbr ‘y’, ALL_DISTINCT_FRONT] + >> Know ‘ALL_DISTINCT (SNOC (LAST Y) (FRONT Y))’ + >- (rw [SNOC_LAST_FRONT]) + >> rw [ALL_DISTINCT_SNOC] +QED + Theorem permutator_thm : !n N Ns. LENGTH Ns = n ==> permutator n @* Ns @@ N == N @* Ns Proof diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml index cae85908dd..58c1371c06 100644 --- a/examples/lambda/barendregt/head_reductionScript.sml +++ b/examples/lambda/barendregt/head_reductionScript.sml @@ -6,7 +6,7 @@ open HolKernel Parse boolLib bossLib BasicProvers; open boolSimps relationTheory pred_setTheory listTheory finite_mapTheory arithmeticTheory llistTheory pathTheory optionTheory rich_listTheory - hurdUtils; + hurdUtils pairTheory; open termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory binderLib horeductionTheory term_posnsTheory finite_developmentsTheory @@ -14,7 +14,8 @@ open termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory binderLib val _ = new_theory "head_reduction" -val _ = ParseExtras.temp_loose_equality() +(* val _ = ParseExtras.temp_loose_equality() *) +val _ = hide "Y"; Inductive hreduce1 : [~BETA:] @@ -31,6 +32,13 @@ val _ = overload_on ("-h->", ``hreduce1``) val _ = set_fixity "-h->*" (Infix(NONASSOC, 450)) val _ = overload_on ("-h->*", ``hreduce1^*``) +Theorem hreduce1_beta_reduce[simp] : + LAM h M @@ VAR h -h-> M +Proof + MP_TAC (Q.SPECL [‘h’, ‘M’, ‘VAR h’] hreduce1_BETA) + >> REWRITE_TAC [lemma14a] +QED + Theorem hreduce_TRANS : !M0 M1 M2. M0 -h->* M1 /\ M1 -h->* M2 ==> M0 -h->* M2 Proof @@ -140,7 +148,7 @@ val hreduce1_unique = store_thm( HO_MATCH_MP_TAC hreduce1_ind THEN SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]); -Theorem hreduce1_rules_appstar : +Theorem hreduce1_appstar : !Ns. M1 -h-> M2 /\ ~is_abs M1 ==> M1 @* Ns -h-> M2 @* Ns Proof Induct_on ‘Ns’ using SNOC_INDUCT @@ -159,7 +167,7 @@ Proof >> Q.EXISTS_TAC ‘[VAR h/h] M @* MAP VAR vs @* MAP VAR l’ >> reverse CONJ_TAC >- rw [Abbr ‘M’] >> REWRITE_TAC [GSYM appstar_APPEND] - >> MATCH_MP_TAC hreduce1_rules_appstar + >> MATCH_MP_TAC hreduce1_appstar >> rw [hreduce1_BETA] QED @@ -218,9 +226,19 @@ QED (* NOTE: Initially M1 is an APP, eventually it may become a VAR, never be LAM - The antecedent ‘!M. M1 -h->* M /\ M -h-> M2 ==> ~is_abs M’ says that - only head reductions between M1 and M2 (excluded) must not be abstractions, - i.e. starting from M2 it can be abstractions. + The condition ‘!M. M1 -h->* M /\ M -h-> M2 ==> ~is_abs M’ cannot be further + reduced. It says that all head reductions between M1 and M2 (excluded) must + not be abstractions. Only starting from M2 it can be abstractions. + + NOTE2: for ‘!M. M1 -h->* M /\ M -h-> M2 ==> ~is_abs M’ to hold, ‘M1’ usually + must be solvable (i.e. having finite head reduction path). If this is NOT the + case, then there may be an infinite head reduction path such that + + M1 -h-> M -h-> ... -h-> M2 -h-> ... -h-> M2 + + which indicates ‘~is_abs M2’ (see also [hreduce_rules_appstar']). + + NOTE3: note that there's no requirements on ‘Ns’, which can be anything. *) Theorem hreduce_rules_appstar : !M1 M2 Ns. ~is_abs M1 /\ (!M. M1 -h->* M /\ M -h-> M2 ==> ~is_abs M) /\ @@ -236,7 +254,7 @@ Proof >> rw [Once RTC_CASES2] >> DISJ2_TAC >> Q.EXISTS_TAC ‘M2 @* Ns’ >> reverse CONJ_TAC - >- (MATCH_MP_TAC hreduce1_rules_appstar >> art [] \\ + >- (MATCH_MP_TAC hreduce1_appstar >> art [] \\ FIRST_X_ASSUM MATCH_MP_TAC >> art []) >> FIRST_X_ASSUM irule >> rw [] >> CCONTR_TAC >> fs [] @@ -331,6 +349,17 @@ Proof rw [substitutive_def, hreduce_substitutive] QED +(* hreduce and ISUB *) +Theorem hreduce_ISUB : + !sub M N. M -h->* N ==> M ISUB sub -h->* N ISUB sub +Proof + Induct_on ‘sub’ >- rw [] + >> SIMP_TAC std_ss [FORALL_PROD, ISUB_def] + >> rpt STRIP_TAC + >> FIRST_X_ASSUM MATCH_MP_TAC + >> MATCH_MP_TAC hreduce_substitutive >> art [] +QED + (* This nice and hard-to-prove theorem gives a precise explicit form for any lambda term whose single-step head reduction is in the form of ‘LAMl vs t’. @@ -685,11 +714,9 @@ val whstar_FV = store_thm( HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN METIS_TAC [relationTheory.RTC_RULES, whead_FV]); - -val _ = reveal "Y" val whY1 = store_thm( "whY1", - ``Y @@ f -w-> Yf f``, + ``chap2$Y @@ f -w-> Yf f``, SRW_TAC [][chap2Theory.Y_def, chap2Theory.Yf_def, LET_THM, Once weak_head_cases] THEN NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN @@ -743,7 +770,7 @@ QED val wh_weaken_cong = store_thm( "wh_weaken_cong", - ``whnf N ⇒ M₁ -w->* M₂ ⇒ (M₁ -w->* N = M₂ -w->* N)``, + ``whnf N ⇒ M₁ -w->* M₂ ⇒ (M₁ -w->* N <=> M₂ -w->* N)``, SIMP_TAC (srw_ss()) [EQ_IMP_THM, IMP_CONJ_THM] THEN CONJ_TAC THENL [ Q_TAC SUFF_TAC `∀M N. M -w->* N ⇒ ∀N'. M -w->* N' ∧ whnf N' ⇒ N -w->* N'` THEN1 METIS_TAC [] THEN @@ -933,11 +960,11 @@ val is_head_redex_unique = store_thm( val is_head_redex_thm = store_thm( "is_head_redex_thm", - ``(p is_head_redex (LAM v t) = ?p0. (p = In::p0) /\ p0 is_head_redex t) /\ - (p is_head_redex (t @@ u) = (p = []) /\ is_abs t \/ + ``(p is_head_redex (LAM v t) <=> ?p0. (p = In::p0) /\ p0 is_head_redex t) /\ + (p is_head_redex (t @@ u) <=> (p = []) /\ is_abs t \/ ?p0. (p = Lt::p0) /\ is_comb t /\ p0 is_head_redex t) /\ - (p is_head_redex (VAR v) = F)``, + (p is_head_redex (VAR v) <=> F)``, REPEAT CONJ_TAC THEN SRW_TAC [][Once is_head_redex_cases, SimpLHS, LAM_eq_thm] THEN SRW_TAC [][EQ_IMP_THM] THENL [ @@ -955,7 +982,7 @@ val head_redex_leftmost = store_thm( val hnf_no_head_redex = store_thm( "hnf_no_head_redex", - ``!t. hnf t = !p. ~(p is_head_redex t)``, + ``!t. hnf t <=> !p. ~(p is_head_redex t)``, HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][hnf_thm, is_head_redex_thm] THEN Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN @@ -969,7 +996,7 @@ val head_redex_is_redex = store_thm( val is_head_redex_vsubst_invariant = store_thm( "is_head_redex_vsubst_invariant", - ``!t v x p. p is_head_redex ([VAR v/x] t) = p is_head_redex t``, + ``!t v x p. p is_head_redex ([VAR v/x] t) <=> p is_head_redex t``, REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v}` THEN SRW_TAC [][is_head_redex_thm, SUB_THM, SUB_VAR]); @@ -994,14 +1021,14 @@ val head_redex_preserved = store_thm( (* moved here from standardisationScript.sml *) Definition is_head_reduction_def : - is_head_reduction s = okpath (labelled_redn beta) s /\ + is_head_reduction s <=> okpath (labelled_redn beta) s /\ !i. i + 1 IN PL s ==> nth_label i s is_head_redex el i s End Theorem is_head_reduction_thm[simp] : - (is_head_reduction (stopped_at x) = T) /\ - (is_head_reduction (pcons x r p) = + (is_head_reduction (stopped_at x) <=> T) /\ + (is_head_reduction (pcons x r p) <=> labelled_redn beta x r (first p) /\ r is_head_redex x /\ is_head_reduction p) Proof @@ -1022,7 +1049,7 @@ End val head_reduce1_def = store_thm( "head_reduce1_def", - ``M -h-> N = (?r. r is_head_redex M /\ labelled_redn beta M r N)``, + ``M -h-> N <=> (?r. r is_head_redex M /\ labelled_redn beta M r N)``, EQ_TAC THENL [ Q_TAC SUFF_TAC `!M N. M -h-> N ==> ?r. r is_head_redex M /\ labelled_redn beta M r N` @@ -1126,7 +1153,7 @@ val head_reduct_NONE = store_thm( val head_reduct_SOME = store_thm( "head_reduct_SOME", - ``(head_reduct M = SOME N) = M -h-> N``, + ``(head_reduct M = SOME N) <=> M -h-> N``, SIMP_TAC (srw_ss()) [EQ_IMP_THM, head_reduct_unique] THEN SRW_TAC [][head_reduct_def] THEN SELECT_ELIM_TAC THEN SRW_TAC [][head_reduce1_def] THEN @@ -1637,8 +1664,7 @@ Proof >> Q.EXISTS_TAC ‘BIGUNION (IMAGE FV (set Ms))’ >> simp [] >> rw [SUBSET_DEF, IN_BIGUNION_IMAGE] - >> Q.EXISTS_TAC ‘EL i Ms’ >> rw [MEM_EL] - >> Q.EXISTS_TAC ‘i’ >> rw [] + >> Q.EXISTS_TAC ‘EL i Ms’ >> rw [EL_MEM] QED Theorem absfree_hnf_head : @@ -1739,7 +1765,7 @@ Proof >> rw [appstar_SNOC] QED -Theorem LAMl_size_hnf_absfree[simp] : +Theorem LAMl_size_appstar[simp] : LAMl_size (VAR y @* args) = 0 Proof Cases_on ‘args = []’ >- rw [] @@ -1783,6 +1809,12 @@ Proof HO_MATCH_MP_TAC simple_induction >> rw [] QED +Theorem hnf_children_size_alt : + !M. hnf M /\ ~is_abs M ==> hnf_children_size M = LENGTH (hnf_children M) +Proof + rw [absfree_hnf_cases] >> rw [] +QED + (*---------------------------------------------------------------------------* * hnf_cases_shared - ‘hnf_cases’ with a given list of fresh variables *---------------------------------------------------------------------------*) @@ -1791,7 +1823,7 @@ QED Theorem hnf_cases_shared : !vs M. ALL_DISTINCT vs /\ LAMl_size M <= LENGTH vs /\ DISJOINT (set vs) (FV M) ==> - (hnf M <=> ?y args. (M = LAMl (TAKE (LAMl_size M) vs) (VAR y @* args))) + (hnf M <=> ?y args. M = LAMl (TAKE (LAMl_size M) vs) (VAR y @* args)) Proof rpt STRIP_TAC >> reverse EQ_TAC @@ -1826,106 +1858,104 @@ QED *---------------------------------------------------------------------------*) Theorem hreduce_LAMl_appstar_lemma[local] : - !pi. ALL_DISTINCT (MAP FST pi) /\ - EVERY (\e. DISJOINT (FV e) (set (MAP FST pi))) (MAP SND pi) ==> - LAMl (MAP FST pi) t @* MAP SND pi -h->* (FEMPTY |++ pi) ' t + !pi t args. + ALL_DISTINCT (MAP FST pi) /\ + EVERY (\e. DISJOINT (FV e) (set (MAP FST pi))) (MAP SND pi) ==> + LAMl (MAP FST pi) t @* MAP SND pi @* args -h->* + (FEMPTY |++ pi) ' t @* args Proof Induct_on ‘pi’ >> rw [FUPDATE_LIST_THM] (* only one goal left *) - (* cleanup antecedents of IH *) - >> Q.PAT_X_ASSUM - ‘_ ==> LAMl (MAP FST pi) t @* MAP SND pi -h->* (FEMPTY |++ pi) ' t’ MP_TAC >> Know ‘EVERY (\e. DISJOINT (FV e) (set (MAP FST pi))) (MAP SND pi)’ >- (POP_ASSUM MP_TAC \\ rw [EVERY_MEM, MEM_MAP]) - >> RW_TAC std_ss [] - (* stage work *) + >> DISCH_THEN (fs o wrap) >> qabbrev_tac ‘vs = MAP FST pi’ >> qabbrev_tac ‘Ns = MAP SND pi’ - >> simp [Once RTC_CASES1] - >> DISJ2_TAC - (* preparing for hreduce1_rules_appstar *) >> qabbrev_tac ‘v = FST h’ >> qabbrev_tac ‘N = SND h’ - >> Q.EXISTS_TAC ‘[N/v] (LAMl vs t) @* Ns’ + >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW + (* stage work *) + >> simp [Once RTC_CASES1] + >> DISJ2_TAC + (* preparing for hreduce1_appstar *) + >> Q.EXISTS_TAC ‘[N/v] (LAMl vs t) @* Ns @* args’ >> CONJ_TAC - >- (MATCH_MP_TAC hreduce1_rules_appstar >> simp [] \\ + >- (REWRITE_TAC [GSYM appstar_APPEND] \\ + MATCH_MP_TAC hreduce1_appstar >> simp [] \\ rw [Once hreduce1_cases] \\ qexistsl_tac [‘v’, ‘LAMl vs t’] >> rw []) - >> Know ‘[N/v] (LAMl vs t) @* Ns = - [N/v] (LAMl vs t @* Ns)’ - >- (simp [appstar_SUB] \\ - Suff ‘MAP [N/v] Ns = Ns’ >- rw [] \\ - rw [LIST_EQ_REWRITE, EL_MAP] \\ - MATCH_MP_TAC lemma14b \\ - rename1 ‘i < LENGTH Ns’ \\ - Q.PAT_X_ASSUM ‘EVERY (\e. DISJOINT (FV e) (set vs) /\ v # e) Ns’ MP_TAC \\ - rw [EVERY_MEM] \\ - POP_ASSUM (MP_TAC o (Q.SPEC ‘EL i Ns’)) \\ - Suff ‘MEM (EL i Ns) Ns’ >- rw [] \\ - rw [MEM_EL] >> Q.EXISTS_TAC ‘i’ >> art []) - >> Rewr' - >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW - >> simp [FUPDATE_LIST_THM] - (* applying FUPDATE_FUPDATE_LIST_COMMUTES *) >> Know ‘FEMPTY |+ (v,N) |++ pi = (FEMPTY |++ pi) |+ (v,N)’ >- (MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES >> rw []) >> Rewr' + (* applying FUPDATE_FUPDATE_LIST_COMMUTES *) >> qabbrev_tac ‘fm = FEMPTY |++ pi’ >> ‘FDOM fm = set vs’ by rw [Abbr ‘fm’, FDOM_FUPDATE_LIST] - (* applying ssub_update_apply_SUBST' *) - >> Know ‘(fm |+ (v,N)) ' t = [fm ' N/v] (fm ' t)’ - >- (MATCH_MP_TAC ssub_update_apply_SUBST' \\ - rw [Once DISJOINT_SYM, MEM_EL, Abbr ‘fm’] \\ - Know ‘(FEMPTY |++ pi) ' (EL n vs) = EL n Ns’ - >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\ - ‘LENGTH pi = LENGTH vs’ by rw [Abbr ‘vs’] \\ - Q.EXISTS_TAC ‘n’ >> rw [] \\ - Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\ - rw [EL_ALL_DISTINCT_EL_EQ]) >> Rewr' \\ - Q.PAT_X_ASSUM ‘EVERY (\e. DISJOINT (FV e) (set vs) /\ v # e) Ns’ MP_TAC \\ - rw [EVERY_MEM] \\ - POP_ASSUM (MP_TAC o (Q.SPEC ‘EL n Ns’)) \\ - Suff ‘MEM (EL n Ns) Ns’ >- rw [] \\ - rw [MEM_EL] >> Q.EXISTS_TAC ‘n’ >> art [] \\ - Suff ‘LENGTH Ns = LENGTH vs’ >- rw [] \\ - rw [Abbr ‘Ns’, Abbr ‘vs’]) + >> Know ‘[N/v] (LAMl vs t) = LAMl vs ([N/v] t)’ + >- (MATCH_MP_TAC LAMl_SUB >> rw [Once DISJOINT_SYM]) >> Rewr' - >> Know ‘fm ' N = N’ - >- (MATCH_MP_TAC ssub_14b >> rw [GSYM DISJOINT_DEF]) + >> Suff ‘(fm |+ (v,N)) ' t = fm ' ([N/v] t)’ >- rw [] + >> MATCH_MP_TAC ssub_update_apply_SUBST + >> rw [Once DISJOINT_SYM] + (* applying FUPDATE_LIST_APPLY_MEM *) + >> fs [MEM_EL, Abbr ‘fm’] + >> ‘LENGTH vs = LENGTH pi /\ LENGTH Ns = LENGTH pi’ by rw [Abbr ‘vs’, Abbr ‘Ns’] + >> Know ‘(FEMPTY |++ pi) ' (EL n vs) = EL n Ns’ + >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\ + Q.EXISTS_TAC ‘n’ >> rw [] \\ + CCONTR_TAC >> fs [] \\ + ‘n < LENGTH vs /\ m <> n’ by RW_TAC arith_ss [] \\ + METIS_TAC [ALL_DISTINCT_EL_IMP]) >> Rewr' - >> MATCH_MP_TAC hreduce_substitutive >> art [] + >> Q.PAT_X_ASSUM ‘EVERY P Ns’ MP_TAC + >> rw [EVERY_EL] QED Theorem hreduce_LAMl_appstar : - !t xs Ns. ALL_DISTINCT xs /\ (LENGTH xs = LENGTH Ns) /\ - EVERY (\e. DISJOINT (FV e) (set xs)) Ns - ==> LAMl xs t @* Ns -h->* (FEMPTY |++ ZIP (xs,Ns)) ' t + !vs Ns t. ALL_DISTINCT vs /\ LENGTH vs = LENGTH Ns /\ + EVERY (\e. DISJOINT (FV e) (set vs)) Ns + ==> LAMl vs t @* Ns -h->* fromPairs vs Ns ' t Proof RW_TAC std_ss [] - >> qabbrev_tac ‘n = LENGTH xs’ - >> qabbrev_tac ‘pi = ZIP (xs,Ns)’ - >> ‘xs = MAP FST pi’ by rw [Abbr ‘pi’, MAP_ZIP] + >> qabbrev_tac ‘n = LENGTH vs’ + >> qabbrev_tac ‘pi = ZIP (vs,Ns)’ + >> ‘vs = MAP FST pi’ by rw [Abbr ‘pi’, MAP_ZIP] >> ‘Ns = MAP SND pi’ by rw [Abbr ‘pi’, MAP_ZIP] - >> simp [] - >> MATCH_MP_TAC hreduce_LAMl_appstar_lemma >> rw [] + >> simp [fromPairs_def] + >> MP_TAC (Q.SPECL [‘pi’, ‘t’, ‘[]’] hreduce_LAMl_appstar_lemma) + >> rw [] QED -val _ = hide "Y"; +(* NOTE: there's no requirements on ‘args’, which can be empty *) +Theorem hreduce_LAMl_appstar_ext : + !vs Ns t args. + ALL_DISTINCT vs /\ LENGTH vs = LENGTH Ns /\ + EVERY (\e. DISJOINT (FV e) (set vs)) Ns + ==> LAMl vs t @* Ns @* args -h->* fromPairs vs Ns ' t @* args +Proof + RW_TAC std_ss [] + >> qabbrev_tac ‘n = LENGTH vs’ + >> qabbrev_tac ‘pi = ZIP (vs,Ns)’ + >> ‘vs = MAP FST pi’ by rw [Abbr ‘pi’, MAP_ZIP] + >> ‘Ns = MAP SND pi’ by rw [Abbr ‘pi’, MAP_ZIP] + >> simp [fromPairs_def] + >> MATCH_MP_TAC hreduce_LAMl_appstar_lemma + >> rw [] +QED (* NOTE: ‘permutator n’ contains n + 1 binding variables. Appending at most n arbitrary terms, each head reduction step consumes just one of them, eventually there should be one more fresh variable left, forming a hnf. NOTE2: added one global excluded list X and more disjointness conclusions. + NOTE3: added ‘LENGTH xs = n - LENGTH Ns’ for the potential needs. *) Theorem permutator_hreduce_thm : !X n Ns. FINITE X /\ LENGTH Ns <= n ==> - ?xs y. permutator n @* Ns -h->* - LAMl xs (LAM y (VAR y @* Ns @* MAP VAR xs)) /\ - ALL_DISTINCT (SNOC y xs) /\ - DISJOINT X (set (SNOC y xs)) /\ - !N. MEM N Ns ==> DISJOINT (FV N) (set (SNOC y xs)) + ?xs y. permutator n @* Ns -h->* LAMl xs (LAM y (VAR y @* Ns @* MAP VAR xs)) /\ + LENGTH xs = n - LENGTH Ns /\ + ALL_DISTINCT (SNOC y xs) /\ DISJOINT X (set (SNOC y xs)) /\ + !N. MEM N Ns ==> DISJOINT (FV N) (set (SNOC y xs)) Proof rw [permutator_def] >> qabbrev_tac ‘Z = GENLIST n2s (n + 1)’ @@ -2012,7 +2042,7 @@ Proof >> qabbrev_tac ‘t1 = LAMl vs2 t’ (* applying hreduce_LAMl_appstar *) >> Know ‘LAMl vs1 t1 @* Ns -h->* (FEMPTY |++ ZIP (vs1,Ns)) ' t1’ - >- (MATCH_MP_TAC hreduce_LAMl_appstar \\ + >- (MATCH_MP_TAC (REWRITE_RULE [fromPairs_def] hreduce_LAMl_appstar) \\ CONJ_TAC >- (qunabbrev_tac ‘vs1’ \\ MATCH_MP_TAC ALL_DISTINCT_TAKE >> art []) \\ CONJ_TAC >- (rw [Abbr ‘vs1’]) \\ @@ -2107,8 +2137,7 @@ Proof >- (rw [LIST_EQ_REWRITE] >- rw [Abbr ‘vs1’] \\ rename1 ‘i < LENGTH vs1’ \\ simp [EL_MAP] \\ - Know ‘MEM (EL i vs1) vs1’ - >- (rw [MEM_EL] >> Q.EXISTS_TAC ‘i’ >> art []) >> Rewr \\ + ‘MEM (EL i vs1) vs1’ by rw [EL_MEM] >> simp [] \\ MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw [] >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\ ‘vs = vs1 ++ vs2’ by rw [Abbr ‘vs1’, Abbr ‘vs2’, TAKE_DROP] \\ @@ -2131,6 +2160,8 @@ Proof >> REWRITE_TAC [appstar_APPEND] >> DISCH_TAC >> qexistsl_tac [‘vs2’, ‘y’] >> art [] + (* extra goal: LENGTH vs2 = n - k *) + >> CONJ_TAC >- rw [Abbr ‘vs2’, LENGTH_DROP] (* extra goal: ALL_DISTINCT *) >> CONJ_TAC >- (reverse (rw [ALL_DISTINCT_SNOC]) @@ -2182,6 +2213,206 @@ Proof >> PROVE_TAC [MEM_DROP_IMP] QED +Theorem permutator_hreduce_lemma[local] : + ALL_DISTINCT vs /\ ~MEM y vs /\ LENGTH vs = LENGTH Ns /\ + EVERY (\e. DISJOINT (FV e) (set (SNOC y vs))) (SNOC N Ns) ==> + LAMl vs (LAM y (VAR y @* MAP VAR vs)) @* Ns @@ N @* args -h->* + N @* Ns @* args +Proof + rpt STRIP_TAC + >> REWRITE_TAC [GSYM LAMl_SNOC, GSYM appstar_SNOC] + >> qabbrev_tac ‘vs' = SNOC y vs’ + >> qabbrev_tac ‘Ns' = SNOC N Ns’ + >> qabbrev_tac ‘t = VAR y @* MAP VAR vs’ + >> Suff ‘N @* Ns = fromPairs vs' Ns' ' t’ + >- (Rewr' \\ + MATCH_MP_TAC hreduce_LAMl_appstar_ext \\ + rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC] \\ + Q.PAT_X_ASSUM ‘EVERY _ (SNOC N Ns)’ MP_TAC \\ + rw [EVERY_MEM, LIST_TO_SET_SNOC] \\ (* 2 subgoals, same tactics *) + METIS_TAC []) + >> ‘LENGTH vs' = LENGTH Ns'’ by rw [Abbr ‘vs'’, Abbr ‘Ns'’] + >> ‘y IN FDOM (fromPairs vs' Ns')’ by rw [FDOM_fromPairs, Abbr ‘vs'’] + >> simp [Abbr ‘t’, ssub_appstar] + >> Know ‘fromPairs vs' Ns' ' y = N’ + >- (‘y = LAST vs'’ by rw [Abbr ‘vs'’, LAST_SNOC] >> POP_ORW \\ + ‘vs' <> []’ by rw [Abbr ‘vs'’] \\ + rw [LAST_EL] \\ + qabbrev_tac ‘n = PRE (LENGTH Ns')’ \\ + Know ‘fromPairs vs' Ns' ' (EL n vs') = EL n Ns'’ + >- (MATCH_MP_TAC fromPairs_FAPPLY_EL \\ + rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC, Abbr ‘n’]) >> Rewr' \\ + ‘Ns' <> []’ by rw [Abbr ‘Ns'’] \\ + ‘EL n Ns' = LAST Ns'’ by rw [LAST_EL, Abbr ‘n’] >> POP_ORW \\ + rw [Abbr ‘Ns'’, LAST_SNOC]) + >> Rewr' + >> Suff ‘MAP ($' (fromPairs vs' Ns')) (MAP VAR vs) = Ns’ >- rw [] + >> rw [LIST_EQ_REWRITE] + >> rename1 ‘i < LENGTH Ns’ + >> Know ‘EL i vs IN FDOM (fromPairs vs' Ns')’ + >- (rw [FDOM_fromPairs] \\ + rw [Abbr ‘vs'’, MEM_EL] \\ + DISJ2_TAC >> Q.EXISTS_TAC ‘i’ >> art []) + >> rw [EL_MAP] + >> Know ‘(EL i vs = EL i vs') /\ (EL i Ns = EL i Ns')’ + >- ASM_SIMP_TAC std_ss [EL_SNOC, Abbr ‘vs'’, Abbr ‘Ns'’] + >> rw [] + >> MATCH_MP_TAC fromPairs_FAPPLY_EL + >> rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC] +QED + +(* NOTE: more arguments remain the same after head reductions *) +Theorem permutator_hreduce_more : + !n N Ns args. LENGTH Ns = n ==> permutator n @* Ns @@ N @* args -h->* N @* Ns @* args +Proof + rpt STRIP_TAC + >> qabbrev_tac ‘X = BIGUNION (IMAGE FV (set Ns)) UNION FV N’ + >> Know ‘FINITE X’ + >- (rw [Abbr ‘X’] >> REWRITE_TAC [FINITE_FV]) + >> DISCH_THEN (MP_TAC o (MATCH_MP permutator_cases)) + >> DISCH_THEN (STRIP_ASSUME_TAC o (Q.SPEC ‘n’)) + >> POP_ORW + >> MATCH_MP_TAC permutator_hreduce_lemma + >> fs [ALL_DISTINCT_SNOC] + >> POP_ASSUM MP_TAC (* DISJOINT X ... *) + >> rw [Abbr ‘X’, EVERY_MEM, LIST_TO_SET_SNOC] >> art [] + >| [ (* goal 1 (of 2) *) + Q.PAT_X_ASSUM ‘!s. P’ (MP_TAC o (Q.SPEC ‘FV (e :term)’)) \\ + impl_tac >- (Q.EXISTS_TAC ‘e’ >> art []) >> rw [], + (* goal 2 (of 2) *) + Q.PAT_X_ASSUM ‘!s. P’ (MP_TAC o (Q.SPEC ‘FV (e :term)’)) \\ + impl_tac >- (Q.EXISTS_TAC ‘e’ >> art []) >> rw [] ] +QED + +(* NOTE: ‘EL n l’ is undefined without ‘n < LENGTH l’ *) +Theorem permutator_hreduce_more' : + !n l. n < LENGTH l ==> + permutator n @* l -h->* EL n l @* TAKE n l @* DROP (SUC n) l +Proof + rpt STRIP_TAC + >> Suff ‘permutator n @* l = + permutator n @* TAKE n l @@ EL n l @* DROP (SUC n) l’ + >- (Rewr' \\ + MATCH_MP_TAC permutator_hreduce_more >> rw [LENGTH_TAKE]) + >> Suff ‘l = TAKE n l ++ [EL n l] ++ DROP (SUC n) l’ + >- (DISCH_THEN + (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites o wrap) \\ + REWRITE_TAC [GSYM SNOC_APPEND] \\ + REWRITE_TAC [appstar_APPEND] \\ + REWRITE_TAC [appstar_SNOC]) + >> MATCH_MP_TAC (GSYM TAKE_DROP_SUC) >> art [] +QED + +Theorem permutator_hreduce_same_length : + !n N Ns. LENGTH Ns = n ==> permutator n @* Ns @@ N -h->* N @* Ns +Proof + rpt STRIP_TAC + >> MP_TAC (Q.SPECL [‘n’, ‘N’, ‘Ns’, ‘[]’] permutator_hreduce_more) + >> rw [] +QED + +(* This is an important theroem, hard to prove. + + To use this theorem, first one defines ‘M0 = principle_hnf M’ as abbreviation, + then define ‘n = LAMl_size M0’ and ‘vs = NEWS n (FV M)’ (or ‘FV M0’, or + ‘X UNION FV M0’, ‘X UNION FV M’), and this give us the needed antecedents: + + ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ LENGTH vs = n + + Then use hnf_cases_shared to derive ‘M0 = LAMl vs (VAR y @* args)’ and then + ‘M1 = principle_hnf (M0 @* MAP VAR vs) = VAR y @* args’. + + The conclusion is that ‘principle_hnf (M @* MAP VAR vs) = M1’. + + Now ‘principle_hnf’ can be used to "denude" the outer LAMl of a solvable term. + + An extra list of free variables ‘l’ may need to append after MAP VAR vs. + *) +Theorem hreduce_hnf_appstar_cong : + !M vs y Ns args. ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ + M -h->* LAMl vs (VAR y @* Ns) ==> + M @* MAP VAR vs @* args -h->* VAR y @* Ns @* args +Proof + rpt STRIP_TAC + >> Know ‘has_hnf M’ + >- (rw [has_hnf_def] \\ + Q.EXISTS_TAC ‘LAMl vs (VAR y @* Ns)’ >> rw [hnf_appstar] \\ + MATCH_MP_TAC hreduces_lameq >> art []) + >> DISCH_TAC + (* eliminating MAP VAR l *) + >> MATCH_MP_TAC hreduce_rules_appstar' + >> rw [is_abs_appstar] + >- (fs [] >> CCONTR_TAC >> fs [] \\ + ‘is_abs (VAR y @* Ns)’ by PROVE_TAC [hreduce_abs] >> fs []) + (* now l is eliminated *) + >> NTAC 4 (POP_ASSUM MP_TAC) + >> Suff ‘!M M0. M -h->* M0 ==> + has_hnf M ==> + !vs t. ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ + (M0 = LAMl vs t) /\ ~is_abs t ==> + M @* MAP VAR vs -h->* t’ + >- (rpt STRIP_TAC >> FIRST_X_ASSUM irule >> rw []) + >> HO_MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1 + >> rw [hreduce_BETA] (* only one goal left *) + >> Q.PAT_X_ASSUM ‘has_hnf M ==> P’ MP_TAC + >> RW_TAC std_ss [] + (* NOTE: this assumption is only possible with RTC_STRONG_INDUCT, etc. *) + >> Know ‘DISJOINT (set vs) (FV M0)’ + >- (MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘FV M’ >> art [] \\ + MATCH_MP_TAC hreduce_FV_SUBSET >> art []) + >> DISCH_TAC + (* stage work. + + Now we need to discuss the possible shapes of M0: + + 1. M0 := LAMl vs (P @@ Q), where P @@ Q -h-> t + 2. M0 := LAMl vs1 (P @@ Q), where P @@ Q -h-> LAMl vs2 t, vs = vs1 ++ vs2 + + The first case is included in the second case. + + Using IH, we have: M @* MAP VAR vs1 -h->* P @@ Q -h-> LAMl vs2 t (hnf) + Thus (using RTC transitivity): M @* MAP VAR vs1 -h->* LAMl vs2 t (hnf) + + Since M @* MAP VAR vs = M @* MAP VAR vs1 @* MAP VAR vs2, the head reduction + process should proceed with the part ‘M @* MAP VAR vs1’ until arrive at + ‘P @@ Q’ (APP) without showing any LAM (otherwise it cannot be P @@ Q), and + then do it again to ‘LAMl vs2 t’, i.e. + + M @* MAP VAR vs1 @* MAP VAR vs2 -h->* P @@ Q @* MAP VAR vs2 + -h-> LAMl vs2 t @* MAP VAR vs2 + -h->* t (QED) + + The possible fact ‘hnf t’ is not used in the above reduction process. + *) + (* applying hreduce1_LAMl_cases *) + >> Know ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0) /\ M0 -h-> LAMl vs t /\ + ~is_abs t’ >- art [] + >> DISCH_THEN (STRIP_ASSUME_TAC o (MATCH_MP hreduce1_LAMl_cases)) + (* stage work *) + >> Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs1’, ‘N’])) + >> Know ‘ALL_DISTINCT vs1’ + >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\ + rw [ALL_DISTINCT_APPEND]) + >> Know ‘DISJOINT (set vs1) (FV M)’ + >- (Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M)’ MP_TAC \\ + rw [LIST_TO_SET_APPEND]) + >> RW_TAC std_ss [] + >> simp [appstar_APPEND] + >> MATCH_MP_TAC hreduce_TRANS + >> Q.EXISTS_TAC ‘LAMl vs2 t @* MAP VAR vs2’ + >> reverse CONJ_TAC >- rw [hreduce_BETA] + >> rw [Once RTC_CASES2] >> DISJ2_TAC + >> Q.EXISTS_TAC ‘N @* MAP VAR vs2’ + >> reverse CONJ_TAC + >- (MATCH_MP_TAC hreduce1_appstar >> art [] \\ + fs [is_comb_APP_EXISTS]) + >> MATCH_MP_TAC hreduce_rules_appstar' >> art [] + >> rw [is_abs_appstar] + >> CCONTR_TAC >> fs [] + >> PROVE_TAC [hreduce_abs] (* is_abs N *) +QED + val _ = export_theory() val _ = html_theory "head_reduction"; diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml index 0c6d1800ad..94b6605420 100644 --- a/examples/lambda/barendregt/solvableScript.sml +++ b/examples/lambda/barendregt/solvableScript.sml @@ -866,7 +866,7 @@ Proof >> Know ‘principle_hnf (LAM q M @@ VAR r @* args) = principle_hnf ([VAR r/q] M @* args)’ >- (MATCH_MP_TAC principle_hnf_hreduce1 \\ - MATCH_MP_TAC hreduce1_rules_appstar >> rw [hreduce1_BETA]) + MATCH_MP_TAC hreduce1_appstar >> rw [hreduce1_BETA]) >> Rewr' >> Know ‘[VAR r/q] M = LAMl (MAP FST pi) ([VAR r/q] t)’ >- (qunabbrev_tac ‘M’ \\ @@ -983,7 +983,29 @@ Proof >> Know ‘principle_hnf (LAM h M @@ VAR h @* args) = principle_hnf ([VAR h/h] M @* args)’ >- (MATCH_MP_TAC principle_hnf_hreduce1 \\ - MATCH_MP_TAC hreduce1_rules_appstar >> rw [hreduce1_BETA]) + MATCH_MP_TAC hreduce1_appstar >> rw [hreduce1_BETA]) + >> Rewr' + >> simp [Abbr ‘M’] +QED + +(* NOTE: ‘~is_abs t’ is required to preserve ‘l’ *) +Theorem principle_hnf_beta_reduce_ext : + !l xs t. hnf t /\ ~is_abs t ==> + principle_hnf (LAMl xs t @* MAP VAR xs @* l) = t @* l +Proof + Q.X_GEN_TAC ‘l’ + >> Induct_on ‘xs’ + >- (rw [] \\ + ‘hnf (t @* l)’ by rw [hnf_appstar] \\ + rw [principle_hnf_reduce]) + >> rw [] + >> qabbrev_tac ‘M = LAMl xs t’ + >> qabbrev_tac ‘args :term list = MAP VAR xs’ + >> Know ‘principle_hnf (LAM h M @@ VAR h @* args @* l) = + principle_hnf (M @* args @* l)’ + >- (MATCH_MP_TAC principle_hnf_hreduce1 \\ + MATCH_MP_TAC hreduce1_appstar >> rw [] \\ + MATCH_MP_TAC hreduce1_appstar >> rw []) >> Rewr' >> simp [Abbr ‘M’] QED @@ -1338,8 +1360,8 @@ QED Theorem lameq_principle_hnf_thm' = lameq_principle_hnf_thm |> REWRITE_RULE [GSYM solvable_iff_has_hnf] -(* NOTE: the difficulty of applying this theorem is to prove the antecedents *) -Theorem principle_hnf_substitutive : +(* NOTE: The difficulty of applying this theorem is to prove the antecedents *) +Theorem principle_hnf_SUB_cong : !M N v P. has_hnf M /\ has_hnf ([P/v] M) /\ has_hnf ([P/v] N) /\ principle_hnf M = N ==> principle_hnf ([P/v] M) = principle_hnf ([P/v] N) @@ -1350,8 +1372,7 @@ Proof >- (MATCH_MP_TAC hnf_principle_hnf >> art []) >> MATCH_MP_TAC hreduce_TRANS >> Q.EXISTS_TAC ‘[P/v] N’ - >> CONJ_TAC - >- (MATCH_MP_TAC hreduce_substitutive >> art []) + >> CONJ_TAC >- (MATCH_MP_TAC hreduce_substitutive >> art []) >> qabbrev_tac ‘M' = [P/v] M’ >> qabbrev_tac ‘N' = [P/v] N’ >> qabbrev_tac ‘Q = principle_hnf N'’ @@ -1359,122 +1380,31 @@ Proof >> rw [principle_hnf_thm] QED -Theorem principle_hnf_substitutive_hnf : - !M N v P. has_hnf M /\ has_hnf ([P/v] M) /\ hnf ([P/v] N) /\ +(* NOTE: Again, the difficulty of applying this theorem is to prove the antecedents *) +Theorem principle_hnf_ISUB_cong : + !M N sub. has_hnf M /\ has_hnf (M ISUB sub) /\ has_hnf (N ISUB sub) /\ principle_hnf M = N ==> - principle_hnf ([P/v] M) = [P/v] N + principle_hnf (M ISUB sub) = principle_hnf (N ISUB sub) Proof rpt STRIP_TAC - >> Know ‘principle_hnf ([P/v] M) = principle_hnf ([P/v] N)’ - >- (MATCH_MP_TAC principle_hnf_substitutive >> art [] \\ - MATCH_MP_TAC hnf_has_hnf >> art []) - >> Rewr' - >> MATCH_MP_TAC principle_hnf_reduce >> art [] -QED - -(* This is an important theroem, hard to prove. - - To use this theorem, first one defines ‘M0 = principle_hnf M’ as abbreviation, - then define ‘n = LAMl_size M0’ and ‘vs = NEWS n (FV M)’ (or ‘FV M0’, or - ‘X UNION FV M0’, ‘X UNION FV M’), and this give us the needed antecedents: - - ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ LENGTH vs = n - - Then use hnf_cases_shared to derive ‘M0 = LAMl vs (VAR y @* args)’ and then - ‘M1 = principle_hnf (M0 @* MAP VAR vs) = VAR y @* args’. - - The conclusion is that ‘principle_hnf (M @* MAP VAR vs) = M1’. - - Now ‘principle_hnf’ can be used to "denude" the outer LAMl of a solvable term. - - An extra list of free variables ‘l’ may need to append after MAP VAR vs. - *) -Theorem principle_hnf_denude_lemma[local] : - !M vs l y Ns. solvable M /\ - ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ - M -h->* LAMl vs (VAR y @* Ns) ==> - M @* MAP VAR vs @* MAP VAR l -h->* VAR y @* Ns @* MAP VAR l -Proof - rpt STRIP_TAC - (* eliminating MAP VAR l *) - >> MATCH_MP_TAC hreduce_rules_appstar' - >> rw [is_abs_appstar] - >- (fs [] >> CCONTR_TAC >> fs [] \\ - ‘is_abs (VAR y @* Ns)’ by PROVE_TAC [hreduce_abs] >> fs []) - (* now l is eliminated *) - >> NTAC 4 (POP_ASSUM MP_TAC) - >> Suff ‘!M M0. M -h->* M0 ==> - solvable M ==> - !vs t. ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ - M0 = LAMl vs t /\ ~is_abs t ==> - M @* MAP VAR vs -h->* t’ - >- (rpt STRIP_TAC >> FIRST_X_ASSUM irule >> rw []) - >> HO_MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1 - >> rw [hreduce_BETA] (* only one goal is left *) - >> Q.PAT_X_ASSUM ‘solvable M ==> P’ MP_TAC - >> RW_TAC std_ss [] - (* NOTE: this assumption is only possible with RTC_STRONG_INDUCT, etc. *) - >> Know ‘DISJOINT (set vs) (FV M0)’ - >- (MATCH_MP_TAC DISJOINT_SUBSET \\ - Q.EXISTS_TAC ‘FV M’ >> art [] \\ - MATCH_MP_TAC hreduce_FV_SUBSET >> art []) - >> DISCH_TAC - (* stage work. - - Now we need to discuss the possible shapes of M0: - - 1. M0 := LAMl vs (P @@ Q), where P @@ Q -h-> t - 2. M0 := LAMl vs1 (P @@ Q), where P @@ Q -h-> LAMl vs2 t, vs = vs1 ++ vs2 - - The first case is included in the second case. - - Using IH, we have: M @* MAP VAR vs1 -h->* P @@ Q -h-> LAMl vs2 t (hnf) - Thus (using RTC transitivity): M @* MAP VAR vs1 -h->* LAMl vs2 t (hnf) - - Since M @* MAP VAR vs = M @* MAP VAR vs1 @* MAP VAR vs2, the head reduction - process should proceed with the part ‘M @* MAP VAR vs1’ until arrive at - ‘P @@ Q’ (APP) without showing any LAM (otherwise it cannot be P @@ Q), and - then do it again to ‘LAMl vs2 t’, i.e. - - M @* MAP VAR vs1 @* MAP VAR vs2 -h->* P @@ Q @* MAP VAR vs2 - -h-> LAMl vs2 t @* MAP VAR vs2 - -h->* t (QED) - - The possible fact ‘hnf t’ is not used in the above reduction process. - *) - (* applying hreduce1_LAMl_cases *) - >> Know ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0) /\ M0 -h-> LAMl vs t /\ ~is_abs t’ - >- art [] - >> DISCH_THEN (STRIP_ASSUME_TAC o (MATCH_MP hreduce1_LAMl_cases)) - (* stage work *) - >> Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs1’, ‘N’])) - >> Know ‘ALL_DISTINCT vs1’ - >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\ - rw [ALL_DISTINCT_APPEND]) - >> Know ‘DISJOINT (set vs1) (FV M)’ - >- (Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M)’ MP_TAC \\ - rw [LIST_TO_SET_APPEND]) - >> RW_TAC std_ss [] - >> simp [appstar_APPEND] + >> POP_ASSUM MP_TAC + >> reverse (rw [principle_hnf_thm]) + >- (MATCH_MP_TAC hnf_principle_hnf >> art []) >> MATCH_MP_TAC hreduce_TRANS - >> Q.EXISTS_TAC ‘LAMl vs2 t @* MAP VAR vs2’ - >> reverse CONJ_TAC >- rw [hreduce_BETA] - >> rw [Once RTC_CASES2] >> DISJ2_TAC - >> Q.EXISTS_TAC ‘N @* MAP VAR vs2’ - >> reverse CONJ_TAC - >- (MATCH_MP_TAC hreduce1_rules_appstar >> art [] \\ - fs [is_comb_APP_EXISTS]) - >> MATCH_MP_TAC hreduce_rules_appstar' >> art [] - >> rw [is_abs_appstar] - >> CCONTR_TAC >> fs [] - >> ‘is_abs N’ by PROVE_TAC [hreduce_abs] + >> Q.EXISTS_TAC ‘N ISUB sub’ + >> CONJ_TAC >- (MATCH_MP_TAC hreduce_ISUB >> art []) + >> qabbrev_tac ‘M' = M ISUB sub’ + >> qabbrev_tac ‘N' = N ISUB sub’ + >> qabbrev_tac ‘Q = principle_hnf N'’ + >> Know ‘principle_hnf N' = Q’ >- rw [Abbr ‘Q’] + >> rw [principle_hnf_thm] QED -Theorem principle_hnf_denude_solvable : - !M vs l y args. solvable M /\ - ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ - principle_hnf M = LAMl vs (VAR y @* args) ==> - solvable (M @* MAP VAR vs @* MAP VAR l) +Theorem principle_hnf_denude_solvable[local] : + !M. solvable M /\ + ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ + principle_hnf M = LAMl vs (VAR y @* args) ==> + solvable (M @* MAP VAR vs @* ls) Proof rpt GEN_TAC >> STRIP_TAC >> qabbrev_tac ‘M0 = principle_hnf M’ @@ -1485,21 +1415,21 @@ Proof >> ‘M0 == M’ by rw [lameq_principle_hnf', Abbr ‘M0’] >> ‘M0 @* MAP VAR vs == VAR y @* args’ by rw [] >> ‘M0 @* MAP VAR vs == M @* MAP VAR vs’ by rw [lameq_appstar_cong] - >> Know ‘M @* MAP VAR vs @* MAP VAR l == VAR y @* args @* MAP VAR l’ + >> Know ‘M @* MAP VAR vs @* ls == VAR y @* args @* ls’ >- (MATCH_MP_TAC lameq_appstar_cong \\ PROVE_TAC [lameq_SYM, lameq_TRANS]) >> DISCH_TAC - >> Suff ‘solvable (VAR y @* args @* MAP VAR l)’ + >> Suff ‘solvable (VAR y @* args @* ls)’ >- PROVE_TAC [lameq_solvable_cong] >> REWRITE_TAC [solvable_iff_has_hnf] >> MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar] QED Theorem principle_hnf_denude_thm : - !l M vs y args. solvable M /\ + !ls M vs y args. solvable M /\ ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ principle_hnf M = LAMl vs (VAR y @* args) ==> - principle_hnf (M @* MAP VAR vs @* MAP VAR l) = VAR y @* args @* MAP VAR l + principle_hnf (M @* MAP VAR vs @* ls) = VAR y @* args @* ls Proof rpt GEN_TAC >> STRIP_TAC >> qabbrev_tac ‘M0 = principle_hnf M’ @@ -1507,16 +1437,15 @@ Proof >> Know ‘principle_hnf M = M0’ >- rw [Abbr ‘M0’] >> simp [principle_hnf_thm', hnf_appstar] >> DISCH_TAC - >> Know ‘solvable (M @* MAP VAR vs @* MAP VAR l)’ + >> Know ‘solvable (M @* MAP VAR vs @* ls)’ >- (MATCH_MP_TAC principle_hnf_denude_solvable \\ - qexistsl_tac [‘y’, ‘args’] \\ Q.PAT_X_ASSUM ‘M0 = _’ (ONCE_REWRITE_TAC o wrap o SYM) \\ rw [Abbr ‘M0’]) >> DISCH_TAC (* applying again principle_hnf_thm' *) >> simp [principle_hnf_thm', hnf_appstar] (* now all ‘principle_hnf’ are eliminated, leaving only -h->* *) - >> MATCH_MP_TAC principle_hnf_denude_lemma >> art [] + >> MATCH_MP_TAC hreduce_hnf_appstar_cong >> art [] QED (* |- !M vs y args. @@ -1527,53 +1456,6 @@ QED Theorem principle_hnf_denude_thm' = principle_hnf_denude_thm |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) [] -Theorem principle_hnf_permutator_lemma[local] : - !vs Ns. ALL_DISTINCT vs /\ ~MEM y vs /\ LENGTH vs = LENGTH Ns /\ - EVERY (\e. DISJOINT (FV e) (set (SNOC y vs))) (SNOC N Ns) ==> - LAMl vs (LAM y (VAR y @* MAP VAR vs)) @* Ns @@ N -h->* N @* Ns -Proof - rpt STRIP_TAC - >> REWRITE_TAC [GSYM LAMl_SNOC, GSYM appstar_SNOC] - >> qabbrev_tac ‘vs' = SNOC y vs’ - >> qabbrev_tac ‘Ns' = SNOC N Ns’ - >> qabbrev_tac ‘t = VAR y @* MAP VAR vs’ - >> Suff ‘N @* Ns = fromPairs vs' Ns' ' t’ - >- (Rewr' >> REWRITE_TAC [fromPairs_def] \\ - MATCH_MP_TAC hreduce_LAMl_appstar \\ - rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC] \\ - Q.PAT_X_ASSUM ‘EVERY _ (SNOC N Ns)’ MP_TAC \\ - rw [EVERY_MEM, LIST_TO_SET_SNOC] \\ (* 2 subgoals, same tactics *) - METIS_TAC []) - >> ‘LENGTH vs' = LENGTH Ns'’ by rw [Abbr ‘vs'’, Abbr ‘Ns'’] - >> ‘y IN FDOM (fromPairs vs' Ns')’ by rw [FDOM_fromPairs, Abbr ‘vs'’] - >> simp [Abbr ‘t’, ssub_appstar] - >> Know ‘fromPairs vs' Ns' ' y = N’ - >- (‘y = LAST vs'’ by rw [Abbr ‘vs'’, LAST_SNOC] >> POP_ORW \\ - ‘vs' <> []’ by rw [Abbr ‘vs'’] \\ - rw [LAST_EL] \\ - qabbrev_tac ‘n = PRE (LENGTH Ns')’ \\ - Know ‘fromPairs vs' Ns' ' (EL n vs') = EL n Ns'’ - >- (MATCH_MP_TAC fromPairs_FAPPLY_EL \\ - rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC, Abbr ‘n’]) >> Rewr' \\ - ‘Ns' <> []’ by rw [Abbr ‘Ns'’] \\ - ‘EL n Ns' = LAST Ns'’ by rw [LAST_EL, Abbr ‘n’] >> POP_ORW \\ - rw [Abbr ‘Ns'’, LAST_SNOC]) - >> Rewr' - >> Suff ‘MAP ($' (fromPairs vs' Ns')) (MAP VAR vs) = Ns’ >- rw [] - >> rw [LIST_EQ_REWRITE] - >> rename1 ‘i < LENGTH Ns’ - >> Know ‘EL i vs IN FDOM (fromPairs vs' Ns')’ - >- (rw [FDOM_fromPairs] \\ - rw [Abbr ‘vs'’, MEM_EL] \\ - DISJ2_TAC >> Q.EXISTS_TAC ‘i’ >> art []) - >> rw [EL_MAP] - >> Know ‘EL i vs = EL i vs' /\ EL i Ns = EL i Ns'’ - >- ASM_SIMP_TAC std_ss [EL_SNOC, Abbr ‘vs'’, Abbr ‘Ns'’] - >> rw [] - >> MATCH_MP_TAC fromPairs_FAPPLY_EL - >> rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC] -QED - Theorem principle_hnf_permutator : !n N Ns. hnf N /\ ~is_abs N /\ LENGTH Ns = n ==> principle_hnf (permutator n @* Ns @@ N) = N @* Ns @@ -1588,83 +1470,7 @@ Proof rw [hnf_appstar]) >> DISCH_TAC >> rw [principle_hnf_thm', hnf_appstar] - >> RW_TAC std_ss [permutator_def] - >> qabbrev_tac ‘n = LENGTH Ns’ - >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’ - by (rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST]) - >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] - >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL] - >> qabbrev_tac ‘M = VAR z @* MAP VAR (FRONT Z)’ - (* preparing for LAMl_ALPHA_ssub *) - >> qabbrev_tac ‘Y = NEWS (n + 1) - (set Z UNION (FV N) UNION (BIGUNION (IMAGE FV (set Ns))))’ - >> ‘FINITE (set Z UNION (FV N) UNION (BIGUNION (IMAGE FV (set Ns))))’ - by (rw [] >> rw [FINITE_FV]) - >> Know ‘ALL_DISTINCT Y /\ - DISJOINT (set Y) (set Z UNION (FV N) UNION (BIGUNION (IMAGE FV (set Ns)))) /\ - LENGTH Y = n + 1’ - >- (ASM_SIMP_TAC std_ss [NEWS_def, Abbr ‘Y’]) - >> rw [] (* this breaks all unions in the DISJOINT *) - (* applying LAMl_ALPHA_ssub *) - >> Know ‘LAMl Z M = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' M)’ - >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\ - Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\ - rw [Abbr ‘M’, FV_appstar] \\ - ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\ - POP_ORW \\ - simp [LIST_TO_SET_SNOC] \\ - rw [Once EXTENSION, MEM_MAP] \\ - EQ_TAC >> rw [] >> fs [] \\ - DISJ2_TAC \\ - Q.EXISTS_TAC ‘FV (VAR x)’ >> rw [] \\ - Q.EXISTS_TAC ‘VAR x’ >> rw []) - >> 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 = LAST Y’ - (* postfix for LAMl_ALPHA_ssub *) - >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’ - by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW - >> REWRITE_TAC [LAMl_SNOC] - >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’ - >- (simp [Abbr ‘M’, ssub_appstar] \\ - Know ‘fm ' z = VAR y’ - >- (rw [Abbr ‘fm’, Abbr ‘z’, LAST_EL] \\ - Know ‘fromPairs Z (MAP VAR Y) ' (EL (PRE (n + 1)) Z) = - EL (PRE (n + 1)) (MAP VAR Y)’ - >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\ - rw [EL_MAP, Abbr ‘y’, LAST_EL]) >> Rewr' \\ - Suff ‘MAP ($' fm) (MAP VAR (FRONT Z)) = MAP VAR (FRONT Y)’ >- rw [] \\ - rw [LIST_EQ_REWRITE, LENGTH_FRONT] \\ - ‘PRE (n + 1) = n’ by rw [] >> POP_ASSUM (fs o wrap) \\ - rename1 ‘i < n’ \\ - simp [EL_MAP, LENGTH_FRONT] \\ - Know ‘MEM (EL i (FRONT Z)) Z’ - >- (rw [MEM_EL] \\ - Q.EXISTS_TAC ‘i’ >> rw [] \\ - MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) \\ - rw [Abbr ‘fm’] \\ - Know ‘EL i (FRONT Z) = EL i Z’ - >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\ - Know ‘EL i (FRONT Y) = EL i Y’ - >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\ - 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]) - >> Rewr' - >> qabbrev_tac ‘vs = FRONT Y’ - >> Know ‘ALL_DISTINCT vs /\ ~MEM y vs’ - >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\ - ‘Y = SNOC y vs’ by METIS_TAC [SNOC_LAST_FRONT] >> POP_ORW \\ - rw [ALL_DISTINCT_SNOC]) - >> STRIP_TAC - >> MATCH_MP_TAC principle_hnf_permutator_lemma - >> ‘SNOC y vs = Y’ by METIS_TAC [SNOC_LAST_FRONT] >> POP_ORW - >> rw [EVERY_MEM, Abbr ‘vs’, LENGTH_FRONT] >- art [] - >> FIRST_X_ASSUM MATCH_MP_TAC - >> Q.EXISTS_TAC ‘e’ >> art [] + >> MATCH_MP_TAC permutator_hreduce_same_length >> art [] QED Theorem principle_hnf_tpm : diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml index 801839b0d5..ff2a07d3b6 100644 --- a/examples/lambda/basics/appFOLDLScript.sml +++ b/examples/lambda/basics/appFOLDLScript.sml @@ -161,6 +161,12 @@ Proof >> rw [appstar_APPEND] QED +Theorem appstar_SING[simp] : + M @* [N] = M @@ N +Proof + rw [GSYM appstar_CONS] +QED + Theorem ssub_appstar : fm ' (M @* Ns) = (fm ' M) @* MAP (ssub fm) Ns Proof @@ -174,6 +180,9 @@ Proof >> rw [appstar_SNOC, MAP_SNOC] QED +(* |- !args t sub. t @* args ISUB sub = (t ISUB sub) @* MAP (\t. t ISUB sub) args *) +Theorem appstar_ISUB = FOLDL_APP_ISUB + Theorem FV_appstar : !M Ns. FV (M @* Ns) = FV M UNION (BIGUNION (IMAGE FV (set Ns))) Proof diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml index a31897f39e..e840d34dd1 100644 --- a/examples/lambda/basics/termScript.sml +++ b/examples/lambda/basics/termScript.sml @@ -1,6 +1,7 @@ open HolKernel Parse boolLib bossLib; -open boolSimps arithmeticTheory pred_setTheory listTheory finite_mapTheory hurdUtils; +open boolSimps arithmeticTheory pred_setTheory listTheory finite_mapTheory + relationTheory pairTheory hurdUtils; open generic_termsTheory binderLib nomsetTheory nomdatatype; @@ -400,11 +401,11 @@ val subst_exists = `vr` |-> `\s (x,N). if s = x then N else VAR s`, `ap` |-> `\r1 r2 t1 t2 p. r1 p @@ r2 p`, `lm` |-> `\r v t p. LAM v (r p)`] - |> CONV_RULE (LAND_CONV (SIMP_CONV (srw_ss()) [pairTheory.FORALL_PROD])) + |> CONV_RULE (LAND_CONV (SIMP_CONV (srw_ss()) [FORALL_PROD])) |> SIMP_RULE (srw_ss()) [support_def, FUN_EQ_THM, fnpm_def, tpm_COND, tpm_fresh, pmact_sing_inv, basic_swapTheory.swapstr_eq_left] - |> SIMP_RULE (srw_ss()) [rewrite_pairing, pairTheory.FORALL_PROD] + |> SIMP_RULE (srw_ss()) [rewrite_pairing, FORALL_PROD] |> CONV_RULE (DEPTH_CONV (rename_vars [("p_1", "u"), ("p_2", "N")])) |> prove_alpha_fcbhyp {ppm = ``pair_pmact string_pmact ^t_pmact_t``, rwts = [], @@ -550,6 +551,12 @@ Theorem FV_SUB: Proof PROVE_TAC [lemma14b, lemma14c] QED +Theorem FV_SUB_SUBSET : + !t u v. closed t ==> FV ([t/v] u) SUBSET FV u +Proof + rw [FV_SUB, closed_def] +QED + Theorem lemma15a: !M. v ∉ FV M ==> [N/v]([VAR v/x]M) = [N/x]M Proof @@ -720,7 +727,7 @@ Theorem ISUB_LAM[simp] : !t. (LAM x t) ISUB R = LAM x (t ISUB R) Proof Induct - >> ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD, + >> ASM_SIMP_TAC (srw_ss()) [ISUB_def, FORALL_PROD, DOM_DEF, FVS_DEF, SUB_THM] QED @@ -734,7 +741,7 @@ Theorem ISUB_APPEND : !R1 R2 t:term. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2) Proof Induct - >> ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def] + >> ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, ISUB_def] QED (* moved here from standardisationScript.sml *) @@ -742,9 +749,10 @@ Theorem ISUB_APP : !sub M N. (M @@ N) ISUB sub = (M ISUB sub) @@ (N ISUB sub) Proof Induct - >> ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def, SUB_THM] + >> ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, ISUB_def, SUB_THM] QED +(* NOTE: This is actually appFOLDLTheory.appstar_ISUB *) Theorem FOLDL_APP_ISUB : !args (t:term) sub. FOLDL APP t args ISUB sub = @@ -753,6 +761,7 @@ Proof Induct >> SRW_TAC [][ISUB_APP] QED +(* NOTE: This is the basis of a "lemma14b" for ISUB, cf. ssub_14b *) Theorem ISUB_VAR_FRESH : !y sub. ~MEM y (MAP SND sub) ==> (VAR y ISUB sub = VAR y) Proof @@ -796,6 +805,20 @@ Proof >> Q.EXISTS_TAC ‘ss' ++ ss’ >> rw [] QED + +Theorem FV_ISUB_SUBSET : + !sub u. FVS sub = {} ==> FV (u ISUB sub) SUBSET FV u +Proof + Induct_on ‘sub’ >- rw [] + >> SIMP_TAC std_ss [FORALL_PROD] + >> rw [FVS_DEF, ISUB_def] + >> MATCH_MP_TAC SUBSET_TRANS + >> Q.EXISTS_TAC ‘FV ([p_1/p_2] u)’ + >> CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) + >> MATCH_MP_TAC FV_SUB_SUBSET + >> rw [closed_def] +QED + (* ---------------------------------------------------------------------- RENAMING: a special iterated substitutions like tpm ---------------------------------------------------------------------- *) @@ -846,7 +869,7 @@ Theorem size_ISUB : !R N:term. RENAMING R ==> (size (N ISUB R) = size N) Proof Induct THEN - ASM_SIMP_TAC (srw_ss())[ISUB_def, pairTheory.FORALL_PROD, + ASM_SIMP_TAC (srw_ss())[ISUB_def, FORALL_PROD, RENAMING_THM] THEN SRW_TAC [][] THEN SRW_TAC [][size_vsubst] QED @@ -1497,6 +1520,101 @@ Proof >> SET_TAC [] QED +(*---------------------------------------------------------------------------* + * ‘tpm’ as an equivalence relation between terms + *---------------------------------------------------------------------------*) + +Definition tpm_rel_def : + tpm_rel M N = ?pi. tpm pi M = N +End + +Theorem tpm_rel_alt : + !M N. tpm_rel M N <=> ?pi. M = tpm pi N +Proof + rw [tpm_rel_def] + >> EQ_TAC >> rpt STRIP_TAC + >| [ (* goal 1 (of 2) *) + fs [tpm_eql] >> Q.EXISTS_TAC ‘REVERSE pi’ >> rw [], + (* goal 2 (of 2) *) + fs [tpm_eqr] >> Q.EXISTS_TAC ‘REVERSE pi’ >> rw [] ] +QED + +Theorem equivalence_tpm_rel : + equivalence tpm_rel +Proof + rw [equivalence_def, reflexive_def, symmetric_def, transitive_def] + >| [ (* goal 1 (of 3) *) + rw [tpm_rel_def] >> Q.EXISTS_TAC ‘[]’ >> rw [], + (* goal 2 (of 3) *) + rw [tpm_rel_def] >> EQ_TAC >> rpt STRIP_TAC >| (* 2 subgoals *) + [ (* goal 2.1 (of 2) *) + ONCE_REWRITE_TAC [EQ_SYM_EQ] >> fs [tpm_eql] \\ + Q.EXISTS_TAC ‘REVERSE pi’ >> rw [], + (* goal 2.2 (of 2) *) + ONCE_REWRITE_TAC [EQ_SYM_EQ] >> fs [tpm_eql] \\ + Q.EXISTS_TAC ‘REVERSE pi’ >> rw [] ], + (* goal 3 (of 3) *) + fs [tpm_rel_def] \\ + POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ + POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ + Q.EXISTS_TAC ‘pi' ++ pi’ \\ + rw [pmact_decompose] ] +QED + +val tpm_rel_thm = equivalence_tpm_rel |> + REWRITE_RULE [equivalence_def, reflexive_def, symmetric_def, transitive_def]; + +(* below are easy-to-use forms of [equivalence_tpm_rel] *) +Theorem tpm_rel_REFL[simp] : + tpm_rel M M +Proof + rw [tpm_rel_thm] +QED + +Theorem tpm_rel_SYM : + !M N. tpm_rel M N ==> tpm_rel N M +Proof + rw [tpm_rel_thm] +QED + +Theorem tpm_rel_SYM_EQ : + !M N. tpm_rel M N <=> tpm_rel N M +Proof + rw [tpm_rel_thm] +QED + +Theorem tpm_rel_TRANS : + !M1 M2 M3. tpm_rel M1 M2 /\ tpm_rel M2 M3 ==> tpm_rel M1 M3 +Proof + rpt STRIP_TAC + >> MATCH_MP_TAC (cj 3 tpm_rel_thm) + >> Q.EXISTS_TAC ‘M2’ >> art [] +QED + +Theorem tpm_rel_tpm[simp] : + tpm_rel (tpm pi M) M /\ tpm_rel M (tpm pi M) +Proof + CONJ_ASM1_TAC + >- (REWRITE_TAC [tpm_rel_alt] \\ + Q.EXISTS_TAC ‘pi’ >> REWRITE_TAC []) + >> MATCH_MP_TAC tpm_rel_SYM >> art [] +QED + +Theorem tpm_rel_cong : + !M M' N N'. tpm_rel M M' /\ tpm_rel N N' ==> (tpm_rel M N <=> tpm_rel M' N') +Proof + rpt STRIP_TAC + >> EQ_TAC >> STRIP_TAC + >| [ (* goal 1 (of 2) *) + MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\ + MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘M’ >> art [] \\ + MATCH_MP_TAC tpm_rel_SYM >> art [], + (* goal 2 (of 2) *) + MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘M'’ >> art [] \\ + MATCH_MP_TAC tpm_rel_TRANS >> Q.EXISTS_TAC ‘N'’ >> art [] \\ + MATCH_MP_TAC tpm_rel_SYM >> art [] ] +QED + (* ---------------------------------------------------------------------- Set up the recursion functionality in binderLib ---------------------------------------------------------------------- *) @@ -1506,7 +1624,7 @@ val lemma = prove( ∀pi t. pmact apm pi (h t) = h (tpm pi t)``, simp_tac (srw_ss()) [EQ_IMP_THM] >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> strip_tac >> Induct_on `pi` >> - asm_simp_tac (srw_ss()) [pmact_nil, pairTheory.FORALL_PROD] >> + asm_simp_tac (srw_ss()) [pmact_nil, FORALL_PROD] >> srw_tac [][Once tpm_CONS] >> srw_tac [][GSYM pmact_decompose]); val tm_recursion_nosideset = save_thm( diff --git a/examples/lambda/completeness/boehm_treeScript.sml b/examples/lambda/completeness/boehm_treeScript.sml deleted file mode 100644 index c3af83eb44..0000000000 --- a/examples/lambda/completeness/boehm_treeScript.sml +++ /dev/null @@ -1,37 +0,0 @@ -(*---------------------------------------------------------------------------* - * boehm_treeScript.sml: (Effective) Boehm Trees (Chapter 10 of [1]) * - *---------------------------------------------------------------------------*) - -open HolKernel boolLib Parse bossLib; - -(* core theories *) -open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory - llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils; - -open basic_swapTheory binderLib termTheory appFOLDLTheory chap2Theory - chap3Theory head_reductionTheory standardisationTheory solvableTheory; - -open pure_dBTheory; - -val _ = new_theory "boehm_tree"; - -val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]; -val o_DEF = combinTheory.o_DEF; (* cannot directly open combinTheory *) - -(* A dB-term M is hnf if its corresponding Lambda term is hnf *) -Overload dhnf = “\M. hnf (toTerm M)” - -Theorem dhnf_fromTerm[simp] : - !M. dhnf (fromTerm M) <=> hnf M -Proof - rw [o_DEF] -QED - -val _ = export_theory (); -val _ = html_theory "boehm_tree"; - -(* References: - - [1] Barendregt, H.P.: The lambda calculus, its syntax and semantics. - College Publications, London (1984). - *) diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml index 8330c88805..e366b87240 100644 --- a/src/coalgebras/ltreeScript.sml +++ b/src/coalgebras/ltreeScript.sml @@ -13,10 +13,14 @@ open HolKernel Parse boolLib bossLib; open arithmeticTheory listTheory llistTheory alistTheory optionTheory; open pred_setTheory relationTheory pairTheory combinTheory hurdUtils; +(* for ltree_el_alt_ltree_lookup *) +open monadsyntax; +val _ = enable_monadsyntax (); +val _ = enable_monad "option"; + val _ = new_theory "ltree"; (* make type definition *) - Type ltree_rep[local] = ``:num list -> 'a # num option``; Overload NOTHING[local] = ``(ARB:'a, SOME (0:num))``; @@ -910,6 +914,30 @@ Proof rw [ltree_lookup_iff_ltree_el, ltree_el_valid_inclusive] QED +(* ltree_lookup returns more information (the entire subtree), thus can be + used to construct the return value of ltree_el. + *) +Theorem ltree_el_alt_ltree_lookup : + !p t. p IN ltree_paths t ==> + ltree_el t p = + do + t' <- ltree_lookup t p; + return (ltree_node t',LLENGTH (ltree_children t')) + od +Proof + Induct_on ‘p’ + >- (Q.X_GEN_TAC ‘t’ \\ + STRIP_ASSUME_TAC (Q.SPEC ‘t’ ltree_cases) >> POP_ORW \\ + rw [ltree_el_def, ltree_lookup_def]) + >> qx_genl_tac [‘h’, ‘t’] + >> STRIP_ASSUME_TAC (Q.SPEC ‘t’ ltree_cases) >> POP_ORW + >> fs [ltree_paths_def] + >> rw [ltree_el_def, ltree_lookup_def] + >> qabbrev_tac ‘t' = LNTH h ts’ + >> Cases_on ‘t' = NONE’ >- rw [] + >> gs [GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS] +QED + (*---------------------------------------------------------------------------* * Rose tree is a finite variant of ltree, defined inductively. *---------------------------------------------------------------------------*) diff --git a/src/coretypes/optionScript.sml b/src/coretypes/optionScript.sml index d219f740da..a74c263627 100644 --- a/src/coretypes/optionScript.sml +++ b/src/coretypes/optionScript.sml @@ -242,6 +242,12 @@ Proof THEN ASM_REWRITE_TAC option_rws QED +Theorem IS_SOME_EQ_NOT_NONE : + !x. IS_SOME x <=> x <> NONE +Proof + REWRITE_TAC [GSYM NOT_IS_SOME_EQ_NONE] +QED + val IS_SOME_EQ_EXISTS = Q.prove( `!x. IS_SOME x = (?v. x = SOME v)`, GEN_TAC diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml index 2089344f0c..d204e5cfb1 100644 --- a/src/list/src/rich_listScript.sml +++ b/src/list/src/rich_listScript.sml @@ -42,6 +42,11 @@ val list_INDUCT = Q.prove( val LIST_INDUCT_TAC = INDUCT_THEN list_INDUCT ASSUME_TAC; val SNOC_INDUCT_TAC = Prim_rec.INDUCT_THEN SNOC_INDUCT ASSUME_TAC; +fun wrap a = [a]; +val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); +val Know = Q_TAC KNOW_TAC; +val Suff = Q_TAC SUFF_TAC; + (* ------------------------------------------------------------------------ *) val ELL = DEF0` @@ -2697,9 +2702,6 @@ val prefixes_is_prefix_total = Q.store_thm("prefixes_is_prefix_total", GEN_TAC THEN Cases THEN SIMP_TAC(srw_ss())[] THEN Cases THEN SRW_TAC[][]) -val Know = Q_TAC KNOW_TAC; -val Suff = Q_TAC SUFF_TAC; - Theorem IS_PREFIX_EQ_TAKE : !l l1. l1 <<= l <=> ?n. n <= LENGTH l /\ l1 = TAKE n l Proof @@ -4644,6 +4646,18 @@ val TAKE_DROP_SWAP = store_thm( rw[] ]); +(* cf. TAKE_DROP |- !n l. TAKE n l ++ DROP n l = l *) +Theorem TAKE_DROP_SUC : + !n l. n < LENGTH l ==> TAKE n l ++ [EL n l] ++ DROP (SUC n) l = l +Proof + rpt STRIP_TAC + >> REWRITE_TAC [GSYM APPEND_ASSOC, Once EQ_SYM_EQ] + >> ‘l = TAKE n l ++ DROP n l’ by rw [TAKE_DROP] + >> POP_ASSUM + (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites o wrap) + >> RW_TAC bool_ss [DROP_BY_DROP_SUC, GSYM CONS_APPEND] +QED + (* Theorem: TAKE (LENGTH l1) (LUPDATE x (LENGTH l1 + k) (l1 ++ l2)) = l1 *) (* Proof: TAKE (LENGTH l1) (LUPDATE x (LENGTH l1 + k) (l1 ++ l2))