pushing the stuff to CAS ... renaming

C11-BackEnds/AutoCorres_wrapper/ROOT

@@ -54,7 +54,7 @@ session Isabelle_C_AutoCorres_examples = Isabelle_C_AutoCorres +
     "examples/FactorialTest"
     "examples/FibProof"
     "examples/IsPrime_linear_CET"
-    "examples/IsPrime_sqrt_ANO"
+    "examples/IsPrime_sqrt_CAS"
     "examples/IsPrime_sqrt_CET"
     "examples/IsPrime_sqrt_opt_CET"
     "examples/IsPrime_TEC"

C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_ANO.thy → C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy

@@ -61,7 +61,7 @@ Of course, since developments can mix C code and HOL developments in an arbitrar
 these two style have to be thought of as extremes in a continuum. \<close>
 
 
-theory IsPrime_sqrt_ANO
+theory IsPrime_sqrt_CAS
 imports
   Isabelle_C_AutoCorres.AutoCorres_Wrapper
   "HOL-Computational_Algebra.Primes"
@@ -305,4 +305,60 @@ proof (rule validNF_assume_pre)
 qed
 
 
+section\<open>A Schematic Presentation for the Automated Proof \<close>
+(* step 0 : "lifting over parameter" over the free variables of the correctness statement: *)
+lemma whileLoopE_inv_lift1 : 
+  "whileLoopE (B n) (C n) = (\<lambda>x. whileLoopE_inv (B n) (C n) x (I n) (measure' (M n)))"
+  by (simp add: whileLoopE_inv_def)
+
+(* step 1 : encapsulating inv and mesure for each loop *)
+definition is_prime_requires : "is_prime_requires n \<equiv> \<lambda>\<sigma>. n \<le> UINT_MAX"
+definition is_prime_ensures  : "is_prime_ensures n \<equiv> \<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n"
+
+definition is_prime_inv\<^sub>1     : "is_prime_inv\<^sub>1 n \<equiv> \<lambda>r s. is_prime_inv n r s"
+definition is_prime_mesure\<^sub>1  : "is_prime_mesure\<^sub>1 n \<equiv> \<lambda>(r, s). (Suc n) * (Suc n) - r * r"
+
+(* step 2 : specific replacement rule for the loop with the annotated loop *)
+lemmas whileLoopE_invL1 = whileLoopE_inv_lift1 [of _ _ _ "is_prime_inv\<^sub>1" "is_prime_mesure\<^sub>1",
+                                                simplified is_prime_inv\<^sub>1 is_prime_mesure\<^sub>1]
+
+declare prime_ge_2_nat[dest] (* misère, preconfig pour le dernier auto. *)
+
+(* configure the general methods "preparation" and annotate loops. *)
+named_theorems prog_annotations
+declare is_prime.is_prime'_def[prog_annotations]
+        is_prime_requires [prog_annotations]
+        is_prime_ensures [prog_annotations]
+
+
+named_theorems folds
+declare dvd_eq_mod_eq_0[symmetric,folds]
+declare SQRT_UINT_MAX_def [symmetric,folds]
+
+method prep declares prog_annotations folds = 
+               (rule validNF_assume_pre, (* always!*)
+                unfold prog_annotations folds)
+
+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'. *)
+
+theorem is_prime_correct'':
+  "\<lbrace>\<lambda>\<sigma>. n \<le> UINT_MAX \<rbrace> 
+   is_prime.is_prime' n 
+   \<lbrace>\<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n \<rbrace>!"
+   apply (annotate_loops n)    
+   by    (wp, auto )  
+  
+(* or also: just another presentation *)
+theorem (in is_prime) is_prime_correct''':
+  "\<lbrace>is_prime_requires n\<rbrace> is_prime' n \<lbrace>is_prime_ensures n\<rbrace>!"
+   apply (annotate_loops n)    
+   by    (wp, auto )  
+
+
 end

C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CET.thy

@@ -304,7 +304,7 @@ proof (rule validNF_assume_pre)
 qed
 
 
-
+(* TODO : REMOVE HERE; WENT TO CAS *)
 section\<open>A Schematic Presentation for the Automated Proof \<close>
 (* step 0 : "lifting over parameter" over the free variables of the correctness statement: *)
 lemma whileLoopE_inv_lift1 :