--- a/src/HOL/Import/HOLLight/HOLLight.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLight/HOLLight.thy Thu Sep 01 14:35:51 2011 +0200
@@ -759,12 +759,12 @@
==> EX f::nat => 'A. ALL x::nat. f x = H f x"
by (import hollight WF_REC_num)
-lemma WF_MEASURE: "wfP (%(a::'A) b::'A. measure (m::'A => nat) (a, b))"
+lemma WF_MEASURE: "wfP (%(a::'A) b::'A. (a, b) : measure (m::'A => nat))"
by (import hollight WF_MEASURE)
lemma MEASURE_LE: "(ALL x::'q_12099.
- measure (m::'q_12099 => nat) (x, a::'q_12099) -->
- measure m (x, b::'q_12099)) =
+ (x, a::'q_12099) : measure (m::'q_12099 => nat) -->
+ (x, b::'q_12099) : measure m) =
(m a <= m b)"
by (import hollight MEASURE_LE)
--- a/src/HOL/Import/HOLLight/hollight.imp Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu Sep 01 14:35:51 2011 +0200
@@ -590,6 +590,8 @@
"UNIONS_INSERT" > "Complete_Lattice.Union_insert"
"UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
"UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
+ "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
+ "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
"UNIONS_0" > "Complete_Lattice.Union_empty"
"UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
"TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
@@ -1595,6 +1597,8 @@
"INTERS_INSERT" > "Complete_Lattice.Inter_insert"
"INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
"INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
+ "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
+ "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
"INTERS_0" > "Complete_Lattice.Inter_empty"
"INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
"INSERT_UNION_EQ" > "Set.Un_insert_left"
@@ -1684,7 +1688,7 @@
"HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
"GE_C" > "HOLLight.hollight.GE_C"
"FUN_IN_IMAGE" > "Set.imageI"
- "FUN_EQ_THM" > "Fun.fun_eq_iff"
+ "FUN_EQ_THM" > "HOL.fun_eq_iff"
"FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
"FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
"FST" > "Product_Type.fst_conv"
@@ -2010,7 +2014,7 @@
"DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
"DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
"DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
- "DEF__dot__dot_" > "HOLLightCompat.DEF__dot__dot_"
+ "DEF__dot__dot_" > "HOLLightCompat.dotdot_def"
"DEF__backslash__slash_" > "HOL.or_def"
"DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
"DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
@@ -2080,7 +2084,7 @@
"DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
"DEF_I" > "Fun.id_apply"
"DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
- "DEF_GSPEC" > "HOLLightCompat.DEF_GSPEC"
+ "DEF_GSPEC" > "Set.Collect_def"
"DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
"DEF_GABS" > "HOLLightCompat.DEF_GABS"
"DEF_FST" > "HOLLightCompat.DEF_FST"
--- a/src/HOL/Import/HOLLightCompat.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLightCompat.thy Thu Sep 01 14:35:51 2011 +0200
@@ -22,19 +22,16 @@
by simp
lemma num_Axiom:
- "\<forall>e f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
- apply (intro allI)
- apply (rule_tac a="nat_rec e (%n e. f e n)" in ex1I)
- apply auto
- apply (simp add: fun_eq_iff)
- apply (intro allI)
- apply (induct_tac xa)
+ "\<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
+ apply (rule ex1I[of _ "nat_rec e (%n e. f e n)"])
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac x)
apply simp_all
done
lemma SUC_INJ:
"\<forall>m n. Suc m = Suc n \<longleftrightarrow> m = n"
- by auto
+ by simp
lemma PAIR:
"(fst x, snd x) = x"
@@ -47,8 +44,7 @@
lemma DEF__star_:
"op * = (SOME mult. (\<forall>n. mult 0 n = 0) \<and> (\<forall>m n. mult (Suc m) n = mult m n + n))"
apply (rule some_equality[symmetric])
- apply auto
- apply (rule ext)+
+ apply (auto simp add: fun_eq_iff)
apply (induct_tac x)
apply auto
done
@@ -93,30 +89,32 @@
lemma DEF_WF:
"wfP = (\<lambda>u. \<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
unfolding fun_eq_iff
- apply (intro allI, rule, intro allI impI, elim exE)
- apply (drule_tac wfE_min[to_pred, unfolded mem_def])
- apply assumption
- prefer 2
- apply assumption
- apply auto[1]
- apply (intro wfI_min[to_pred, unfolded mem_def])
- apply (drule_tac x="Q" in spec)
- apply auto
- apply (rule_tac x="xb" in bexI)
- apply (auto simp add: mem_def)
- done
+proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
+ fix P :: "'a \<Rightarrow> bool" and xa :: "'a"
+ assume "P xa"
+ then show "xa \<in> Collect P" by simp
+next
+ fix x P xa z
+ assume "P xa" "z \<in> {a. P a}" "\<And>y. x y z \<Longrightarrow> y \<notin> {a. P a}"
+ then show "\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y)" by auto
+next
+ fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
+ assume a: "xa \<in> Q"
+ assume b: "\<forall>P. Ex P \<longrightarrow> (\<exists>xa. P xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> P y))"
+ then have "Ex (\<lambda>x. x \<in> Q) \<longrightarrow> (\<exists>xa. (\<lambda>x. x \<in> Q) xa \<and> (\<forall>y. x y xa \<longrightarrow> \<not> (\<lambda>x. x \<in> Q) y))" by auto
+ then show "\<exists>z\<in>Q. \<forall>y. x y z \<longrightarrow> y \<notin> Q" using a by auto
+qed
-lemma DEF_UNIV: "UNIV = (%x. True)"
- by (auto simp add: mem_def)
+lemma DEF_UNIV: "top = (%x. True)"
+ by (rule ext) (simp add: top1I)
lemma DEF_UNIONS:
"Sup = (\<lambda>u. {ua. \<exists>x. (\<exists>ua. ua \<in> u \<and> x \<in> ua) \<and> ua = x})"
- by (simp add: fun_eq_iff Collect_def)
- (metis UnionE complete_lattice_class.Sup_upper mem_def predicate1D)
+ by (auto simp add: Union_eq)
lemma DEF_UNION:
"op \<union> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<or> x \<in> ua) \<and> ub = x})"
- by (auto simp add: mem_def fun_eq_iff Collect_def)
+ by auto
lemma DEF_SUBSET: "op \<subseteq> = (\<lambda>u ua. \<forall>x. x \<in> u \<longrightarrow> x \<in> ua)"
by (metis set_rev_mp subsetI)
@@ -129,7 +127,7 @@
definition [simp, hol4rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> ua)"
- by (auto simp add: mem_def fun_eq_iff)
+ by (metis psubset_eq)
definition [hol4rew]: "Pred n = n - (Suc 0)"
@@ -174,8 +172,8 @@
definition "MEASURE = (%u x y. (u x :: nat) < u y)"
lemma [hol4rew]:
- "MEASURE u = (%a b. measure u (a, b))"
- unfolding MEASURE_def measure_def fun_eq_iff inv_image_def Collect_def
+ "MEASURE u = (%a b. (a, b) \<in> measure u)"
+ unfolding MEASURE_def measure_def
by simp
definition
@@ -187,12 +185,11 @@
lemma DEF_INTERS:
"Inter = (\<lambda>u. {ua. \<exists>x. (\<forall>ua. ua \<in> u \<longrightarrow> x \<in> ua) \<and> ua = x})"
- by (auto simp add: fun_eq_iff mem_def Collect_def)
- (metis InterD InterI mem_def)+
+ by auto
lemma DEF_INTER:
"op \<inter> = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<in> ua) \<and> ub = x})"
- by (auto simp add: mem_def fun_eq_iff Collect_def)
+ by auto
lemma DEF_INSERT:
"insert = (%u ua y. y \<in> ua | y = u)"
@@ -202,10 +199,6 @@
"op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
by (simp add: fun_eq_iff image_def Bex_def)
-lemma DEF_GSPEC:
- "Collect = (\<lambda>u. u)"
- by (simp add: Collect_def ext)
-
lemma DEF_GEQ:
"(op =) = (op =)"
by simp
@@ -226,9 +219,7 @@
apply (erule finite_induct)
apply auto[2]
apply (drule_tac x="finite" in spec)
- apply auto
- apply (metis Collect_def Collect_empty_eq finite.emptyI)
- by (metis (no_types) finite.insertI predicate1I sup.commute sup_absorb1)
+ by (metis finite_insert infinite_imp_nonempty infinite_super predicate1I)
lemma DEF_FACT:
"fact = (SOME FACT. FACT 0 = 1 & (\<forall>n. FACT (Suc n) = Suc n * FACT n))"
@@ -260,10 +251,9 @@
apply simp_all
done
-lemma DEF_EMPTY: "{} = (%x. False)"
- unfolding fun_eq_iff empty_def
- by auto
-
+lemma DEF_EMPTY: "bot = (%x. False)"
+ by (rule ext) auto
+
lemma DEF_DIV:
"op div = (SOME q. \<exists>r. \<forall>m n. if n = (0 :: nat) then q m n = 0 \<and> r m n = m
else m = q m n * n + r m n \<and> r m n < n)"
@@ -286,8 +276,7 @@
lemma DEF_DIFF:
"op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
- by (simp add: fun_eq_iff Collect_def)
- (metis DiffE DiffI mem_def)
+ by (metis set_diff_eq)
definition [hol4rew]: "DELETE s e = s - {e}"
@@ -345,11 +334,8 @@
lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
by (simp add: mem_def)
-definition dotdot :: "nat => nat => nat => bool"
- where "dotdot == %(u::nat) ua::nat. {ub::nat. EX x::nat. (u <= x & x <= ua) & ub = x}"
-
-lemma DEF__dot__dot_: "dotdot = (%u ua. {ub. EX x. (u <= x & x <= ua) & ub = x})"
- by (simp add: dotdot_def)
+definition dotdot :: "nat => nat => nat set"
+ where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
lemma [hol4rew]: "dotdot a b = {a..b}"
unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def
--- a/src/HOL/Import/HOLLightReal.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Import/HOLLightReal.thy Thu Sep 01 14:35:51 2011 +0200
@@ -301,10 +301,7 @@
"(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
(\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
(\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
- apply (intro allI impI, elim conjE)
- apply (drule complete_real[unfolded Ball_def mem_def])
- apply simp_all
- done
+ using complete_real[unfolded Ball_def, of "Collect P"] by auto
lemma REAL_COMPLETE_SOMEPOS:
"(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
--- a/src/HOL/Limits.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Limits.thy Thu Sep 01 14:35:51 2011 +0200
@@ -916,21 +916,6 @@
thus ?thesis by (rule BfunI)
qed
-lemma tendsto_inverse_lemma:
- fixes a :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>(f ---> a) F; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) F\<rbrakk>
- \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) F"
- apply (subst tendsto_Zfun_iff)
- apply (rule Zfun_ssubst)
- apply (erule eventually_elim1)
- apply (erule (1) inverse_diff_inverse)
- apply (rule Zfun_minus)
- apply (rule Zfun_mult_left)
- apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
- apply (erule (1) Bfun_inverse)
- apply (simp add: tendsto_Zfun_iff)
- done
-
lemma tendsto_inverse [tendsto_intros]:
fixes a :: "'a::real_normed_div_algebra"
assumes f: "(f ---> a) F"
@@ -942,8 +927,15 @@
by (rule tendstoD)
then have "eventually (\<lambda>x. f x \<noteq> 0) F"
unfolding dist_norm by (auto elim!: eventually_elim1)
- with f a show ?thesis
- by (rule tendsto_inverse_lemma)
+ with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
+ - (inverse (f x) * (f x - a) * inverse a)) F"
+ by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
+ moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
+ by (intro Zfun_minus Zfun_mult_left
+ bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
+ Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
+ ultimately show ?thesis
+ unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
qed
lemma tendsto_divide [tendsto_intros]:
--- a/src/HOL/List.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/List.thy Thu Sep 01 14:35:51 2011 +0200
@@ -2929,6 +2929,14 @@
by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
qed
+(* The next two lemmas help Sledgehammer. *)
+
+lemma distinct_singleton: "distinct [x]" by simp
+
+lemma distinct_length_2_or_more:
+"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
+by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
@@ -4906,8 +4914,11 @@
lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
by (induct xs) auto
+lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
+by (induct xs, auto)
+
lemma list_size_pointwise[termination_simp]:
- "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
+ "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
by (induct xs) force+
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 01 14:35:51 2011 +0200
@@ -378,9 +378,7 @@
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
- force_sos |> the_default I)
- #> Config.put Sledgehammer_Provers.measure_run_time true
- #> Config.put Sledgehammer_Provers.atp_sound_modulo_infiniteness false)
+ force_sos |> the_default I))
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
@@ -416,12 +414,12 @@
let
val _ = if is_appropriate_prop concl_t then ()
else raise Fail "inappropriate"
- val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
+ val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp
- relevance_override chained_ths hyp_ts concl_t
+ Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
+ chained_ths hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
(the_default default_max_relevant max_relevant)
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Sep 01 14:35:51 2011 +0200
@@ -129,12 +129,12 @@
val relevance_override = {add = [], del = [], only = false}
val subgoal = 1
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
- val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
+ val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
+ Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
chained_ths hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
(the_default default_max_relevant max_relevant)
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 01 14:35:51 2011 +0200
@@ -524,7 +524,7 @@
show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
unfolding * apply auto
apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
- apply(rule_tac x=u in exI) by(auto intro!: exI)
+ apply(rule_tac x=u in exI) by force
qed
lemma mem_affine:
@@ -3028,7 +3028,7 @@
hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
- by(auto simp add: inner_commute elim!: ballE)
+ by(auto simp add: inner_commute del: ballE elim!: ballE)
thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
qed(insert closed_halfspace_ge, auto)
then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
@@ -3062,7 +3062,7 @@
apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
apply(rule assms[unfolded convex_def, rule_format]) prefer 6
- by (auto intro!: tendsto_intros)
+ by (auto del: tendsto_const intro!: tendsto_intros)
lemma convex_interior:
fixes s :: "'a::real_normed_vector set"
@@ -4156,7 +4156,7 @@
using component_le_norm[of "y - x" i]
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
thus "y $$ i \<le> x $$ i + ?d" by auto qed
- also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat by(auto simp add: Suc_le_eq)
+ also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat by(auto simp add: Suc_le_eq)
finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
proof safe fix i assume i:"i<DIM('a)"
have "norm (x - y) < x$$i" apply(rule less_le_trans)
@@ -4176,7 +4176,7 @@
show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof safe
fix i assume i:"i<DIM('a)" show "0 < ?a $$ i" unfolding **[OF i] by(auto simp add: Suc_le_eq)
next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real DIM('a))) ?D" apply(rule setsum_cong2, rule **) by auto
- also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
+ also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
finally show "setsum (op $$ ?a) ?D < 1" by auto qed qed
lemma rel_interior_substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
@@ -4251,7 +4251,7 @@
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
by(auto simp add: norm_minus_commute)
thus "y $$ i \<le> x $$ i + ?d" by auto qed
- also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat
+ also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat
using `0 < card d` by auto
finally show "setsum (op $$ y) d \<le> 1" .
@@ -4294,7 +4294,7 @@
finally show "0 < ?a $$ i" by auto
next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"
by(rule setsum_cong2, rule **)
- also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym]
+ also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat real_divide_def[THEN sym]
by (auto simp add:field_simps)
finally show "setsum (op $$ ?a) ?D < 1" by auto
next fix i assume "i<DIM('a)" and "i~:d"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Sep 01 14:35:51 2011 +0200
@@ -7,7 +7,7 @@
theory Euclidean_Space
imports
- Complex_Main
+ L2_Norm
"~~/src/HOL/Library/Inner_Product"
"~~/src/HOL/Library/Product_Vector"
begin
@@ -216,10 +216,20 @@
simp add: inner_setsum_left inner_setsum_right
dot_basis if_distrib setsum_cases mult_commute)
+lemma euclidean_dist_l2:
+ fixes x y :: "'a::euclidean_space"
+ shows "dist x y = setL2 (\<lambda>i. dist (x $$ i) (y $$ i)) {..<DIM('a)}"
+ unfolding dist_norm norm_eq_sqrt_inner setL2_def
+ by (simp add: euclidean_inner power2_eq_square)
+
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
unfolding euclidean_component_def
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
+lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
+ unfolding euclidean_dist_l2 [where 'a='a]
+ by (cases "i < DIM('a)", rule member_le_setL2, auto)
+
subsection {* Subclass relationships *}
instance euclidean_space \<subseteq> perfect_space
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Sep 01 14:35:51 2011 +0200
@@ -206,6 +206,9 @@
by simp
qed
+lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
+ unfolding isCont_def by (rule tendsto_vec_nth)
+
lemma eventually_Ball_finite: (* TODO: move *)
assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
@@ -296,44 +299,45 @@
apply (simp add: setL2_mono dist_triangle2)
done
next
- (* FIXME: long proof! *)
fix S :: "('a ^ 'b) set"
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
- unfolding open_vec_def open_dist
- apply safe
- apply (drule (1) bspec)
- apply clarify
- apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
- apply clarify
- apply (rule_tac x=e in exI, clarify)
- apply (drule spec, erule mp, clarify)
- apply (drule spec, drule spec, erule mp)
- apply (erule le_less_trans [OF dist_vec_nth_le])
- apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i")
- apply (drule finite_choice [OF finite], clarify)
- apply (rule_tac x="Min (range f)" in exI, simp)
- apply clarify
- apply (drule_tac x=i in spec, clarify)
- apply (erule (1) bspec)
- apply (drule (1) bspec, clarify)
- apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV")
- apply clarify
- apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI)
- apply (rule conjI)
- apply clarify
- apply (rule conjI)
- apply (clarify, rename_tac y)
- apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp)
- apply clarify
- apply (simp only: less_diff_eq)
- apply (erule le_less_trans [OF dist_triangle])
- apply simp
- apply clarify
- apply (drule spec, erule mp)
- apply (simp add: dist_vec_def setL2_strict_mono)
- apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI)
- apply (simp add: divide_pos_pos setL2_constant)
- done
+ proof
+ assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
+ proof
+ fix x assume "x \<in> S"
+ obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i"
+ and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
+ using `open S` and `x \<in> S` unfolding open_vec_def by metis
+ have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
+ using A unfolding open_dist by simp
+ hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
+ by (rule finite_choice [OF finite])
+ then obtain r where r1: "\<forall>i. 0 < r i"
+ and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
+ have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"
+ by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le])
+ thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
+ qed
+ next
+ assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S"
+ proof (unfold open_vec_def, rule)
+ fix x assume "x \<in> S"
+ then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S"
+ using * by fast
+ def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))"
+ from `0 < e` have r: "\<forall>i. 0 < r i"
+ unfolding r_def by (simp_all add: divide_pos_pos)
+ from `0 < e` have e: "e = setL2 r UNIV"
+ unfolding r_def by (simp add: setL2_constant)
+ def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}"
+ have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
+ unfolding A_def by (simp add: open_ball r)
+ moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
+ by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
+ ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
+ (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
+ qed
+ qed
qed
end
@@ -434,9 +438,6 @@
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
done
-lemmas isCont_vec_nth [simp] =
- bounded_linear.isCont [OF bounded_linear_vec_nth]
-
instance vec :: (banach, finite) banach ..
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 01 14:35:51 2011 +0200
@@ -2534,8 +2534,6 @@
unfolding infnorm_set_image ball_simps
by (metis component_le_norm)
-lemma card_enum: "card {1 .. n} = n" by auto
-
lemma norm_le_infnorm: "norm(x) <= sqrt(real DIM('a)) * infnorm(x::'a::euclidean_space)"
proof-
let ?d = "DIM('a)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 01 14:35:51 2011 +0200
@@ -7,19 +7,9 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
begin
-(* to be moved elsewhere *)
-
-lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
- unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
- by(auto simp add:power2_eq_square)
-
-lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
- apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
- apply(rule member_le_setL2) by auto
-
subsection {* General notion of a topology as a value *}
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
@@ -2252,6 +2242,8 @@
unfolding convergent_def by auto
qed
+instance euclidean_space \<subseteq> banach ..
+
lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
proof(simp add: complete_def, rule, rule)
fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
@@ -2286,21 +2278,13 @@
lemma convergent_eq_cauchy:
fixes s :: "nat \<Rightarrow> 'a::complete_space"
- shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
-proof
- assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
- thus ?rhs using convergent_imp_cauchy by auto
-next
- assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto
-qed
+ shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s"
+ unfolding Cauchy_convergent_iff convergent_def ..
lemma convergent_imp_bounded:
fixes s :: "nat \<Rightarrow> 'a::metric_space"
- shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
- using convergent_imp_cauchy[of s]
- using cauchy_imp_bounded[of s]
- unfolding image_def
- by auto
+ shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
+ by (intro cauchy_imp_bounded convergent_imp_cauchy)
subsubsection{* Total boundedness *}
@@ -2953,7 +2937,7 @@
"\<forall>n. (s n \<noteq> {})"
"\<forall>m n. m \<le> n --> s n \<subseteq> s m"
"\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
- shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s n"
+ shows "\<exists>a::'a::complete_space. \<forall>n::nat. a \<in> s n"
proof-
have "\<forall>n. \<exists> x. x\<in>s n" using assms(2) by auto
hence "\<exists>t. \<forall>n. t n \<in> s n" using choice[of "\<lambda> n x. x \<in> s n"] by auto
@@ -2982,7 +2966,7 @@
text {* Strengthen it to the intersection actually being a singleton. *}
lemma decreasing_closed_nest_sing:
- fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
+ fixes s :: "nat \<Rightarrow> 'a::complete_space set"
assumes "\<forall>n. closed(s n)"
"\<forall>n. s n \<noteq> {}"
"\<forall>m n. m \<le> n --> s n \<subseteq> s m"
@@ -5874,10 +5858,6 @@
ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
qed
-
-(** TODO move this someplace else within this theory **)
-instance euclidean_space \<subseteq> banach ..
-
declare tendsto_const [intro] (* FIXME: move *)
end
--- a/src/HOL/TPTP/atp_export.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Thu Sep 01 14:35:51 2011 +0200
@@ -27,8 +27,7 @@
val fact_name_of = prefix fact_prefix o ascii_of
fun facts_of thy =
- Sledgehammer_Filter.all_facts (Proof_Context.init_global thy)
- false(*FIXME works only for first-order*)
+ Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) false
Symtab.empty true [] []
|> filter (curry (op =) @{typ bool} o fastype_of
o Object_Logic.atomize_term thy o prop_of o snd)
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 01 14:35:51 2011 +0200
@@ -479,14 +479,19 @@
fun declared_syms_in_problem problem =
fold (fold add_declared_syms_in_problem_line o snd) problem []
+fun nary_type_constr_type n =
+ funpow n (curry AFun atype_of_types) atype_of_types
+
fun undeclared_syms_in_problem declared problem =
let
fun do_sym name ty =
if member (op =) declared name then I else AList.default (op =) (name, ty)
- fun do_type_name name = do_sym name (K atype_of_types)
- fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
+ fun do_type (AType (name as (s, _), tys)) =
+ is_tptp_user_symbol s
+ ? do_sym name (fn _ => nary_type_constr_type (length tys))
+ #> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
- | do_type (ATyAbs (names, ty)) = fold do_type_name names #> do_type ty
+ | do_type (ATyAbs (_, ty)) = do_type ty
fun do_term pred_sym (ATerm (name as (s, _), tms)) =
is_tptp_user_symbol s
? do_sym name (fn _ => default_type pred_sym (length tms))
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Sep 01 14:35:51 2011 +0200
@@ -21,7 +21,7 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
- datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+ datatype soundness = Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
Noninf_Nonmono_Types of soundness |
@@ -139,6 +139,11 @@
val elimN = "elim"
val simpN = "simp"
+(* TFF1 is still in development, and it is still unclear whether symbols will be
+ allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
+ "dummy" type variables. *)
+val exploit_tff1_dummy_type_vars = false
+
val bound_var_prefix = "B_"
val all_bound_var_prefix = "BA_"
val exist_bound_var_prefix = "BE_"
@@ -360,27 +365,19 @@
(** Definitions and functions for FOL clauses and formulas for TPTP **)
-(* The first component is the type class; the second is a "TVar" or "TFree". *)
-datatype type_literal =
- TyLitVar of name * name |
- TyLitFree of name * name
-
-
(** Isabelle arities **)
-datatype arity_literal =
- TConsLit of name * name * name list |
- TVarLit of name * name
+type arity_atom = name * name * name list
val type_class = the_single @{sort type}
-fun add_packed_sort tvar =
- fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
-
type arity_clause =
{name : string,
- prem_lits : arity_literal list,
- concl_lits : arity_literal}
+ prem_atoms : arity_atom list,
+ concl_atom : arity_atom}
+
+fun add_prem_atom tvar =
+ fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
fun make_axiom_arity_clause (tcons, name, (cls, args)) =
@@ -389,9 +386,9 @@
val tvars_srts = ListPair.zip (tvars, args)
in
{name = name,
- prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
- concl_lits = TConsLit (`make_type_class cls, `make_fixed_type_const tcons,
- tvars ~~ tvars)}
+ prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
+ concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
+ tvars ~~ tvars)}
end
fun arity_clause _ _ (_, []) = []
@@ -539,7 +536,7 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
+datatype soundness = Sound_Modulo_Infiniteness | Sound
datatype type_level =
All_Types |
Noninf_Nonmono_Types of soundness |
@@ -718,24 +715,40 @@
Explicit_Type_Args)
end
-(* Make literals for sorted type variables. *)
+(* Make atoms for sorted type variables. *)
fun generic_add_sorts_on_type (_, []) = I
| generic_add_sorts_on_type ((x, i), s :: ss) =
generic_add_sorts_on_type ((x, i), ss)
#> (if s = the_single @{sort HOL.type} then
I
else if i = ~1 then
- insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
+ insert (op =) (`make_type_class s, `make_fixed_type_var x)
else
- insert (op =) (TyLitVar (`make_type_class s,
- (make_schematic_type_var (x, i), x))))
+ insert (op =) (`make_type_class s,
+ (make_schematic_type_var (x, i), x)))
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
| add_sorts_on_tfree _ = I
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
| add_sorts_on_tvar _ = I
-fun type_literals_for_types type_enc add_sorts_on_typ Ts =
+val tvar_a_str = "'a"
+val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
+val itself_name = `make_fixed_type_const @{type_name itself}
+val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
+val tvar_a_atype = AType (tvar_a_name, [])
+val a_itself_atype = AType (itself_name, [tvar_a_atype])
+
+fun type_class_formula type_enc class arg =
+ AAtom (ATerm (class, arg ::
+ (case type_enc of
+ Simple_Types (_, Polymorphic, _) =>
+ if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
+ | _ => [])))
+fun formulas_for_types type_enc add_sorts_on_typ Ts =
[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
+ |> map (fn (class, name) =>
+ type_class_formula type_enc class (ATerm (name, [])))
fun mk_aconns c phis =
let val (phis', phi') = split_last phis in
@@ -1120,11 +1133,10 @@
(* These types witness that the type classes they belong to allow infinite
models and hence that any types with these type classes is monotonic. *)
val known_infinite_types =
- [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
+ [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
- soundness <> Sound andalso
- is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
+ soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
@@ -1276,8 +1288,6 @@
K (add_iterm_syms_to_table ctxt explicit_apply)
|> formula_fold NONE |> fact_lift
-val tvar_a = TVar (("'a", 0), HOLogic.typeS)
-
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = []})
@@ -1450,16 +1460,8 @@
(("If", true), @{thms if_True if_False True_or_False})]
|> map (apsnd (map zero_var_indexes))
-fun fo_literal_from_type_literal (TyLitVar (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
- | fo_literal_from_type_literal (TyLitFree (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-fun bound_tvars type_enc Ts =
- mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
- (type_literals_for_types type_enc add_sorts_on_tvar Ts))
+fun bound_tvars type_enc =
+ mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar
fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
@@ -1738,25 +1740,23 @@
fun formula_line_for_class_rel_clause type_enc
({name, subclass, superclass, ...} : class_rel_clause) =
- let val ty_arg = ATerm ((make_schematic_type_var ("'a", 0), "'a"), []) in
+ let val ty_arg = ATerm (tvar_a_name, []) in
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
- AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
- AAtom (ATerm (superclass, [ty_arg]))])
+ AConn (AImplies,
+ [type_class_formula type_enc subclass ty_arg,
+ type_class_formula type_enc superclass ty_arg])
|> close_formula_universally type_enc, isabelle_info introN, NONE)
end
-fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
- (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
- | fo_literal_from_arity_literal (TVarLit (c, sort)) =
- (false, ATerm (c, [ATerm (sort, [])]))
+fun formula_from_arity_atom type_enc (class, t, args) =
+ ATerm (t, map (fn arg => ATerm (arg, [])) args)
+ |> type_class_formula type_enc class
fun formula_line_for_arity_clause type_enc
- ({name, prem_lits, concl_lits, ...} : arity_clause) =
+ ({name, prem_atoms, concl_atom, ...} : arity_clause) =
Formula (arity_clause_prefix ^ name, Axiom,
- mk_ahorn (map (formula_from_fo_literal o apfst not
- o fo_literal_from_arity_literal) prem_lits)
- (formula_from_fo_literal
- (fo_literal_from_arity_literal concl_lits))
+ mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
+ (formula_from_arity_atom type_enc concl_atom)
|> close_formula_universally type_enc, isabelle_info introN, NONE)
fun formula_line_for_conjecture ctxt format mono type_enc
@@ -1768,24 +1768,24 @@
|> bound_tvars type_enc atomic_types
|> close_formula_universally type_enc, NONE, NONE)
-fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
- atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
- |> map fo_literal_from_type_literal
-
-fun formula_line_for_free_type j lit =
- Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
- formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types type_enc facts =
+fun formula_line_for_free_type j phi =
+ Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
+fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
let
- val litss = map (free_type_literals type_enc) facts
- val lits = fold (union (op =)) litss []
- in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
+ val phis =
+ fold (union (op =)) (map #atomic_types facts) []
+ |> formulas_for_types type_enc add_sorts_on_tfree
+ in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
(** Symbol declarations **)
fun decl_line_for_class s =
let val name as (s, _) = `make_type_class s in
- Decl (sym_decl_prefix ^ s, name, AFun (atype_of_types, bool_atype))
+ Decl (sym_decl_prefix ^ s, name,
+ if exploit_tff1_dummy_type_vars then
+ AFun (atype_of_types, bool_atype)
+ else
+ ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
end
fun decl_lines_for_classes type_enc classes =
@@ -1833,7 +1833,7 @@
fun add_undefined_const T =
let
val (s, s') =
- `(make_fixed_const (SOME format)) @{const_name undefined}
+ `(make_fixed_const NONE) @{const_name undefined}
|> (case type_arg_policy type_enc @{const_name undefined} of
Mangled_Type_Args _ => mangled_const_name format type_enc [T]
| _ => I)
@@ -1841,22 +1841,32 @@
Symtab.map_default (s, [])
(insert_type ctxt #3 (s', [T], T, false, 0, false))
end
+ fun add_TYPE_const () =
+ let val (s, s') = TYPE_name in
+ Symtab.map_default (s, [])
+ (insert_type ctxt #3
+ (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
+ end
in
Symtab.empty
|> is_type_enc_fairly_sound type_enc
? (fold (add_fact_syms true) conjs
#> fold (add_fact_syms false) facts
#> (case type_enc of
- Simple_Types _ => I
+ Simple_Types (_, poly, _) =>
+ if poly = Polymorphic then add_TYPE_const () else I
| _ => fold add_undefined_const (var_types ())))
end
(* We add "bool" in case the helper "True_or_False" is included later. *)
-val default_mono =
+fun default_mono level =
{maybe_finite_Ts = [@{typ bool}],
surely_finite_Ts = [@{typ bool}],
maybe_infinite_Ts = known_infinite_types,
- surely_infinite_Ts = known_infinite_types,
+ surely_infinite_Ts =
+ case level of
+ Noninf_Nonmono_Types Sound => []
+ | _ => known_infinite_types,
maybe_nonmono_Ts = [@{typ bool}]}
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
@@ -1911,7 +1921,7 @@
(add_iterm_mononotonicity_info ctxt level) iformula
fun mononotonicity_info_for_facts ctxt type_enc facts =
let val level = level_of_type_enc type_enc in
- default_mono
+ default_mono level
|> is_type_level_monotonicity_based level
? fold (add_fact_mononotonicity_info ctxt level) facts
end
--- a/src/HOL/Tools/Metis/metis_tactics.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu Sep 01 14:35:51 2011 +0200
@@ -121,7 +121,7 @@
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
- val type_enc = type_enc_from_string Unsound type_enc
+ val type_enc = type_enc_from_string Sound type_enc
val (sym_tab, axioms, old_skolems) =
prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 01 14:35:51 2011 +0200
@@ -52,7 +52,7 @@
Proof.context -> bool -> relevance_override -> thm list -> term list -> term
-> (((unit -> string) * locality) * thm) list
val relevant_facts :
- Proof.context -> bool -> real * real -> int
+ Proof.context -> real * real -> int
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
-> relevance_override -> thm list -> term list -> term
-> (((unit -> string) * locality) * thm) list
@@ -586,7 +586,7 @@
facts are included. *)
val special_fact_index = 75
-fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const
+fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
(fudge as {threshold_divisor, ridiculous_threshold, ...})
({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
let
@@ -938,9 +938,9 @@
|> uniquify
end
-fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant
- is_built_in_const fudge (override as {only, ...}) chained_ths
- hyp_ts concl_t facts =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
+ fudge (override as {only, ...}) chained_ths hyp_ts concl_t
+ facts =
let
val thy = Proof_Context.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -954,9 +954,9 @@
max_relevant = 0 then
[]
else
- relevance_filter ctxt ho_atp threshold0 decay max_relevant
- is_built_in_const fudge override facts (chained_ths |> map prop_of)
- hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy)))
+ relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
+ fudge override facts (chained_ths |> map prop_of) hyp_ts
+ (concl_t |> theory_constify fudge (Context.theory_name thy)))
|> map (apfst (apfst (fn f => f ())))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Sep 01 14:35:51 2011 +0200
@@ -62,10 +62,8 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
- val measure_run_time : bool Config.T
val atp_lambda_translation : string Config.T
val atp_full_names : bool Config.T
- val atp_sound_modulo_infiniteness : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
val smt_weight_min_facts : int Config.T
@@ -340,8 +338,6 @@
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
val problem_prefix =
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val measure_run_time =
- Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
val atp_lambda_translation =
Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
@@ -351,9 +347,6 @@
provers (e.g., E). For these reason, short names are enabled by default. *)
val atp_full_names =
Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
-val atp_sound_modulo_infiniteness =
- Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
- (K true)
val smt_triggers =
Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
@@ -510,9 +503,6 @@
#> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
is_exhaustive_finite)
-fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
- | int_opt_add _ _ = NONE
-
(* Important messages are important but not so important that users want to see
them each time. *)
val atp_important_message_keep_quotient = 10
@@ -573,7 +563,6 @@
Path.append (Path.explode dest_dir) problem_file_name
else
error ("No such directory: " ^ quote dest_dir ^ ".")
- val measure_run_time = verbose orelse Config.get ctxt measure_run_time
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
fun split_time s =
let
@@ -585,7 +574,7 @@
val num3 = as_num (digit ::: digit ::: (digit >> single))
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
val as_time = Scan.read Symbol.stopper time o raw_explode
- in (output, as_time t) end
+ in (output, as_time t |> the_default 0 (* can't happen *)) end
fun run_on prob_file =
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
(home_var, _) :: _ =>
@@ -627,13 +616,7 @@
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val soundness =
- if sound then
- if Config.get ctxt atp_sound_modulo_infiniteness then
- Sound_Modulo_Infiniteness
- else
- Sound
- else
- Unsound
+ if sound then Sound else Sound_Modulo_Infiniteness
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc
@@ -676,11 +659,7 @@
File.shell_path command ^ " " ^
arguments ctxt full_proof extra slice_timeout weights ^ " " ^
File.shell_path prob_file
- val command =
- (if measure_run_time then
- "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
- else
- "exec " ^ core) ^ " 2>&1"
+ val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
val _ =
atp_problem
|> tptp_lines_for_atp_problem format
@@ -691,13 +670,13 @@
upto conjecture_offset + length hyp_ts + 1
|> map single
val ((output, msecs), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
+ TimeLimit.timeLimit generous_slice_timeout
+ Isabelle_System.bash_output command
|>> (if overlord then
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
I)
- |> fst
- |> (if measure_run_time then split_time else rpair NONE)
+ |> fst |> split_time
|> (fn accum as (output, _) =>
(accum,
extract_tstplike_proof_and_outcome verbose complete
@@ -706,7 +685,7 @@
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut =>
- (("", SOME (Time.toMilliseconds slice_timeout)),
+ (("", Time.toMilliseconds slice_timeout),
([], SOME TimedOut))
val outcome =
case outcome of
@@ -733,15 +712,15 @@
if Time.<= (time_left, Time.zeroTime) then
result
else
- (run_slice slice time_left
- |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
- (stuff, (output, int_opt_add msecs0 msecs,
- atp_proof, outcome))))
+ run_slice slice time_left
+ |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
+ (stuff, (output, msecs0 + msecs, atp_proof,
+ outcome)))
end
| maybe_run_slice _ result = result
in
((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
- ("", SOME 0, [], SOME InternalError))
+ ("", 0, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
else
@@ -802,7 +781,7 @@
in proof_text ctxt isar_proof isar_params one_line_params end,
(if verbose then
"\nATP real CPU time: " ^
- string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+ string_from_time (Time.fromMilliseconds msecs) ^ "."
else
"") ^
(if important_message <> "" then
@@ -814,7 +793,7 @@
| SOME failure =>
([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
+ {outcome = outcome, used_facts = used_facts, run_time_in_msecs = SOME msecs,
preplay = preplay, message = message, message_tail = message_tail}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Sep 01 14:35:51 2011 +0200
@@ -269,9 +269,10 @@
val {facts = chained_ths, goal, ...} = Proof.goal state
val chained_ths = chained_ths |> normalize_chained_theorems
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
- val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
- val facts = nearly_all_facts ctxt is_ho_atp relevance_override
- chained_ths hyp_ts concl_t
+ val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+ val facts =
+ nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts
+ concl_t
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
@@ -323,9 +324,9 @@
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
- |> relevant_facts ctxt is_ho_atp relevance_thresholds
- max_max_relevant is_built_in_const relevance_fudge
- relevance_override chained_ths hyp_ts concl_t
+ |> relevant_facts ctxt relevance_thresholds max_max_relevant
+ is_built_in_const relevance_fudge relevance_override
+ chained_ths hyp_ts concl_t
|> tap (fn facts =>
if debug then
label ^ plural_s (length provers) ^ ": " ^
--- a/src/HOL/ex/sledgehammer_tactics.ML Thu Sep 01 14:10:52 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Sep 01 14:35:51 2011 +0200
@@ -37,13 +37,11 @@
val relevance_fudge =
Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
- val is_ho_atp =
- exists (Sledgehammer_Provers.is_ho_atp ctxt)
- provers(*FIXME: duplicated from sledgehammer_run.ML*)
+ val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
+ Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
chained_ths hyp_ts concl_t
- |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =