Commit 9c12e4d7 authored by MARCHE Claude's avatar MARCHE Claude

Merge remote-tracking branch 'berghofer/master'

parents 467c7a6b 70b9f3f6
......@@ -1089,22 +1089,22 @@ ifeq (@enable_isabelle_libs@,yes)
ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
ISABELLELIBS_BOOL_FILES = # not yet realized : Bool
ISABELLELIBS_BOOL_FILES = Bool
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/bool/, $(ISABELLELIBS_BOOL_FILES)))
ISABELLELIBS_REAL_FILES = # not yet realized : Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES)))
ISABELLELIBS_NUMBER_FILES = # not yet realized : Divisibility Gcd Parity Prime
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/number/, $(ISABELLELIBS_NUMBER_FILES)))
ISABELLELIBS_SET_FILES = Set Fset
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_MAP_FILES = Map # not yet realized : MapPermut
ISABELLELIBS_MAP_FILES = Map Occ MapPermut MapInjection
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELIBS_MAP_FILES)))
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/list/, $(ISABELLELIBS_LIST_FILES)))
drivers/isabelle-realizations.aux: Makefile
......
......@@ -28,6 +28,7 @@ end
theory bool.Bool
syntax function andb "<app><const name=\"HOL.conj\"/>%1%2</app>"
syntax function orb "<app><const name=\"HOL.disj\"/>%1%2</app>"
syntax function xorb "<app><const name=\"HOL.Not\"/><app><const name=\"HOL.eq\"/>%1%2</app></app>"
syntax function notb "<app><const name=\"HOL.Not\"/>%1</app>"
syntax function implb "<app><const name=\"HOL.implies\"/>%1%2</app>"
end
......@@ -109,6 +110,15 @@ theory list.NthNoOpt
syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
end
theory list.HdTlNoOpt
syntax function hd "<app><const name=\"List.hd\"/>%1</app>"
syntax function tl "<app><const name=\"List.tl\"/>%1</app>"
end
theory list.Distinct
syntax predicate distinct "<app><const name=\"List.distinct\"/>%1</app>"
end
theory option.Option
syntax type option "<type name=\"Option.option\">%1</type>"
......@@ -135,5 +145,26 @@ theory set.Fset
syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
end
theory number.Parity
syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.odd\"/>%1</app>"
end
theory number.Divisibility
syntax predicate divides "<app><const name=\"Rings.dvd_class.dvd\"/>%1%2</app>"
end
theory number.Gcd
syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime_class.prime\"/>%1</app>"
end
theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
end
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "isabelle-realizations.aux"
......@@ -4,6 +4,8 @@ imports
Why3_Set
Why3_List
Why3_Int
Why3_Bool
Why3_Number
begin
end
theory Why3_Bool
imports Why3_Setup
begin
section {* Basic theory of Booleans *}
why3_open "bool/Bool.xml"
why3_vc andb_def by (simp split add: bool.split)
why3_vc orb_def by (simp split add: bool.split)
why3_vc xorb_def by (simp split add: bool.split)
why3_vc notb_def by (simp split add: bool.split)
why3_vc implb_def by (simp split add: bool.split)
why3_end
end
......@@ -83,6 +83,15 @@ why3_open "list/HdTl.xml"
why3_end
why3_open "list/HdTlNoOpt.xml"
why3_vc hd_cons by simp
why3_vc tl_cons by simp
why3_end
section {* Relation between head, tail, and nth *}
why3_open "list/NthHdTl.xml"
......@@ -158,4 +167,119 @@ why3_vc reverse_reverse by simp
why3_end
section {* Reverse append *}
why3_open "list/RevAppend.xml"
why3_vc rev_append_append_l
by (induct r arbitrary: t) simp_all
why3_vc rev_append_append_r
proof (induct s arbitrary: r)
case (Cons x xs)
show ?case by (simp add: Cons [symmetric])
qed simp
why3_vc rev_append_length
by (induct s arbitrary: t) simp_all
why3_end
section {* Zip *}
why3_open "list/Combine.xml"
why3_end
section {* List with pairwise distinct elements *}
why3_open "list/Distinct.xml"
why3_vc distinct_zero by simp
why3_vc distinct_one by simp
why3_vc distinct_many using assms by simp
why3_vc distinct_append using assms by auto
why3_end
section {* Number of occurrences in a list *}
why3_open "list/NumOcc.xml"
lemma num_occ_nonneg: "0 \<le> num_occ x xs"
by (induct xs) simp_all
why3_vc Mem_Num_Occ
proof (induct l)
case (Cons y ys)
from num_occ_nonneg [of y ys]
have "0 < 1 + num_occ y ys" by simp
with Cons show ?case by simp
qed simp
why3_vc Append_Num_Occ
by (induct l1) simp_all
why3_end
section {* Permutation of lists *}
why3_open "list/Permut.xml"
why3_vc Permut_refl by (simp add: permut_def)
why3_vc Permut_sym using assms by (simp add: permut_def)
why3_vc Permut_trans using assms by (simp add: permut_def)
why3_vc Permut_cons using assms by (simp add: permut_def)
why3_vc Permut_swap by (simp add: permut_def)
why3_vc Permut_cons_append by (simp add: permut_def Append_Num_Occ)
why3_vc Permut_assoc by (simp add: permut_def)
why3_vc Permut_append using assms by (simp add: permut_def Append_Num_Occ)
why3_vc Permut_append_swap by (simp add: permut_def Append_Num_Occ)
why3_vc Permut_mem using assms by (simp add: permut_def Mem_Num_Occ)
why3_vc Permut_length
using assms
proof (induct l1 arbitrary: l2)
case Nil
then show ?case
proof (cases l2)
case (Cons x xs)
with Nil num_occ_nonneg [of x xs]
show ?thesis by (auto simp add: permut_def dest: spec [of _ x])
qed simp
next
case (Cons x xs)
from `permut (x # xs) l2` have "x \<in> set l2"
by (rule Permut_mem) simp
then obtain ys zs where "l2 = ys @ x # zs"
by (auto simp add: in_set_conv_decomp)
with Cons have "permut (x # xs) (ys @ x # zs)" by simp
moreover have "permut (ys @ x # zs) ((x # zs) @ ys)"
by (rule Permut_append_swap)
ultimately have "permut (x # xs) ((x # zs) @ ys)"
by (rule Permut_trans)
then have "permut xs (zs @ ys)" by (simp add: permut_def)
then have "int (length xs) = int (length (zs @ ys))" by (rule Cons)
with `l2 = ys @ x # zs` show ?case by simp
qed
why3_end
end
......@@ -2,6 +2,8 @@ theory Why3_Map
imports Why3_Setup
begin
section {* Generic Maps *}
why3_open "map/Map.xml"
why3_vc Const by simp
......@@ -16,4 +18,152 @@ why3_vc Select_neq
why3_end
section {* Number of occurrences *}
definition occ :: "'a \<Rightarrow> (int \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
"occ v m l u = int (card (m -` {v} \<inter> {l..<u}))"
why3_open "map/Occ.xml"
constants
occ = occ
why3_vc occ_empty
using assms
by (simp add: occ_def)
why3_vc occ_right_no_add
proof -
from assms have "{l..<u} = {l..<u - 1} \<union> {u - 1}" by auto
with assms show ?thesis by (simp add: occ_def)
qed
why3_vc occ_right_add
proof -
from assms have "{l..<u} = {l..<u - 1} \<union> {u - 1}" by auto
with assms show ?thesis by (simp add: occ_def)
qed
why3_vc occ_bounds
proof -
have "card ({l..<u} \<inter> m -` {v}) \<le> card {l..<u}"
by (blast intro: card_mono)
moreover have "card ({l..<u} - m -` {v}) = card {l..<u} - card ({l..<u} \<inter> m -` {v})"
by (blast intro: card_Diff_subset_Int)
ultimately have "card {l..<u} = card ({l..<u} - m -` {v}) + card ({l..<u} \<inter> m -` {v})"
by simp
with assms show ?C2
by (simp add: occ_def Int_commute)
qed (simp add: occ_def)
why3_vc occ_append
proof -
from assms have "{l..<u} = {l..<mid} \<union> {mid..<u}"
by (simp add: ivl_disj_un)
moreover have "m -` {v} \<inter> {l..<mid} \<inter> (m -` {v} \<inter> {mid..<u}) =
m -` {v} \<inter> ({l..<mid} \<inter> {mid..<u})"
by auto
ultimately show ?thesis
by (simp add: occ_def Int_Un_distrib card_Un_disjoint)
qed
why3_vc occ_neq
using assms
by (auto simp add: occ_def)
why3_vc occ_exists
using assms
by (auto simp add: occ_def card_gt_0_iff)
why3_vc occ_pos
using assms
by (auto simp add: occ_def card_gt_0_iff)
why3_vc occ_eq
proof -
from assms have "m1 -` {v} \<inter> {l..<u} = m2 -` {v} \<inter> {l..<u}" by auto
then show ?thesis by (simp add: occ_def)
qed
why3_end
why3_open "map/MapPermut.xml"
why3_vc permut_trans
using assms
by (simp add: permut_def)
why3_vc permut_exists
proof -
from assms have "0 < occ (a2 i) a1 l u"
by (simp add: permut_def occ_pos)
then show ?thesis by (auto dest: occ_exists)
qed
why3_end
section {* Injectivity and surjectivity for maps (indexed by integers) *}
why3_open "map/MapInjection.xml"
why3_vc injective_surjective
proof -
have "finite {0..<n}" by simp
moreover from assms have "a ` {0..<n} \<subseteq> {0..<n}"
by (auto simp add: range_def)
moreover from assms have "inj_on a {0..<n}"
by (force intro!: inj_onI simp add: injective_def)
ultimately have "a ` {0..<n} = {0..<n}" by (rule endo_inj_surj)
then have "{0..<n} \<subseteq> a ` {0..<n}" by simp
then show ?thesis by (force simp add: surjective_def)
qed
why3_vc injection_occ
unfolding injective_def occ_def
proof
assume H: "\<forall>i j. 0 \<le> i \<and> i < n \<longrightarrow> 0 \<le> j \<and> j < n \<longrightarrow> i \<noteq> j \<longrightarrow> m i \<noteq> m j"
show "\<forall>v. int (card (m -` {v} \<inter> {0..<n})) \<le> 1"
proof
fix v
let ?S = "m -` {v} \<inter> {0..<n}"
show "int (card ?S) \<le> 1"
proof (rule ccontr)
assume "\<not> int (card ?S) \<le> 1"
with card_le_Suc_iff [of ?S 1]
obtain x S where "?S = insert x S"
"x \<notin> S" "1 \<le> card S" "finite S"
by auto
with card_le_Suc_iff [of S 0]
obtain x' S' where "S = insert x' S'" by auto
with `?S = insert x S` `x \<notin> S`
have "m x = v" "m x' = v" "x \<noteq> x'" "0 \<le> x" "x < n" "0 \<le> x'" "x' < n"
by auto
with H show False by auto
qed
qed
next
assume H: "\<forall>v. int (card (m -` {v} \<inter> {0..<n})) \<le> 1"
show "\<forall>i j. 0 \<le> i \<and> i < n \<longrightarrow> 0 \<le> j \<and> j < n \<longrightarrow> i \<noteq> j \<longrightarrow> m i \<noteq> m j"
proof (intro strip notI)
fix i j
let ?S = "m -` {m i} \<inter> {0..<n}"
assume "0 \<le> i \<and> i < n" "0 \<le> j \<and> j < n" "i \<noteq> j" "m i = m j"
have "finite ?S" by simp
moreover from `0 \<le> i \<and> i < n` have "i \<in> ?S" by simp
ultimately have S: "card ?S = Suc (card (?S - {i}))"
by (rule card.remove)
have "finite (?S - {i})" by simp
moreover from `0 \<le> j \<and> j < n` `i \<noteq> j` `m i = m j`
have "j \<in> ?S - {i}" by simp
ultimately have "card (?S - {i}) = Suc (card (?S - {i} - {j}))"
by (rule card.remove)
with S have "\<not> int (card ?S) \<le> 1" by simp
with H show False by simp
qed
qed
why3_end
end
theory Why3_Number
imports
Why3_Int
"~~/src/HOL/Number_Theory/Primes"
begin
section {* Parity properties *}
why3_open "number/Parity.xml"
why3_vc even_def by (simp add: even_equiv_def)
why3_vc odd_def by (simp add: odd_equiv_def)
why3_vc even_or_odd by auto
why3_vc even_not_odd using assms by simp
why3_vc odd_not_even using assms by simp
why3_vc even_odd using assms by simp
why3_vc odd_even using assms by simp
why3_vc even_even using assms by simp
why3_vc odd_odd using assms by simp
why3_vc even_2k by simp
why3_vc odd_2k1 by simp
why3_end
section {* Divisibility *}
why3_open "number/Divisibility.xml"
why3_vc divides_def by (simp add: dvd_def mult_commute)
why3_vc divides_refl by simp
why3_vc divides_1_n by simp
why3_vc divides_0 by simp
why3_vc divides_left using assms by simp
why3_vc divides_right using assms by simp
why3_vc divides_oppr using assms by simp
why3_vc divides_oppl using assms by simp
why3_vc divides_oppr_rev using assms by simp
why3_vc divides_oppl_rev using assms by simp
why3_vc divides_plusr using assms by simp
why3_vc divides_minusr using assms by simp
why3_vc divides_multl using assms by simp
why3_vc divides_multr using assms by simp
why3_vc divides_factorl by simp
why3_vc divides_factorr by simp
why3_vc divides_n_1 using assms by auto
why3_vc divides_antisym
using assms
by (auto dest: zdvd_antisym_abs)
why3_vc divides_trans using assms by (rule dvd_trans)
why3_vc divides_bounds using assms by (simp add: dvd_imp_le_int)
why3_vc mod_divides_euclidean
using assms
by (auto simp add: emod_def split add: split_if_asm)
why3_vc divides_mod_euclidean
using assms
by (simp add: emod_def dvd_eq_mod_eq_0 zabs_def zmod_zminus2_eq_if)
why3_vc mod_divides_computer
using assms
by (auto simp add: cmod_def zabs_def sgn_0_0 zmod_zminus1_eq_if
not_sym [OF less_imp_neq [OF pos_mod_bound]]
split add: split_if_asm)
why3_vc divides_mod_computer
using assms
by (simp add: cmod_def dvd_eq_mod_eq_0 zabs_def
zmod_zminus1_eq_if zmod_zminus2_eq_if)
why3_vc even_divides by (rule int_even_iff_2_dvd)
why3_vc odd_divides by (simp add: int_even_iff_2_dvd)
why3_end
section {* Greateast Common Divisor *}
why3_open "number/Gcd.xml"
why3_vc gcd_nonneg by simp
why3_vc gcd_def1 by simp
why3_vc gcd_def2 by simp
why3_vc gcd_def3 using assms by (rule gcd_greatest_int)
why3_vc gcd_unique using assms
by (simp add: gcd_unique_int [symmetric])
why3_vc Comm by (rule gcd_commute_int)
why3_vc Assoc by (rule gcd_assoc_int)
why3_vc gcd_0_pos using assms by simp
why3_vc gcd_0_neg using assms by simp
why3_vc gcd_opp by simp
why3_vc gcd_euclid
using gcd_add_mult_int [of a "- q" b]
by (simp add: sign_simps)
why3_vc Gcd_computer_mod
using assms gcd_add_mult_int [of b "- 1" "a mod b"]
by (simp add: cmod_def zabs_def gcd_red_int [symmetric] sgn_if sign_simps)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b])
why3_vc Gcd_euclidean_mod
using assms gcd_add_mult_int [of b "- 1" "a mod b"]
by (simp add: emod_def zabs_def gcd_red_int [symmetric] sign_simps)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b])
why3_vc gcd_mult using assms
by (simp add: gcd_mult_distrib_int [symmetric])
why3_end
section {* Prime numbers *}
why3_open "number/Prime.xml"
why3_vc prime_def
unfolding prime_int_altdef
proof
assume "1 < p \<and> (\<forall>m\<ge>0. m dvd p \<longrightarrow> m = 1 \<or> m = p)"
then have "1 < p" and H: "\<And>m. m \<ge> 0 \<Longrightarrow> m dvd p \<Longrightarrow> m = 1 \<or> m = p"
by auto
show "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)"
proof
from `1 < p` show "2 \<le> p" by simp
show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
proof (intro strip)
fix n
assume "1 < n \<and> n < p"
with H [of n] show "\<not> n dvd p" by auto
qed
qed
next
assume "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)"
then have "2 \<le> p" and H: "\<And>n. 1 < n \<Longrightarrow> n < p \<Longrightarrow> \<not> n dvd p"
by auto
show "1 < p \<and> (\<forall>m\<ge>0. m dvd p \<longrightarrow> m = 1 \<or> m = p)"
proof
from `2 \<le> p` show "1 < p" by simp
show "\<forall>m\<ge>0. m dvd p \<longrightarrow> m = 1 \<or> m = p"
proof (intro strip)
fix m
assume "0 \<le> m" "m dvd p"
with `2 \<le> p` have "1 \<le> m" by (cases "m = 0") auto
show "m = 1 \<or> m = p"
proof (cases "m = 1")
case False
show ?thesis
proof (cases "m = p")
case False
from `2 \<le> p` `m dvd p` have "m \<le> p" by (simp add: zdvd_imp_le)
with False `m \<noteq> 1` `1 \<le> m` `m dvd p` H show ?thesis by simp
qed simp
qed simp
qed
qed
qed
why3_vc not_prime_1 by simp
why3_vc prime_2 by simp
why3_vc prime_3 by simp
why3_vc prime_divisors
using assms
by (auto simp add: prime_int_altdef dest: spec [of _ "\<bar>d\<bar>"])
lemma small_divisors_aux:
"1 < (n::nat) \<Longrightarrow> n < p \<Longrightarrow> n dvd p \<Longrightarrow> \<exists>d. prime d \<and> d * d \<le> p \<and> d dvd p"
proof (induct n rule: less_induct)
case (less n)
then obtain m where "p = n * m" by (auto simp add: dvd_def)
show ?case
proof (cases "prime n")
case True
show ?thesis
proof (cases "n \<le> m")
case True
with `p = n * m` `prime n`
show ?thesis by auto
next
case False
then have "m < n" by simp
moreover from `n < p` `p = n * m` have "1 < m" by simp
moreover from `1 < n` `n < p` `p = n * m` have "m < p" by simp
moreover from `p = n * m` have "m dvd p" by simp
ultimately show ?thesis by (rule less)
qed
next
case False
with `1 < n` obtain k where "k dvd n" "k \<noteq> 1" "k \<noteq> n"
by (auto simp add: prime_nat_def)
with `1 < n` have "k \<le> n" by (simp add: dvd_imp_le)
with `k \<noteq> n` have "k < n" by simp
moreover from `k dvd n` `1 < n` have "k \<noteq> 0" by (rule_tac notI) simp
with `k \<noteq> 1` have "1 < k" by simp
moreover from `k < n` `n < p` have "k < p" by simp
moreover from `k dvd n` `n dvd p` have "k dvd p" by (rule dvd.order_trans)
ultimately show ?thesis by (rule less)
qed
qed
why3_vc small_divisors
unfolding prime_def
proof
show "2 \<le> p" by fact
show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
proof (intro strip)
fix n
assume "1 < n \<and> n < p"
show "\<not> n dvd p"
proof
assume "n dvd p"
with `1 < n \<and> n < p`
have "1 < nat n" "nat n < nat p" "nat n dvd nat p"
by (simp_all add: transfer_nat_int_relations)
then have "\<exists>d. prime d \<and> d * d \<le> nat p \<and> d dvd (nat p)"
by (rule small_divisors_aux)
with `2 \<le> p` obtain d
where d: "prime (int d)" "int d * int d \<le> p" "int d dvd p"
by (auto simp add: prime_int_def int_dvd_iff le_nat_iff int_mult)
from `prime (int d)` have "2 \<le> int d" by auto
with `2 \<le> int d` have "2 * 2 \<le> int d * int d"
by (rule mult_mono) simp_all
with d assms `2 \<le> int d` show False by auto
qed
qed
qed
why3_vc even_prime
proof -
from `prime p` have "2 \<le> p" by auto
with `prime p` `even p` show ?thesis
by (auto simp add: order_le_less prime_odd_int)
qed
why3_vc odd_prime
proof -
from `prime p` have "2 \<le> p" by auto
with `prime p` `3 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_int)
qed
why3_end
section {* Coprime numbers *}
why3_open "number/Coprime.xml"
why3_vc coprime_def ..
why3_vc prime_coprime
proof -
have "(\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p) =
(\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p)"
proof
assume H: "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
show "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
proof (intro strip)
fix n
assume H': "1 \<le> n \<and> n < p"
{
fix d
assume "0 \<le> d" "d dvd n" "d dvd p"
with H' have "d \<noteq> 0" by auto
have "d = 1"
proof (rule ccontr)
assume "d \<noteq> 1"
with `0 \<le> d` `d \<noteq> 0` have "1 < d" by simp
moreover from `d dvd p` H' have "d \<le> p" by (auto dest: zdvd_imp_le)
moreover from `d dvd n` H' have "d \<noteq> p" by (auto dest: zdvd_imp_le)
ultimately show False using `d dvd p` H by auto