Skip to content
Snippets Groups Projects
Commit abc9ac81 authored by bu's avatar bu
Browse files

first sorry-free, complete solution (but not yet cleaned up).

parent 535ea708
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy
+ 93
− 9
View file @ abc9ac81
......@@ -453,7 +453,11 @@ proof (rule validNF_assume_pre)
next
text\<open>@{term is_prime_inv} initially holds when entering the loop.\<close>
fix s::lifted_globals
have **** : "\<not> n < 4 \<Longrightarrow> partial_prime n 5" sorry
have **** : "\<not> n < 4 \<Longrightarrow> partial_prime n 5"
apply(insert \<open>odd n\<close> \<open>\<not> 3 dvd n\<close>)
apply(auto simp: partial_prime_def)
by (metis dvd_trans even_Suc even_zero le_def less_antisym numeral_2_eq_2
numeral_3_eq_3 numeral_eqs(4))
show "if n < 2 then (0 \<noteq> 0) = prime n
else if n < 4 then (1 \<noteq> 0) = prime n
else is_prime_inv n 5 s"
......@@ -509,25 +513,105 @@ proof (rule validNF_assume_pre)
apply(insert 100 \<open>r * r \<le> n\<close> \<open>5 \<le> r\<close>)
by(erule exE, rename_tac "m", simp add: Nat.add_mult_distrib)
qed
next
next
text\<open>@{term is_prime_inv} implies postcond when leaving the loop.\<close>
fix r::nat fix s::lifted_globals
assume * :"\<not> (r < 65531 \<and> r * r \<le> n)"
have ** : "r\<ge>65531 \<or> r * r>n" using "*" leI by blast
assume ***: "is_prime_inv n r s"
show "((1::nat) \<noteq> 0) = prime n"
apply simp
apply(case_tac "r\<ge>65531") defer 1
using "*" "***" apply auto[1]
using "**" partial_prime_sqr apply blast
apply(insert ***)
have **** : "partial_prime n r" using "***" by auto
show "((1::nat) \<noteq> 0) = prime n"
proof(simp,insert **,elim disjE)
assume "65531 \<le> r"
have 1000 : "r = 65531 \<or> r = 65532 \<or> r = 65533 \<or> r = 65534 \<or> r = 65535 \<or> r \<ge> SQRT_UINT_MAX"
unfolding SQRT_UINT_MAX_def
apply(insert \<open>65531 \<le> r\<close>)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
by(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
have "r\<le>n" using "***" by auto
show "prime n"
(* feasible : between 65531 and 65536 (the integer square of no primes,
SQRT_UINT_MAX), there are no primes. *)
sorry
apply(rule partial_prime_sqr[of _ "SQRT_UINT_MAX", THEN iffD1])
apply (metis "1" One_nat_def SQRT_UINT_MAX_def mult_is_0 nat_le_Suc_less
neq0_conv rel_simps(76) uint_max_factor)
unfolding SQRT_UINT_MAX_def
apply(insert **** \<open>r\<le>n\<close> \<open>65531 \<le> r\<close>)
apply (subst partial_prime_def, auto)
apply(erule_tac Q = "i dvd n" in contrapos_pp)
apply(case_tac "i < r")
apply (simp add: partial_prime_def, simp add: not_less_eq less_Suc_eq_le)
proof -
fix i :: nat
assume a : "partial_prime n r"
and b: "65531 \<le> r"
and c: "i < n"
and d: "i < 65536"
and e: "r \<le> i"
have g : "r \<le> n"
by (simp add: \<open>r \<le> n\<close>)
have h : "65531 \<le> i"
using b e order.trans by blast
have i : "i = 65531 \<or> i = 65532 \<or> i = 65533 \<or> i = 65534 \<or> i = 65535"
apply(insert \<open>65531 \<le> i\<close>)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
apply(subst (asm) Nat.less_eq_Suc_le, simp)
apply(subst (asm) Nat.le_eq_less_or_eq, elim disjE, simp_all)
using d by linarith
show "\<not> i dvd n"
proof(insert i, elim disjE)
have X : "(19::nat) dvd 65531" by simp
have "r\<le>n" using "***" by auto
have "\<not>((19::nat) dvd n)" apply(insert b)
using a g partial_prime_def by fastforce
show "i = 65531 \<Longrightarrow> \<not> i dvd n"
apply(insert **** X \<open>r\<le>n\<close> )
using \<open>\<not> 19 dvd n\<close> gcd_nat.trans by blast
next
show "i = 65532 \<Longrightarrow> \<not> i dvd n"
using \<open>odd n\<close> aux99 gcd_nat.trans by blast
next
have "(13::nat) dvd 65533" by simp
have "\<not>((13::nat) dvd n)" apply(insert b)
using a g partial_prime_def by fastforce
show "i = 65533 \<Longrightarrow> \<not> i dvd n"
using \<open>\<not> 13 dvd n\<close> aux98 gcd_nat.trans by blast
next
show "i = 65534 \<Longrightarrow> \<not> i dvd n"
using \<open>odd n\<close> aux97 gcd_nat.trans
by blast
next
have "(3::nat) dvd 65535" by(simp)
have "\<not> 3 dvd n"
by (simp add: False)
show "i = 65535 \<Longrightarrow> \<not> i dvd n"
using False \<open>3 dvd 65535\<close> dvd_trans by blast
qed
qed
next
assume "n < r * r"
show "prime n"
using "****" \<open>n < r * r\<close> partial_prime_sqr by blast
qed
qed
qed
qed
qed
qed
end
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment