diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml index c621bb499e..4e4ea5f2b6 100644 --- a/examples/lambda/barendregt/boehmScript.sml +++ b/examples/lambda/barendregt/boehmScript.sml @@ -2762,7 +2762,7 @@ Proof >> ‘LENGTH as = d - m’ by rw [Abbr ‘as’, LENGTH_FRONT] >> qabbrev_tac ‘b = LAST l’ >> Know ‘l = SNOC b as’ - >- (ASM_SIMP_TAC std_ss [Abbr ‘as’, Abbr ‘b’, SNOC_LAST_FRONT]) + >- (ASM_SIMP_TAC std_ss [Abbr ‘as’, Abbr ‘b’, SNOC_OF_LAST_FRONT]) >> DISCH_TAC >> qabbrev_tac ‘p3 = MAP rightctxt (REVERSE (MAP VAR l))’ >> ‘Boehm_transform p3’ by rw [Abbr ‘p3’, MAP_MAP_o, GSYM MAP_REVERSE] @@ -3342,7 +3342,7 @@ Proof Know ‘LAMl Z (VAR z) = LAMl (FRONT Z) (LAM z (VAR z))’ >- (REWRITE_TAC [GSYM LAMl_SNOC] \\ Suff ‘SNOC z (FRONT Z) = Z’ >- Rewr \\ - qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_LAST_FRONT >> art []) >> Rewr' \\ + qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) >> Rewr' \\ REWRITE_TAC [appstar_APPEND] \\ qabbrev_tac ‘t :term = LAM z (VAR z)’ \\ MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘t @* MAP VAR vs’ \\ @@ -3369,7 +3369,7 @@ Proof Know ‘LAMl Z (VAR z) = LAMl (FRONT Z) (LAM z (VAR z))’ >- (REWRITE_TAC [GSYM LAMl_SNOC] \\ Suff ‘SNOC z (FRONT Z) = Z’ >- Rewr \\ - qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_LAST_FRONT >> art []) >> Rewr' \\ + qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) >> Rewr' \\ Know ‘args2' ++ MAP VAR vs = SNOC (VAR b0) (args2' ++ MAP VAR (FRONT vs))’ >- (qunabbrev_tac ‘b0’ \\ Know ‘VAR (LAST bs) :term = LAST (MAP VAR vs)’ @@ -3379,7 +3379,7 @@ Proof MATCH_MP_TAC (GSYM FRONT_APPEND_NOT_NIL) >> rw []) >> Rewr' \\ Suff ‘LAST (MAP VAR vs) = LAST (args2' ++ MAP VAR vs)’ >- (Rewr' >> qabbrev_tac ‘l = args2' ++ MAP VAR vs’ \\ - MATCH_MP_TAC (GSYM SNOC_LAST_FRONT) >> rw [Abbr ‘l’]) \\ + MATCH_MP_TAC SNOC_LAST_FRONT >> rw [Abbr ‘l’]) \\ MATCH_MP_TAC (GSYM LAST_APPEND_NOT_NIL) >> rw []) >> Rewr' \\ REWRITE_TAC [appstar_SNOC] \\ qabbrev_tac ‘t :term = LAM z (VAR z)’ \\ diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 9b383a7bd2..adee2e9ba3 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -1225,7 +1225,7 @@ Proof >- (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] \\ + ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] \\ POP_ORW \\ simp [LIST_TO_SET_SNOC] \\ rw [Once EXTENSION, MEM_MAP] \\ @@ -1241,7 +1241,7 @@ Proof >> 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 + by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_OF_LAST_FRONT]) >> POP_ORW >> REWRITE_TAC [LAMl_SNOC] >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’ >- (simp [Abbr ‘M’, ssub_appstar] \\ diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml index 5d295c27cc..1ab3be1d79 100644 --- a/examples/lambda/barendregt/chap3Script.sml +++ b/examples/lambda/barendregt/chap3Script.sml @@ -1164,6 +1164,13 @@ val beta_eta_lameta = store_thm( ] ]); +(* |- !M N. + lameta M N ==> ?Z. reduction (beta RUNION eta) M Z /\ + reduction (beta RUNION eta) N Z + *) +Theorem lameta_CR = REWRITE_RULE [beta_eta_lameta, beta_eta_CR] + (Q.SPEC ‘beta RUNION eta’ theorem3_13) + val beta_eta_normal_form_benf = store_thm( "beta_eta_normal_form_benf", ``normal_form (beta RUNION eta) = benf``, diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml index cae85908dd..2687d1e2ed 100644 --- a/examples/lambda/barendregt/head_reductionScript.sml +++ b/examples/lambda/barendregt/head_reductionScript.sml @@ -1654,7 +1654,7 @@ Theorem lameq_hnf_fresh_subst : Proof Induct_on ‘as’ using SNOC_INDUCT >> rw [] >> Cases_on ‘args = []’ >- fs [] - >> ‘args = SNOC (LAST args) (FRONT args)’ by PROVE_TAC [SNOC_LAST_FRONT] + >> ‘args = SNOC (LAST args) (FRONT args)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] >> POP_ORW >> REWRITE_TAC [appstar_SNOC, SUB_THM] >> MATCH_MP_TAC lameq_TRANS @@ -1951,7 +1951,7 @@ Proof >- (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] \\ + ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] \\ POP_ORW \\ simp [LIST_TO_SET_SNOC] \\ rw [Once EXTENSION, MEM_MAP] \\ @@ -1966,7 +1966,7 @@ Proof >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’] >> qabbrev_tac ‘y = LAST Y’ >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’ - by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW + by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_OF_LAST_FRONT]) >> POP_ORW >> REWRITE_TAC [LAMl_SNOC] >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’ >- (simp [Abbr ‘M’, ssub_appstar] \\ @@ -2066,7 +2066,7 @@ Proof Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\ Know ‘SNOC y vs = Y’ >- (qunabbrevl_tac [‘y’, ‘vs’] \\ - MATCH_MP_TAC SNOC_LAST_FRONT >> art []) \\ + MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) \\ DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\ rw [ALL_DISTINCT_SNOC] >- (qunabbrev_tac ‘vs1’ >> PROVE_TAC [MEM_TAKE]) \\ @@ -2094,7 +2094,7 @@ Proof >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\ Know ‘SNOC y vs = Y’ >- (qunabbrevl_tac [‘y’, ‘vs’] \\ - MATCH_MP_TAC SNOC_LAST_FRONT >> art []) \\ + MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) \\ DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\ rw [ALL_DISTINCT_SNOC] \\ qunabbrev_tac ‘vs1’ >> PROVE_TAC [MEM_TAKE]) @@ -2139,7 +2139,7 @@ Proof Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\ Know ‘SNOC y vs = Y’ >- (qunabbrevl_tac [‘y’, ‘vs’] \\ - MATCH_MP_TAC SNOC_LAST_FRONT >> art []) \\ + MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) \\ DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\ rw [ALL_DISTINCT_SNOC] \\ CCONTR_TAC >> fs [Abbr ‘vs2’] \\ diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml index 0c6d1800ad..d5c5233be1 100644 --- a/examples/lambda/barendregt/solvableScript.sml +++ b/examples/lambda/barendregt/solvableScript.sml @@ -1610,7 +1610,7 @@ Proof >- (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] \\ + ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] \\ POP_ORW \\ simp [LIST_TO_SET_SNOC] \\ rw [Once EXTENSION, MEM_MAP] \\ @@ -1626,7 +1626,7 @@ Proof >> 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 + by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_OF_LAST_FRONT]) >> POP_ORW >> REWRITE_TAC [LAMl_SNOC] >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’ >- (simp [Abbr ‘M’, ssub_appstar] \\ @@ -1657,11 +1657,11 @@ Proof >> 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 \\ + ‘Y = SNOC y vs’ by METIS_TAC [SNOC_OF_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 + >> ‘SNOC y vs = Y’ by METIS_TAC [SNOC_OF_LAST_FRONT] >> POP_ORW >> rw [EVERY_MEM, Abbr ‘vs’, LENGTH_FRONT] >- art [] >> FIRST_X_ASSUM MATCH_MP_TAC >> Q.EXISTS_TAC ‘e’ >> art []