diff options
| author | Son Ho | 2023-06-02 11:24:23 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | 435d75174a12a47da84537cc7c9730a0eccf6d1f (patch) | |
| tree | 4ef5fb4b8d1a14d53c80dac87de99fb47e06ed55 /backends | |
| parent | 61566b9739ca01bee87daf508a3afc2a4c0c21c6 (diff) | |
Simplify a proof
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index decb1109..928fc39b 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -46,21 +46,15 @@ Proof rw [] >> try_tac cooper_tac QED -(* This induction theorem works well with [Induct_on] *) +(* THIS INDUCTION theorem works well with [Induct_on] *) Theorem int_induction: !(P : int -> bool). (∀i. i < 0 ⇒ P i) ∧ P 0 /\ (!i. P i ==> P (i+1)) ==> !i. P i Proof - ntac 3 strip_tac >> - Cases_on ‘i < 0’ >- (last_assum irule >> fs []) >> - fs [not_lt_eq_ge] >> - Induct_on ‘Num i’ >> rpt strip_tac >> pop_last_assum ignore_tac - >-(sg ‘i = 0’ >- cooper_tac >> fs []) >> - last_assum (qspec_assume ‘i-1’) >> - fs [] >> pop_assum irule >> - rw [] >> try_tac cooper_tac >> - first_assum (qspec_assume ‘i - 1’) >> - pop_assum irule >> - rw [] >> try_tac cooper_tac + rw [] >> + qspec_assume ‘P’ int_induction_ideal >> + gvs [] >> + Cases_on ‘0 ≤ i’ >> gvs [] >> + last_x_assum irule >> int_tac QED val _ = TypeBase.update_induction int_induction |