--- a/NEWS Tue Aug 29 17:41:11 2017 +0100
+++ b/NEWS Tue Aug 29 17:41:27 2017 +0100
@@ -212,6 +212,10 @@
Residues. Definition changed so that "totient 1 = 1" in agreement with
the literature. Minor INCOMPATIBILITY.
+* New styles in theory "HOL-Library.LaTeXsugar":
+ - "dummy_pats" for printing equations with "_" on the lhs;
+ - "eta_expand" for printing eta-expanded terms.
+
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Aug 29 17:41:27 2017 +0100
@@ -1386,6 +1386,22 @@
lemmas fps_numeral_simps =
fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
+lemma subdegree_div:
+ assumes "q dvd p"
+ shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p - subdegree q"
+proof (cases "p = 0")
+ case False
+ from assms have "p = p div q * q" by simp
+ also from assms False have "subdegree \<dots> = subdegree (p div q) + subdegree q"
+ by (intro subdegree_mult) (auto simp: dvd_div_eq_0_iff)
+ finally show ?thesis by simp
+qed simp_all
+
+lemma subdegree_div_unit:
+ assumes "q $ 0 \<noteq> 0"
+ shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p"
+ using assms by (subst subdegree_div) simp_all
+
subsection \<open>Formal power series form a Euclidean ring\<close>
--- a/src/HOL/Computational_Algebra/Polynomial.thy Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Tue Aug 29 17:41:27 2017 +0100
@@ -1388,6 +1388,9 @@
for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
by (auto simp: degree_mult_eq)
+lemma degree_power_eq: "p \<noteq> 0 \<Longrightarrow> degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
+ by (induction n) (simp_all add: degree_mult_eq)
+
lemma degree_mult_right_le:
fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
assumes "q \<noteq> 0"
@@ -2454,9 +2457,6 @@
qed
qed
-lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
- by (induct n arbitrary: f) auto
-
lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
unfolding pderiv_coeffs_def
proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
@@ -2539,6 +2539,10 @@
apply (simp add: algebra_simps)
done
+lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
+ by (induction p rule: pCons_induct)
+ (auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
+
lemma pderiv_prod: "pderiv (prod f (as)) = (\<Sum>a\<in>as. prod f (as - {a}) * pderiv (f a))"
proof (induct as rule: infinite_finite_induct)
case (insert a as)
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Tue Aug 29 17:41:27 2017 +0100
@@ -92,10 +92,15 @@
subsubsection \<open>\<open>link\<close>\<close>
-definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
- "link t\<^sub>1 t\<^sub>2 = (case (t\<^sub>1,t\<^sub>2) of (Node r x\<^sub>1 c\<^sub>1, Node _ x\<^sub>2 c\<^sub>2) \<Rightarrow>
- if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2)
- )"
+context
+includes pattern_aliases
+begin
+
+fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+ "link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) =
+ (if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#ts\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#ts\<^sub>2))"
+
+end
lemma invar_btree_link:
assumes "invar_btree t\<^sub>1"
@@ -103,20 +108,20 @@
assumes "rank t\<^sub>1 = rank t\<^sub>2"
shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
using assms
-by (auto simp: link_def split: tree.split)
+by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
lemma invar_link_otree:
assumes "invar_otree t\<^sub>1"
assumes "invar_otree t\<^sub>2"
shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
using assms
-by (auto simp: link_def split: tree.split)
+by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
-by (auto simp: link_def split: tree.split)
+by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
-by (auto simp: link_def split: tree.split)
+by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
subsubsection \<open>\<open>ins_tree\<close>\<close>
@@ -254,9 +259,7 @@
fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
"get_min [t] = root t"
-| "get_min (t#ts) = (let x = root t;
- y = get_min ts
- in if x \<le> y then x else y)"
+| "get_min (t#ts) = min (root t) (get_min ts)"
lemma invar_otree_root_min:
assumes "invar_otree t"
@@ -273,7 +276,7 @@
using assms
apply (induction ts arbitrary: x rule: get_min.induct)
apply (auto
- simp: invar_otree_root_min intro: order_trans;
+ simp: invar_otree_root_min min_def intro: order_trans;
meson linear order_trans invar_otree_root_min
)+
done
@@ -287,7 +290,7 @@
lemma get_min_member:
"ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
-by (induction ts rule: get_min.induct) (auto)
+by (induction ts rule: get_min.induct) (auto simp: min_def)
lemma get_min:
assumes "mset_heap ts \<noteq> {#}"
@@ -308,7 +311,7 @@
assumes "get_min_rest ts = (t',ts')"
shows "root t' = get_min ts"
using assms
-by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits)
+by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)
lemma mset_get_min_rest:
assumes "get_min_rest ts = (t',ts')"
@@ -445,7 +448,7 @@
qed
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
-lemma size_mset_heap:
+lemma size_mset_bheap:
assumes "invar_bheap ts"
shows "2^length ts \<le> size (mset_heap ts) + 1"
proof -
@@ -500,7 +503,7 @@
unfolding t_insert_def by (rule t_ins_tree_simple_bound)
also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
proof -
- from size_mset_heap[of ts] assms
+ from size_mset_bheap[of ts] assms
have "2 ^ length ts \<le> size (mset_heap ts) + 1"
unfolding invar_def by auto
hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
@@ -549,8 +552,8 @@
by (rule power_increasing) auto
also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"
by (auto simp: algebra_simps power_add power_mult)
- also note BINVARS(1)[THEN size_mset_heap]
- also note BINVARS(2)[THEN size_mset_heap]
+ also note BINVARS(1)[THEN size_mset_bheap]
+ also note BINVARS(2)[THEN size_mset_bheap]
finally have "2 ^ t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
from le_log2_of_power[OF this] have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"
@@ -593,7 +596,7 @@
have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto
also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
proof -
- from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
unfolding invar_def by auto
thus ?thesis using le_log2_of_power by blast
qed
@@ -617,7 +620,7 @@
have 1: "t_get_min_rest ts = length ts" using assms t_get_min_rest_estimate by auto
also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
proof -
- from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
by auto
thus ?thesis using le_log2_of_power by blast
qed
@@ -649,7 +652,7 @@
proof -
have "t_rev ts = length ts + 1" by (auto simp: t_rev_def)
hence "2^t_rev ts = 2*2^length ts" by auto
- also have "\<dots> \<le> 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def)
+ also have "\<dots> \<le> 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def)
finally have "2 ^ t_rev ts \<le> 2 * n + 2" .
from le_log2_of_power[OF this] have "t_rev ts \<le> log 2 (2 * (n + 1))"
by auto
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Sorting.thy Tue Aug 29 17:41:27 2017 +0100
@@ -0,0 +1,207 @@
+(* Author: Tobias Nipkow *)
+
+(* FIXME adjust List.sorted to work like below; [code] is different! *)
+
+theory Sorting
+imports
+ Complex_Main
+ "HOL-Library.Multiset"
+begin
+
+hide_const List.sorted List.insort
+
+declare Let_def [simp]
+
+fun sorted :: "'a::linorder list \<Rightarrow> bool" where
+"sorted [] = True" |
+"sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> y) & sorted xs)"
+
+lemma sorted_append:
+ "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
+by (induct xs) (auto)
+
+
+subsection "Insertion Sort"
+
+fun insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort x [] = [x]" |
+"insort x (y#ys) =
+ (if x \<le> y then x#y#ys else y#(insort x ys))"
+
+fun isort :: "'a::linorder list \<Rightarrow> 'a list" where
+"isort [] = []" |
+"isort (x#xs) = insort x (isort xs)"
+
+subsubsection "Functional Correctness"
+
+lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)"
+apply(induction xs)
+apply auto
+done
+
+lemma mset_isort: "mset (isort xs) = mset xs"
+apply(induction xs)
+apply simp
+apply (simp add: mset_insort)
+done
+
+lemma "sorted (insort a xs) = sorted xs"
+apply(induction xs)
+apply (auto)
+oops
+
+lemma set_insort: "set (insort x xs) = insert x (set xs)"
+by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
+
+lemma set_isort: "set (isort xs) = set xs"
+by (metis mset_isort set_mset_mset)
+
+lemma sorted_insort: "sorted (insort a xs) = sorted xs"
+apply(induction xs)
+apply(auto simp add: set_insort)
+done
+
+lemma "sorted (isort xs)"
+apply(induction xs)
+apply(auto simp: sorted_insort)
+done
+
+subsection "Time Complexity"
+
+text \<open>We count the number of function calls.\<close>
+
+text\<open>
+\<open>insort x [] = [x]\<close>
+\<open>insort x (y#ys) =
+ (if x \<le> y then x#y#ys else y#(insort x ys))\<close>
+\<close>
+fun t_insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_insort x [] = 1" |
+"t_insort x (y#ys) =
+ (if x \<le> y then 0 else t_insort x ys) + 1"
+
+text\<open>
+\<open>isort [] = []\<close>
+\<open>isort (x#xs) = insort x (isort xs)\<close>
+\<close>
+fun t_isort :: "'a::linorder list \<Rightarrow> nat" where
+"t_isort [] = 1" |
+"t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1"
+
+
+lemma t_insort_length: "t_insort x xs \<le> length xs + 1"
+apply(induction xs)
+apply auto
+done
+
+lemma length_insort: "length (insort x xs) = length xs + 1"
+apply(induction xs)
+apply auto
+done
+
+lemma length_isort: "length (isort xs) = length xs"
+apply(induction xs)
+apply (auto simp: length_insort)
+done
+
+lemma t_isort_length: "t_isort xs \<le> (length xs + 1) ^ 2"
+proof(induction xs)
+ case Nil show ?case by simp
+next
+ case (Cons x xs)
+ have "t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1" by simp
+ also have "\<dots> \<le> (length xs + 1) ^ 2 + t_insort x (isort xs) + 1"
+ using Cons.IH by simp
+ also have "\<dots> \<le> (length xs + 1) ^ 2 + length xs + 1 + 1"
+ using t_insort_length[of x "isort xs"] by (simp add: length_isort)
+ also have "\<dots> \<le> (length(x#xs) + 1) ^ 2"
+ by (simp add: power2_eq_square)
+ finally show ?case .
+qed
+
+
+subsection "Merge Sort"
+
+fun merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"merge [] ys = ys" |
+"merge xs [] = xs" |
+"merge (x#xs) (y#ys) = (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
+
+fun msort :: "'a::linorder list \<Rightarrow> 'a list" where
+"msort xs = (let n = length xs in
+ if n \<le> 1 then xs
+ else merge (msort (take (n div 2) xs)) (msort (drop (n div 2) xs)))"
+
+declare msort.simps [simp del]
+
+(* We count the number of comparisons between list elements only *)
+
+fun c_merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> nat" where
+"c_merge [] ys = 0" |
+"c_merge xs [] = 0" |
+"c_merge (x#xs) (y#ys) = 1 + (if x \<le> y then c_merge xs (y#ys) else c_merge (x#xs) ys)"
+
+lemma c_merge_ub: "c_merge xs ys \<le> length xs + length ys"
+by (induction xs ys rule: c_merge.induct) auto
+
+fun c_msort :: "'a::linorder list \<Rightarrow> nat" where
+"c_msort xs =
+ (let n = length xs;
+ ys = take (n div 2) xs;
+ zs = drop (n div 2) xs
+ in if n \<le> 1 then 0
+ else c_msort ys + c_msort zs + c_merge (msort ys) (msort zs))"
+
+declare c_msort.simps [simp del]
+
+lemma length_merge: "length(merge xs ys) = length xs + length ys"
+apply (induction xs ys rule: merge.induct)
+apply auto
+done
+
+lemma length_msort: "length(msort xs) = length xs"
+proof (induction xs rule: msort.induct)
+ case (1 xs)
+ thus ?case by (auto simp: msort.simps[of xs] length_merge)
+qed
+text \<open>Why structured proof?
+ To have the name "xs" to specialize msort.simps with xs
+ to ensure that msort.simps cannot be used recursively.
+Also works without this precaution, but that is just luck.\<close>
+
+lemma c_msort_le: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> k * 2^k"
+proof(induction k arbitrary: xs)
+ case 0 thus ?case by (simp add: c_msort.simps)
+next
+ case (Suc k)
+ let ?n = "length xs"
+ let ?ys = "take (?n div 2) xs"
+ let ?zs = "drop (?n div 2) xs"
+ show ?case
+ proof (cases "?n \<le> 1")
+ case True
+ thus ?thesis by(simp add: c_msort.simps)
+ next
+ case False
+ have "c_msort(xs) =
+ c_msort ?ys + c_msort ?zs + c_merge (msort ?ys) (msort ?zs)"
+ by (simp add: c_msort.simps msort.simps)
+ also have "\<dots> \<le> c_msort ?ys + c_msort ?zs + length ?ys + length ?zs"
+ using c_merge_ub[of "msort ?ys" "msort ?zs"] length_msort[of ?ys] length_msort[of ?zs]
+ by arith
+ also have "\<dots> \<le> k * 2^k + c_msort ?zs + length ?ys + length ?zs"
+ using Suc.IH[of ?ys] Suc.prems by simp
+ also have "\<dots> \<le> k * 2^k + k * 2^k + length ?ys + length ?zs"
+ using Suc.IH[of ?zs] Suc.prems by simp
+ also have "\<dots> = 2 * k * 2^k + 2 * 2 ^ k"
+ using Suc.prems by simp
+ finally show ?thesis by simp
+ qed
+qed
+
+(* Beware of conversions: *)
+lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
+using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
+by (metis (mono_tags) numeral_power_eq_real_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
+
+end
--- a/src/HOL/List.thy Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/List.thy Tue Aug 29 17:41:27 2017 +0100
@@ -3108,7 +3108,10 @@
done
lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
+ by (induct n) simp_all
+
+lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
+ by (induct n arbitrary: f) auto
lemma nth_take_lemma:
--- a/src/HOL/ROOT Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/ROOT Tue Aug 29 17:41:27 2017 +0100
@@ -203,6 +203,7 @@
"HOL-Library.Multiset"
"HOL-Number_Theory.Fib"
theories
+ Sorting
Balance
Tree_Map
AVL_Map
--- a/src/HOL/SMT.thy Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/SMT.thy Tue Aug 29 17:41:27 2017 +0100
@@ -1,12 +1,13 @@
(* Title: HOL/SMT.thy
Author: Sascha Boehme, TU Muenchen
+ Author: Jasmin Blanchette, VU Amsterdam
*)
section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
theory SMT
-imports Divides
-keywords "smt_status" :: diag
+ imports Divides
+ keywords "smt_status" :: diag
begin
subsection \<open>A skolemization tactic and proof method\<close>
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 29 17:41:27 2017 +0100
@@ -173,45 +173,43 @@
""
val missing_message_tail =
- " appears to be missing. You will need to install it if you want to invoke \
- \remote provers."
+ " appears to be missing; you will need to install it if you want to invoke \
+ \remote provers"
fun from_lemmas [] = ""
| from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
-fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable."
- | string_of_atp_failure Unprovable = "The generated problem is unprovable."
- | string_of_atp_failure GaveUp = "The prover gave up."
+fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable"
+ | string_of_atp_failure Unprovable = "The generated problem is unprovable"
+ | string_of_atp_failure GaveUp = "The prover gave up"
| string_of_atp_failure ProofMissing =
- "The prover claims the conjecture is a theorem but did not provide a proof."
+ "The prover claims the conjecture is a theorem but did not provide a proof"
| string_of_atp_failure ProofIncomplete =
- "The prover claims the conjecture is a theorem but provided an incomplete proof."
+ "The prover claims the conjecture is a theorem but provided an incomplete proof"
| string_of_atp_failure ProofUnparsable =
- "The prover claims the conjecture is a theorem but provided an unparsable proof."
+ "The prover claims the conjecture is a theorem but provided an unparsable proof"
| string_of_atp_failure (UnsoundProof (false, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
- ". Specify a sound type encoding or omit the \"type_enc\" option."
+ "; specify a sound type encoding or omit the \"type_enc\" option"
| string_of_atp_failure (UnsoundProof (true, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
- ", which could be due to inconsistent axioms (including \"sorry\"s) or to \
- \a bug in Sledgehammer."
- | string_of_atp_failure CantConnect = "Cannot connect to server."
- | string_of_atp_failure TimedOut = "Timed out."
+ ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
+ | string_of_atp_failure CantConnect = "Cannot connect to server"
+ | string_of_atp_failure TimedOut = "Timed out"
| string_of_atp_failure Inappropriate =
- "The generated problem lies outside the prover's scope."
- | string_of_atp_failure OutOfResources = "The prover ran out of resources."
+ "The generated problem lies outside the prover's scope"
+ | string_of_atp_failure OutOfResources = "The prover ran out of resources"
| string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail
| string_of_atp_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
- | string_of_atp_failure MalformedInput = "The generated problem is malformed."
- | string_of_atp_failure MalformedOutput = "The prover output is malformed."
- | string_of_atp_failure Interrupted = "The prover was interrupted."
- | string_of_atp_failure Crashed = "The prover crashed."
- | string_of_atp_failure InternalError = "An internal prover error occurred."
+ | string_of_atp_failure MalformedInput = "The generated problem is malformed"
+ | string_of_atp_failure MalformedOutput = "The prover output is malformed"
+ | string_of_atp_failure Interrupted = "The prover was interrupted"
+ | string_of_atp_failure Crashed = "The prover crashed"
+ | string_of_atp_failure InternalError = "An internal prover error occurred"
| string_of_atp_failure (UnknownError s) =
"A prover error occurred" ^
- (if s = "" then ". (Pass the \"verbose\" option for details.)"
- else ":\n" ^ s)
+ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s)
fun extract_delimited (begin_delim, end_delim) output =
(case first_field begin_delim output of
@@ -347,10 +345,13 @@
|| (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [])
-- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
>> AType)
- -- Scan.option ($$ tptp_fun_type |-- parse_type)
+ -- Scan.option (($$ tptp_fun_type || $$ tptp_product_type) -- parse_type)
>> (fn (a, NONE) => a
- | (a, SOME b) => AFun (a, b))) x
-and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
+ | (a, SOME (fun_or_product, b)) =>
+ if fun_or_product = tptp_fun_type then AFun (a, b)
+ else AType ((tptp_product_type, []), [a, b]))) x
+and parse_types x =
+ (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
(* We currently half ignore types. *)
fun parse_optional_type_signature x =
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 29 17:41:27 2017 +0100
@@ -717,7 +717,7 @@
remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
(K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["4.2", "4.0"]
+ remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
(K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
--- a/src/HOL/Tools/SMT/cvc4_interface.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML Tue Aug 29 17:41:27 2017 +0100
@@ -7,24 +7,30 @@
signature CVC4_INTERFACE =
sig
val smtlib_cvc4C: SMT_Util.class
+ val hosmtlib_cvc4C: SMT_Util.class
end;
structure CVC4_Interface: CVC4_INTERFACE =
struct
-val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
+val cvc4C = ["cvc4"]
+val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
+val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
(* interface *)
local
- fun translate_config ctxt =
- {logic = K "(set-logic ALL_SUPPORTED)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
- serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+ fun translate_config order ctxt =
+ {order = order,
+ logic = K "(set-logic ALL_SUPPORTED)\n",
+ fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+ serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
in
-val _ =
- Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
+val _ = Theory.setup (Context.theory_map
+ (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
+ SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
end
--- a/src/HOL/Tools/SMT/smt_builtin.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Aug 29 17:41:27 2017 +0100
@@ -11,11 +11,11 @@
(*built-in types*)
val add_builtin_typ: SMT_Util.class ->
- typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+ typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
Context.generic
val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
Context.generic
- val dest_builtin_typ: Proof.context -> typ -> string option
+ val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
val is_builtin_typ_ext: Proof.context -> typ -> bool
(*built-in numbers*)
@@ -93,7 +93,8 @@
structure Builtins = Generic_Data
(
type T =
- (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+ (Proof.context -> typ -> bool,
+ (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
(term list bfun, bfunr option bfun) btab
val empty = ([], Symtab.empty)
val extend = I
--- a/src/HOL/Tools/SMT/smt_config.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Aug 29 17:41:27 2017 +0100
@@ -32,6 +32,7 @@
val statistics: bool Config.T
val monomorph_limit: int Config.T
val monomorph_instances: int Config.T
+ val higher_order: bool Config.T
val nat_as_int: bool Config.T
val infer_triggers: bool Config.T
val debug_files: string Config.T
@@ -180,6 +181,7 @@
val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
--- a/src/HOL/Tools/SMT/smt_real.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Tue Aug 29 17:41:27 2017 +0100
@@ -32,7 +32,7 @@
val setup_builtins =
SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
- (@{typ real}, K (SOME "Real"), real_num) #>
+ (@{typ real}, K (SOME ("Real", [])), real_num) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
(@{const less (real)}, "<"),
(@{const less_eq (real)}, "<="),
--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Aug 29 17:41:27 2017 +0100
@@ -62,6 +62,7 @@
end
+
(* CVC4 *)
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
@@ -75,8 +76,16 @@
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
fun select_class ctxt =
- if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
- else SMTLIB_Interface.smtlibC
+ if Config.get ctxt cvc4_extensions then
+ if Config.get ctxt SMT_Config.higher_order then
+ CVC4_Interface.hosmtlib_cvc4C
+ else
+ CVC4_Interface.smtlib_cvc4C
+ else
+ if Config.get ctxt SMT_Config.higher_order then
+ SMTLIB_Interface.hosmtlibC
+ else
+ SMTLIB_Interface.smtlibC
in
val cvc4: SMT_Solver.solver_config = {
@@ -93,11 +102,20 @@
end
+
(* veriT *)
+local
+ fun select_class ctxt =
+ if Config.get ctxt SMT_Config.higher_order then
+ SMTLIB_Interface.hosmtlibC
+ else
+ SMTLIB_Interface.smtlibC
+in
+
val veriT: SMT_Solver.solver_config = {
name = "verit",
- class = K SMTLIB_Interface.smtlibC,
+ class = select_class,
avail = make_avail "VERIT",
command = make_command "VERIT",
options = (fn ctxt => [
@@ -113,6 +131,9 @@
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = NONE }
+end
+
+
(* Z3 *)
val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Aug 29 17:41:27 2017 +0100
@@ -10,8 +10,8 @@
datatype squant = SForall | SExists
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
datatype sterm =
- SVar of int |
- SApp of string * sterm list |
+ SVar of int * sterm list |
+ SConst of string * sterm list |
SQua of squant * string list * sterm spattern list * sterm
(*translation configuration*)
@@ -21,6 +21,7 @@
dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
funcs: (string * (string list * string)) list }
type config = {
+ order: SMT_Util.order,
logic: term list -> string,
fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -50,8 +51,8 @@
SPat of 'a list | SNoPat of 'a list
datatype sterm =
- SVar of int |
- SApp of string * sterm list |
+ SVar of int * sterm list |
+ SConst of string * sterm list |
SQua of squant * string list * sterm spattern list * sterm
@@ -64,6 +65,7 @@
funcs: (string * (string list * string)) list }
type config = {
+ order: SMT_Util.order,
logic: term list -> string,
fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -147,7 +149,7 @@
fun add_typ' T proper =
(case SMT_Builtin.dest_builtin_typ ctxt' T of
- SOME n => pair n
+ SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
| NONE => add_typ T proper)
fun tr_select sel =
@@ -425,11 +427,12 @@
| transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
| transT (T as Type _) =
(case SMT_Builtin.dest_builtin_typ ctxt T of
- SOME n => pair n
+ SOME (n, []) => pair n
+ | SOME (n, Ts) =>
+ fold_map transT Ts
+ #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
| NONE => add_typ T true)
- fun app n ts = SApp (n, ts)
-
fun trans t =
(case Term.strip_comb t of
(Const (qn, _), [Abs (_, T, t1)]) =>
@@ -440,17 +443,17 @@
| NONE => raise TERM ("unsupported quantifier", [t]))
| (u as Const (c as (_, T)), ts) =>
(case builtin ctxt c ts of
- SOME (n, _, us, _) => fold_map trans us #>> app n
- | NONE => transs u T ts)
- | (u as Free (_, T), ts) => transs u T ts
- | (Bound i, []) => pair (SVar i)
+ SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
+ | NONE => trans_applied_fun u T ts)
+ | (u as Free (_, T), ts) => trans_applied_fun u T ts
+ | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
| _ => raise TERM ("bad SMT term", [t]))
- and transs t T ts =
+ and trans_applied_fun t T ts =
let val (Us, U) = SMT_Util.dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
- add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
+ add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
end
val (us, trx') = fold_map trans ts trx
@@ -480,7 +483,7 @@
fun translate ctxt smt_options comments ithms =
let
- val {logic, fp_kinds, serialize} = get_config ctxt
+ val {order, logic, fp_kinds, serialize} = get_config ctxt
fun no_dtyps (tr_context, ctxt) ts =
((Termtab.empty, [], tr_context, ctxt), ts)
@@ -510,10 +513,14 @@
|> rpair ctxt1
|-> Lambda_Lifting.lift_lambdas NONE is_binder
|-> (fn (ts', ll_defs) => fn ctxt' =>
- (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
-
+ let
+ val ts'' = map mk_trigger ll_defs @ ts'
+ |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
+ in
+ (ctxt', (ts'', ll_defs))
+ end)
val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
- |>> apfst (cons fun_app_eq)
+ |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
in
(ts4, tr_context)
|-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
--- a/src/HOL/Tools/SMT/smt_util.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Tue Aug 29 17:41:27 2017 +0100
@@ -10,6 +10,8 @@
val repeat: ('a -> 'a option) -> 'a -> 'a
val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
+ datatype order = First_Order | Higher_Order
+
(*class dictionaries*)
type class = string list
val basicC: class
@@ -79,6 +81,11 @@
in rep end
+(* order *)
+
+datatype order = First_Order | Higher_Order
+
+
(* class dictionaries *)
type class = string list
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Aug 29 17:41:27 2017 +0100
@@ -8,8 +8,9 @@
signature SMTLIB_INTERFACE =
sig
val smtlibC: SMT_Util.class
+ val hosmtlibC: SMT_Util.class
val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
- val translate_config: Proof.context -> SMT_Translate.config
+ val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
val assert_name_of_index: int -> string
val assert_index_of_name: string -> int
val assert_prefix : string
@@ -18,7 +19,10 @@
structure SMTLIB_Interface: SMTLIB_INTERFACE =
struct
-val smtlibC = ["smtlib"]
+val hoC = ["ho"]
+
+val smtlibC = ["smtlib"] (* SMT-LIB 2 *)
+val hosmtlibC = smtlibC @ hoC (* possibly SMT-LIB 3 *)
(* builtins *)
@@ -36,9 +40,11 @@
in
val setup_builtins =
+ SMT_Builtin.add_builtin_typ hosmtlibC
+ (@{typ "'a => 'b"}, fn Type (@{type_name fun}, Ts) => SOME ("->", Ts), K (K NONE)) #>
fold (SMT_Builtin.add_builtin_typ smtlibC) [
- (@{typ bool}, K (SOME "Bool"), K (K NONE)),
- (@{typ int}, K (SOME "Int"), int_num)] #>
+ (@{typ bool}, K (SOME ("Bool", [])), K (K NONE)),
+ (@{typ int}, K (SOME ("Int", [])), int_num)] #>
fold (SMT_Builtin.add_builtin_fun' smtlibC) [
(@{const True}, "true"),
(@{const False}, "false"),
@@ -90,9 +96,11 @@
fun var i = "?v" ^ string_of_int i
-fun tree_of_sterm l (SMT_Translate.SVar i) = SMTLIB.Sym (var (l - i - 1))
- | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
- | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
+fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
+ | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
+ SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
+ | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
+ | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
| tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
let
@@ -157,13 +165,15 @@
(* interface *)
-fun translate_config ctxt = {
+fun translate_config order ctxt = {
+ order = order,
logic = choose_logic ctxt,
fp_kinds = [],
serialize = serialize}
val _ = Theory.setup (Context.theory_map
(setup_builtins #>
- SMT_Translate.add_config (smtlibC, translate_config)))
+ SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
+ SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
end;
--- a/src/HOL/Tools/SMT/z3_interface.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Aug 29 17:41:27 2017 +0100
@@ -24,15 +24,19 @@
structure Z3_Interface: Z3_INTERFACE =
struct
-val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
+val z3C = ["z3"]
+
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
(* interface *)
local
fun translate_config ctxt =
- {logic = K "", fp_kinds = [BNF_Util.Least_FP],
- serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+ {order = SMT_Util.First_Order,
+ logic = K "",
+ fp_kinds = [BNF_Util.Least_FP],
+ serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
fun is_div_mod @{const divide (int)} = true
| is_div_mod @{const modulo (int)} = true
--- a/src/HOL/Word/Tools/smt_word.ML Tue Aug 29 17:41:11 2017 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML Tue Aug 29 17:41:27 2017 +0100
@@ -28,7 +28,8 @@
fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
- fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T)
+ fun word_typ (Type (@{type_name word}, [T])) =
+ Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
| word_typ _ = NONE
fun word_num (Type (@{type_name word}, [T])) k =