--- a/src/HOL/Main.thy Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Main.thy Wed Mar 12 12:18:41 2014 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Predicate_Compile Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
begin
text {*
--- a/src/HOL/Probability/Measurable.thy Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy Wed Mar 12 12:18:41 2014 +0100
@@ -263,10 +263,9 @@
subsection {* Measurability for (co)inductive predicates *}
lemma measurable_lfp:
- assumes "P = lfp F"
assumes "Order_Continuity.continuous F"
assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
- shows "pred M P"
+ shows "pred M (lfp F)"
proof -
{ fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
by (induct i) (auto intro!: *) }
@@ -274,16 +273,15 @@
by measurable
also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
by (auto simp add: bot_fun_def)
- also have "\<dots> = P"
- unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
+ also have "\<dots> = lfp F"
+ by (rule continuous_lfp[symmetric]) fact
finally show ?thesis .
qed
lemma measurable_gfp:
- assumes "P = gfp F"
assumes "Order_Continuity.down_continuous F"
assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
- shows "pred M P"
+ shows "pred M (gfp F)"
proof -
{ fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
by (induct i) (auto intro!: *) }
@@ -291,8 +289,8 @@
by measurable
also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
by (auto simp add: top_fun_def)
- also have "\<dots> = P"
- unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
+ also have "\<dots> = gfp F"
+ by (rule down_continuous_gfp[symmetric]) fact
finally show ?thesis .
qed
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Wed Mar 12 12:18:41 2014 +0100
@@ -3,7 +3,7 @@
header {* Counterexample generator performing narrowing-based testing *}
theory Quickcheck_Narrowing
-imports Quickcheck_Exhaustive
+imports Quickcheck_Random
keywords "find_unused_assms" :: diag
begin
--- a/src/HOL/Record.thy Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Record.thy Wed Mar 12 12:18:41 2014 +0100
@@ -9,7 +9,7 @@
header {* Extensible records with structural subtyping *}
theory Record
-imports Quickcheck_Narrowing
+imports Quickcheck_Exhaustive
keywords "record" :: thy_decl
begin
--- a/src/HOL/SMT.thy Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/SMT.thy Wed Mar 12 12:18:41 2014 +0100
@@ -425,7 +425,6 @@
by auto
-
hide_type (open) pattern
hide_const Pattern fun_app term_true term_false z3div z3mod
hide_const (open) trigger pat nopat weight
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Wed Mar 12 12:18:41 2014 +0100
@@ -5,7 +5,7 @@
header {* Word examples for for SMT binding *}
theory SMT_Word_Examples
-imports Word
+imports "~~/src/HOL/Word/Word"
begin
declare [[smt_oracle = true]]
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Mar 12 12:18:41 2014 +0100
@@ -1222,7 +1222,7 @@
fold_thms lthy ctr_defs'
(unfold_thms lthy (pre_rel_def :: abs_inverse ::
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
- @{thms vimage2p_def Inl_Inr_False})
+ @{thms vimage2p_def sum.inject Inl_Inr_False})
(cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc
|> singleton (Proof_Context.export names_lthy no_defs_lthy);