Isabelle2018: AutoCorresTest

tools/autocorres/Makefile

@@ -45,7 +45,7 @@ tests/All.thy: \
 %.thy: %.c
 	@echo "Generating '$@' from '$<'..."
 	@printf '(* @LICENSE(NICTA) *)\n\n' > $@
-	@printf 'theory %s\nimports "../../AutoCorres"\nbegin\n\n' $(notdir $(basename $<)) > $@
+	@printf 'theory %s\nimports "AutoCorres.AutoCorres"\nbegin\n\n' $(notdir $(basename $<)) > $@
 	@printf 'install_C_file "%s"\n\n' $(notdir $<) >> $@
 	@printf 'autocorres "%s"\n\n' $(notdir $<) >> $@
 	@printf 'end\n' >> $@

tools/autocorres/tests/examples/BinarySearch.thy

@@ -126,8 +126,8 @@ lemma array_Ex:
   done
 
 lemma sorted_index_lt:
-    "\<lbrakk> sorted xs; unat (xs ! m) < v; n \<le> m; m < length xs \<rbrakk> \<Longrightarrow>  unat (xs ! n) < v"
-  by (metis (hide_lams, no_types) le_less_trans sorted_equals_nth_mono word_le_nat_alt)
+  "\<lbrakk> sorted xs; unat (xs ! m) < v; n \<le> m; m < length xs \<rbrakk> \<Longrightarrow>  unat (xs ! n) < v"
+  by (meson le_less_trans sorted_nth_mono unat_arith_simps(1))
 
 lemma sorted_index_gt:
     "\<lbrakk> sorted xs; v < unat (xs ! m); m \<le> n; n < length xs \<rbrakk> \<Longrightarrow>  v < unat (xs ! n)"

tools/autocorres/tests/examples/FactorialTest.thy

@@ -11,7 +11,7 @@
 (*
 Termination for recursive functions.
 *)
-theory Factorial
+theory FactorialTest
 imports
   "AutoCorres.AutoCorres"
   "Lib.OptionMonadWP"
@@ -116,9 +116,8 @@ thm call_factorial'_def
 lemma "\<lbrace> \<top> \<rbrace> call_factorial' \<lbrace> \<lambda>r s. r = fact 42 \<rbrace>!"
   unfolding call_factorial'_def
   apply wp
-   using factorial'_correct_old
-   apply force
-  apply (force simp: option_monad_mono_eq (* factorial'_mono *))
+   apply (force simp: option_monad_mono_eq)
+  using factorial'_correct_old apply force
   done
 
 end

tools/autocorres/tests/examples/FibProof.thy

@@ -197,7 +197,7 @@ lemma fib_simpl_spec: "\<forall>n. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<lbrace
   apply (hoare_rule HoareTotal.ProcRec1[where r = "measure (\<lambda>(s, d). unat \<^bsup>s\<^esup>n)"])
   apply (unfold creturn_def | vcg_step)+
   apply (subst fibo32.simps, simp)
-  apply (subst fibo32.simps, simp add: scast_id)
+  apply (subst fibo32.simps, simp)
   apply (subst fibo32.simps[where n = n])
   apply unat_arith
   done
@@ -410,7 +410,7 @@ lemma fib'_term: "no_ofail (\<lambda>_. rec_measure' > unat n) (fib' rec_measure
   apply (induct n arbitrary: rec_measure' rule: less_induct)
   apply (subgoal_tac "\<And>y P rec_measure'. ovalidNF (\<lambda>_. y < x \<and> unat y < rec_measure' \<and> P) (fib' rec_measure' y) (\<lambda>_ _. P)")
   apply (rule fib'_term_rec_helper, assumption)
-  apply (metis ovalidNF_assume_pre)
+  apply (metis (full_types) ovalidNF_assume_pre)
   done
 
 (* The overall correctness proof. *)

tools/autocorres/tests/examples/IsPrime.thy

@@ -57,7 +57,7 @@ lemma mod_to_dvd:
   by (clarsimp simp: dvd_eq_mod_eq_0)
 
 lemma prime_of_product [simp]: "prime ((a::nat) * b) = ((a = 1 \<and> prime b) \<or> (prime a \<and> b = 1))"
-  using prime_product by force
+  by (metis mult.commute mult.right_neutral prime_product)
 
 lemma partial_prime_2 [simp]: "(partial_prime a 2) = (a > 1)"
   by (clarsimp simp: partial_prime_def)
@@ -100,7 +100,7 @@ lemma sqrt_prime:
 lemma partial_prime_sqr:
      "\<lbrakk> n * n > p \<rbrakk> \<Longrightarrow> partial_prime p n = prime p"
   apply (case_tac "n \<ge> p")
-   apply (clarsimp simp: partial_prime_ge)
+   apply clarsimp
   apply (case_tac "partial_prime p n")
    apply clarsimp
    apply (erule sqrt_prime)
@@ -161,7 +161,9 @@ theorem is_prime_faster_correct:
       where I="\<lambda>r s. is_prime_inv n r s"
       and M="(\<lambda>(r, s). (Suc n) * (Suc n) - r * r)"])
    apply wp
-    apply (fastforce elim: nat_leE simp: partial_prime_sqr prime_dvd)+
+    apply clarsimp
+    apply (metis One_nat_def Suc_leI Suc_lessD nat_leE prime_dvd leD mult_le_mono n_less_n_mult_m)
+   apply (fastforce elim: nat_leE simp: partial_prime_sqr)
   apply (clarsimp simp: SQRT_UINT_MAX_def)
   done
 

tools/autocorres/tests/examples/Quicksort.thy

@@ -850,7 +850,6 @@ lemma partitioned_array_sorted:
   apply (subst sorted_append, simp)
   apply (rule conjI)
    apply (subst the_array_concat2[where m = "1"], simp+)
-   apply (subst sorted_Cons)
    apply (simp add: partitioned_def)
    apply (subst all_set_conv_all_nth)
    apply (clarsimp simp: the_array_elem)

tools/autocorres/tests/examples/Simple.thy

@@ -11,7 +11,6 @@
 theory Simple
 imports
   "AutoCorres.AutoCorres"
-  GCD
 begin
 
 (* Parse the input file. *)