--- a/src/Doc/Datatypes/Datatypes.thy Tue Jun 24 15:05:58 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Jun 25 07:49:21 2014 +0200
@@ -941,7 +941,7 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct t]"}\rm:] ~ \\
@{thm list.induct[no_vars]}
\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
@@ -1727,8 +1727,9 @@
\begin{description}
\item[\begin{tabular}{@ {}l@ {}}
- @{text "t."}\hthm{coinduct} @{text "[coinduct t, consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
- \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
+ @{text "t."}\hthm{coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+ \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
+ D\<^sub>n, coinduct t]"}\rm:
\end{tabular}] ~ \\
@{thm llist.coinduct[no_vars]}
@@ -1739,9 +1740,17 @@
@{thm llist.strong_coinduct[no_vars]}
\item[\begin{tabular}{@ {}l@ {}}
+ @{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+ \phantom{@{text "t."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
+ D\<^sub>n, coinduct pred]"}\rm:
+\end{tabular}] ~ \\
+@{thm llist.rel_coinduct[no_vars]}
+
+\item[\begin{tabular}{@ {}l@ {}}
@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
- \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
+ \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
+ @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
\end{tabular}] ~ \\
Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
used to prove $m$ properties simultaneously.
--- a/src/HOL/BNF_FP_Base.thy Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy Wed Jun 25 07:49:21 2014 +0200
@@ -16,6 +16,9 @@
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
by auto
+lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
+ by auto
+
lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
by blast
@@ -83,6 +86,9 @@
"setr (Inr x) = {x}"
unfolding sum_set_defs by simp+
+lemma Inl_Inr_False: "(Inl x = Inr y) = False"
+ by simp
+
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jun 25 07:49:21 2014 +0200
@@ -155,6 +155,8 @@
fun heading_sort_key heading =
if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
+val max_dependencies = 100
+
fun problem_of_theory ctxt thy format infer_policy type_enc =
let
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -182,11 +184,10 @@
facts
|> map (fn (_, th) =>
(fact_name_of (Thm.get_name_hint th),
- th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs)
- |> map fact_name_of))
+ th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
+ |> these |> map fact_name_of))
val all_problem_names =
- problem |> maps (map ident_of_problem_line o snd)
- |> distinct (op =)
+ problem |> maps (map ident_of_problem_line o snd) |> distinct (op =)
val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
val infers =
infers |> filter (Symtab.defined all_problem_name_set o fst)
@@ -195,16 +196,13 @@
val ordered_names =
String_Graph.empty
|> fold (String_Graph.new_node o rpair ()) all_problem_names
- |> fold (fn (to, froms) =>
- fold (fn from => maybe_add_edge (from, to)) froms)
- infers
+ |> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers
|> fold (fn (to, from) => maybe_add_edge (from, to))
- (tl all_problem_names ~~ fst (split_last all_problem_names))
+ (tl all_problem_names ~~ fst (split_last all_problem_names))
|> String_Graph.topological_order
val order_tab =
Symtab.empty
- |> fold (Symtab.insert (op =))
- (ordered_names ~~ (1 upto length ordered_names))
+ |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names))
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
in
problem
--- a/src/HOL/TPTP/mash_eval.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jun 25 07:49:21 2014 +0200
@@ -111,7 +111,7 @@
| NONE => error ("No fact called \"" ^ name ^ "\".")
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
- val isar_deps = isar_dependencies_of name_tabs th
+ val isar_deps = these (isar_dependencies_of name_tabs th)
val facts =
facts
|> filter (fn (_, th') =>
--- a/src/HOL/TPTP/mash_export.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jun 25 07:49:21 2014 +0200
@@ -90,6 +90,7 @@
val prover_marker = "$a"
val isar_marker = "$i"
+val missing_marker = "$m"
val omitted_marker = "$o"
val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
val prover_failed_marker = "$x"
@@ -105,9 +106,14 @@
let
val deps =
(case isar_deps_opt of
- SOME deps => deps
- | NONE => isar_dependencies_of name_tabs th)
- in (if null deps then unprovable_marker else isar_marker, deps) end)
+ NONE => isar_dependencies_of name_tabs th
+ | deps => deps)
+ in
+ ((case deps of
+ NONE => missing_marker
+ | SOME [] => unprovable_marker
+ | SOME deps => isar_marker), [])
+ end)
in
(case trim_dependencies deps of
SOME deps => (marker, deps)
@@ -147,7 +153,7 @@
fun is_bad_query ctxt ho_atp step j th isar_deps =
j mod step <> 0 orelse
Thm.legacy_get_kind th = "" orelse
- null isar_deps orelse
+ null (the_list isar_deps) orelse
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
@@ -170,7 +176,7 @@
|> sort_wrt fst
val access_facts = filter_accessible_from th new_facts @ old_facts
val (marker, deps) =
- smart_dependencies_of ctxt params_opt access_facts name_tabs th (SOME isar_deps)
+ smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
fun extra_features_of (((_, stature), th), weight) =
[prop_of th]
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Jun 25 07:49:21 2014 +0200
@@ -83,8 +83,8 @@
val mk_map: int -> typ list -> typ list -> term -> term
val mk_rel: int -> typ list -> typ list -> term -> term
- val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
- val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
+ val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
+ val build_rel: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
'a list
@@ -533,10 +533,12 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun build_map_or_rel mk const of_bnf dest ctxt build_simple =
+fun build_map_or_rel mk const of_bnf dest ctxt simpleTs build_simple =
let
fun build (TU as (T, U)) =
- if T = U then
+ if exists (curry (op =) T) simpleTs then
+ build_simple TU
+ else if T = U andalso not (exists_subtype_in simpleTs T) then
const T
else
(case TU of
@@ -1284,7 +1286,7 @@
(mk_Ball (setA $ x) (Term.absfree (dest_Free a)
(mk_Ball (setB $ y) (Term.absfree (dest_Free b)
(HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
- val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
+ val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
in
@@ -1399,7 +1401,7 @@
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
- val (mk_wit_thms, nontriv_wit_goals) =
+ val (mk_wit_thms, nontriv_wit_goals) =
(case triv_tac_opt of
NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
| SOME tac => (mk_triv_wit_thms tac, []));
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jun 25 07:49:21 2014 +0200
@@ -359,7 +359,7 @@
val cpss = map2 (map o rapp) cs pss;
- fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
+ fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd);
fun build_dtor_corec_arg _ [] [cg] = cg
| build_dtor_corec_arg T [cq] [cg, cg'] =
@@ -574,7 +574,7 @@
if T = U then
x
else
- build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
+ build_map lthy [] (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
(fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
@@ -597,6 +597,129 @@
(rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
end;
+fun coinduct_attrs fpTs ctr_sugars mss =
+ let
+ val nn = length fpTs;
+ val fp_b_names = map base_name_of_typ fpTs;
+ val ctrss = map #ctrs ctr_sugars;
+ val discss = map #discs ctr_sugars;
+ fun mk_coinduct_concls ms discs ctrs =
+ let
+ fun mk_disc_concl disc = [name_of_disc disc];
+ fun mk_ctr_concl 0 _ = []
+ | mk_ctr_concl _ ctor = [name_of_ctr ctor];
+ val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
+ val ctr_concls = map2 mk_ctr_concl ms ctrs;
+ in
+ flat (map2 append disc_concls ctr_concls)
+ end;
+ val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
+ val coinduct_conclss =
+ map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
+
+ val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
+ val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
+
+ val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
+ val coinduct_case_concl_attrs =
+ map2 (fn casex => fn concls =>
+ Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
+ coinduct_cases coinduct_conclss;
+
+ val common_coinduct_attrs =
+ common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
+ val coinduct_attrs =
+ coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
+ in
+ (coinduct_attrs, common_coinduct_attrs)
+ end;
+
+fun postproc_coinduct nn prop prop_conj =
+ Drule.zero_var_indexes
+ #> `(conj_dests nn)
+ #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop))
+ ##> (fn thm => Thm.permute_prems 0 nn
+ (if nn = 1 then thm RS prop
+ else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm));
+
+fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
+ ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
+ let
+ val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
+
+ val (Rs, IRs, fpAs, fpBs, names_lthy) =
+ let
+ val fp_names = map base_name_of_typ fpA_Ts;
+ val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy
+ |> mk_Frees "R" (map2 mk_pred2T As Bs)
+ ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts)
+ ||>> Variable.variant_fixes fp_names
+ ||>> Variable.variant_fixes (map (suffix "'") fp_names);
+ in
+ (Rs, IRs,
+ map2 (curry Free) fpAs_names fpA_Ts,
+ map2 (curry Free) fpBs_names fpB_Ts,
+ names_lthy)
+ end;
+
+ val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) =
+ let
+ val discss = map #discs ctr_sugars;
+ val selsss = map #selss ctr_sugars;
+ fun mk_discss ts Ts = map2 (map o rapp) ts (map (map (mk_disc_or_sel Ts)) discss);
+ fun mk_selsss ts Ts = map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts)))
+ selsss);
+ in
+ ((mk_discss fpAs As, mk_selsss fpAs As),
+ (mk_discss fpBs Bs, mk_selsss fpBs Bs))
+ end;
+
+ fun choose_relator AB = the (find_first
+ (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
+
+ val premises =
+ let
+ fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
+
+ fun build_rel_app selA_t selB_t =
+ (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t
+
+ fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts =
+ (if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @
+ (case (selA_ts, selB_ts) of
+ ([], []) => []
+ | (_ :: _, _ :: _) =>
+ [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t],
+ Library.foldr1 HOLogic.mk_conj (map2 build_rel_app selA_ts selB_ts))]);
+
+ fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss =
+ Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n)
+ (1 upto n) discA_ts selA_tss discB_ts selB_tss))
+ handle List.Empty => @{term True};
+
+ fun mk_prem IR tA tB n discA_ts selA_tss discB_ts selB_tss =
+ fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB),
+ HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss)));
+ in
+ map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
+ end;
+
+ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts))));
+
+ val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
+ (fn {context = ctxt, prems = prems} =>
+ mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
+ (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
+ (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
+ rel_pre_defs abs_inverses)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation;
+ in
+ (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
+ coinduct_attrs fpA_Ts ctr_sugars mss)
+ end;
+
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
@@ -647,7 +770,7 @@
fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
fun build_the_rel rs' T Xs_T =
- build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
+ build_rel lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
|> Term.subst_atomic_types (Xs ~~ fpTs);
fun build_rel_app rs' usel vsel Xs_T =
@@ -688,37 +811,14 @@
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
- val postproc =
- Drule.zero_var_indexes
- #> `(conj_dests nn)
- #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp))
- ##> (fn thm => Thm.permute_prems 0 nn
- (if nn = 1 then thm RS mp
- else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm));
-
val rel_eqs = map rel_eq_of_bnf pre_bnfs;
val rel_monos = map rel_mono_of_bnf pre_bnfs;
val dtor_coinducts =
[dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
in
- map2 (postproc oo prove) dtor_coinducts goals
+ map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals
end;
- fun mk_coinduct_concls ms discs ctrs =
- let
- fun mk_disc_concl disc = [name_of_disc disc];
- fun mk_ctr_concl 0 _ = []
- | mk_ctr_concl _ ctor = [name_of_ctr ctor];
- val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
- val ctr_concls = map2 mk_ctr_concl ms ctrs;
- in
- flat (map2 append disc_concls ctr_concls)
- end;
-
- val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
- val coinduct_conclss =
- map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
-
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
val gcorecs = map (lists_bmoc pgss) corecs;
@@ -741,7 +841,7 @@
let val T = fastype_of cqg in
if exists_subtype_in Cs T then
let val U = mk_U T in
- build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
+ build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg
end
else
@@ -810,22 +910,8 @@
map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
-
- val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
- val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
-
- val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
- val coinduct_case_concl_attrs =
- map2 (fn casex => fn concls =>
- Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
- coinduct_cases coinduct_conclss;
-
- val common_coinduct_attrs =
- common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
- val coinduct_attrs =
- coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
in
- ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)),
+ ((coinduct_thms_pairs, coinduct_attrs fpTs ctr_sugars mss),
(corec_thmss, code_nitpicksimp_attrs),
(disc_corec_thmss, []),
(disc_corec_iff_thmss, simp_attrs),
@@ -946,7 +1032,7 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_rec_thms, ...},
+ xtor_co_rec_thms, rel_xtor_co_induct_thm, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy0
@@ -1227,7 +1313,7 @@
val lhs = selB $ (Term.list_comb (map_term, fs) $ ta);
val lhsT = fastype_of lhs;
val map_rhsT = map_atyps (perhaps (AList.lookup (op =) (Bs ~~ As))) lhsT;
- val map_rhs = build_map lthy
+ val map_rhs = build_map lthy []
(the o (AList.lookup (op =) ((As ~~ Bs) ~~ fs))) (map_rhsT, lhsT);
val rhs = (case map_rhs of
Const (@{const_name id}, _) => selA $ ta
@@ -1481,9 +1567,15 @@
abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
(Proof_Context.export lthy' no_defs_lthy) lthy;
+ val ((rel_coinduct_thms, rel_coinduct_thm),
+ (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
+ derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
+ abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
+
val sel_corec_thmss = map flat sel_corec_thmsss;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
+ val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
val flat_corec_thms = append oo append;
@@ -1494,15 +1586,18 @@
val common_notes =
(if nn > 1 then
- [(coinductN, [coinduct_thm], common_coinduct_attrs),
- (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
- else
- [])
+ [(rel_coinductN, [rel_coinduct_thm], common_rel_coinduct_attrs),
+ (coinductN, [coinduct_thm], common_coinduct_attrs),
+ (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
+ else
+ [])
|> massage_simple_notes fp_common_name;
val notes =
[(coinductN, map single coinduct_thms,
fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
+ (rel_coinductN, map single rel_coinduct_thms,
+ K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
(corecN, corec_thmss, K corec_attrs),
(disc_corecN, disc_corec_thmss, K disc_corec_attrs),
(disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jun 25 07:49:21 2014 +0200
@@ -26,6 +26,9 @@
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
+ val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
+ thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
+ thm list -> thm list -> tactic
val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
@@ -41,6 +44,7 @@
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
+val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
val sumprod_thms_set =
@@ -205,6 +209,27 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
+fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
+ dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses =
+ rtac dtor_rel_coinduct 1 THEN
+ EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
+ fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
+ (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
+ (dtac (rotate_prems (~1) ((cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm
+ arg_cong2}) RS iffD1)) THEN'
+ atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
+ REPEAT_DETERM o etac conjE))) 1 THEN
+ Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
+ @ simp_thms') THEN
+ Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
+ abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps
+ rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject
+ prod.inject}) THEN
+ REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
+ (rtac refl ORELSE' atac))))
+ cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
+ abs_inverses);
+
fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
TRYALL Goal.conjunction_tac THEN
ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jun 25 07:49:21 2014 +0200
@@ -340,11 +340,11 @@
val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
val T = mk_co_algT TY U;
in
- (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of
+ (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of
SOME f => mk_co_product f
(fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
| NONE => mk_map_co_product
- (build_map lthy co_proj1_const
+ (build_map lthy [] co_proj1_const
(dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
(HOLogic.id_const X))
end)
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Jun 25 07:49:21 2014 +0200
@@ -239,7 +239,7 @@
let
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
- val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd);
+ val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
fun massage_mutual_call bound_Ts U T t =
if has_call t then
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jun 25 07:49:21 2014 +0200
@@ -1223,8 +1223,7 @@
val prems = map4 mk_prem phis ctors FTs_setss xFs;
fun mk_concl phi z = phi $ z;
- val concl =
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
+ val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
val goal = Logic.list_implies (prems, concl);
in
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Jun 25 07:49:21 2014 +0200
@@ -68,7 +68,7 @@
fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
val typof = curry fastype_of1 bound_Ts;
- val build_map_fst = build_map ctxt (fst_const o fst);
+ val build_map_fst = build_map ctxt [] (fst_const o fst);
val yT = typof y;
val yU = typof y';
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Jun 25 07:49:21 2014 +0200
@@ -275,7 +275,7 @@
fun mk_rec_arg_arg (x as Free (_, T)) =
let val U = B_ify T in
- if T = U then x else build_map lthy2 (the o AList.lookup (op =) ABgs) (T, U) $ x
+ if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x
end;
fun mk_rec_o_map_arg rec_arg_T h =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jun 25 07:49:21 2014 +0200
@@ -83,7 +83,7 @@
val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
(string * real) list
val trim_dependencies : string list -> string list option
- val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list
+ val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
string Symtab.table * string Symtab.table -> thm -> bool * string list
val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
@@ -497,7 +497,7 @@
fun add_th weight t =
let
val im = Array.sub (sfreq, t)
- fun fold_fn s sf = Inttab.update (s, weight + the_default 0 (Inttab.lookup im s)) sf
+ fun fold_fn s sf = Inttab.map_default (s, 0) (Integer.add weight) sf
in
Array.update (tfreq, t, weight + Array.sub (tfreq, t));
Array.update (sfreq, t, fold fold_fn feats im)
@@ -1153,21 +1153,22 @@
if length deps > max_dependencies then NONE else SOME deps
fun isar_dependencies_of name_tabs th =
- let val deps = thms_in_proof (SOME name_tabs) th in
+ thms_in_proof max_dependencies (SOME name_tabs) th
+ |> Option.map (fn deps =>
if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
is_size_def deps th then
[]
else
- deps
- end
+ deps)
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
name_tabs th =
(case isar_dependencies_of name_tabs th of
- [] => (false, [])
- | isar_deps =>
+ SOME [] => (false, [])
+ | isar_deps0 =>
let
+ val isar_deps = these isar_deps0
val thy = Proof_Context.theory_of ctxt
val goal = goal_of_thm thy th
val name = nickname_of_thm th
@@ -1533,7 +1534,6 @@
|> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
else
isar_dependencies_of name_tabs th
- |> trim_dependencies
fun do_commit [] [] [] state = state
| do_commit learns relearns flops {access_G, num_known_facts, dirty} =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 24 15:05:58 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jun 25 07:49:21 2014 +0200
@@ -19,7 +19,8 @@
val parse_time : string -> string -> Time.time
val subgoal_count : Proof.state -> int
val reserved_isar_keyword_table : unit -> unit Symtab.table
- val thms_in_proof : (string Symtab.table * string Symtab.table) option -> thm -> string list
+ val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
+ string list option
val thms_of_name : Proof.context -> string -> thm list
val one_day : Time.time
val one_year : Time.time
@@ -84,11 +85,13 @@
fun reserved_isar_keyword_table () =
Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
+exception TOO_MANY of unit
+
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
be missing over there; or maybe the two code portions are not doing the same? *)
-fun fold_body_thm outer_name (map_plain_name, map_inclass_name) =
+fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
let
- fun app_thm map_name (_, (name, _, body)) accum =
+ fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) =
let
val (anonymous, enter_class) =
(* The "name = outer_name" case caters for the uncommon case where the proved theorem
@@ -98,18 +101,25 @@
else (false, false)
in
if anonymous then
- accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body)
+ app_body (if enter_class then map_inclass_name else map_name) (Future.join body) accum
else
- accum |> union (op =) (the_list (map_name name))
+ (case map_name name of
+ SOME name' =>
+ if member (op =) names name' then accum
+ else if num_thms = max_thms then raise TOO_MANY ()
+ else (num_thms + 1, name' :: names)
+ | NONE => accum)
end
and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
in
- app_body map_plain_name
+ snd (app_body map_plain_name body (0, []))
end
-fun thms_in_proof name_tabs th =
+fun thms_in_proof max_thms name_tabs th =
let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
- fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) []
+ SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names
+ (Proofterm.strip_thm (Thm.proof_body_of th)))
+ handle TOO_MANY () => NONE
end
fun thms_of_name ctxt name =