# HG changeset patch # User wenzelm # Date 1347650586 -7200 # Node ID ab677b04cbf4f14d200984efc8b79f3a7f9472e4 # Parent c6216518897127270a9072d79c2091655e760c0d# Parent 37c1297aa562c4ff989556113a58bc5ac345d267 merged diff -r 37c1297aa562 -r ab677b04cbf4 NEWS --- 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 diff -r 37c1297aa562 -r ab677b04cbf4 src/Doc/Sledgehammer/document/root.tex --- 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} diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/BNF_FP.thy --- 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: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" by auto -lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" by simp - -lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" by clarsimp +lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" +by simp -(* FIXME: needed? *) -lemma False_imp_eq: "(False \ P) \ Trueprop True" -by presburger - -(* FIXME: needed? *) -lemma all_point_1: "(\z. z = b \ phi z) \ Trueprop (phi b)" -by presburger +lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" +by clarsimp lemma rev_bspec: "a \ A \ \z \ A. P z \ 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: +"\{y. \x \ A. y = {}} = {}" +"\{y. \x \ A. y = {x}} = A" +"\{y. \x \ A. y = {f x}} = {y. \x \ A. y = f x}" +by blast+ + +lemma induct_set_step: "\B \ A; c \ f B\ \ \C. (\a \ A. C = f a) \ c \ 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" diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Examples/Stream.thy --- 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 \ nat stream" where [simp]: "ns n = scalar n ones" lemma "ones \ ones = twos" -by (intro stream_coind[where phi="%x1 x2. \x. x1 = ones \ ones \ x2 = twos"]) +by (intro stream_coind[where P="%x1 x2. \x. x1 = ones \ ones \ x2 = twos"]) auto lemma "n \ twos = ns (2 * n)" -by (intro stream_coind[where phi="%x1 x2. \n. x1 = n \ twos \ x2 = ns (2 * n)"]) +by (intro stream_coind[where P="%x1 x2. \n. x1 = n \ twos \ x2 = ns (2 * n)"]) force+ lemma prod_scalar: "(n * m) \ xs = n \ m \ xs" -by (intro stream_coind[where phi="%x1 x2. \n m xs. x1 = (n * m) \ xs \ x2 = n \ m \ xs"]) +by (intro stream_coind[where P="%x1 x2. \n m xs. x1 = (n * m) \ xs \ x2 = n \ m \ xs"]) force+ lemma scalar_plus: "n \ (xs \ ys) = n \ xs \ n \ ys" -by (intro stream_coind[where phi="%x1 x2. \n xs ys. x1 = n \ (xs \ ys) \ x2 = n \ xs \ n \ ys"]) +by (intro stream_coind[where P="%x1 x2. \n xs ys. x1 = n \ (xs \ ys) \ x2 = n \ xs \ n \ ys"]) (force simp: add_mult_distrib2)+ lemma plus_comm: "xs \ ys = ys \ xs" -by (intro stream_coind[where phi="%x1 x2. \xs ys. x1 = xs \ ys \ x2 = ys \ xs"]) +by (intro stream_coind[where P="%x1 x2. \xs ys. x1 = xs \ ys \ x2 = ys \ xs"]) force+ lemma plus_assoc: "(xs \ ys) \ zs = xs \ ys \ zs" -by (intro stream_coind[where phi="%x1 x2. \xs ys zs. x1 = (xs \ ys) \ zs \ x2 = xs \ ys \ zs"]) +by (intro stream_coind[where P="%x1 x2. \xs ys zs. x1 = (xs \ ys) \ zs \ x2 = xs \ ys \ zs"]) force+ end diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Examples/TreeFsetI.thy --- 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. \x. x1 = tmap (f o g) x \ x2 = tmap f (tmap g x)"]) +by (intro treeFsetI_coind[where P="%x1 x2. \x. x1 = tmap (f o g) x \ x2 = tmap f (tmap g x)"]) force+ end diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- 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 ~~ diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- 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; diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- 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; diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_gfp.ML --- 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 diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- 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; diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_lfp.ML --- 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; diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_util.ML --- 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); diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Codatatype/Tools/bnf_wrap.ML --- 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 () = diff -r 37c1297aa562 -r ab677b04cbf4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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