--- a/src/HOL/Groups_List.thy Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/Groups_List.thy Mon Jun 22 21:50:56 2015 +0200
@@ -238,15 +238,15 @@
using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
lemma listsum_map_eq_setsum_count:
- "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) (set xs)"
+ "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
proof(induction xs)
case (Cons x xs)
show ?case (is "?l = ?r")
proof cases
assume "x \<in> set xs"
- have "?l = f x + (\<Sum>x\<in>set xs. List.count xs x * f x)" by (simp add: Cons.IH)
+ have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH)
also have "set xs = insert x (set xs - {x})" using `x \<in> set xs`by blast
- also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). List.count xs x * f x) = ?r"
+ also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r"
by (simp add: setsum.insert_remove eq_commute)
finally show ?thesis .
next
@@ -258,9 +258,9 @@
lemma listsum_map_eq_setsum_count2:
assumes "set xs \<subseteq> X" "finite X"
-shows "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) X"
+shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
proof-
- let ?F = "\<lambda>x. List.count xs x * f x"
+ let ?F = "\<lambda>x. count_list xs x * f x"
have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
using Un_absorb1[OF assms(1)] by(simp)
also have "\<dots> = setsum ?F (set xs)"
--- a/src/HOL/IMP/Compiler.thy Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/IMP/Compiler.thy Mon Jun 22 21:50:56 2015 +0200
@@ -146,7 +146,7 @@
\<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
by (drule exec_appendL[where P'=P']) simp
-text{* Split the execution of a compound program up into the excution of its
+text{* Split the execution of a compound program up into the execution of its
parts: *}
lemma exec_append_trans[intro]:
--- a/src/HOL/List.thy Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/List.thy Mon Jun 22 21:50:56 2015 +0200
@@ -181,13 +181,11 @@
"find _ [] = None" |
"find P (x#xs) = (if P x then Some x else find P xs)"
-hide_const (open) find
-
-primrec count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
-"count [] y = 0" |
-"count (x#xs) y = (if x=y then count xs y + 1 else count xs y)"
-
-hide_const (open) count
+text \<open>In the context of multisets, @{text count_list} is equivalent to
+ @{term "count o mset"} and it it advisable to use the latter.\<close>
+primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
+"count_list [] y = 0" |
+"count_list (x#xs) y = (if x=y then count_list xs y + 1 else count_list xs y)"
definition
"extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
@@ -304,7 +302,7 @@
@{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
-@{lemma "List.count [0,1,0,2::int] 0 = 2" by (simp)}\\
+@{lemma "count_list [0,1,0,2::int] 0 = 2" by (simp)}\\
@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
@@ -3717,16 +3715,16 @@
by (induct xs) simp_all
-subsubsection {* @{const List.count} *}
-
-lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> List.count xs x = 0"
+subsubsection {* @{const count_list} *}
+
+lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> count_list xs x = 0"
by (induction xs) auto
-lemma count_le_length: "List.count xs x \<le> length xs"
+lemma count_le_length: "count_list xs x \<le> length xs"
by (induction xs) auto
lemma setsum_count_set:
- "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (List.count xs) X = length xs"
+ "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (count_list xs) X = length xs"
apply(induction xs arbitrary: X)
apply simp
apply (simp add: setsum.If_cases)
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Jun 22 21:50:56 2015 +0200
@@ -288,9 +288,19 @@
Type_Ind => @{typ ind}
| Type_Bool => HOLogic.boolT
| Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
+ (*FIXME these types are currently unsupported, so they're treated as
+ individuals*)
+ (*
| Type_Int => @{typ int}
| Type_Rat => @{typ rat}
| Type_Real => @{typ real}
+ *)
+ | Type_Int =>
+ interpret_type config thy type_map (Defined_type Type_Ind)
+ | Type_Rat =>
+ interpret_type config thy type_map (Defined_type Type_Ind)
+ | Type_Real =>
+ interpret_type config thy type_map (Defined_type Type_Ind)
| Type_Dummy => dummyT)
| Sum_type _ =>
raise MISINTERPRET_TYPE (*FIXME*)
@@ -305,13 +315,17 @@
fun permute_type_args perm Ts = map (nth Ts) perm
-fun the_const thy const_map str tyargs =
+fun the_const config thy const_map str tyargs =
(case AList.lookup (op =) const_map str of
SOME (Const (s, _), tyarg_perm) =>
Sign.mk_const thy (s, permute_type_args tyarg_perm tyargs)
- | _ => raise MISINTERPRET_TERM
- ("Could not find the interpretation of this constant in the \
- \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
+ | _ =>
+ if const_exists config thy str then
+ Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), [])
+ else
+ raise MISINTERPRET_TERM
+ ("Could not find the interpretation of this constant in the \
+ \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
(*Eta-expands n-ary function.
"str" is the name of an Isabelle/HOL constant*)
@@ -360,6 +374,7 @@
fun type_arity_of_symbol thy config (Uninterpreted n) =
let val s = full_name thy config n in
length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
+ handle TYPE _ => 0
end
| type_arity_of_symbol _ _ _ = 0
@@ -368,7 +383,7 @@
Uninterpreted n =>
(*Constant would have been added to the map at the time of
declaration*)
- the_const thy const_map n tyargs
+ the_const config thy const_map n tyargs
| Interpreted_ExtraLogic interpreted_symbol =>
(*FIXME not interpreting*)
Sign.mk_const thy ((Sign.full_name thy (mk_binding config
@@ -513,10 +528,10 @@
var_types type_map (hd tptp_ts)))
| _ =>
let
- val typ_arity = type_arity_of_symbol thy config symb
+ val typ_arity = type_arity_of_symbol thy' config symb
val (tptp_type_args, tptp_term_args) = chop typ_arity tptp_ts
val tyargs =
- map (interpret_type config thy type_map o termtype_to_type)
+ map (interpret_type config thy' type_map o termtype_to_type)
tptp_type_args
in
(*apply symb to tptp_ts*)
@@ -564,12 +579,27 @@
| Term_Num (number_kind, num) =>
let
(*FIXME hack*)
+ (*
val tptp_type = case number_kind of
Int_num => Type_Int
| Real_num => Type_Real
| Rat_num => Type_Rat
val T = interpret_type config thy type_map (Defined_type tptp_type)
in (HOLogic.mk_number T (the (Int.fromString num)), thy) end
+ *)
+
+ val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)
+ val prefix = case number_kind of
+ Int_num => "intn_"
+ | Real_num => "realn_"
+ | Rat_num => "ratn_"
+ val const_name = prefix ^ num
+ in
+ if const_exists config thy const_name then
+ (Sign.mk_const thy ((Sign.full_name thy (mk_binding config const_name)), []), thy)
+ else
+ declare_constant config const_name ind_type thy
+ end
| Term_Distinct_Object str =>
declare_constant config ("do_" ^ str)
(interpret_type config thy type_map (Defined_type Type_Ind)) thy
--- a/src/HOL/TPTP/atp_problem_import.ML Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Jun 22 21:50:56 2015 +0200
@@ -243,7 +243,7 @@
(auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
- ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Mon Jun 22 21:50:56 2015 +0200
@@ -24,10 +24,12 @@
TIMEOUT=$1
shift
+isabelle build -b HOL-TPTP
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"
+ "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Mon Jun 22 21:50:56 2015 +0200
@@ -24,10 +24,12 @@
TIMEOUT=$1
shift
+isabelle build -b HOL-TPTP
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"
+ "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Mon Jun 22 21:50:56 2015 +0200
@@ -24,10 +24,12 @@
TIMEOUT=$1
shift
+isabelle build -b HOL-TPTP
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"
+ "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Mon Jun 22 21:50:56 2015 +0200
@@ -23,10 +23,12 @@
TIMEOUT=$1
shift
+isabelle build -b HOL-TPTP
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"
+ "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Mon Jun 22 21:50:56 2015 +0200
@@ -24,10 +24,12 @@
TIMEOUT=$1
shift
+isabelle build -b HOL-TPTP
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"
+ "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Mon Jun 22 21:50:56 2015 +0200
@@ -23,7 +23,9 @@
args=("$@")
+isabelle build -b HOL-TPTP
+
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end;" \
+ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
> /tmp/$SCRATCH.thy
-"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"
+"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 22 21:50:56 2015 +0200
@@ -66,16 +66,22 @@
fun is_metis_method (Metis_Method _) = true
| is_metis_method _ = false
+fun add_chained [] t = t
+ | add_chained chained ((t as Const (@{const_name Pure.all}, _)) $ Abs (s, T, u)) =
+ t $ Abs (s, T, add_chained chained u)
+ | add_chained chained t = Logic.list_implies (chained, t)
+
fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
if timeout = Time.zeroTime then
(used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
else
let
- val fact_names = map fst used_facts
+ val ctxt = Proof.context_of state
- val {context = ctxt, facts = chained, goal} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
- val goal_t = Logic.list_implies (map Thm.prop_of chained @ hyp_ts, concl_t)
+ val fact_names = map fst used_facts
+ val {facts = chained, goal, ...} = Proof.goal state
+ val goal_t = Logic.get_goal (Thm.prop_of goal) i
+ |> add_chained (map Thm.prop_of chained)
fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
| try_methss ress [] =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 22 21:50:12 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 22 21:50:56 2015 +0200
@@ -132,7 +132,7 @@
(case xs of
[] => t
| _ =>
- (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+ (* proof obligation: !!thesis. (!!x1...xn. t ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
val frees = map Free xs
@@ -140,10 +140,10 @@
Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
val thesis_prop = HOLogic.mk_Trueprop thesis
- (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+ (* !!x1...xn. t ==> thesis *)
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
in
- (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+ (* !!thesis. (!!x1...xn. t ==> thesis) ==> thesis *)
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)