Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

more results of terms having head normal forms (has_hnf) #1150

Merged
merged 3 commits into from
Oct 4, 2023
Merged

more results of terms having head normal forms (has_hnf) #1150

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
74a24fe
[examples/lambda] more results of terms having head normal forms (has…
binghe Oct 3, 2023
c15737f
[examples/lambda] generalized "abs_betastar" (using `-b->*` instead o…
binghe Oct 3, 2023
2ca53c3
Improved hnf_appstar and abs_betastar, etc. after code review @mn200
binghe Oct 4, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions examples/lambda/barendregt/chap3Script.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -925,9 +925,11 @@ Proof
>> MATCH_MP_TAC grandbeta_imp_betastar >> art []
QED

(* cf. abs_grandbeta, added by Chun Tian *)
(* |- !R x y z. R^+ x y /\ R^+ y z ==> R^+ x z *)
Theorem TC_TRANS[local] = REWRITE_RULE [transitive_def] TC_TRANSITIVE

Theorem abs_betastar :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could be an iff.

!x M Z. LAM x M -b->* Z ==> ?N'. (Z = LAM x N') /\ M == N'
!x M Z. LAM x M -b->* Z ==> ?N'. (Z = LAM x N') /\ M -b->* N'
Proof
rpt GEN_TAC
>> REWRITE_TAC [SYM theorem3_17]
Expand All @@ -936,13 +938,13 @@ Proof
>> rpt STRIP_TAC
>- (FULL_SIMP_TAC std_ss [abs_grandbeta] \\
Q.EXISTS_TAC ‘N0’ >> art [] \\
MATCH_MP_TAC grandbeta_imp_lameq >> art [])
MATCH_MP_TAC TC_SUBSET >> art [])
>> Q.PAT_X_ASSUM ‘Z = LAM x N'’ (FULL_SIMP_TAC std_ss o wrap)
>> FULL_SIMP_TAC std_ss [abs_grandbeta]
>> Q.EXISTS_TAC ‘N0’ >> art []
>> MATCH_MP_TAC lameq_TRANS
>> MATCH_MP_TAC TC_TRANS
>> Q.EXISTS_TAC ‘N'’ >> art []
>> MATCH_MP_TAC grandbeta_imp_lameq >> art []
>> MATCH_MP_TAC TC_SUBSET >> art []
QED

val lameq_consistent = store_thm(
Expand Down
14 changes: 8 additions & 6 deletions examples/lambda/barendregt/standardisationScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2523,7 +2523,7 @@ Proof
>> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []
QED

(* Proposition 8.3.13 (i) *)
(* Proposition 8.3.13 (i) [1, p.174] *)
Theorem has_hnf_iff_LAM[simp] :
!x M. has_hnf (LAM x M) <=> has_hnf M
Proof
Expand All @@ -2536,11 +2536,13 @@ Proof
rw [hnf_cases])
(* stage work *)
>> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR]
>> Suff ‘?N'. (Z = LAM x N') /\ M == N'’
>- (STRIP_TAC \\
‘hnf Z’ by PROVE_TAC [hnf_preserved] \\
Q.EXISTS_TAC ‘N'’ >> gs [hnf_thm])
>> MATCH_MP_TAC abs_betastar >> art []
>> Know ‘?N'. (Z = LAM x N') /\ M -b->* N'’
>- (MATCH_MP_TAC abs_betastar >> art [])
>> STRIP_TAC
>> Q.EXISTS_TAC ‘N'’
>> ‘hnf Z’ by PROVE_TAC [hnf_preserved]
>> gs [hnf_thm]
>> MATCH_MP_TAC betastar_lameq >> art []
QED

val _ = export_theory()
Expand Down