Added Fred's B gcd example. Slight modifs in sqrt_CASS for pedagogical reasons

C11-BackEnds/AutoCorres_wrapper/examples/GCD_Fred.thy

+theory GCD_Fred
+  imports   Isabelle_C_AutoCorres.AutoCorres_Wrapper
+  "HOL-Computational_Algebra.Primes"
+begin
+
+text\<open>This is Fred's GCD example\<close>
+
+section\<open>Background\<close>
+
+section\<open>The Program\<close>
+
+declare [[AutoCorres]]
+
+text \<open>Setup of AutoCorres for semantically representing this C element:\<close>
+
+declare_autocorres pgcd [ ts_rules = nondet, unsigned_word_abs = pgcd ]
+
+
+C\<open>
+int pgcd(int m, int n) {
+  int a = m;
+  int b = n;
+  while (a != b) {
+    if (a < b) {
+      b = b - a;
+    } else {
+      a = a - b;
+    }
+  }
+  return a;
+}
+
+\<close>
+
+print_theorems
+find_theorems name:pgcd
+
+
+
+section\<open>The Correctness-Proof\<close>
+
+definition "pgcd_inv (a::int) b m n \<equiv> a > 0 \<and> b > 0 \<and>  m < INT_MAX \<and> n < INT_MAX \<and> 
+                                      a \<le> m \<and> b \<le> n \<and>
+                                      (\<forall> g. g = gcd a b \<longrightarrow> g = gcd m n)"
+
+
+
+theorem (in pgcd) pgcd'_correct:
+    "\<lbrace> \<lambda>\<sigma>. m > 0 \<and> n > 0 \<and> m < INT_MAX \<and> n < INT_MAX \<rbrace> pgcd' m n \<lbrace> \<lambda>res \<sigma>. res = gcd m n \<rbrace>!"
+  unfolding pgcd'_def
+  apply(rule validNF_assume_pre)
+  apply(subst whileLoop_add_inv   [  where I = "\<lambda>(a, b) s. pgcd_inv a b m n"
+                                     and   M = "\<lambda>((a, b),s) . nat a + nat b"])
+  proof(wp, auto simp: pgcd_inv_def, fold INT_MAX_def)
+      fix a b
+      show "0 < a \<Longrightarrow> m < INT_MAX \<Longrightarrow> n < INT_MAX \<Longrightarrow> a \<le> m \<Longrightarrow> b \<le> n \<Longrightarrow>  a < b \<Longrightarrow> b - a \<le> INT_MAX"  
+         using INT_MAX_def by linarith
+   next
+      fix a b
+       show "m < INT_MAX \<Longrightarrow> n < INT_MAX \<Longrightarrow> 0 < b \<Longrightarrow> a \<le> m \<Longrightarrow> b \<le> n \<Longrightarrow> \<not> a < b \<Longrightarrow> a - b \<le> INT_MAX" 
+          using INT_MAX_def by linarith
+   next
+      fix a b
+      show " gcd a b = gcd m n \<Longrightarrow> gcd a (b - a) = gcd m n"
+        by (metis (no_types, hide_lams)  gcd.commute gcd_diff1)
+   next
+       fix a b
+       show " gcd a b = gcd m n \<Longrightarrow>  gcd (a - b) b = gcd m n"
+         by (simp add: gcd_diff1)
+  qed
+

C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy

@@ -53,6 +53,14 @@ imports
 begin
 \<comment> \<open>Derived from: \<^file>\<open>../../../src_ext/l4v/src/tools/autocorres/tests/examples/IsPrime.thy\<close>\<close>
 
+section \<open>Setup Standard Mapping\<close>
+setup \<open>C_Module.C_Term.map_expression
+        (fn expr => fn _ => fn _ => 
+          case expr of C_Ast.CVar0 (C_Ast.Ident0 (_, x, _), _) =>
+                         Free (C_Grammar_Rule_Lib.ident_decode x, dummyT)
+                     | s => Free (\<^make_string> s, dummyT))\<close>
+
+
 section\<open>The Theory of the \<open>O(sqrt(n))\<close> Primality Test Algorithm\<close>
 text\<open>This section develops basic concepts of the invariant. This bit is presented here \<^emph>\<open>before\<close>
 the actual code, but could also be after or even inside the \<^theory_text>\<open>C\<close> command as comment-annotation of 
@@ -157,13 +165,9 @@ text\<open> This C code contains a function that determines if the given number
  
       This is a faster version than a linear primality test; runs in O(sqrt(n)). \<close>
 
-declare [[AutoCorres]]
 
-setup \<open>C_Module.C_Term.map_expression
-        (fn expr => fn _ => fn _ => 
-          case expr of C_Ast.CVar0 (C_Ast.Ident0 (_, x, _), _) =>
-                         Free (C_Grammar_Rule_Lib.ident_decode x, dummyT)
-                     | s => Free (\<^make_string> s, dummyT))\<close>
+
+declare [[AutoCorres]]
 
 C \<open>
      #define SQRT_UINT_MAX 65536
@@ -356,6 +360,7 @@ 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)  
 
 

C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy

@@ -178,19 +178,27 @@ lemma five_and_divides : "prime (p::nat) \<Longrightarrow> 5 < p \<Longrightarro
 
 section\<open>The C code for \<open>O(sqrt(n))\<close> Primality Test Algorithm\<close>
 
+text\<open> This C code contains a function that determines if the given number
+      @{term n} is prime.
+
+      It returns 0 if @{term n}  is composite, or non-zero if @{term n}  is prime.
+ 
+      This is a faster version than a linear primality test; runs in O(sqrt(n)). \<close>
+
 text \<open>The invocation of AutoCorres:\<close>
 
 declare [[AutoCorres]]
 
 text \<open>Setup of AutoCorres for semantically representing this C element:\<close>
+
 declare_autocorres is_prime [ ts_rules = nondet, unsigned_word_abs = is_prime ]
 
-text\<open> This C code contains a function that determines if the given number
-      @{term n} is prime.
 
-      It returns 0 if @{term n}  is composite, or non-zero if @{term n}  is prime.
- 
-      This is a faster version than a linear primality test; runs in O(sqrt(n)). \<close>
+
+
+
+
+
 
 C \<open>
 #define SQRT_UINT_MAX 65536
@@ -211,6 +219,17 @@ unsigned int is_prime(unsigned int n)
     return TRUE;
 }\<close>
 
+
+
+
+
+
+
+
+
+
+
+
 section\<open>The Results of the AutoCorres Evaluation\<close>
 
 C_export_file  (* This exports the C code into a C file ready to be compiled by gcc. *)