diff options
| author | Son Ho | 2023-05-15 12:01:48 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | 74e8e6b80b31b1df9123fbec9a7f910a68a0b1cd (patch) | |
| tree | 9df48d661d5cfdb994bbdbecc06c136e07fc7acd /backends/hol4/divDefTheory.sig | |
| parent | c6e9e51197833a8685c63e6c40d8eabf4e64c22d (diff) | |
Introduce fix_exec, an executable version of fix
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/divDefTheory.sig | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/backends/hol4/divDefTheory.sig b/backends/hol4/divDefTheory.sig index 15592052..ec69c44f 100644 --- a/backends/hol4/divDefTheory.sig +++ b/backends/hol4/divDefTheory.sig @@ -4,12 +4,15 @@ sig (* Definitions *) val fix_def : thm + val fix_exec_def : thm val fix_fuel_P_def : thm val fix_fuel_def : thm + val fix_nexec_def : thm val is_valid_fp_body_def : thm (* Theorems *) val case_result_switch_eq : thm + val fix_exec_fixed_eq : thm val fix_fixed_diverges : thm val fix_fixed_eq : thm val fix_fixed_terminates : thm @@ -21,6 +24,7 @@ sig val fix_fuel_mono_least : thm val fix_fuel_not_diverge_eq_fix : thm val fix_fuel_not_diverge_eq_fix_aux : thm + val fix_nexec_eq_fix : thm val fix_not_diverge_implies_fix_fuel : thm val fix_not_diverge_implies_fix_fuel_aux : thm val is_valid_fp_body_compute : thm @@ -37,6 +41,10 @@ sig fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge + [fix_exec_def] Definition + + ⊢ fix_exec = fix_nexec 1000000 + [fix_fuel_P_def] Definition ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x) @@ -46,6 +54,12 @@ sig ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x + [fix_nexec_def] Definition + + ⊢ ∀n f x. + fix_nexec n f x = + if fix_fuel_P f x n then fix_fuel n f x else fix f x + [is_valid_fp_body_def] Definition ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ @@ -75,6 +89,10 @@ sig | Fail e => Fail e | Diverge => Diverge + [fix_exec_fixed_eq] Theorem + + ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix_exec f x = f (fix_exec f) x + [fix_fixed_diverges] Theorem ⊢ ∀N f. @@ -151,6 +169,10 @@ sig ∀n x. g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x + [fix_nexec_eq_fix] Theorem + + ⊢ ∀N f n. is_valid_fp_body N f ⇒ fix_nexec n f = fix f + [fix_not_diverge_implies_fix_fuel] Theorem ⊢ ∀N f. |