ftuong
/
citadelle-devel
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13748 3260e6d1-4efc-4170-b0a7-36055960796d

This commit is contained in:
Burkhart Wolff 2019-03-26 13:10:50 +00:00
parent 4a0f8d2d2a
commit 6beec7b2b2
6 changed files with 537 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
C11-FrontEnd/examples/C2.thy
View File

@ -175,6 +175,12 @@ int linearsearch(int x, int t[], int n) {
}
\<close>
ML\<open>
val p = @{here};
open Position;
ML_Syntax.print_position p;
writeln it;
\<close>
section\<open>Some realistic Selection sort with Input and Output\<close>
C\<open>
@ -189,8 +195,7 @@ int main()
printf("Enter %d integers\n", n);
for (c = 0; c < n; c++)
scanf("%d", &array[c]);
for (c = 0; c < n; c++) scanf("%d", &array[c]);
for (c = 0; c < (n - 1); c++)
{

3
C11-FrontEnd/examples/tp-preuve-c/README Normal file
View File

@ -0,0 +1,3 @@
/usr/local/isabelle/Isabelle2016-1 jedit -d autocorres-1.3 -l AutoCorres tp06a.thy

106
C11-FrontEnd/examples/tp-preuve-c/intro.thy Normal file
View File

@ -0,0 +1,106 @@
theory intro
imports AutoCorres
begin
(***
Equivalents to some of the terms from Xavier Rival's lecture on Coq: slides 6--7.
http://www.di.ens.fr/~rival/semverif-2017/sem-04-coq.pdf
***)
term "0"
term "1"
term "True"
typ nat
typ bool
term "\<lambda>(n::nat). n + 1"
value "(\<lambda>(n::nat). n + 1) 8"
term "\<exists>p::nat. 8 = 2 * p"
term "\<And>a b. a \<and> b \<Longrightarrow> a"
term "\<forall>a b. a \<and> b \<longrightarrow> a"
definition myzero :: nat
where
"myzero \<equiv> 0"
definition myone :: nat
where
"myone \<equiv> Suc 0"
fun myincr :: "nat \<Rightarrow> nat"
where
"myincr n = n + 1"
print_theorems
thm myincr.simps (* automatically generated rewrite rules *)
(***
Some simple proofs
***)
(* To type "\<and>", type "/" and then "\". *)
(* Similarly, "-->" gives "\<longrightarrow>", and "==>" gives "\<Longrightarrow>". *)
(* Alternatively, type (part of) the name in latex (<backslash> Longrightarrow...). *)
lemma "(a \<and> b) \<longrightarrow> (b \<and> a)"
find_theorems intro
apply (rule impI)
find_theorems elim
apply (erule conjE)
apply (rule conjI)
apply assumption
apply assumption
done
(* You can Ctrl-click on rules and symbols to jump to their definitions. *)
(* Pressing Ctrl-` jumps back to the previous file. *)
lemma "(a \<and> b) \<longrightarrow> (a \<and> b)"
apply simp (* Apply rewriting rules: LHS = RHS. *)
done
lemma "(a \<and> b) \<longrightarrow> (a \<and> b)"
apply clarsimp (* Safely apply rewriting rules and intro/elim/dest rules. *)
done
lemma "(a \<and> b) \<longrightarrow> (a \<and> b)"
apply auto (* Try lots of stuff... sometimes gives a mess. *)
done
lemma "(a \<and> b) \<longrightarrow> (b \<and> a)"
sledgehammer (* Ask Miami... *)
oops (* give up on proof *)
(* Type "[" then "|" for "\<lbrakk>". *)
lemma "\<lbrakk> a; b \<rbrakk> \<Longrightarrow> b \<and> a"
sorry (* cheat *)
lemma "myincr myzero = myone"
apply clarsimp (* apply myincr.simps *)
unfolding myzero_def myone_def
apply (rule refl)
done
(***
Equivalents to some of the Hoare rules in Antoine Miné's lecture on Axiomatic semantics:
slides 13--23
http://www.di.ens.fr/~rival/semverif-2015/sem-07-hoare.pdf
***)
find_theorems "\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>!"
thm skip_nf (* axiom for skip *)
thm validNF_return (* like rule of assignment *)
thm validNF_weaken_pre (* like rule of consequence *)
thm validNF_split_if (* Tests *)
thm validNF_bind (* Sequences *)
thm validNF_whileLoop (* loops *)
lemma "\<lbrace>\<lambda>s. True\<rbrace> do i \<leftarrow> return 2; return (i + 3) od \<lbrace>\<lambda>r s. r = 5 \<rbrace>!"
apply (rule validNF_bind)
apply (rule validNF_return)
apply (rule validNF_weaken_pre)
apply (rule validNF_return)
apply simp
done
(* try: apply wp
to activate the Verification Condition Generator / Weakest Precondition Calculator *)
end

21
C11-FrontEnd/examples/tp-preuve-c/tp06a.c Normal file
View File

@ -0,0 +1,21 @@
/*
* Determiner si le nombre donne 'n' est premier.
*
* Nous renvoyons 0 si 'n' est compose, ou pas-zero si 'n' est premier.
*/
unsigned int is_prime(unsigned int n)
{
/* Les nombres plus petits que 2 ne sont pas premiers. */
if (n < 2)
return 0;
/* Trouver le premier non insignifiant facteur de 'n'. */
unsigned int i = 2;
while (n % i != 0) {
i++;
}
/* Si le premier facteur est 'n' lui-meme, 'n' est premier. */
return (i == n);
}

147
C11-FrontEnd/examples/tp-preuve-c/tp06a.thy Normal file
View File

@ -0,0 +1,147 @@
theory tp06a
imports AutoCorres "~~/src/HOL/Number_Theory/Number_Theory"
begin
(* Parse the C file into the SIMPL language. *)
install_C_file "tp06a.c"
find_theorems (140) name:"tp06"
context tp06a begin
thm is_prime_impl (* The specification \<Gamma> maps names to program terms. *)
thm is_prime_body_def (* This is the SIMPL model of the imported C function. *)
end
(* Abstract the SIMPL model into a monadic model. *)
autocorres[ts_rules = nondet, unsigned_word_abs = is_prime is_prime] "tp06a.c"
print_theorems
context tp06a begin
typ "('a,'b) nondet_monad"
thm is_prime'_def (* This is the monadic model of the C function. *)
thm is_prime'_ac_corres (* This lemma relates monadic and SIMP models. *)
(* Loop invariant for "is_prime". *)
definition
is_prime_inv :: "nat \<Rightarrow> nat \<Rightarrow> bool"
where
"is_prime_inv i n \<equiv> i>1 \<and> 2 \<le> n \<and> n \<ge> i \<and> (\<forall>k<i. k>1 \<longrightarrow> n mod k \<noteq> 0) "
(* The loop invariant holds coming into the loop. *)
lemma is_prime_precond_implies_inv:
"\<lbrakk> 2 \<le> n; n \<le> UINT_MAX \<rbrakk> \<Longrightarrow> is_prime_inv 2 n"
by(auto simp: is_prime_inv_def)
(* The loop invariant holds for each loop iteration. *)
lemma is_prime_body_obeys_inv:
"\<lbrakk> is_prime_inv i n; n mod i \<noteq> 0 \<rbrakk> \<Longrightarrow> is_prime_inv (i + 1) n"
unfolding is_prime_inv_def apply auto
using less_SucE apply auto
by (metis Suc_leI le_neq_implies_less mod_self neq0_conv)
find_theorems (205) "prime (_::nat) = _"
thm prime_nat_simp
find_theorems "_ dvd _" "_ mod _"
thm dvd_eq_mod_eq_0[symmetric]
(* Q4. The loop invariant implies the post-condition. *)
lemma is_prime_inv_implies_postcondition:
"\<lbrakk> is_prime_inv i n; n mod i = 0 \<rbrakk> \<Longrightarrow> (i = n) \<longleftrightarrow> prime n"
unfolding is_prime_inv_def
proof (rule iffI, elim conjE, hypsubst)
assume "2 \<le> n" and "\<forall>k<n. 1 < k \<longrightarrow> n mod k \<noteq> 0"
show "prime n"
by (metis Suc_eq_plus1 Suc_le_eq \<open>2 \<le> n\<close> \<open>\<forall>k<n. 1 < k \<longrightarrow> n mod k \<noteq> 0\<close>
add.left_neutral dvd_eq_mod_eq_0 gr_implies_not0 less_one linorder_neqE_nat
nat_dvd_not_less numeral_2_eq_2 prime_factor_nat prime_gt_1_nat)
next
assume "1 < i \<and> 2 \<le> n \<and> i \<le> n \<and> (\<forall>k<i. 1 < k \<longrightarrow> n mod k \<noteq> 0)"
and "n mod i = 0" and "prime n "
have *: "1 < i"
using \<open>1 < i \<and> 2 \<le> n \<and> i \<le> n \<and> (\<forall>k<i. 1 < k \<longrightarrow> n mod k \<noteq> 0)\<close> by blast
show "i = n"
apply(insert `prime n` *)
apply(subst (asm) prime_nat_iff, clarify)
apply(subst (asm) Divides.semiring_div_class.dvd_eq_mod_eq_0)
apply(erule_tac x=i in allE)
by(simp only: `n mod i = 0`,auto)
qed
(* Measure function for "is_prime". Must be strictly decreasing
* for each loop iteration. *)
definition
is_prime_measure :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"is_prime_measure i n \<equiv> (n-i) (*** Q5. TODO ***)"
(* The loop measure decrements each loop iteration. *)
lemma is_prime_body_obeys_measure:
"\<lbrakk> is_prime_inv i n; n mod i \<noteq> 0 \<rbrakk>
\<Longrightarrow> is_prime_measure i n > is_prime_measure (i + 1) n"
unfolding is_prime_measure_def is_prime_inv_def
apply auto using le_eq_less_or_eq by auto
(*
* Show that "is_prime' n" is correct.
*
* AutoCorres has applied "word abstraction" to this function,
* meaning that you are able to reason using "nats" instead of
* "word32" data types, at the price of having to reason that
* your values do not overflow UINT_MAX.
*)
lemma is_prime_correct:
"\<lbrace>\<lambda>s. n \<le> UINT_MAX \<rbrace> is_prime' n \<lbrace>\<lambda>r s. r = (if prime n then 1 else 0) \<rbrace>!"
(* Move the precondition into the assumptions. *)
apply (rule validNF_assume_pre)
(* Unfold the program body. *)
apply (unfold is_prime'_def)
(* Annotate the loop with an invariant and measure. *)
apply (subst whileLoop_add_inv [
where I="\<lambda>r s. is_prime_inv r n"
and M="(\<lambda>(r, s). Suc n - r)"])
(*
* Run "wp" to generate verification conditions.
*)
proof (wp, intro conjI, elim conjE,simp_all)
(* 1. The loop body obeys the invariant; *)
fix s r
assume "n \<le> UINT_MAX" and "is_prime_inv r n" and "0 < n mod r"
then show "is_prime_inv (Suc r) n"
using is_prime_body_obeys_inv by auto
next
(* 2. The loop body causes the measure to decrease; *)
fix r fix sa sb::lifted_globals
assume "n \<le> UINT_MAX" and "is_prime_inv r n \<and> 0 < n mod r \<and> sb = sa"
then show "n - r < Suc n - r"
by (simp add: Suc_diff_le tp06a.is_prime_inv_def)
next
(* The loop counter never exceeds UINT_MAX. *)
fix r fix sa sb::lifted_globals (* very ugly that this pops up ... *)
assume "n \<le> UINT_MAX" and "is_prime_inv r n \<and> 0 < n mod r \<and> sb = sa"
then show "Suc r \<le> UINT_MAX"
by (metis Suc_eq_plus1 dual_order.trans gr_implies_not0 is_prime_body_obeys_inv
tp06a.is_prime_inv_def)
next
fix r
assume "n \<le> UINT_MAX" and "is_prime_inv r n" and "n mod r = 0"
then show " (r = n \<longrightarrow> prime n) \<and> (r \<noteq> n \<longrightarrow> \<not> prime n)"
by (simp add: tp06a.is_prime_inv_implies_postcondition)
next
(* The invariant implies the post-condition of the function. *)
assume " n \<le> UINT_MAX"
then show " (n < 2 \<longrightarrow> \<not> prime n) \<and> (\<not> n < 2 \<longrightarrow> is_prime_inv 2 n)"
by (metis le_antisym nat_le_linear nat_less_le prime_ge_2_nat
tp06a.is_prime_precond_implies_inv)
qed
end
end

253
C11-FrontEnd/examples/tp-preuve-c/tp06b.thy Normal file
View File

@ -0,0 +1,253 @@
theory tp06b
imports AutoCorres "~~/src/HOL/Number_Theory/Number_Theory"
begin
(* Parse the C file into SIMPL. *)
install_C_file "tp06a.c"
(* Note: The autocorres tool is not applied.
Here we reason on the SIMPL model directly *)
context tp06a begin
thm is_prime_impl (* The specification \<Gamma> maps names to program terms. *)
thm is_prime_body_def (* This is the SIMPL model of the imported C function. *)
term "unat"
(* with associated tactic: apply unat_arith *)
(* Nat version of is_prime_inv. *)
definition
is_prime_inv' :: "nat \<Rightarrow> nat \<Rightarrow> bool"
where
"is_prime_inv' i n \<equiv> 2 \<le> i \<and> i \<le> n \<and> (\<forall>m < i. 2 \<le> m \<longrightarrow> n mod m \<noteq> 0)"
(* Loop invariant for "is_prime". *)
definition
is_prime_inv :: "word32 \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool"
where
"is_prime_inv i init_n curr_n \<equiv> is_prime_inv' (unat i) (unat init_n) \<and> init_n = curr_n"
(* Measure function for "is_prime". Must be strictly decreasing
* for each loop iteration. *)
definition
is_prime_measure :: "word32 \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> nat"
where
"is_prime_measure i init_n curr_n \<equiv> unat init_n - unat i"
declare is_prime_inv_def [simp]
(* The loop invariant holds coming into the loop. *)
lemma is_prime_precond_implies_inv:
assumes "n \<ge> 2"
shows "is_prime_inv 2 n n"
proof -
have "unat n \<ge> 2" using assms by unat_arith
then show ?thesis by (clarsimp simp: is_prime_inv'_def )
qed
lemma is_prime_body_obeys_inv':
assumes "is_prime_inv' i n"
and "n mod i \<noteq> 0"
shows "is_prime_inv' (i + 1) n"
unfolding is_prime_inv'_def
proof(clarsimp , intro conjI)
show "Suc 0 \<le> i" using assms(1) is_prime_inv'_def by auto
next
show "Suc i \<le> n" by (metis Suc_leI assms(1) assms(2) le_neq_implies_less mod_self
tp06a.is_prime_inv'_def)
next
have * :"\<forall>m<i. 2 \<le> m \<longrightarrow> 0 < n mod m" using assms(1) tp06a.is_prime_inv'_def by blast
show "\<forall>m<Suc i. 2 \<le> m \<longrightarrow> 0 < n mod m" using "*" assms(2) less_antisym by blast
qed
(* The loop invariant holds for each loop iteration. *)
lemma is_prime_body_obeys_inv:
"\<lbrakk> is_prime_inv i init_n curr_n; curr_n mod i \<noteq> 0 \<rbrakk> \<Longrightarrow> is_prime_inv (i + 1) init_n curr_n"
apply clarsimp
apply (drule is_prime_body_obeys_inv')
apply (metis unat_eq_zero unat_mod)
apply (clarsimp simp: is_prime_inv'_def)
proof -
assume a1: "curr_n mod i \<noteq> 0"
assume a2: "Suc 0 \<le> unat i"
assume a3: "Suc (unat i) \<le> unat curr_n"
assume a4: "\<forall>m<Suc (unat i). 2 \<le> m \<longrightarrow> 0 < unat curr_n mod m"
{ fix nn :: nat
have ff1: "\<And>n na. (n::nat) < na \<or> \<not> n + 1 \<le> na"
by presburger
have ff2: "of_nat (unat curr_n mod unat i) \<noteq> (0::32 word)"
using a1 by (metis word_arith_nat_defs(7))
have ff3: "unat (1::32 word) = 1 \<or> (1::32 word) = 0"
by (metis (no_types) Groups.add_ac(2) Suc_eq_plus1 add.right_neutral unatSuc unat_0)
have ff4: "unat i \<noteq> 0"
using a2 by linarith
have "unat (1 + i) = 1 + unat i \<or> (0::32 word) = 1"
using ff3 a3 by (metis (no_types) Groups.add_ac(2) Suc_eq_plus1 le_simps(2)
less_Suc_unat_less_bound unat_add_lem)
then have "unat i \<noteq> 1 \<and> 1 + i \<noteq> 0"
using ff4 ff2 by (metis Groups.add_ac(2) Suc_eq_plus1 add_0_left mod_less_divisor nat.simps(3)
neq0_conv not_less_eq semiring_1_class.of_nat_simps(1) unat_0)
then have "2 \<le> unat (i + 1) \<and> unat (i + 1) \<le> unat curr_n \<and>
(\<not> nn < unat (i + 1) \<or> \<not> 2 \<le> nn \<or> 0 < unat curr_n mod nn)"
using ff4 ff1 a4 a3 by (metis (no_types) Divides.mod_less Groups.add_ac(2) Suc_eq_plus1
le_less linorder_not_less mod2_gr_0 neq0_conv unatSuc) }
then show "2 \<le> unat (i + 1) \<and> unat (i + 1) \<le> unat curr_n \<and>
(\<forall>n<unat (i + 1). 2 \<le> n \<longrightarrow> 0 < unat curr_n mod n)"
by blast
qed
lemma unat_plus_one:
"a < (b :: 'a::len word) \<Longrightarrow> unat (a + 1) = unat a + 1"
using less_is_non_zero_p1 word_overflow_unat by blast
(* The loop measure decrements each loop iteration. *)
lemma is_prime_body_obeys_measure:
"\<lbrakk> is_prime_inv i init_n curr_n; curr_n mod i \<noteq> 0 \<rbrakk>
\<Longrightarrow> is_prime_measure i init_n curr_n > is_prime_measure (i + 1) init_n curr_n"
apply (clarsimp simp: is_prime_inv'_def is_prime_measure_def)
apply (case_tac "curr_n = i")
apply clarsimp
apply (metis mod_self unat_eq_zero unat_mod)
apply (subst unat_plus_one [where b=curr_n])
apply (metis word_le_less_eq word_le_nat_alt)
apply (metis One_nat_def add.commute add_Suc diff_less_mono2 le_neq_implies_less
lessI monoid_add_class.add.left_neutral word_unat.Rep_inject)
done
(* The loop invariant implies the post-condition. *)
lemma is_prime_inv_implies_postcondition:
"\<lbrakk> is_prime_inv i init_n curr_n; curr_n mod i = 0 \<rbrakk>
\<Longrightarrow> prime (unat init_n) \<longleftrightarrow> (i = curr_n)"
apply (clarsimp simp: is_prime_inv'_def)
apply (rule iffI)
apply (clarsimp simp: prime_nat_code)
apply (metis (no_types, hide_lams) greaterThanLessThan_iff le_neq_implies_less less_eq_Suc_le
less_numeral_extra(3) mod_greater_zero_iff_not_dvd numeral_2_eq_2 unat_0 unat_mod
word_unat.Rep_inject)
apply (clarsimp simp: prime_nat_iff')
apply (drule_tac x=n in spec)
apply (metis Suc_1 arith_is_1 dvd_imp_mod_0 eq_iff less_eq_Suc_le not_less_eq_eq )
done
(*
* Show that "is_prime' n" is correct.
*
* Note that there are two ways of writing variables: \<acute>n and
* (n_' s). The first fetches the value "n" from an implicitly
* specified state, while the second fetches the value "n" from state
* "s". While less pretty, it is generally easier to use the latter.
*)
lemma is_prime_correct:
"\<Gamma> \<turnstile>\<^sub>t {s. n_' s = n }
\<acute>ret__unsigned :== PROC is_prime(n)
{t. ret__unsigned_' t = (if prime (unat n) then 1 else 0) }"
(* Unfold the program's body. *)
apply (hoare_rule HoareTotal.ProcNoRec1)
apply (unfold creturn_def)
(* Annotate the loop with an invariant and measure. *)
apply (subst whileAnno_def)
apply (subst whileAnno_def [symmetric, where
I="{s. is_prime_inv (i_' s) n (n_' s) }" and
V="measure (\<lambda>s. is_prime_measure (i_' s) n (n_' s))"])
(*
* Run the VCG.
*
* You will need to prove (i) the function's precondition implies your
* loop's invariant; (ii) the loop invariant holds each time the loop
* executes; (iii) the measure decreases each time the loop exceutes;
* and (iv) when the loop has finished, the loop invariant implies the
* functions post-condition.
*
* Spend some time looking at the vcg's output to make sure you know
* what the goals it is leaving you correspond to.
*)
apply vcg
apply (clarsimp simp del: is_prime_inv_def)
apply rule
apply (fastforce dest: x_less_2_0_1)
apply (clarsimp simp del: is_prime_inv_def)
apply (rule is_prime_precond_implies_inv, simp)
apply (clarsimp simp del: is_prime_inv_def)
apply (intro conjI)
apply (clarsimp simp: is_prime_inv'_def)
apply (metis le_eq_less_or_eq less_is_non_zero_p1 mod_self
unat_eq_zero unat_mod word_less_nat_alt word_unat.Rep_inject)
apply (erule (1) is_prime_body_obeys_measure)
apply (erule (1) is_prime_body_obeys_inv)
apply (drule is_prime_inv_implies_postcondition)
apply simp
apply clarsimp
done
lemma is_prime_correct_structured:
"\<Gamma> \<turnstile>\<^sub>t {s. n_' s = n }
\<acute>ret__unsigned :== PROC is_prime(n)
{t. ret__unsigned_' t = (if prime (unat n) then 1 else 0) }"
(* Unfold the program's body. *)
apply (hoare_rule HoareTotal.ProcNoRec1,unfold creturn_def)
(* Annotate the loop with an invariant and measure. *)
apply (subst whileAnno_def)
apply (subst whileAnno_def [symmetric, where
I="{s. is_prime_inv (i_' s) n (n_' s) }" and
V="measure (\<lambda>s. is_prime_measure (i_' s) n (n_' s))"])
proof vcg (* run vcg, the verification condition generator *)
text{* prove (i) the function's precondition implies your loop's invariant *}
fix n::"32 word"
show "(n < scast (2::32 signed word)
\<longrightarrow> scast (0::32 signed word) = (if prime (unat n) then 1 else 0)) \<and>
(\<not> n < scast (2::32 signed word)
\<longrightarrow> scast (2::32 signed word) \<noteq> (0::32 word)
\<and> is_prime_inv (scast (2::32 signed word)) n n)"
apply (clarsimp simp del: is_prime_inv_def, rule)
apply (fastforce dest: x_less_2_0_1, rule)
by (rule is_prime_precond_implies_inv, simp)
next
text{* prove loop correctness: *}
fix n' i ::"32 word"
assume *:"is_prime_inv i n n'"
and **:"n' mod i \<noteq> scast (0::32 signed word)"
have ***: "i + 1 \<noteq> 0" apply (insert * **, clarsimp simp del: is_prime_inv_def)
apply (clarsimp simp: is_prime_inv'_def)
by (metis le_eq_less_or_eq less_is_non_zero_p1 mod_self
unat_eq_zero unat_mod word_less_nat_alt word_unat.Rep_inject)
show "i + scast (1::32 signed word) \<noteq> (0::32 word)
\<and> is_prime_measure (i + scast (1::32 signed word)) n n' < is_prime_measure i n n'
\<and> is_prime_inv (i + scast (1::32 signed word)) n n'"
proof(auto simp: *** simp del: is_prime_inv_def)
text{* This breaks down to prove (ii) the loop measure decreases *}
show "is_prime_measure (i + 1) n n' < is_prime_measure i n n'"
using "*" "**" is_prime_body_obeys_measure by auto
next
text{* and to prove (iii) invariant holds each time the loop executes*}
show "is_prime_inv (i + 1) n n'"
using "*" "**" is_prime_body_obeys_inv by auto
qed
next
text{* prove (iv) when the loop has finished, the loop invariant implies the post-condition*}
fix n' i ::"32 word"
assume *:"is_prime_inv i n n'"
and **:"\<not> n' mod i \<noteq> scast (0::32 signed word)"
show "scast (if i = n' then 1 else (0::32 signed word)) =
(if prime (unat n) then 1 else 0)"
by (insert * **,drule is_prime_inv_implies_postcondition) clarsimp+
qed
text{* The comparison of these two styles is interesting: one the one hand, the apply style is
much shorter since all the hairy details of typing words and constants 0 and 1's were implicitly
and safely inferred from prior proof states; on the other hand, a fine eye for these gory details
reveals much of the underlying semantic complexity going on in this proof. *}
end
end