--- a/NEWS Fri Sep 14 21:15:59 2012 +0200
+++ b/NEWS Fri Sep 14 21:23:06 2012 +0200
@@ -126,6 +126,7 @@
- Added MaSh relevance filter based on machine-learning; see the
Sledgehammer manual for details.
- Rationalized type encodings ("type_enc" option).
+ - Renamed "kill_provers" subcommand to "kill"
- Renamed options:
max_relevant ~> max_facts
relevance_thresholds ~> fact_thresholds
--- a/src/Doc/Sledgehammer/document/root.tex Fri Sep 14 21:15:59 2012 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Sep 14 21:23:06 2012 +0200
@@ -675,14 +675,14 @@
currently running automatic provers, including elapsed runtime and remaining
time until timeout.
-\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
-automatic provers.
+\item[\labelitemi] \textbf{\textit{kill}:} Terminates all running
+threads (automatic provers and machine learners).
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
\end{enum}
-In addition, the following subcommands provide fine control over machine
+In addition, the following subcommands provide finer control over machine
learning with MaSh:
\begin{enum}
--- a/src/HOL/Codatatype/BNF_FP.thy Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Fri Sep 14 21:23:06 2012 +0200
@@ -26,17 +26,11 @@
lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
by auto
-lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
-
-lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
+lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()"
+by simp
-(* FIXME: needed? *)
-lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
-by presburger
-
-(* FIXME: needed? *)
-lemma all_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
-by presburger
+lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
+by clarsimp
lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
by simp
@@ -110,6 +104,21 @@
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
+lemma UN_compreh_bex:
+"\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
+"\<Union>{y. \<exists>x \<in> A. y = {x}} = A"
+"\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
+by blast+
+
+lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
+apply (rule exI)
+apply (rule conjI)
+ apply (rule bexI)
+ apply (rule refl)
+ apply assumption
+apply assumption
+done
+
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_sugar_tactics.ML"
ML_file "Tools/bnf_fp_sugar.ML"
--- a/src/HOL/Codatatype/Examples/Stream.thy Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Stream.thy Fri Sep 14 21:23:06 2012 +0200
@@ -133,27 +133,27 @@
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
lemma "ones \<oplus> ones = twos"
-by (intro stream_coind[where phi="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"])
+by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"])
auto
lemma "n \<cdot> twos = ns (2 * n)"
-by (intro stream_coind[where phi="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"])
+by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"])
force+
lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (intro stream_coind[where phi="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"])
+by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"])
force+
lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-by (intro stream_coind[where phi="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
+by (intro stream_coind[where P="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
(force simp: add_mult_distrib2)+
lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (intro stream_coind[where phi="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"])
+by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"])
force+
lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (intro stream_coind[where phi="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"])
+by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"])
force+
end
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 14 21:23:06 2012 +0200
@@ -52,7 +52,7 @@
lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct]
lemma "tmap (f o g) x = tmap f (tmap g x)"
-by (intro treeFsetI_coind[where phi="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
+by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
force+
end
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 21:23:06 2012 +0200
@@ -34,9 +34,9 @@
val simp_attrs = @{attributes [simp]};
-fun split_list11 xs =
+fun split_list10 xs =
(map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
- map #9 xs, map #10 xs, map #11 xs);
+ map #9 xs, map #10 xs);
fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T
| strip_map_type T = ([], T);
@@ -51,9 +51,6 @@
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
-fun mk_id T = Const (@{const_name id}, T --> T);
-fun mk_id_fun T = Abs (Name.uu, T, Bound 0);
-
fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
fun mk_uncurried2_fun f xss =
@@ -66,8 +63,6 @@
Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z)
end;
-fun fold_def_rule n thm = funpow n (fn thm => thm RS fun_cong) (thm RS meta_eq_to_obj_eq) RS sym;
-
fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
fun merge_type_arg T T' = if T = T' then T else cannot_merge_types ();
@@ -94,7 +89,9 @@
val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
else ();
- val N = length specs;
+ val nn = length specs;
+ val fp_bs = map type_binding_of specs;
+ val fp_common_name = mk_common_name fp_bs;
fun prepare_type_arg (ty, c) =
let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
@@ -108,8 +105,8 @@
val ((Bs, Cs), no_defs_lthy) =
no_defs_lthy0
|> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
- |> mk_TFrees N
- ||>> mk_TFrees N;
+ |> mk_TFrees nn
+ ||>> mk_TFrees nn;
(* TODO: cleaner handling of fake contexts, without "background_theory" *)
(*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
@@ -123,9 +120,6 @@
Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
unsorted_As);
- val fp_bs = map type_binding_of specs;
- val fp_common_name = mk_common_name fp_bs;
-
val fake_Ts = map mk_fake_T fp_bs;
val mixfixes = map mixfix_of specs;
@@ -178,17 +172,20 @@
fp_iter_thms, fp_rec_thms), lthy)) =
fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
- val add_nested_bnf_names =
+ fun add_nesty_bnf_names Us =
let
fun add (Type (s, Ts)) ss =
let val (needs, ss') = fold_map add Ts ss in
if exists I needs then (true, insert (op =) s ss') else (false, ss')
end
- | add T ss = (member (op =) As T, ss);
+ | add T ss = (member (op =) Us T, ss);
in snd oo add end;
- val nested_bnfs =
- map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssBs []);
+ fun nesty_bnfs Us =
+ map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssBs []);
+
+ val nesting_bnfs = nesty_bnfs As;
+ val nested_bnfs = nesty_bnfs Bs;
val timer = time (Timer.startRealTimer ());
@@ -205,6 +202,8 @@
val fpTs = map (domain_type o fastype_of) unfs;
+ val exists_fp_subtype = exists_subtype (member (op =) fpTs);
+
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs;
val ns = map length ctr_Tsss;
val kss = map (fn n => 1 upto n) ns;
@@ -337,12 +336,14 @@
val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
- val ((((u, v), fs), xss), _) =
+ val ((((u, fs), xss), v'), _) =
no_defs_lthy
|> yield_singleton (mk_Frees "u") unfT
- ||>> yield_singleton (mk_Frees "v") fpT
||>> mk_Frees "f" case_Ts
- ||>> mk_Freess "x" ctr_Tss;
+ ||>> mk_Freess "x" ctr_Tss
+ ||>> yield_singleton (Variable.variant_fixes) (Binding.name_of fp_b);
+
+ val v = Free (v', fpT);
val ctr_rhss =
map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
@@ -440,8 +441,7 @@
val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
- ((ctrs, selss0, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
- lthy)
+ ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy)
end;
fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
@@ -481,8 +481,8 @@
val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
- ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
- corec_def), lthy)
+ ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def),
+ lthy)
end;
fun wrap lthy =
@@ -498,7 +498,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val map_ids = map map_id_of_bnf nested_bnfs;
+ val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
+ val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
fun mk_map Ts Us t =
let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
@@ -513,36 +514,93 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
- fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _,
+ fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
iter_defs, rec_defs), lthy) =
let
+ val (((phis, phis'), vs'), names_lthy) =
+ lthy
+ |> mk_Frees' "P" (map mk_predT fpTs)
+ ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
+
+ val vs = map2 (curry Free) vs' fpTs;
+
+ fun mk_sets_nested bnf =
+ let
+ val Type (T_name, Us) = T_of_bnf bnf;
+ val lives = lives_of_bnf bnf;
+ val sets = sets_of_bnf bnf;
+ fun mk_set U =
+ (case find_index (curry (op =) U) lives of
+ ~1 => Term.dummy
+ | i => nth sets i);
+ in
+ (T_name, map mk_set Us)
+ end;
+
+ val setss_nested = map mk_sets_nested nested_bnfs;
+
val (induct_thms, induct_thm) =
let
- val sym_ctr_defss = map2 (map2 fold_def_rule) mss ctr_defss;
+ fun mk_set Ts t =
+ let val Type (_, Ts0) = domain_type (fastype_of t) in
+ Term.subst_atomic_types (Ts0 ~~ Ts) t
+ end;
- val ss = @{simpset} |> fold Simplifier.add_simp
- @{thms collect_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]
- fsts_def[abs_def] snds_def[abs_def] False_imp_eq all_point_1};
-
- val induct_thm0 = fp_induct OF (map mk_sumEN_tupled_balanced mss);
+ fun mk_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) =
+ (case find_index (curry (op =) T) fpTs of
+ ~1 =>
+ (case AList.lookup (op =) setss_nested T_name of
+ NONE => []
+ | SOME raw_sets0 =>
+ let
+ val (Ts, raw_sets) =
+ split_list (filter (exists_fp_subtype o fst) (Ts0 ~~ raw_sets0));
+ val sets = map (mk_set Ts0) raw_sets;
+ val (ys, names_lthy') = names_lthy |> mk_Frees s Ts;
+ val heads =
+ map2 (fn y => fn set => HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x)))
+ ys sets;
+ val bodiess = map (mk_prem_prems names_lthy') ys;
+ in
+ flat (map2 (map o curry Logic.mk_implies) heads bodiess)
+ end)
+ | i => [HOLogic.mk_Trueprop (nth phis i $ x)])
+ | mk_prem_prems _ _ = [];
- val spurious_fs =
- Term.add_vars (prop_of induct_thm0) []
- |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT
- | _ => false);
+ fun close_prem_prem (Free x') t =
+ fold_rev Logic.all
+ (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
+
+ fun mk_raw_prem phi ctr ctr_Ts =
+ let
+ val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
+ val prem_prems =
+ maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs;
+ in
+ (xs, prem_prems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
+ end;
- val cxs =
- map (fn s as (_, T) =>
- (certify lthy (Var s), certify lthy (mk_id_fun (domain_type T)))) spurious_fs;
+ val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
+
+ fun mk_prem (xs, prem_prems, concl) =
+ fold_rev Logic.all xs (Logic.list_implies (prem_prems, concl));
+
+ val goal =
+ Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 (curry (op $)) phis vs)));
+
+ val rss = map (map (length o #2)) raw_premss;
+
+ val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
val induct_thm =
- Drule.cterm_instantiate cxs induct_thm0
- |> Tactic.rule_by_tactic lthy (ALLGOALS (REPEAT_DETERM o bound_hyp_subst_tac))
- |> Local_Defs.unfold lthy
- (@{thm triv_forall_equality} :: flat sym_ctr_defss @ flat pre_set_defss)
- |> Simplifier.full_simplify ss;
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss
+ nested_set_natural's)
+ |> singleton (Proof_Context.export names_lthy lthy)
in
- `(conj_dests N) induct_thm
+ `(conj_dests nn) induct_thm
end;
val (iter_thmss, rec_thmss) =
@@ -557,7 +615,7 @@
fun build_call fiter_likes maybe_tick (T, U) =
if T = U then
- mk_id T
+ id_const T
else
(case find_index (curry (op =) T) fpTs of
~1 => build_map (build_call fiter_likes maybe_tick) T U
@@ -569,7 +627,7 @@
fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
if member (op =) fpTs T then
maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
- else if exists_subtype (member (op =) fpTs) T then
+ else if exists_fp_subtype T then
[build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
else
[x];
@@ -581,9 +639,11 @@
val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss;
val iter_tacss =
- map2 (map o mk_iter_like_tac pre_map_defs map_ids iter_defs) fp_iter_thms ctr_defss;
+ map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
+ ctr_defss;
val rec_tacss =
- map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
+ map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
+ ctr_defss;
in
(map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
goal_iterss iter_tacss,
@@ -592,7 +652,7 @@
end;
val common_notes =
- (if N > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
+ (if nn > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
|> map (fn (thmN, thms, attrs) =>
((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
@@ -608,14 +668,20 @@
lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
- fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _,
- ctr_defss, discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
+ fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
+ discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
let
+ val (vs', _) =
+ lthy
+ |> Variable.variant_fixes (map Binding.name_of fp_bs);
+
+ val vs = map2 (curry Free) vs' fpTs;
+
val (coinduct_thms, coinduct_thm) =
let
val coinduct_thm = fp_induct;
in
- `(conj_dests N) coinduct_thm
+ `(conj_dests nn) coinduct_thm
end;
val (coiter_thmss, corec_thmss) =
@@ -633,7 +699,7 @@
fun build_call fiter_likes maybe_tack (T, U) =
if T = U then
- mk_id T
+ id_const T
else
(case find_index (curry (op =) U) fpTs of
~1 => build_map (build_call fiter_likes maybe_tack) T U
@@ -659,10 +725,10 @@
map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss';
val coiter_tacss =
- map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
+ map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
ctr_defss;
val corec_tacss =
- map3 (map oo mk_coiter_like_tac corec_defs map_ids) fp_rec_thms pre_map_defs
+ map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
ctr_defss;
in
(map2 (map2 (fn goal => fn tac =>
@@ -698,7 +764,7 @@
map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
val common_notes =
- (if N > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
+ (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
|> map (fn (thmN, thms, attrs) =>
((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
@@ -715,11 +781,11 @@
SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
[(thms, [])])) (fp_bs ~~ thmss));
in
- lthy |> Local_Theory.notes notes |> snd
+ lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
- fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11
+ fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10
val lthy' = lthy
|> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 21:23:06 2012 +0200
@@ -10,9 +10,11 @@
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
- val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
- -> tactic
+ val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
+ tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_induct_tac: Proof.context -> int list -> int list list -> int list list -> thm list ->
+ thm -> thm list list -> thm list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> tactic
val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
end;
@@ -24,6 +26,23 @@
open BNF_Util
open BNF_FP_Util
+val meta_mp = @{thm meta_mp};
+val meta_spec = @{thm meta_spec};
+
+fun smash_spurious_fs lthy thm =
+ let
+ val spurious_fs =
+ Term.add_vars (prop_of thm) []
+ |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
+ val cxs =
+ map (fn s as (_, T) =>
+ (certify lthy (Var s), certify lthy (id_abs (domain_type T)))) spurious_fs;
+ in
+ Drule.cterm_instantiate cxs thm
+ end;
+
+val smash_spurious_fs_tac = PRIMITIVE o smash_spurious_fs;
+
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
(rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
@@ -33,8 +52,8 @@
fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
- EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec},
- etac @{thm meta_mp}, atac]) (1 upto n)) 1;
+ EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec,
+ etac meta_mp, atac]) (1 upto n)) 1;
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
(rtac iffI THEN'
@@ -67,6 +86,58 @@
subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
Local_Defs.unfold_tac ctxt @{thms id_def} THEN
- (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1;
+ TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
+
+fun mk_induct_prelude_tac ctxt ctr_defs fld_induct' =
+ Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN smash_spurious_fs_tac ctxt;
+
+fun mk_induct_prepare_prem_tac n m k =
+ EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
+ REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1;
+
+fun mk_induct_prepare_prem_prems_tac 0 = all_tac
+ | mk_induct_prepare_prem_prems_tac r =
+ REPEAT_DETERM_N r ((rotate_tac ~1) 1 THEN dtac meta_mp 1 THEN
+ defer_tac 2 THEN PRIMITIVE (Thm.permute_prems 0 ~1) THEN rotate_tac 1 1) THEN
+ PRIMITIVE Raw_Simplifier.norm_hhf;
+
+val induct_prem_prem_thms =
+ @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
+ Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
+ snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
+
+(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
+ delay them. *)
+val induct_prem_prem_thms_delayed =
+ @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
+
+(* TODO: Get rid of the "blast_tac" *)
+fun mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's =
+ EVERY' (maps (fn i =>
+ [dtac meta_spec, rotate_tac ~1, etac meta_mp,
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs),
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
+ TRY o rtac (mk_UnIN r i), (* FIXME: crude hack, doesn't work in the general case *)
+ atac ORELSE'
+ rtac @{thm singletonI} ORELSE'
+ (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
+ etac @{thm induct_set_step}) THEN'
+ (atac ORELSE' blast_tac ctxt))]) (r downto 1)) 1;
+
+fun mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's =
+ EVERY [mk_induct_prepare_prem_tac n m k,
+ mk_induct_prepare_prem_prems_tac r, atac 1,
+ mk_induct_discharge_prem_prems_tac ctxt r pre_set_defs set_natural's];
+
+fun mk_induct_tac ctxt ns mss rss ctr_defs fld_induct' pre_set_defss set_natural's =
+ let val n = Integer.sum ns in
+ mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
+ EVERY (map4 (fn pre_set_defs =>
+ EVERY ooo map3 (fn m => fn k => fn r =>
+ mk_induct_discharge_prem_tac ctxt n m k r pre_set_defs set_natural's))
+ pre_set_defss mss (unflat mss (1 upto n)) rss)
+ end;
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Fri Sep 14 21:23:06 2012 +0200
@@ -99,6 +99,9 @@
val mk_sumTN: typ list -> typ
val mk_sumTN_balanced: typ list -> typ
+ val id_const: typ -> term
+ val id_abs: typ -> term
+
val Inl_const: typ -> typ -> term
val Inr_const: typ -> typ -> term
@@ -256,6 +259,9 @@
val mk_sumTN = Library.foldr1 mk_sumT;
val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
+fun id_const T = Const (@{const_name id}, T --> T);
+fun id_abs T = Abs (Name.uu, T, Bound 0);
+
fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 14 21:23:06 2012 +0200
@@ -1873,7 +1873,7 @@
||>> mk_Frees "f" coiter_fTs
||>> mk_Frees "g" coiter_fTs
||>> mk_Frees "s" corec_sTs
- ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts);
+ ||>> mk_Frees "P" (map (fn T => T --> mk_predT T) Ts);
fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
val unf_name = Binding.name_of o unf_bind;
@@ -2309,9 +2309,9 @@
||>> mk_Frees "u" uTs
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
- ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
+ ||>> mk_Freess "P" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
||>> mk_Frees "R" JRTs
- ||>> mk_Frees "phi" JphiTs
+ ||>> mk_Frees "P" JphiTs
||>> mk_Frees "B1" B1Ts
||>> mk_Frees "B2" B2Ts
||>> mk_Frees "A" AXTs
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 14 21:23:06 2012 +0200
@@ -206,7 +206,7 @@
fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
EVERY' (map (TRY oo stac) defs @
map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,
- mk_UnN n i] @
+ mk_UnIN n i] @
[etac @{thm UN_I}, atac]) 1;
fun mk_set_incl_hin_tac incls =
@@ -535,7 +535,7 @@
hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
- [rtac (mk_UnN n i), dtac (def RS subst_id),
+ [rtac (mk_UnIN n i), dtac (def RS subst_id),
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
REPEAT_DETERM_N m o (rtac conjI THEN' atac),
CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
@@ -678,7 +678,7 @@
rtac Lev_0, rtac @{thm singletonI},
REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
- rtac Lev_Suc, rtac (mk_UnN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
+ rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
etac mp, etac conjI, atac]) ks])
(Lev_0s ~~ Lev_Sucs)] 1
@@ -753,7 +753,7 @@
then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
CONJ_WRAP' (fn (i'', Lev_0'') =>
EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
- rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i''),
+ rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
rtac @{thm singletonI}])
@@ -770,7 +770,7 @@
CONJ_WRAP' (fn i' => rtac impI THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
- rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnN n i),
+ rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
rtac conjI, atac, dtac (sym RS trans RS sym),
rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
@@ -972,7 +972,7 @@
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
- rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI,
+ rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
@@ -986,7 +986,7 @@
atac, atac, hyp_subst_tac, atac]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
- rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI,
+ rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
@@ -1196,7 +1196,7 @@
REPEAT_DETERM_N n o rtac @{thm Un_upper1},
REPEAT_DETERM_N n o
EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
- EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnN n i), etac @{thm UN_I},
+ EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
(1 upto n) set_hsets set_hset_hsetss)] 1;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 14 21:23:06 2012 +0200
@@ -794,7 +794,7 @@
||>> mk_Frees' "x" init_FTs
||>> mk_Frees "f" init_fTs
||>> mk_Frees "f" init_fTs
- ||>> mk_Frees "phi" (replicate n (mk_predT initT));
+ ||>> mk_Frees "P" (replicate n (mk_predT initT));
val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
(HOLogic.mk_conj (HOLogic.mk_eq (iidx,
@@ -1374,7 +1374,7 @@
||>> mk_Frees "p2" p2Ts
||>> mk_Frees' "y" passiveAs
||>> mk_Frees "R" IRTs
- ||>> mk_Frees "phi" IphiTs;
+ ||>> mk_Frees "P" IphiTs;
val map_FTFT's = map2 (fn Ds =>
mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 14 21:23:06 2012 +0200
@@ -111,7 +111,7 @@
val mk_nthI: int -> int -> thm
val mk_nth_conv: int -> int -> thm
val mk_ordLeq_csum: int -> int -> thm -> thm
- val mk_UnN: int -> int -> thm
+ val mk_UnIN: int -> int -> thm
val ctrans: thm
val o_apply: thm
@@ -542,12 +542,12 @@
end;
local
- fun mk_UnN' 0 = @{thm UnI2}
- | mk_UnN' m = mk_UnN' (m - 1) RS @{thm UnI1};
+ fun mk_UnIN' 0 = @{thm UnI2}
+ | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1};
in
- fun mk_UnN 1 1 = @{thm TrueE[OF TrueI]}
- | mk_UnN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
- | mk_UnN n m = mk_UnN' (n - m)
+ fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]}
+ | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
+ | mk_UnIN n m = mk_UnIN' (n - m)
end;
fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 14 21:23:06 2012 +0200
@@ -157,8 +157,8 @@
val casex = mk_case As B;
val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
- val (((((((xss, yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
- mk_Freess "x" ctr_Tss
+ val ((((((((xss, xss'), yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
+ mk_Freess' "x" ctr_Tss
||>> mk_Freess "y" ctr_Tss
||>> mk_Frees "f" case_Ts
||>> mk_Frees "g" case_Ts
@@ -206,16 +206,19 @@
fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k));
+ fun mk_default T t =
+ let
+ val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []);
+ val Ts = map TFree (Term.add_tfreesT T []);
+ in Term.subst_atomic_types (Ts0 ~~ Ts) t end;
+
fun mk_sel_case_args b proto_sels T =
map2 (fn Ts => fn k =>
(case AList.lookup (op =) proto_sels k of
NONE =>
- let val def_T = Ts ---> T in
- (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
- NONE => mk_undefined def_T
- | SOME t => fold_rev (fn T => Term.lambda (Free (Name.uu, T))) Ts
- (Term.subst_atomic_types [(fastype_of t, T)] t))
- end
+ (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
+ NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
+ | SOME t => mk_default (Ts ---> T) t)
| SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
fun sel_spec b proto_sels =
@@ -355,20 +358,23 @@
([], [], [], [], [], [], [], [])
else
let
- fun make_sel_thm case_thm sel_def = case_thm RS (sel_def RS trans);
+ fun make_sel_thm xs' case_thm sel_def =
+ zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
+ (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
fun has_undefined_rhs thm =
(case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
Const (@{const_name undefined}, _) => true
| _ => false);
- val sel_thmss = map2 (map o make_sel_thm) case_thms sel_defss;
+ val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
val all_sel_thms =
(if all_sels_distinct andalso forall null sel_defaultss then
flat sel_thmss
else
- map_product (fn s => fn c => make_sel_thm c s) sel_defs case_thms)
+ map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
+ (xss' ~~ case_thms))
|> filter_out has_undefined_rhs;
fun mk_unique_disc_def () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 14 21:15:59 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 14 21:23:06 2012 +0200
@@ -37,9 +37,8 @@
val minN = "min"
val messagesN = "messages"
val supported_proversN = "supported_provers"
-val kill_proversN = "kill_provers"
+val killN = "kill"
val running_proversN = "running_provers"
-val kill_learnersN = "kill_learners"
val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
@@ -392,8 +391,8 @@
messages opt_i
else if subcommand = supported_proversN then
supported_provers ctxt
- else if subcommand = kill_proversN then
- kill_provers ()
+ else if subcommand = killN then
+ (kill_provers (); kill_learners ())
else if subcommand = running_proversN then
running_provers ()
else if subcommand = unlearnN then
@@ -413,8 +412,6 @@
("preplay_timeout", ["0"])]))
fact_override (#facts (Proof.goal state))
(subcommand = learn_atpN orelse subcommand = relearn_atpN))
- else if subcommand = kill_learnersN then
- kill_learners ()
else if subcommand = running_learnersN then
running_learners ()
else if subcommand = refresh_tptpN then