From 5585b36c520f203cf253b8f39111d0733768b3bf Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Mon, 27 Apr 2020 12:33:49 +0200
Subject: [PATCH] optimizations with frederic in CAS.
---
.../examples/IsPrime_sqrt_CAS.thy | 26 +++++++++++++++++--
1 file changed, 24 insertions(+), 2 deletions(-)
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
index 732b9d89f7c..e39b0249ab2 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
@@ -283,7 +283,7 @@ lemma aux9[simp]:
using not_less_eq_eq by force
-
+
theorem (in is_prime) is_prime_correct':
"\<lbrace> \<lambda>\<sigma>. n \<le> UINT_MAX \<rbrace> is_prime' n \<lbrace> \<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n \<rbrace>!"
@@ -343,7 +343,6 @@ method annotate_loops for n::nat = (prep, subst whileLoopE_invL1[of _ n])
(* this must be generalized for several loops *)
-
(* and now the scheme for an automated proof, provided that sufficient
background knowledge had been inserted into the prover 'auto'. *)
@@ -361,4 +360,27 @@ theorem (in is_prime) is_prime_correct''':
by (wp, auto )
+(* yet another way with Frederics stuff *)
+
+method vcg = (subst is_prime.is_prime'_annot,prep, wp)
+
+thm is_prime.is_prime'_annot
+
+context is_prime
+begin
+
+definition [prog_annotations]:"requires = is_prime_requires"
+definition [prog_annotations]:"ensures = is_prime_ensures"
+
+
+
+theorem is_prime_correct'''':
+ "\<lbrace>requires n\<rbrace> is_prime' n \<lbrace>ensures n\<rbrace>!"
+ by(vcg, auto)
+
+
+
+end
+
+
end
--
GitLab