# HG changeset patch # User Andreas Lochbihler # Date 1403675361 -7200 # Node ID 52dfde98be4adc8bc262d4b0f1d7d4babe2af803 # Parent 7938a6881b26dab73e9315840c51b275cbc8c794# Parent e02fcb7e63c377e6842c529434f784b1a78060a1 merged diff -r e02fcb7e63c3 -r 52dfde98be4a src/Doc/Datatypes/Datatypes.thy --- 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 \ C\<^sub>n]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n, induct t]"}\rm:] ~ \\ @{thm list.induct[no_vars]} \item[@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \ 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 \ t\<^sub>m,"} \\ - \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ D\<^sub>n]"}\rm: + @{text "t."}\hthm{coinduct} @{text "[consumes m, case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + 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 \ t\<^sub>m,"} \\ + \phantom{@{text "t."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ + D\<^sub>n, coinduct pred]"}\rm: +\end{tabular}] ~ \\ +@{thm llist.rel_coinduct[no_vars]} + +\item[\begin{tabular}{@ {}l@ {}} @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m, case_conclusion D\<^sub>1 \ D\<^sub>n]"} \\ @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{strong\_coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m,"} \\ - \phantom{@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ D\<^sub>n]"}\rm: + \phantom{@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{strong\_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ D\<^sub>n]"}\rm: \\ + @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m, case_conclusion D\<^sub>1 \ D\<^sub>n]"} \\ \end{tabular}] ~ \\ Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be used to prove $m$ properties simultaneously. diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/BNF_FP_Base.thy --- 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 \ Q) \ R \ P \ R \ Q" by auto +lemma predicate2D_conj: "P \ Q \ R \ P x y \ R \ 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: "\x y. P x y \ P x y" by blast diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/TPTP/mash_eval.ML --- 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') => diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/TPTP/mash_export.ML --- 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] diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_def.ML --- 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, [])); diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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), diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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 diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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) diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_lfp.ML --- 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 diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- 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'; diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 = diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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} = diff -r e02fcb7e63c3 -r 52dfde98be4a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 =