# HG changeset patch # User paulson # Date 1504024887 -3600 # Node ID 6ab32ffb2bddb385c02c53765e18f239b2236ac1 # Parent 4df6b0ae900dd8877008dbe21ff0968377cab983# Parent 507a42c0a0ffc599c9d35ec0e372af13e324bbac merged diff -r 507a42c0a0ff -r 6ab32ffb2bdd NEWS --- 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. diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Computational_Algebra/Formal_Power_Series.thy --- 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 \ = 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 \ 0" + shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p" + using assms by (subst subdegree_div) simp_all + subsection \Formal power series form a Euclidean ring\ diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Computational_Algebra/Polynomial.thy --- 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 \ 0 \ 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 \ 0" @@ -2454,9 +2457,6 @@ qed qed -lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\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)) = (\a\as. prod f (as - {a}) * pderiv (f a))" proof (induct as rule: infinite_finite_induct) case (insert a as) diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Data_Structures/Binomial_Heap.thy --- 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 \\link\\ -definition link :: "'a::linorder tree \ 'a tree \ '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) \ - if x\<^sub>1\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 \ 'a tree \ '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\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 \\ins_tree\\ @@ -254,9 +259,7 @@ fun get_min :: "'a::linorder heap \ 'a" where "get_min [t] = root t" -| "get_min (t#ts) = (let x = root t; - y = get_min ts - in if x \ 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\[] \ get_min ts \# 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 \ {#}" @@ -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 \The length of a binomial heap is bounded by the number of its elements\ -lemma size_mset_heap: +lemma size_mset_bheap: assumes "invar_bheap ts" shows "2^length ts \ size (mset_heap ts) + 1" proof - @@ -500,7 +503,7 @@ unfolding t_insert_def by (rule t_ins_tree_simple_bound) also have "\ \ 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 \ size (mset_heap ts) + 1" unfolding invar_def by auto hence "2 ^ (length ts + 1) \ 2 * (size (mset_heap ts) + 1)" by auto @@ -549,8 +552,8 @@ by (rule power_increasing) auto also have "\ = 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 \ 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 \ log 2 \" @@ -593,7 +596,7 @@ have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto also have "\ \ log 2 (size (mset_heap ts) + 1)" proof - - from size_mset_heap[of ts] assms have "2 ^ length ts \ size (mset_heap ts) + 1" + from size_mset_bheap[of ts] assms have "2 ^ length ts \ 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 "\ \ log 2 (size (mset_heap ts) + 1)" proof - - from size_mset_heap[of ts] assms have "2 ^ length ts \ size (mset_heap ts) + 1" + from size_mset_bheap[of ts] assms have "2 ^ length ts \ 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 "\ \ 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def) + also have "\ \ 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def) finally have "2 ^ t_rev ts \ 2 * n + 2" . from le_log2_of_power[OF this] have "t_rev ts \ log 2 (2 * (n + 1))" by auto diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Data_Structures/Sorting.thy --- /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 \ bool" where +"sorted [] = True" | +"sorted (x # xs) = ((\y\set xs. x \ y) & sorted xs)" + +lemma sorted_append: + "sorted (xs@ys) = (sorted xs & sorted ys & (\x \ set xs. \y \ set ys. x\y))" +by (induct xs) (auto) + + +subsection "Insertion Sort" + +fun insort :: "'a::linorder \ 'a list \ 'a list" where +"insort x [] = [x]" | +"insort x (y#ys) = + (if x \ y then x#y#ys else y#(insort x ys))" + +fun isort :: "'a::linorder list \ '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 \We count the number of function calls.\ + +text\ +\insort x [] = [x]\ +\insort x (y#ys) = + (if x \ y then x#y#ys else y#(insort x ys))\ +\ +fun t_insort :: "'a::linorder \ 'a list \ nat" where +"t_insort x [] = 1" | +"t_insort x (y#ys) = + (if x \ y then 0 else t_insort x ys) + 1" + +text\ +\isort [] = []\ +\isort (x#xs) = insort x (isort xs)\ +\ +fun t_isort :: "'a::linorder list \ 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 \ 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 \ (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 "\ \ (length xs + 1) ^ 2 + t_insort x (isort xs) + 1" + using Cons.IH by simp + also have "\ \ (length xs + 1) ^ 2 + length xs + 1 + 1" + using t_insort_length[of x "isort xs"] by (simp add: length_isort) + also have "\ \ (length(x#xs) + 1) ^ 2" + by (simp add: power2_eq_square) + finally show ?case . +qed + + +subsection "Merge Sort" + +fun merge :: "'a::linorder list \ 'a list \ 'a list" where +"merge [] ys = ys" | +"merge xs [] = xs" | +"merge (x#xs) (y#ys) = (if x \ y then x # merge xs (y#ys) else y # merge (x#xs) ys)" + +fun msort :: "'a::linorder list \ 'a list" where +"msort xs = (let n = length xs in + if n \ 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 \ 'a list \ nat" where +"c_merge [] ys = 0" | +"c_merge xs [] = 0" | +"c_merge (x#xs) (y#ys) = 1 + (if x \ y then c_merge xs (y#ys) else c_merge (x#xs) ys)" + +lemma c_merge_ub: "c_merge xs ys \ length xs + length ys" +by (induction xs ys rule: c_merge.induct) auto + +fun c_msort :: "'a::linorder list \ nat" where +"c_msort xs = + (let n = length xs; + ys = take (n div 2) xs; + zs = drop (n div 2) xs + in if n \ 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 \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.\ + +lemma c_msort_le: "length xs = 2^k \ c_msort xs \ 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 \ 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 "\ \ 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 "\ \ k * 2^k + c_msort ?zs + length ?ys + length ?zs" + using Suc.IH[of ?ys] Suc.prems by simp + also have "\ \ k * 2^k + k * 2^k + length ?ys + length ?zs" + using Suc.IH[of ?zs] Suc.prems by simp + also have "\ = 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 \ c_msort xs \ 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/List.thy --- 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 (\n. n - Suc 0) [Suc m..i. f (Suc i)) [0 ..< n]" + by (induct n arbitrary: f) auto lemma nth_take_lemma: diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/ROOT --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/SMT.thy --- 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 \Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\ theory SMT -imports Divides -keywords "smt_status" :: diag + imports Divides + keywords "smt_status" :: diag begin subsection \A skolemization tactic and proof method\ diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/ATP/atp_proof.ML --- 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 = diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/ATP/atp_systems.ML --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/cvc4_interface.ML --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smt_builtin.ML --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smt_config.ML --- 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 "") diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smt_real.ML --- 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)}, "<="), diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smt_systems.ML --- 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) diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smt_translate.ML --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smt_util.ML --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/smtlib_interface.ML --- 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; diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Tools/SMT/z3_interface.ML --- 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 diff -r 507a42c0a0ff -r 6ab32ffb2bdd src/HOL/Word/Tools/smt_word.ML --- 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 =