diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/GCD_Fred.thy b/C11-BackEnds/AutoCorres_wrapper/examples/GCD_Fred.thy
new file mode 100644
index 0000000000000000000000000000000000000000..c07dd8e8fd4d1f8f67f297717fa29288a7cdea2e
--- /dev/null
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/GCD_Fred.thy
@@ -0,0 +1,71 @@
+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
+
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
index 806e7dbdbb1d6f73ec860b898317e20ef4d28819..448619689840b19a15fa5bc1dcd263c9f88d1b9a 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
+++ b/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)
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy
index bcf915ab2ce73abf645c5ebe2ceb58f6f1602814..8b958a8a52c21ade1ad0bdbde395989f2b8c7714 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy
+++ b/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. *)