diff options
Diffstat (limited to 'backends/hol4/divDefTheory.sig')
-rw-r--r-- | backends/hol4/divDefTheory.sig | 187 |
1 files changed, 187 insertions, 0 deletions
diff --git a/backends/hol4/divDefTheory.sig b/backends/hol4/divDefTheory.sig new file mode 100644 index 00000000..15592052 --- /dev/null +++ b/backends/hol4/divDefTheory.sig @@ -0,0 +1,187 @@ +signature divDefTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val fix_def : thm + val fix_fuel_P_def : thm + val fix_fuel_def : thm + val is_valid_fp_body_def : thm + + (* Theorems *) + val case_result_switch_eq : thm + val fix_fixed_diverges : thm + val fix_fixed_eq : thm + val fix_fixed_terminates : thm + val fix_fuel_P_least : thm + val fix_fuel_compute : thm + val fix_fuel_eq_fix : thm + val fix_fuel_mono : thm + val fix_fuel_mono_aux : thm + 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_not_diverge_implies_fix_fuel : thm + val fix_not_diverge_implies_fix_fuel_aux : thm + val is_valid_fp_body_compute : thm + + val divDef_grammars : type_grammar.grammar * term_grammar.grammar +(* + [primitives] Parent theory of "divDef" + + [fix_def] Definition + + ⊢ ∀f x. + fix f x = + if ∃n. fix_fuel_P f x n then + fix_fuel ($LEAST (fix_fuel_P f x)) f x + else Diverge + + [fix_fuel_P_def] Definition + + ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x) + + [fix_fuel_def] Definition + + ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ + ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x + + [is_valid_fp_body_def] Definition + + ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ + ∀n f. + is_valid_fp_body (SUC n) f ⇔ + ∀x. (∀g h. f g x = f h x) ∨ + ∃h y. + is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od + + [case_result_switch_eq] Theorem + + ⊢ (case + case x of + Return y => f y + | Fail e => Fail e + | Diverge => Diverge + of + Return y => g y + | Fail e => Fail e + | Diverge => Diverge) = + case x of + Return y => + (case f y of + Return y => g y + | Fail e => Fail e + | Diverge => Diverge) + | Fail e => Fail e + | Diverge => Diverge + + [fix_fixed_diverges] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x + + [fix_fixed_eq] Theorem + + ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x + + [fix_fixed_terminates] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x + + [fix_fuel_P_least] Theorem + + ⊢ ∀f n x. + fix_fuel n f x ≠ Diverge ⇒ + fix_fuel_P f x ($LEAST (fix_fuel_P f x)) + + [fix_fuel_compute] Theorem + + ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ + (∀n f x. + fix_fuel (NUMERAL (BIT1 n)) f x = + f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧ + ∀n f x. + fix_fuel (NUMERAL (BIT2 n)) f x = + f (fix_fuel (NUMERAL (BIT1 n)) f) x + + [fix_fuel_eq_fix] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x + + [fix_fuel_mono] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. + fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x + + [fix_fuel_mono_aux] Theorem + + ⊢ ∀n N M g f. + is_valid_fp_body M f ⇒ + is_valid_fp_body N g ⇒ + ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒ + ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x + + [fix_fuel_mono_least] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. + fix_fuel_P f x n ⇒ + fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x + + [fix_fuel_not_diverge_eq_fix] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. + f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x + + [fix_fuel_not_diverge_eq_fix_aux] Theorem + + ⊢ ∀N M g f. + is_valid_fp_body M f ⇒ + is_valid_fp_body N g ⇒ + ∀n x. + g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x + + [fix_not_diverge_implies_fix_fuel] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x + + [fix_not_diverge_implies_fix_fuel_aux] Theorem + + ⊢ ∀N M g f. + is_valid_fp_body M f ⇒ + is_valid_fp_body N g ⇒ + ∀x. g (fix f) x ≠ Diverge ⇒ + ∃n. g (fix f) x = g (fix_fuel n f) x ∧ + ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x + + [is_valid_fp_body_compute] Theorem + + ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ + (∀n f. + is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔ + ∀x. (∀g h. f g x = f h x) ∨ + ∃h y. + is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧ + ∀g. f g x = do z <- g y; h g z od) ∧ + ∀n f. + is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔ + ∀x. (∀g h. f g x = f h x) ∨ + ∃h y. + is_valid_fp_body (NUMERAL (BIT1 n)) h ∧ + ∀g. f g x = do z <- g y; h g z od + + +*) +end |