Realize more of the map, number and bool theories in Isabelle

Makefile.in

@@ -1089,19 +1089,19 @@ 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

drivers/isabelle-common.gen

@@ -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
@@ -135,5 +136,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"

lib/isabelle/Why3.thy

@@ -4,6 +4,8 @@ imports
   Why3_Set
   Why3_List
   Why3_Int
+  Why3_Bool
+  Why3_Number
 begin
 
 end

lib/isabelle/Why3_Bool.thy

+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

lib/isabelle/Why3_Map.thy

@@ -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

lib/isabelle/Why3_Number.thy

+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
+        qed
+      }
+      then show "coprime n p"
+        by (auto simp add: coprime_int)
+    qed
+  next
+    assume H: "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
+    show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
+    proof (intro strip notI)
+      fix n
+      assume H': "1 < n \<and> n < p" "n dvd p"
+      then have "1 \<le> n \<and> n < p" by simp
+      with H have "coprime n p" by simp
+      with H' show False by (simp add: coprime_int)
+    qed
+  qed
+  then show ?thesis by (simp add: prime_def)
+qed
+
+why3_vc Gauss
+proof -
+  from assms
+  have "coprime a b" "a dvd c * b" by (simp_all add: mult_commute)
+  then show ?thesis by (rule coprime_dvd_mult_int)
+qed
+
+why3_vc Euclid using assms by auto
+
+why3_vc gcd_coprime
+proof -
+  have "gcd a (b * c) = gcd (b * c) a" by (simp add: gcd_commute_int)
+  also from assms have "coprime b a" by (simp add: gcd_commute_int)
+  then have "gcd (b * c) a = gcd c a" by (simp add: gcd_mult_cancel_int)
+  finally show ?thesis by (simp add: gcd_commute_int)
+qed
+
+why3_end
+
+end