Skip to content

Commit f5e5217

Browse files
binghemn200
binghe
authored and
mn200
committed
[lambda] The "congruence" of subterm properties w.r.t different excluded lists
1 parent 1033d02 commit f5e5217

File tree

5 files changed

+442
-4
lines changed

5 files changed

+442
-4
lines changed

‎examples/lambda/barendregt/boehmScript.sml

Lines changed: 324 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@
22
* boehmScript.sml: (Effective) Boehm Trees (Chapter 10 of [1]) *
33
*---------------------------------------------------------------------------*)
44

5-
open HolKernel boolLib Parse bossLib;
5+
open HolKernel boolLib Parse bossLib BasicProvers;
66

77
(* core theories *)
88
open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory
99
llistTheory relationTheory ltreeTheory pathTheory posetTheory hurdUtils
1010
finite_mapTheory;
1111

12-
open binderLib termTheory appFOLDLTheory chap2Theory chap3Theory
12+
open binderLib termTheory appFOLDLTheory chap2Theory chap3Theory nomsetTheory
1313
head_reductionTheory standardisationTheory solvableTheory reductionEval;
1414

1515
open horeductionTheory takahashiS3Theory;
@@ -207,7 +207,7 @@ Proof
207207
>> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
208208
(* applying ltree_bisimulation *)
209209
>> rw [ltree_bisimulation]
210-
(* NOTE: ‘solvable P /\ solvable Q’ cannot be added into the next relation *)
210+
(* NOTE: ‘solvable P /\ solvable Q’ cannot be added here *)
211211
>> Q.EXISTS_TAC ‘\x y. ?P Q Y. FINITE Y /\ FV P UNION FV Q SUBSET Y /\
212212
P == Q /\ x = BTe Y P /\ y = BTe Y Q’
213213
>> BETA_TAC
@@ -570,6 +570,48 @@ Proof
570570
>> Cases_on ‘p'’ >> fs [subterm_def]
571571
QED
572572

