Skip to content

Commit

Permalink
Add subterm_length and use in agree_upto_lemma
Browse files Browse the repository at this point in the history
  • Loading branch information
binghe committed Dec 6, 2024
1 parent db50d5f commit b796f07
Showing 1 changed file with 93 additions and 3 deletions.
96 changes: 93 additions & 3 deletions examples/lambda/barendregt/boehmScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -2942,6 +2942,19 @@ Definition subterm_width_def[nocompute] :
else 0) {q | q <<= p})
End

(* ‘subterm_length M p’ is the maximal length of LAMl binding list of subterms
given by ‘subterm X M q r’ such that ‘q <<= p’, irrelevant with X and r.
NOTE: The proof of subterm_length property is often dual of subterm_width.
*)
Definition subterm_length_def[nocompute] :
subterm_length M p =
MAX_SET (IMAGE (\q. let N = subterm (FV M) M q 0 in
if N <> NONE /\ solvable (FST (THE N)) then
LAMl_size (principle_hnf (FST (THE N)))
else 0) {q | q <<= p})
End

Theorem subterm_width_nil :
!M. subterm_width M [] = if solvable M then
hnf_children_size (principle_hnf M)
Expand All @@ -2950,6 +2963,14 @@ Proof
rw [subterm_width_def]
QED

Theorem subterm_length_nil :
!M. subterm_length M [] = if solvable M then
LAMl_size (principle_hnf M)
else 0
Proof
rw [subterm_length_def]
QED

Theorem subterm_width_inclusive :
!M p q. q <<= p /\ subterm_width M p <= d ==> subterm_width M q <= d
Proof
Expand All @@ -2970,6 +2991,26 @@ Proof
>> Q_TAC (TRANS_TAC isPREFIX_TRANS) ‘q’ >> art []
QED

Theorem subterm_length_inclusive :
!M p q. q <<= p /\ subterm_length M p <= d ==> subterm_length M q <= d
Proof
simp [subterm_length_def]
>> rpt GEN_TAC
>> qmatch_abbrev_tac ‘q <<= p /\ a <= d ==> b <= d’
>> STRIP_TAC
>> Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘a’
>> POP_ASSUM (REWRITE_TAC o wrap)
>> simp [Abbr ‘a’, Abbr ‘b’]
>> MATCH_MP_TAC SUBSET_MAX_SET
>> CONJ_TAC
>- (MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix])
>> CONJ_TAC
>- (MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix])
>> MATCH_MP_TAC IMAGE_SUBSET
>> rw [SUBSET_DEF]
>> Q_TAC (TRANS_TAC isPREFIX_TRANS) ‘q’ >> art []
QED

Theorem subterm_width_thm :
!X M p r.
FINITE X /\ FV M SUBSET X UNION RANK r ==>
Expand Down Expand Up @@ -2997,6 +3038,33 @@ Proof
simp [principle_hnf_tpm'] ]
QED

Theorem subterm_length_thm :
!X M p r.
FINITE X /\ FV M SUBSET X UNION RANK r ==>
subterm_length M p =
MAX_SET
(IMAGE
(\q. let N = subterm X M q r in
if N <> NONE /\ solvable (FST (THE N)) then
LAMl_size (principle_hnf (FST (THE N)))
else 0) {q | q <<= p})
Proof
rw [subterm_length_def]
>> AP_TERM_TAC
>> rw [Once EXTENSION]
>> EQ_TAC >> rw []
>| [ (* goal 1 (of 2) *)
Q.EXISTS_TAC ‘q’ >> art [] \\
MP_TAC (Q.SPECL [‘X’, ‘FV M’, ‘M’, ‘q’, ‘r’, ‘0’] subterm_tpm_cong) \\
rw [tpm_rel_alt] >> gs [] \\
simp [principle_hnf_tpm'],
(* goal 2 (of 2) *)
Q.EXISTS_TAC ‘q’ >> art [] \\
MP_TAC (Q.SPECL [‘X’, ‘FV M’, ‘M’, ‘q’, ‘r’, ‘0’] subterm_tpm_cong) \\
rw [tpm_rel_alt] >> gs [] \\
simp [principle_hnf_tpm'] ]
QED

Theorem subterm_width_first :
!X M p r. FINITE X /\ FV M SUBSET X UNION RANK r /\ solvable M ==>
hnf_children_size (principle_hnf M) <= subterm_width M p
Expand All @@ -3011,6 +3079,20 @@ Proof
>> Q.EXISTS_TAC ‘[]’ >> rw []
QED

Theorem subterm_length_first :
!X M p r. FINITE X /\ FV M SUBSET X UNION RANK r /\ solvable M ==>
LAMl_size (principle_hnf M) <= subterm_length M p
Proof
rpt STRIP_TAC
>> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’, ‘r’] subterm_length_thm)
>> simp [] >> DISCH_THEN K_TAC
>> irule MAX_SET_PROPERTY
>> CONJ_TAC
>- (MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix])
>> simp []
>> Q.EXISTS_TAC ‘[]’ >> rw []
QED

Theorem subterm_width_last :
!X M p q r. FINITE X /\ FV M SUBSET X UNION RANK r /\ q <<= p /\
subterm X M q r <> NONE /\
Expand Down Expand Up @@ -5754,10 +5836,18 @@ Proof
rw [GSYM solvable_iff_has_hnf] >> fs [EVERY_EL])
>> DISCH_TAC
>> qabbrev_tac ‘n = \i. LAMl_size (M0 i)’
>> qabbrev_tac ‘n_max = MAX_SET (IMAGE n (count k))’
(* NOTE: This n_max was redefined from previous ‘MAX_SET (IMAGE n (count k))’ *)
>> qabbrev_tac ‘n_max = MAX_LIST (MAP (\e. subterm_length e p) Ms)’
>> Know ‘!i. i < k ==> subterm_length (M i) p <= n_max’
>- (rw [Abbr ‘n_max’] \\
MATCH_MP_TAC MAX_LIST_PROPERTY >> rw [MEM_MAP] \\
Q.EXISTS_TAC ‘M i’ >> rw [EL_MEM, Abbr ‘M’])
>> DISCH_TAC
>> Know ‘!i. i < k ==> n i <= n_max’
>- (rw [Abbr ‘M0’, Abbr ‘n_max’] \\
irule MAX_SET_PROPERTY >> rw [])
>- (RW_TAC std_ss [] \\
Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_length (M i) p’ \\
MP_TAC (Q.SPECL [‘X’, ‘(M :num -> term) i’, ‘p’, ‘r’] subterm_length_first) \\
simp [Abbr ‘n’])
>> DISCH_TAC
>> qabbrev_tac ‘Y = BIGUNION (IMAGE FV (set Ms))’
>> ‘FINITE Y’ by (rw [Abbr ‘Y’] >> REWRITE_TAC [FINITE_FV])
Expand Down

0 comments on commit b796f07

Please sign in to comment.