summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-06-02 11:24:23 +0200
committerSon HO2023-06-04 21:54:38 +0200
commit435d75174a12a47da84537cc7c9730a0eccf6d1f (patch)
tree4ef5fb4b8d1a14d53c80dac87de99fb47e06ed55 /backends
parent61566b9739ca01bee87daf508a3afc2a4c0c21c6 (diff)
Simplify a proof
Diffstat (limited to '')
-rw-r--r--backends/hol4/primitivesArithScript.sml18
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