# HG changeset patch # User huffman # Date 1333094103 -7200 # Node ID c610b61c74a3dd75bc17bff23d7dbd5cd3c9197c # Parent e1b0c8236ae42b5ace8e3f6eb6443bcf11a50cbf# Parent d3168cf76258551e926464c3363e74b486c06363 merged diff -r e1b0c8236ae4 -r c610b61c74a3 NEWS --- a/NEWS Fri Mar 30 08:15:29 2012 +0200 +++ b/NEWS Fri Mar 30 09:55:03 2012 +0200 @@ -163,7 +163,8 @@ mod_mult_distrib2 ~> mult_mod_right * More default pred/set conversions on a couple of relation operations -and predicates. Consolidation of some relation theorems: +and predicates. Added powers of predicate relations. +Consolidation of some relation theorems: converse_def ~> converse_unfold rel_comp_def ~> rel_comp_unfold @@ -425,6 +426,9 @@ - Added possibility to specify lambda translations scheme as a parenthesized argument (e.g., "by (metis (lifting) ...)"). +* SMT: + - renamed "smt_fixed" option to "smt_read_only_certificates". + * Command 'try0': - Renamed from 'try_methods'. INCOMPATIBILITY. diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/IsaMakefile Fri Mar 30 09:55:03 2012 +0200 @@ -1605,6 +1605,7 @@ HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz $(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \ + Quickcheck_Examples/Completeness.thy \ Quickcheck_Examples/Find_Unused_Assms_Examples.thy \ Quickcheck_Examples/Quickcheck_Examples.thy \ Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Mar 30 09:55:03 2012 +0200 @@ -1186,7 +1186,7 @@ lemma single_Bag [code]: "{#x#} = Bag (DAList.update x 1 DAList.empty)" - by (simp add: multiset_eq_iff alist.Alist_inverse update_code_eqn empty_code_eqn) + by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq) lemma union_Bag [code]: "Bag xs + Bag ys = Bag (join (\x (n1, n2). n1 + n2) xs ys)" @@ -1199,7 +1199,7 @@ lemma filter_Bag [code]: "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \ fst) xs)" -by (rule multiset_eqI) (simp add: count_of_filter filter_code_eqn) +by (rule multiset_eqI) (simp add: count_of_filter filter.rep_eq) lemma mset_less_eq_Bag [code]: "Bag xs \ A \ (\(x, n) \ set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \ count A x)" diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 30 09:55:03 2012 +0200 @@ -26,6 +26,7 @@ val sh_minimizeK = "sh_minimize" (*refers to minimizer run within Sledgehammer*) val max_new_mono_instancesK = "max_new_mono_instances" val max_mono_itersK = "max_mono_iters" +val check_trivialK = "check_trivial" (*false by default*) fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " @@ -701,8 +702,11 @@ val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK val trivial = - Try0.try0 (SOME try_timeout) ([], [], [], []) pre - handle TimeLimit.TimeOut => false + if AList.lookup (op =) args check_trivialK |> the_default "false" + |> Bool.fromString |> the then + Try0.try0 (SOME try_timeout) ([], [], [], []) pre + handle TimeLimit.TimeOut => false + else false fun apply_reconstructor m1 m2 = if metis_ft then diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Quickcheck_Examples/Completeness.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy Fri Mar 30 09:55:03 2012 +0200 @@ -0,0 +1,218 @@ +(* Title: HOL/Quickcheck_Examples/Completeness.thy + Author: Lukas Bulwahn + Copyright 2012 TU Muenchen +*) + +header {* Proving completeness of exhaustive generators *} + +theory Completeness +imports Main +begin + +subsection {* Preliminaries *} + +primrec is_some +where + "is_some (Some t) = True" +| "is_some None = False" + +setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} + +subsection {* Defining the size of values *} + +hide_const size + +class size = + fixes size :: "'a => nat" + +instantiation int :: size +begin + +definition size_int :: "int => nat" +where + "size_int n = nat (abs n)" + +instance .. + +end + +instantiation code_numeral :: size +begin + +definition size_code_numeral :: "code_numeral => nat" +where + "size_code_numeral = Code_Numeral.nat_of" + +instance .. + +end + +instantiation nat :: size +begin + +definition size_nat :: "nat => nat" +where + "size_nat n = n" + +instance .. + +end + +instantiation list :: (size) size +begin + +primrec size_list :: "'a list => nat" +where + "size [] = 1" +| "size (x # xs) = max (size x) (size xs) + 1" + +instance .. + +end + +subsection {* Completeness *} + +class complete = exhaustive + size + +assumes + complete: "(\ v. size v \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + +lemma complete_imp1: + "size (v :: 'a :: complete) \ n \ is_some (f v) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" +by (metis complete) + +lemma complete_imp2: + assumes "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + obtains v where "size (v :: 'a :: complete) \ n" "is_some (f v)" +using assms by (metis complete) + +subsubsection {* Instance Proofs *} + +declare exhaustive'.simps [simp del] + +lemma complete_exhaustive': + "(\ i. j <= i & i <= k & is_some (f i)) \ is_some (Quickcheck_Exhaustive.exhaustive' f k j)" +proof (induct rule: Quickcheck_Exhaustive.exhaustive'.induct[of _ f k j]) + case (1 f d i) + show ?case + proof (cases "f i") + case None + from this 1 show ?thesis + unfolding exhaustive'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def + apply auto + apply (metis is_some.simps(2) order_le_neq_trans zless_imp_add1_zle) + apply (metis add1_zle_eq less_int_def) + done + next + case Some + from this show ?thesis + unfolding exhaustive'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def by auto + qed +qed + +lemma int_of_nat: + "Code_Numeral.int_of (Code_Numeral.of_nat n) = int n" +unfolding int_of_def by simp + +instance int :: complete +proof + fix n f + show "(\v. size (v :: int) \ n \ is_some (f v)) = is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + unfolding exhaustive_int_def complete_exhaustive'[symmetric] + apply auto apply (rule_tac x="v" in exI) + unfolding size_int_def by (metis int_of_nat abs_le_iff minus_le_iff nat_le_iff)+ +qed + +declare exhaustive_code_numeral'.simps[simp del] + +lemma complete_code_numeral': + "(\n. j \ n \ n \ k \ is_some (f n)) = + is_some (Quickcheck_Exhaustive.exhaustive_code_numeral' f k j)" +proof (induct rule: exhaustive_code_numeral'.induct[of _ f k j]) + case (1 f k j) + show "(\n\j. n \ k \ is_some (f n)) = is_some (Quickcheck_Exhaustive.exhaustive_code_numeral' f k j)" + unfolding exhaustive_code_numeral'.simps[of f k j] Quickcheck_Exhaustive.orelse_def + apply auto + apply (auto split: option.split) + apply (insert 1[symmetric]) + apply simp + apply (metis is_some.simps(2) less_eq_code_numeral_def not_less_eq_eq order_antisym) + apply simp + apply (split option.split_asm) + defer apply fastforce + apply simp by (metis Suc_leD) +qed + +instance code_numeral :: complete +proof + fix n f + show "(\v. size (v :: code_numeral) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + unfolding exhaustive_code_numeral_def complete_code_numeral'[symmetric] + by (auto simp add: size_code_numeral_def) +qed + +instance nat :: complete +proof + fix n f + show "(\v. size (v :: nat) \ n \ is_some (f v)) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + unfolding exhaustive_nat_def complete[of n "%x. f (Code_Numeral.nat_of x)", symmetric] + apply auto + apply (rule_tac x="Code_Numeral.of_nat v" in exI) + apply (auto simp add: size_code_numeral_def size_nat_def) done +qed + +instance list :: (complete) complete +proof + fix n f + show "(\ v. size (v :: 'a list) \ n \ is_some (f (v :: 'a list))) \ is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))" + proof (induct n arbitrary: f) + case 0 + { fix v have "size (v :: 'a list) > 0" by (induct v) auto } + from this show ?case by (simp add: list.exhaustive_list.simps) + next + case (Suc n) + show ?case + proof + assume "\v. Completeness.size_class.size v \ Suc n \ is_some (f v)" + from this guess v .. note v = this + show "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))" + proof (cases "v") + case Nil + from this v show ?thesis + unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def + by (auto split: option.split) + next + case (Cons v' vs') + from Cons v have size_v': "Completeness.size_class.size v' \ n" + and "Completeness.size_class.size vs' \ n" by auto + from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\xs. f (v' # xs)) (Code_Numeral.of_nat n))" + by metis + from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\xs. f (x # xs)) (Code_Numeral.of_nat n))", OF this] + show ?thesis + unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def + by (auto split: option.split) + qed + next + assume is_some: "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))" + show "\v. size v \ Suc n \ is_some (f v)" + proof (cases "f []") + case Some + from this show ?thesis + by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1)) + next + case None + from this is_some have + "is_some (exhaustive_class.exhaustive (\x. exhaustive_class.exhaustive (\xs. f (x # xs)) (Code_Numeral.of_nat n)) (Code_Numeral.of_nat n))" + unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def + by simp + from complete_imp2[OF this] guess v' . note v = this + from Suc[of "%xs. f (v' # xs)"] this(2) obtain vs' where "size vs' \ n" "is_some (f (v' # vs'))" + by metis + note vs' = this + from this v have "size (v' # vs') \ Suc n" by auto + from this vs' v show ?thesis by metis + qed + qed + qed +qed + +end diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Quickcheck_Examples/ROOT.ML --- a/src/HOL/Quickcheck_Examples/ROOT.ML Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Fri Mar 30 09:55:03 2012 +0200 @@ -1,7 +1,8 @@ use_thys [ "Find_Unused_Assms_Examples", "Quickcheck_Examples", - "Quickcheck_Lattice_Examples" + "Quickcheck_Lattice_Examples", + "Completeness" ]; if getenv "ISABELLE_GHC" = "" then () diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Mar 30 09:55:03 2012 +0200 @@ -587,7 +587,7 @@ use "Tools/Quickcheck/abstract_generators.ML" -hide_fact orelse_def +hide_fact (open) orelse_def no_notation orelse (infixr "orelse" 55) hide_fact diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Fri Mar 30 09:55:03 2012 +0200 @@ -1103,7 +1103,7 @@ then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b by auto have f: "card_list (removeAll a l) = m" using e d by (simp) - have g: "removeAll a l \ removeAll a r" using remove_fset_rsp b by simp + have g: "removeAll a l \ removeAll a r" using remove_fset.rsp b by simp have "(removeAll a l) \2 (removeAll a r)" by (rule Suc.hyps[OF f g]) then have h: "(a # removeAll a l) \2 (a # removeAll a r)" by (rule list_eq2.intros(5)) have i: "l \2 (a # removeAll a l)" diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Mar 30 09:55:03 2012 +0200 @@ -419,10 +419,9 @@ (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t in fold (fn (name, eq) => Local_Theory.note - ((Binding.conceal - (Binding.qualify true prfx - (Binding.qualify true name (Binding.name "simps"))), - Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd) + ((Binding.qualify true prfx + (Binding.qualify true name (Binding.name "simps")), + [Code.add_default_eqn_attrib]), [eq]) #> snd) (names ~~ eqs) lthy end) diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 30 09:55:03 2012 +0200 @@ -189,9 +189,13 @@ (* data storage *) val qconst_data = {qconst = trm, rconst = rhs, def = def_thm} - val lhs_name = #1 var - val rsp_thm_name = Binding.suffix_name "_rsp" lhs_name - val code_eqn_thm_name = Binding.suffix_name "_code_eqn" lhs_name + + fun qualify defname suffix = Binding.name suffix + |> Binding.qualify true defname + + val lhs_name = Binding.name_of (#1 var) + val rsp_thm_name = qualify lhs_name "rsp" + val code_eqn_thm_name = qualify lhs_name "rep_eq" val lthy'' = lthy' |> Local_Theory.declaration {syntax = false, pervasive = true} diff -r e1b0c8236ae4 -r c610b61c74a3 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Mar 30 08:15:29 2012 +0200 +++ b/src/HOL/Transitive_Closure.thy Fri Mar 30 09:55:03 2012 +0200 @@ -710,14 +710,24 @@ overloading relpow == "compow :: nat \ ('a \ 'a) set \ ('a \ 'a) set" + relpowp == "compow :: nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" begin primrec relpow :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where "relpow 0 R = Id" | "relpow (Suc n) R = (R ^^ n) O R" +primrec relpowp :: "nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" where + "relpowp 0 R = HOL.eq" + | "relpowp (Suc n) R = (R ^^ n) OO R" + end +lemma relpowp_relpow_eq [pred_set_conv]: + fixes R :: "'a rel" + shows "(\x y. (x, y) \ R) ^^ n = (\x y. (x, y) \ R ^^ n)" + by (induct n) (simp_all add: rel_compp_rel_comp_eq) + text {* for code generation *} definition relpow :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where diff -r e1b0c8236ae4 -r c610b61c74a3 src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML Fri Mar 30 08:15:29 2012 +0200 +++ b/src/Pure/PIDE/xml.ML Fri Mar 30 09:55:03 2012 +0200 @@ -327,7 +327,8 @@ fun option _ NONE = [] | option f (SOME x) = [node (f x)]; -fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))]; +fun variant fs x = + [tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))]; end;