--- 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.
--- 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 \
--- 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 (\<lambda>x (n1, n2). n1 + n2) xs ys)"
@@ -1199,7 +1199,7 @@
lemma filter_Bag [code]:
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> 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 \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
--- 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
--- /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: "(\<exists> v. size v \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat n))"
+
+lemma complete_imp1:
+ "size (v :: 'a :: complete) \<le> n \<Longrightarrow> is_some (f v) \<Longrightarrow> 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) \<le> n" "is_some (f v)"
+using assms by (metis complete)
+
+subsubsection {* Instance Proofs *}
+
+declare exhaustive'.simps [simp del]
+
+lemma complete_exhaustive':
+ "(\<exists> i. j <= i & i <= k & is_some (f i)) \<longleftrightarrow> 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 "(\<exists>v. size (v :: int) \<le> n \<and> 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':
+ "(\<exists>n. j \<le> n \<and> n \<le> k \<and> 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 "(\<exists>n\<ge>j. n \<le> k \<and> 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 "(\<exists>v. size (v :: code_numeral) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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 "(\<exists>v. size (v :: nat) \<le> n \<and> is_some (f v)) \<longleftrightarrow> 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 "(\<exists> v. size (v :: 'a list) \<le> n \<and> is_some (f (v :: 'a list))) \<longleftrightarrow> 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 "\<exists>v. Completeness.size_class.size v \<le> Suc n \<and> 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' \<le> n"
+ and "Completeness.size_class.size vs' \<le> n" by auto
+ from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (Code_Numeral.of_nat n))"
+ by metis
+ from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\<lambda>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 "\<exists>v. size v \<le> Suc n \<and> 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 (\<lambda>x. exhaustive_class.exhaustive (\<lambda>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' \<le> n" "is_some (f (v' # vs'))"
+ by metis
+ note vs' = this
+ from this v have "size (v' # vs') \<le> Suc n" by auto
+ from this vs' v show ?thesis by metis
+ qed
+ qed
+ qed
+qed
+
+end
--- 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 ()
--- 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
--- 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 \<approx> removeAll a r" using remove_fset_rsp b by simp
+ have g: "removeAll a l \<approx> removeAll a r" using remove_fset.rsp b by simp
have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
have i: "l \<approx>2 (a # removeAll a l)"
--- 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)
--- 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}
--- 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 \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
+ relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
begin
primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
"relpow 0 R = Id"
| "relpow (Suc n) R = (R ^^ n) O R"
+primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 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 "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
+ by (induct n) (simp_all add: rel_compp_rel_comp_eq)
+
text {* for code generation *}
definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
--- 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;