573+
Theorem subterm_solvable_lemma :
574+
!X M p. FINITE X /\ p <> [] /\
575+
p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==>
576+
(!q. q <<= p ==> subterm X M q <> NONE) /\
577+
(!q. q <<= FRONT p ==> solvable (subterm' X M q))
578+
Proof
579+
rpt GEN_TAC >> STRIP_TAC
580+
>> CONJ_ASM1_TAC
581+
>- (Q.X_GEN_TAC ‘q’ >> DISCH_TAC \\
582+
CCONTR_TAC \\
583+
POP_ASSUM (MP_TAC o (REWRITE_RULE [Once subterm_is_none_iff_children])) \\
584+
DISCH_THEN (MP_TAC o (Q.SPEC ‘p’)) >> rw [])
585+
>> ‘0 < LENGTH p’ by rw [GSYM NOT_NIL_EQ_LENGTH_NOT_0]
586+
>> Q.X_GEN_TAC ‘q’
587+
>> Suff ‘!l. l <> [] /\ l <<= p ==> solvable (subterm' X M (FRONT l))’
588+
>- (DISCH_TAC \\
589+
DISCH_THEN (STRIP_ASSUME_TAC o (REWRITE_RULE [IS_PREFIX_EQ_TAKE])) \\
590+
Know ‘q = FRONT (TAKE (SUC n) p)’
591+
>- (Know ‘FRONT (TAKE (SUC n) p) = TAKE (SUC n - 1) p’
592+
>- (MATCH_MP_TAC FRONT_TAKE \\
593+
rfs [LENGTH_FRONT]) >> Rewr' \\
594+
POP_ASSUM (ONCE_REWRITE_TAC o wrap) >> simp [] \\
595+
MATCH_MP_TAC TAKE_FRONT >> rfs [LENGTH_FRONT]) >> Rewr' \\
596+
FIRST_X_ASSUM MATCH_MP_TAC \\
597+
qabbrev_tac ‘l = TAKE (SUC n) p’ \\
598+
CONJ_TAC
599+
>- (rfs [LENGTH_FRONT, NOT_NIL_EQ_LENGTH_NOT_0, Abbr ‘l’, LENGTH_TAKE]) \\
600+
rw [IS_PREFIX_EQ_TAKE] \\
601+
Q.EXISTS_TAC ‘SUC n’ >> rw [Abbr ‘l’] \\
602+
rfs [LENGTH_FRONT])
603+
>> rpt STRIP_TAC
604+
>> MP_TAC (Q.SPECL [‘l’, ‘X’, ‘M’] subterm_is_none_iff_parent_unsolvable)
605+
>> ‘l IN ltree_paths (BTe X M)’ by PROVE_TAC [ltree_paths_inclusive]
606+
>> simp []
607+
>> Suff ‘subterm X M (FRONT l) <> NONE’ >- PROVE_TAC []
608+
>> FIRST_X_ASSUM MATCH_MP_TAC
609+
>> MATCH_MP_TAC IS_PREFIX_TRANS
610+
>> Q.EXISTS_TAC ‘l’ >> rw []
611+
>> MATCH_MP_TAC IS_PREFIX_BUTLAST' >> art []
612+
QED
613+
614+
(* NOTE: cf. [subterm_some_none_cong] when X changes but M remains *)
573615
Theorem lameq_subterm_cong_none :
574616
!p X M N. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==>
575617
(subterm X M p = NONE <=> subterm X N p = NONE)
@@ -794,6 +836,226 @@ Proof
794836
qunabbrev_tac ‘M0'’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [] ]
795837
QED
796838

839+
(* NOTE: This lemma is more general than subterm_tpm_cong, which cannot be
840+
directly proved. The current statements of this lemma, suitable for doing
841+
induction, were due to repeated experiments. -- Chun Tian, 19 feb 2024.
842+
*)
843+
Theorem subterm_tpm_lemma :
844+
!p X Y M pi. FINITE X /\ FINITE Y ==>
845+
(subterm X M p = NONE ==> subterm Y (tpm pi M) p = NONE) /\
846+
(subterm X M p <> NONE ==>
847+
?pi'. tpm pi' (subterm' X M p) = subterm' Y (tpm pi M) p)
848+
Proof
849+
Induct_on ‘p’
850+
>- (rw [] >> Q.EXISTS_TAC ‘pi’ >> rw [])
851+
>> rpt GEN_TAC >> STRIP_TAC
852+
>> reverse (Cases_on ‘solvable M’)
853+
>- (‘unsolvable (tpm pi M)’ by PROVE_TAC [solvable_tpm] \\
854+
simp [subterm_def])
855+
>> ‘solvable (tpm pi M)’ by PROVE_TAC [solvable_tpm]
856+
(* BEGIN Michael Norrish's tactics *)
857+
>> CONV_TAC (UNBETA_CONV “subterm X M (h::p)”)
858+
>> qmatch_abbrev_tac ‘P _’
859+
>> RW_TAC bool_ss [subterm_of_solvables]
860+
>> simp [Abbr ‘P’]
861+
(* END Michael Norrish's tactics.
862+
preparing for expanding ‘subterm' Y (tpm pi M) (h::p)’ *)
863+
>> qabbrev_tac ‘M0' = principle_hnf (tpm pi M)’
864+
>> Know ‘M0' = tpm pi M0’
865+
>- (qunabbrevl_tac [‘M0’, ‘M0'’] \\
866+
MATCH_MP_TAC principle_hnf_tpm' >> art [])
867+
>> DISCH_TAC
868+
>> qabbrev_tac ‘m' = hnf_children_size M0'’
869+
>> Know ‘m' = m’ >- (rw [Abbr ‘m’, Abbr ‘m'’, hnf_children_size_tpm])
870+
>> DISCH_TAC
871+
>> qabbrev_tac ‘n' = LAMl_size M0'’
872+
>> Know ‘n' = n’ >- (rw [Abbr ‘n’, Abbr ‘n'’, LAMl_size_tpm])
873+
>> DISCH_TAC
874+
(* special case *)
875+
>> reverse (Cases_on ‘h < m’)
876+
>- (rw [] >> rw [subterm_of_solvables])
877+
(* stage work, now h < m *)
878+
>> simp [] (* eliminate ‘h < m’ in the goal *)
879+
(* BEGIN Michael Norrish's tactics, again *)
880+
>> CONV_TAC (UNBETA_CONV “subterm Y (tpm pi M) (h::p)”)
881+
>> qmatch_abbrev_tac ‘P _’
882+
>> RW_TAC bool_ss [subterm_of_solvables]
883+
>> simp [Abbr ‘P’]
884+
(* END Michael Norrish's tactics. *)
885+
>> Q.PAT_X_ASSUM ‘tpm pi M0 = principle_hnf (tpm pi M)’ (rfs o wrap o SYM)
886+
>> Q.PAT_X_ASSUM ‘n = n'’ (fs o wrap o SYM)
887+
>> Q.PAT_X_ASSUM ‘n = n''’ (fs o wrap o SYM)
888+
>> Q.PAT_X_ASSUM ‘m' = m''’ (fs o wrap o SYM)
889+
>> Q.PAT_X_ASSUM ‘m = m'’ (fs o wrap o SYM)
890+
(* stage work *)
891+
>> Know ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (X UNION FV M0) /\ LENGTH vs = n’
892+
>- rw [Abbr ‘vs’, FRESH_list_def]
893+
>> DISCH_THEN (STRIP_ASSUME_TAC o (REWRITE_RULE [DISJOINT_UNION']))
894+
>> Know ‘ALL_DISTINCT vs' /\ DISJOINT (set vs') (Y UNION FV (tpm pi M0)) /\
895+
LENGTH vs' = n’
896+
>- rw [Abbr ‘vs'’, FRESH_list_def]
897+
>> DISCH_THEN (STRIP_ASSUME_TAC o (REWRITE_RULE [DISJOINT_UNION']))
898+
(* vs1p is a permutated version of vs', to be used as first principles *)
899+
>> qabbrev_tac ‘vs1p = listpm string_pmact (REVERSE pi) vs'’
900+
>> ‘ALL_DISTINCT vs1p’ by rw [Abbr ‘vs1p’]
901+
(* rewriting inside the abbreviation of M1' *)
902+
>> Know ‘tpm pi M0 @* MAP VAR vs' = tpm pi (M0 @* MAP VAR vs1p)’
903+
>- (rw [Abbr ‘vs1p’, tpm_appstar] \\
904+
Suff ‘listpm term_pmact pi (MAP VAR (listpm string_pmact (REVERSE pi) vs')) =
905+
MAP VAR vs'’ >- rw [] \\
906+
rw [LIST_EQ_REWRITE, EL_MAP])
907+
>> DISCH_THEN (fs o wrap)
908+
(* prove that ‘M0 @* MAP VAR vs1p’ correctly denude M0
909+
910+
NOTE: ‘DISJOINT (set vs1p) X’ seems NOT true (but seems not needed)
911+
*)
912+
>> Know ‘DISJOINT (set vs1p) (FV M0)’
913+
>- (rw [Abbr ‘vs1p’, DISJOINT_ALT', MEM_listpm] \\
914+
Q.PAT_X_ASSUM ‘DISJOINT (set vs') (FV (tpm pi M0))’ MP_TAC \\
915+
rw [DISJOINT_ALT', FV_tpm])
916+
>> DISCH_TAC
917+
>> ‘LENGTH vs1p = n’ by rw [Abbr ‘vs1p’, LENGTH_listpm]
918+
(* now create Z and vs2
919+
920+
Z is the union of all known variables so far, no harm to include even more.
921+
*)
922+
>> qabbrev_tac ‘Z = X UNION Y UNION FV M0 UNION set vs UNION set vs1p’
923+
>> ‘FINITE Z’ by rw [Abbr ‘Z’]
924+
>> qabbrev_tac ‘vs2 = FRESH_list n Z’
925+
>> Know ‘ALL_DISTINCT vs2 /\ DISJOINT (set vs2) Z /\ LENGTH vs2 = n’
926+
>- rw [Abbr ‘vs2’, FRESH_list_def]
927+
>> Q.PAT_X_ASSUM ‘FINITE Z’ K_TAC
928+
>> qunabbrev_tac ‘Z’
929+
>> DISCH_THEN (STRIP_ASSUME_TAC o (REWRITE_RULE [DISJOINT_UNION']))
930+
(* stage work *)
931+
>> ‘hnf M0’ by PROVE_TAC [hnf_principle_hnf']
932+
>> hnf_tac (“M0 :term”, “vs2 :string list”,
933+
“M2 :term”, “y :string”, “args :term list”)
934+
>> ‘TAKE n vs2 = vs2’ by rw [TAKE_LENGTH_ID_rwt]
935+
>> POP_ASSUM (rfs o wrap)
936+
>> ‘hnf M2’ by rw [hnf_appstar]
937+
>> Know ‘DISJOINT (set vs) (FV M2) /\
938+
DISJOINT (set vs1p) (FV M2)’
939+
>- (rpt CONJ_TAC (* 2 subgoals, same tactics *) \\
940+
(MATCH_MP_TAC DISJOINT_SUBSET \\
941+
Q.EXISTS_TAC ‘FV M0 UNION set vs2’ \\
942+
CONJ_TAC >- (Q.PAT_X_ASSUM ‘M0 = LAMl vs2 (VAR y @* args)’ K_TAC \\
943+
reverse (rw [DISJOINT_UNION']) >- rw [Once DISJOINT_SYM] \\
944+
MATCH_MP_TAC DISJOINT_SUBSET \\
945+
Q.EXISTS_TAC ‘FV M’ >> art []) \\
946+
‘FV M0 UNION set vs2 = FV (M0 @* MAP VAR vs2)’ by rw [] >> POP_ORW \\
947+
qunabbrev_tac ‘M2’ \\
948+
MATCH_MP_TAC principle_hnf_FV_SUBSET' \\
949+
Know ‘solvable (VAR y @* args)’
950+
>- (rw [solvable_iff_has_hnf] \\
951+
MATCH_MP_TAC hnf_has_hnf \\
952+
rw [hnf_appstar]) >> DISCH_TAC \\
953+
Suff ‘M0 @* MAP VAR vs2 == VAR y @* args’
954+
>- PROVE_TAC [lameq_solvable_cong] \\
955+
rw [lameq_LAMl_appstar_VAR]))
956+
>> STRIP_TAC
957+
(* rewriting M1 and M1' (much harder) by tpm of M2 *)
958+
>> Know ‘M1 = tpm (ZIP (vs2,vs)) M2’
959+
>- (simp [Abbr ‘M1’] \\
960+
MATCH_MP_TAC principle_hnf_LAMl_appstar \\
961+
Q.PAT_X_ASSUM ‘M2 = VAR y @* args’ (ONCE_REWRITE_TAC o wrap o SYM) >> art [])
962+
>> DISCH_TAC
963+
>> qabbrev_tac ‘p1 = ZIP (vs2,vs)’
964+
>> Know ‘M1' = tpm pi (principle_hnf (M0 @* MAP VAR vs1p))’
965+
>- (qunabbrev_tac ‘M1'’ \\
966+
MATCH_MP_TAC principle_hnf_tpm >> art [] \\
967+
REWRITE_TAC [has_hnf_thm] \\
968+
Q.EXISTS_TAC ‘(FEMPTY |++ ZIP (vs2,MAP VAR vs1p)) ' (VAR y @* args)’ \\
969+
CONJ_TAC
970+
>- (MATCH_MP_TAC hreduce_LAMl_appstar \\
971+
rw [EVERY_MEM, MEM_MAP] >> rw [] \\
972+
Q.PAT_X_ASSUM ‘DISJOINT (set vs2) (set vs1p)’ MP_TAC \\
973+
rw [DISJOINT_ALT']) \\
974+
REWRITE_TAC [GSYM fromPairs_def] \\
975+
‘FDOM (fromPairs vs2 (MAP VAR vs1p)) = set vs2’ by rw [FDOM_fromPairs] \\
976+
Cases_on ‘MEM y vs2’
977+
>- (simp [ssub_thm, ssub_appstar, hnf_appstar] \\
978+
fs [MEM_EL] >> rename1 ‘i < LENGTH vs2’ \\
979+
Know ‘fromPairs vs2 (MAP VAR vs1p) ' (EL i vs2) = EL i (MAP VAR vs1p)’
980+
>- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
981+
rw [EL_MAP]) \\
982+
simp [ssub_thm, ssub_appstar, hnf_appstar])
983+
>> DISCH_TAC
984+
>> Know ‘M1' = tpm pi (tpm (ZIP (vs2,vs1p)) M2)’
985+
>- (POP_ORW >> simp [] \\
986+
MATCH_MP_TAC principle_hnf_LAMl_appstar \\
987+
Q.PAT_X_ASSUM ‘M2 = VAR y @* args’ (ONCE_REWRITE_TAC o wrap o SYM) >> art [])
988+
>> POP_ASSUM K_TAC (* M1' = ... (already used) *)
989+
>> REWRITE_TAC [GSYM pmact_decompose]
990+
>> qabbrev_tac ‘p2 = pi ++ ZIP (vs2,vs1p)’
991+
>> DISCH_TAC
992+
(* cleanups, the definition details of vs2 are useless *)
993+
>> Q.PAT_X_ASSUM ‘Abbrev (vs2 = _)’ K_TAC
994+
(* applying hnf_children_tpm *)
995+
>> Know ‘Ms = MAP (tpm p1) args’
996+
>- (simp [Abbr ‘Ms’] \\
997+
‘hnf_children M2 = args’ by rw [hnf_children_hnf] \\
998+
Q.PAT_X_ASSUM ‘M2 = VAR y @* args’ (ONCE_REWRITE_TAC o wrap o SYM) \\
999+
rw [hnf_children_tpm])
1000+
>> Rewr'
1001+
>> Know ‘Ms' = MAP (tpm p2) args’
1002+
>- (simp [Abbr ‘Ms'’] \\
1003+
‘hnf_children M2 = args’ by rw [hnf_children_hnf] \\
1004+
Q.PAT_X_ASSUM ‘M2 = VAR y @* args’ (ONCE_REWRITE_TAC o wrap o SYM) \\
1005+
rw [hnf_children_tpm])
1006+
>> Rewr'
1007+
>> ‘LENGTH args = m’ by rw [Abbr ‘m’]
1008+
>> simp [EL_MAP]
1009+
>> qabbrev_tac ‘N = EL h args’
1010+
(* final stage *)
1011+
>> Know ‘?pi'. tpm p2 N = tpm pi' (tpm p1 N)’
1012+
>- (Q.EXISTS_TAC ‘p2 ++ REVERSE p1’ \\
1013+
rw [pmact_decompose])
1014+
>> STRIP_TAC
1015+
>> POP_ORW
1016+
>> qabbrev_tac ‘N' = tpm p1 N’
1017+
(* finally, using IH *)
1018+
>> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
1019+
QED
1020+
1021+
(* NOTE: since ‘subterm X M p’ is correct for whatever X supplied, changing ‘X’ to
1022+
something else shouldn't change the properties of ‘subterm X M p’, as long as
1023+
these properties are not directly related to specific choices of ‘vs’.
1024+
*)
1025+
Theorem subterm_tpm_cong :
1026+
!p X Y M. FINITE X /\ FINITE Y ==>
1027+
(subterm X M p = NONE <=> subterm Y M p = NONE) /\
1028+
(subterm X M p <> NONE ==> ?pi. tpm pi (subterm' X M p) = subterm' Y M p)
1029+
Proof
1030+
rpt GEN_TAC >> STRIP_TAC
1031+
>> CONJ_ASM1_TAC
1032+
>- (EQ_TAC >> DISCH_TAC >| (* 2 subgoals *)
1033+
[ (* goal 1 (of 2) *)
1034+
MP_TAC (Q.SPECL [‘p’, ‘X’, ‘Y’, ‘M’, ‘[]’] subterm_tpm_lemma) >> rw [],
1035+
(* goal 2 (of 2) *)
1036+
MP_TAC (Q.SPECL [‘p’, ‘Y’, ‘X’, ‘M’, ‘[]’] subterm_tpm_lemma) >> rw [] ])
1037+
>> DISCH_TAC
1038+
>> MP_TAC (Q.SPECL [‘p’, ‘X’, ‘Y’, ‘M’, ‘[]’] (cj 2 subterm_tpm_lemma))
1039+
>> rw []
1040+
QED
1041+
1042+
(* In this way, two such terms have the same ‘hnf_children_size o principle_hnf’,
1043+
because head reductions are congruence w.r.t. tpm.
1044+
*)
1045+
Theorem subterm_hnf_children_size_cong :
1046+
!X Y M p. FINITE X /\ FINITE Y /\
1047+
subterm X M p <> NONE /\ solvable (subterm' X M p) ==>
1048+
hnf_children_size (principle_hnf (subterm' X M p)) =
1049+
hnf_children_size (principle_hnf (subterm' Y M p))
1050+
Proof
1051+
rpt STRIP_TAC
1052+
>> ‘subterm Y M p <> NONE /\
1053+
?pi. tpm pi (subterm' X M p) = subterm' Y M p’ by METIS_TAC [subterm_tpm_cong]
1054+
>> POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM)
1055+
>> qabbrev_tac ‘N = subterm' X M p’
1056+
>> rw [principle_hnf_tpm']
1057+
QED
1058+
7971059
(*---------------------------------------------------------------------------*
7981060
* Equivalent terms
7991061
*---------------------------------------------------------------------------*)
@@ -1409,6 +1671,65 @@ Proof
14091671
>> MATCH_MP_TAC Boehm_apply_lameq_cong >> rw []
14101672
QED
14111673

1674+
(* ‘subterm_width M p’ is the maximal number of children of all subterms in form
1675+
‘subterm X M t’ such that ‘t <<= p’ (prefix). The choice of X is irrelevant.
1676+
1677+
In other words, it's the maximal ‘hnf_children_size o pH’ of all terms of the
1678+
form ‘subterm X M t’ such that ‘t <<= FRONT p’ (The pH of ‘subterm X M p’ can
1679+
can be ignored, because its hnf children are never considered.
1680+
1681+
NOTE: This definition assumes ‘p <> []’ and ‘p IN ltree_paths (BTe X M)’ and
1682+
‘subterm X M p <> NONE’, because otherwise there will be no hnf children to
1683+
consider.
1684+
*)
1685+
Definition subterm_width_def :
1686+
subterm_width M p = let Ms = {subterm' {} M p' | p' <<= FRONT p} in
1687+
MAX_SET (IMAGE (hnf_children_size o principle_hnf) Ms)
1688+
End
1689+
1690+
(* NOTE: The actual difficulty of this theorem is to prove that
1691+
1692+
|- !X Y. hnf_children_size (principle_hnf (subterm' X M p) =
1693+
hnf_children_size (principle_hnf (subterm' Y M p)
1694+
*)
1695+
Theorem subterm_width_thm :
1696+
!X M p p'. FINITE X /\
1697+
p <> [] /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE /\
1698+
p' <<= FRONT p ==>
1699+
hnf_children_size (principle_hnf (subterm' X M p')) <= subterm_width M p
1700+
Proof
1701+
RW_TAC std_ss [subterm_width_def]
1702+
>> ‘0 < LENGTH p’ by rw [GSYM NOT_NIL_EQ_LENGTH_NOT_0]
1703+
>> qabbrev_tac ‘J = IMAGE (hnf_children_size o principle_hnf) Ms’
1704+
>> Know ‘J <> {}’
1705+
>- (rw [Abbr ‘J’, GSYM MEMBER_NOT_EMPTY, Abbr ‘Ms’] \\
1706+
Q.EXISTS_TAC ‘[]’ >> rw [])
1707+
>> DISCH_TAC
1708+
>> Know ‘FINITE J’
1709+
>- (qunabbrev_tac ‘J’ >> MATCH_MP_TAC IMAGE_FINITE \\
1710+
‘Ms = IMAGE (subterm' {} M) {p' | p' <<= FRONT p}’
1711+
by (rw [Abbr ‘Ms’, Once EXTENSION]) >> POP_ORW \\
1712+
MATCH_MP_TAC IMAGE_FINITE \\
1713+
rw [FINITE_prefix])
1714+
>> DISCH_TAC
1715+
>> qabbrev_tac ‘m = hnf_children_size (principle_hnf (subterm' X M p'))’
1716+
>> Suff ‘m IN J’ >- PROVE_TAC [MAX_SET_DEF]
1717+
>> rw [Abbr ‘m’, Abbr ‘J’]
1718+
>> Q.EXISTS_TAC ‘subterm' {} M p'’
1719+
>> reverse CONJ_TAC
1720+
>- (rw [Abbr ‘Ms’] \\
1721+
Q.EXISTS_TAC ‘p'’ >> art [])
1722+
>> ‘!p'. p' <<= p ==> subterm X M p' <> NONE’
1723+
by PROVE_TAC [cj 1 subterm_solvable_lemma]
1724+
(* applying subterm_hnf_children_size_cong *)
1725+
>> MATCH_MP_TAC subterm_hnf_children_size_cong >> rw []
1726+
>- (POP_ASSUM MATCH_MP_TAC \\
1727+
MATCH_MP_TAC IS_PREFIX_TRANS \\
1728+
Q.EXISTS_TAC ‘FRONT p’ >> art [] \\
1729+
MATCH_MP_TAC IS_PREFIX_BUTLAST' >> art [])
1730+
>> PROVE_TAC [cj 2 subterm_solvable_lemma]
1731+
QED
1732+
14121733
(*---------------------------------------------------------------------------*
14131734
* Separability of terms
14141735
*---------------------------------------------------------------------------*)

0 commit comments

Comments
 (0)