# HG changeset patch # User wenzelm # Date 1553635110 -3600 # Node ID 3fd083253a1cc5bcb560a1d79fc717dcc8b6da9e # Parent e7648f104d6bc6feda259ae0b165fd15b59a130f# Parent bd3c10813cc452b51316590eea3101f8de8277c4 merged diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Library/old_recdef.ML Tue Mar 26 22:18:30 2019 +0100 @@ -2842,7 +2842,7 @@ |> Global_Theory.add_thmss (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])] - ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules) + ||> Spec_Rules.add_global Spec_Rules.equational_recdef ([lhs], flat rules) ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules)); val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs}; val thy3 = diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Mar 26 22:18:30 2019 +0100 @@ -53,8 +53,7 @@ let fun tac [] st = all_tac st | tac (type_enc :: type_encs) st = - st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *) - |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1) + st |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1) THEN Metis_Tactic.metis_tac [type_enc] ATP_Problem_Generate.combsN ctxt ths 1 THEN COND (has_fewer_prems 2) all_tac no_tac diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Quotient.thy Tue Mar 26 22:18:30 2019 +0100 @@ -141,21 +141,17 @@ and q2: "Quotient3 R2 abs2 rep2" shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" proof - - have "\a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + have "(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" for a using q1 q2 by (simp add: Quotient3_def fun_eq_iff) moreover - have "\a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + have "(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" for a by (rule rel_funI) (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], simp (no_asm) add: Quotient3_def, simp) - moreover - { - fix r s have "(R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ - (rep1 ---> abs2) r = (rep1 ---> abs2) s)" + (rep1 ---> abs2) r = (rep1 ---> abs2) s)" for r s proof - - have "(R1 ===> R2) r s \ (R1 ===> R2) r r" unfolding rel_fun_def using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] by (metis (full_types) part_equivp_def) @@ -163,16 +159,15 @@ using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] by (metis (full_types) part_equivp_def) moreover have "(R1 ===> R2) r s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s" - apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis + by (auto simp add: rel_fun_def fun_eq_iff) + (use q1 q2 in \unfold Quotient3_def, metis\) moreover have "((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s) \ (R1 ===> R2) r s" - apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def - by (metis map_fun_apply) - + by (auto simp add: rel_fun_def fun_eq_iff) + (use q1 q2 in \unfold Quotient3_def, metis map_fun_apply\) ultimately show ?thesis by blast - qed - } - ultimately show ?thesis by (intro Quotient3I) (assumption+) + qed + ultimately show ?thesis by (intro Quotient3I) (assumption+) qed lemma lambda_prs: diff -r e7648f104d6b -r 3fd083253a1c src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Mar 26 22:18:30 2019 +0100 @@ -931,7 +931,6 @@ fun biggest_hyp_first_tac i = fn st => let val results = TERMFUN biggest_hypothesis (SOME i) st -val _ = tracing ("result=" ^ @{make_string} results) in if null results then no_tac st else diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 26 22:18:30 2019 +0100 @@ -1414,10 +1414,10 @@ |> massage_simple_notes fp_b_name; val (noted, lthy') = lthy - |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) + |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) map_thms) |> fp = Least_FP - ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms) - |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms) + ? Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) rel_code_thms) + |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) set0_thms) |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms)) |> Local_Theory.notes (anonymous_notes @ notes); @@ -2689,7 +2689,7 @@ |> massage_multi_notes fp_b_names fpTs; in lthy - |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) + |> Spec_Rules.add Spec_Rules.equational (recs, flat rec_thmss) |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss)) |> Local_Theory.notes (common_notes @ notes) (* for "datatype_realizer.ML": *) @@ -2869,7 +2869,7 @@ |> massage_multi_notes fp_b_names fpTs; in lthy - |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs) + |> fold (curry (Spec_Rules.add Spec_Rules.equational) corecs) [flat corec_sel_thmss, flat corec_thmss] |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms) |> Local_Theory.notes (common_notes @ notes) diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Mar 26 22:18:30 2019 +0100 @@ -2154,10 +2154,10 @@ in lthy (* TODO: - |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat sel_thmss) - |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat ctr_thmss) + |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss) + |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss) *) - |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], [code_thm]) + |> Spec_Rules.add Spec_Rules.equational ([fun_t0], [code_thm]) |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)] |> Local_Theory.notes (anonymous_notes @ notes) |> snd diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 26 22:18:30 2019 +0100 @@ -1532,9 +1532,9 @@ val fun_ts0 = map fst def_infos; in lthy - |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat sel_thmss) - |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat ctr_thmss) - |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat code_thmss) + |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat sel_thmss) + |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat ctr_thmss) + |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat code_thmss) |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss)) |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Mar 26 22:18:30 2019 +0100 @@ -580,7 +580,7 @@ ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs), [(thms, [])])); in - (((fun_names, qualifys, defs), + (((fun_names, qualifys, arg_Ts, defs), fn lthy => fn defs => let val def_thms = map (snd o snd) defs; @@ -605,24 +605,29 @@ val nonexhaustives = replicate actual_nn nonexhaustive; val transfers = replicate actual_nn transfer; - val (((names, qualifys, defs), prove), lthy') = + val (((names, qualifys, arg_Ts, defs), prove), lthy') = prepare_primrec plugins nonexhaustives transfers fixes ts lthy; in lthy' |> fold_map Local_Theory.define defs |> tap (uncurry (print_def_consts int)) |-> (fn defs => fn lthy => - let val ((jss, simpss), lthy) = prove lthy defs in - (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) - end) + let + val ((jss, simpss), lthy) = prove lthy defs; + val res = + {prefix = (names, qualifys), + types = map (#1 o dest_Type) arg_Ts, + result = (map fst defs, map (snd o snd) defs, (jss, simpss))}; + in (res, lthy) end) end; fun primrec_simple int fixes ts lthy = primrec_simple0 int Plugin_Name.default_filter false false fixes ts lthy + |>> (fn {prefix, result, ...} => (prefix, result)) handle OLD_PRIMREC () => Old_Primrec.primrec_simple int fixes ts lthy - |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single - |>> apfst (map_split (rpair I)); + |>> (fn {prefix, result = (ts, thms), ...} => + (map_split (rpair I) [prefix], (ts, [], ([], [thms])))) fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy = let @@ -648,8 +653,8 @@ in lthy |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs) - |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) => - Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) + |-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} => + Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, flat simpss) #> Local_Theory.notes (mk_notes jss names qualifys simpss) #-> (fn notes => plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes)) @@ -657,7 +662,7 @@ end handle OLD_PRIMREC () => old_primrec int raw_fixes raw_specs lthy - |>> (fn (ts, thms) => (ts, [], [thms])); + |>> (fn {result = (ts, thms), ...} => (ts, [], [thms])); val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs; val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs; diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 26 22:18:30 2019 +0100 @@ -373,8 +373,8 @@ val (noted, lthy3) = lthy2 - |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) - |> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps) + |> Spec_Rules.add Spec_Rules.equational (size_consts, size_simps) + |> Spec_Rules.add Spec_Rules.equational (overloaded_size_consts, overloaded_size_simps) |> Code.declare_default_eqns (map (rpair true) (flat size_thmss)) (*Ideally, this would be issued only if the "code" plugin is enabled.*) |> Local_Theory.notes notes; diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Mar 26 22:18:30 2019 +0100 @@ -1111,10 +1111,10 @@ ((qualify true (Binding.name thmN), attrs), [(thms, [])])); val (noted, lthy') = lthy - |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms) - |> fold (Spec_Rules.add Spec_Rules.Equational) + |> Spec_Rules.add Spec_Rules.equational ([casex], case_thms) + |> fold (Spec_Rules.add Spec_Rules.equational) (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms)) - |> fold (Spec_Rules.add Spec_Rules.Equational) + |> fold (Spec_Rules.add Spec_Rules.equational) (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss)) |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Case_Translation.register diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Function/function.ML Tue Mar 26 22:18:30 2019 +0100 @@ -210,7 +210,7 @@ lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_function_data (transform_function_data phi info')) - |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) + |> Spec_Rules.add Spec_Rules.equational_recdef (fs, tsimps)) end) end in diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Function/partial_function.ML Tue Mar 26 22:18:30 2019 +0100 @@ -302,7 +302,7 @@ val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule]) in lthy'' - |> Spec_Rules.add Spec_Rules.Equational ([f], [rec_rule']) + |> Spec_Rules.add Spec_Rules.equational_recdef ([f], [rec_rule']) |> note_qualified ("simps", [rec_rule']) |> note_qualified ("mono", [mono_thm]) |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm])) diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 26 22:18:30 2019 +0100 @@ -1354,7 +1354,7 @@ fun all_nondefs_of ctxt subst = ctxt |> Spec_Rules.get - |> filter (curry (op =) Spec_Rules.Unknown o fst) + |> filter (Spec_Rules.is_unknown o fst) |> maps (snd o snd) |> filter_out (is_built_in_theory o Thm.theory_id) |> map (subst_atomic subst o Thm.prop_of) @@ -1948,8 +1948,8 @@ def_table_for (maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of) o snd o snd) - (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse - cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst + (filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o #1) + (Spec_Rules.get ctxt))) subst end fun ground_theorem_table thy = diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Nunchaku/nunchaku_collect.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Mar 26 22:18:30 2019 +0100 @@ -471,13 +471,6 @@ card_of [] end; -fun int_of_classif Spec_Rules.Equational = 1 - | int_of_classif Spec_Rules.Inductive = 2 - | int_of_classif Spec_Rules.Co_Inductive = 3 - | int_of_classif Spec_Rules.Unknown = 4; - -val classif_ord = int_ord o apply2 int_of_classif; - fun spec_rules_of ctxt (x as (s, T)) = let val thy = Proof_Context.theory_of ctxt; @@ -503,7 +496,7 @@ fun spec_rules () = Spec_Rules.retrieve ctxt (Const x) - |> sort (classif_ord o apply2 fst); + |> sort (Spec_Rules.rough_classification_ord o apply2 fst); val specs = if s = \<^const_name>\The\ then @@ -513,7 +506,7 @@ if card = Inf orelse card = Fin_or_Inf then spec_rules () else - [(Spec_Rules.Equational, ([Logic.varify_global \<^term>\finite\], + [(Spec_Rules.equational, ([Logic.varify_global \<^term>\finite\], [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\finite A = True\)]))] end else @@ -544,7 +537,7 @@ val orphan_axioms_of = Spec_Rules.get - #> filter (curry (op =) Spec_Rules.Unknown o fst) + #> filter (Spec_Rules.is_unknown o fst) #> map snd #> filter (null o fst) #> maps snd @@ -959,7 +952,7 @@ val (props', cmds) = if null props then ([], map IVal consts) - else if classif = Spec_Rules.Equational then + else if Spec_Rules.is_equational classif then (case partition_props consts props of SOME propss => (props, @@ -968,15 +961,15 @@ pat_complete = is_apparently_pat_complete ctxt props}) consts propss)]) | NONE => def_or_spec ()) - else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] - classif then + else if (Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) classif + then if is_inductive_set_intro (hd props) then def_or_spec () else (case partition_props consts props of SOME propss => (props, - [ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP + [ICoPred (if Spec_Rules.is_inductive classif then BNF_Util.Least_FP else BNF_Util.Greatest_FP, length consts = 1 andalso is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Tue Mar 26 22:18:30 2019 +0100 @@ -9,16 +9,18 @@ signature OLD_PRIMREC = sig val primrec: bool -> (binding * typ option * mixfix) list -> - Specification.multi_specs -> local_theory -> (term list * thm list) * local_theory + Specification.multi_specs -> local_theory -> + {types: string list, result: term list * thm list} * local_theory val primrec_cmd: bool -> (binding * string option * mixfix) list -> - Specification.multi_specs_cmd -> local_theory -> (term list * thm list) * local_theory + Specification.multi_specs_cmd -> local_theory -> + {types: string list, result: term list * thm list} * local_theory val primrec_global: bool -> (binding * typ option * mixfix) list -> Specification.multi_specs -> theory -> (term list * thm list) * theory val primrec_overloaded: bool -> (string * (string * typ) * bool) list -> (binding * typ option * mixfix) list -> Specification.multi_specs -> theory -> (term list * thm list) * theory - val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> - local_theory -> (string * (term list * thm list)) * local_theory + val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> local_theory -> + {prefix: string, types: string list, result: term list * thm list} * local_theory end; structure Old_Primrec : OLD_PRIMREC = @@ -195,13 +197,13 @@ fun make_def ctxt fixes fs (fname, ls, rec_name) = let - val SOME (var, varT) = get_first (fn ((b, T), mx) => + val SOME (var, varT) = get_first (fn ((b, T), mx: mixfix) => if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes; val def_name = Thm.def_name (Long_Name.base_name fname); val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT]) (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1)))) val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs); - in (var, ((Binding.concealed (Binding.name def_name), []), rhs)) end; + in (var, ((Binding.concealed (Binding.name def_name), []): Attrib.binding, rhs)) end; (* find datatypes which contain all datatypes in tnames' *) @@ -250,7 +252,7 @@ (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac ctxt' [refl] 1])) eqs end; - in ((prefix, (fs, defs)), prove) end + in ((prefix, tnames, (fs, defs)), prove) end handle PrimrecError (msg, some_eqn) => error ("Primrec definition error:\n" ^ msg ^ (case some_eqn of @@ -262,12 +264,13 @@ fun primrec_simple int fixes ts lthy = let - val ((prefix, (_, defs)), prove) = distill lthy fixes ts; + val ((prefix, tnames, (_, defs)), prove) = distill lthy fixes ts; in lthy |> fold_map Local_Theory.define defs |> tap (uncurry (BNF_FP_Rec_Sugar_Util.print_def_consts int)) - |-> (fn defs => `(fn lthy => (prefix, (map fst defs, prove lthy defs)))) + |-> (fn defs => + `(fn lthy => {prefix = prefix, types = tnames, result = (map fst defs, prove lthy defs)})) end; local @@ -282,13 +285,13 @@ in lthy |> primrec_simple int fixes (map snd spec) - |-> (fn (prefix, (ts, simps)) => - Spec_Rules.add Spec_Rules.Equational (ts, simps) + |-> (fn {prefix, types, result = (ts, simps)} => + Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, simps) #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps) #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps') - #-> (fn (_, simps'') => - Code.declare_default_eqns (map (rpair true) simps'') - #> pair (ts, simps'')))) + #-> (fn (_, simps'') => + Code.declare_default_eqns (map (rpair true) simps'') + #> pair {types = types, result = (ts, simps'')}))) end; in @@ -301,14 +304,14 @@ fun primrec_global int fixes specs thy = let val lthy = Named_Target.theory_init thy; - val ((ts, simps), lthy') = primrec int fixes specs lthy; + val ({result = (ts, simps), ...}, lthy') = primrec int fixes specs lthy; val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; fun primrec_overloaded int ops fixes specs thy = let val lthy = Overloading.overloading ops thy; - val ((ts, simps), lthy') = primrec int fixes specs lthy; + val ({result = (ts, simps), ...}, lthy') = primrec int fixes specs lthy; val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Mar 26 22:18:30 2019 +0100 @@ -317,11 +317,11 @@ *) val specs = Spec_Rules.get ctxt val (rec_defs, nonrec_defs) = specs - |> filter (curry (op =) Spec_Rules.Equational o fst) + |> filter (Spec_Rules.is_equational o fst) |> maps (snd o snd) |> List.partition (is_rec_def o Thm.prop_of) val spec_intros = specs - |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst) + |> filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o fst) |> maps (snd o snd) in Termtab.empty diff -r e7648f104d6b -r 3fd083253a1c src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/HOL/Tools/record.ML Tue Mar 26 22:18:30 2019 +0100 @@ -1814,7 +1814,7 @@ fun add_spec_rule rule = let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in - Spec_Rules.add_global Spec_Rules.Equational ([head], [rule]) + Spec_Rules.add_global Spec_Rules.equational ([head], [rule]) end; (* definition *) diff -r e7648f104d6b -r 3fd083253a1c src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/Pure/Isar/object_logic.ML Tue Mar 26 22:18:30 2019 +0100 @@ -17,6 +17,7 @@ val ensure_propT: Proof.context -> term -> term val dest_judgment: Proof.context -> cterm -> cterm val judgment_conv: Proof.context -> conv -> conv + val is_propositional: Proof.context -> typ -> bool val elim_concl: Proof.context -> thm -> term option val declare_atomize: attribute val declare_rulify: attribute @@ -146,6 +147,11 @@ then Conv.arg_conv cv ct else raise CTERM ("judgment_conv", [ct]); +fun is_propositional ctxt T = + T = propT orelse + let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T)) + in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end; + (* elimination rules *) diff -r e7648f104d6b -r 3fd083253a1c src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/Pure/Isar/spec_rules.ML Tue Mar 26 22:18:30 2019 +0100 @@ -8,7 +8,17 @@ signature SPEC_RULES = sig - datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive + datatype recursion = Primrec of string list | Recdef | Unknown_Recursion + val recursion_ord: recursion * recursion -> order + datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown + val rough_classification_ord: rough_classification * rough_classification -> order + val equational_primrec: string list -> rough_classification + val equational_recdef: rough_classification + val equational: rough_classification + val is_equational: rough_classification -> bool + val is_inductive: rough_classification -> bool + val is_co_inductive: rough_classification -> bool + val is_unknown: rough_classification -> bool type spec = rough_classification * (term list * thm list) val get: Proof.context -> spec list val get_global: theory -> spec list @@ -21,9 +31,35 @@ structure Spec_Rules: SPEC_RULES = struct +(* recursion *) + +datatype recursion = Primrec of string list | Recdef | Unknown_Recursion; + +fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2) + | recursion_ord rs = + int_ord (apply2 (fn Primrec _ => 0 | Recdef => 1 | Unknown_Recursion => 2) rs); + + +(* rough classification *) + +datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown; + +fun rough_classification_ord (Equational r1, Equational r2) = recursion_ord (r1, r2) + | rough_classification_ord cs = + int_ord (apply2 (fn Equational _ => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3) cs); + +val equational_primrec = Equational o Primrec; +val equational_recdef = Equational Recdef; +val equational = Equational Unknown_Recursion; + +val is_equational = fn Equational _ => true | _ => false; +val is_inductive = fn Inductive => true | _ => false; +val is_co_inductive = fn Co_Inductive => true | _ => false; +val is_unknown = fn Unknown => true | _ => false; + + (* rules *) -datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive; type spec = rough_classification * (term list * thm list); structure Rules = Generic_Data @@ -31,8 +67,8 @@ type T = spec Item_Net.T; val empty : T = Item_Net.init - (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) => - class1 = class2 andalso + (fn ((c1, (ts1, ths1)), (c2, (ts2, ths2))) => + is_equal (rough_classification_ord (c1, c2)) andalso eq_list (op aconv) (ts1, ts2) andalso eq_list Thm.eq_thm_prop (ths1, ths2)) (#1 o #2); diff -r e7648f104d6b -r 3fd083253a1c src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/Pure/Isar/specification.ML Tue Mar 26 22:18:30 2019 +0100 @@ -263,7 +263,7 @@ |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs)); val th = prove lthy2 raw_th; - val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]); + val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.equational ([lhs], [th]); val ([(def_name, [th'])], lthy4) = lthy3 |> Local_Theory.notes [((name, atts), [([th], [])])]; diff -r e7648f104d6b -r 3fd083253a1c src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/Pure/Proof/extraction.ML Tue Mar 26 22:18:30 2019 +0100 @@ -801,7 +801,7 @@ [((Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft)), [])] |-> (fn [def_thm] => - Spec_Rules.add_global Spec_Rules.Equational ([head], [def_thm]) + Spec_Rules.add_global Spec_Rules.equational ([head], [def_thm]) #> Code.declare_default_eqns_global [(def_thm, true)]) end; diff -r e7648f104d6b -r 3fd083253a1c src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Tue Mar 26 17:01:55 2019 +0000 +++ b/src/Pure/Thy/export_theory.ML Tue Mar 26 22:18:30 2019 +0100 @@ -101,6 +101,14 @@ (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I); +(* spec rules *) + +fun primrec_types ctxt const = + Spec_Rules.retrieve ctxt (Const const) + |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME types | _ => NONE) + |> the_default []; + + (* locales content *) fun locale_content thy loc = @@ -230,16 +238,21 @@ (* consts *) val encode_const = - let open XML.Encode Term_XML.Encode - in pair encode_syntax (pair (list string) (pair typ (option term))) end; + let open XML.Encode Term_XML.Encode in + pair encode_syntax + (pair (list string) (pair typ (pair (option term) (pair bool (list string))))) + end; fun export_const c (T, abbrev) = let val syntax = get_syntax_const thy_ctxt c; - val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts; + val U = Logic.unvarifyT_global T; + val U0 = Type.strip_sorts U; + val primrec_types = primrec_types thy_ctxt (c, U); val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts); - val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T')); - in encode_const (syntax, (args, (T', abbrev'))) end; + val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0)); + val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); + in encode_const (syntax, (args, (U0, (abbrev', (propositional, primrec_types))))) end; val _ = export_entities "consts" (SOME oo export_const) Sign.const_space diff -r e7648f104d6b -r 3fd083253a1c src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Tue Mar 26 17:01:55 2019 +0000 +++ b/src/Pure/Thy/export_theory.scala Tue Mar 26 22:18:30 2019 +0100 @@ -251,27 +251,33 @@ syntax: Syntax, typargs: List[String], typ: Term.Typ, - abbrev: Option[Term.Term]) + abbrev: Option[Term.Term], + propositional: Boolean, + primrec_types: List[String]) { def cache(cache: Term.Cache): Const = Const(entity.cache(cache), syntax, typargs.map(cache.string(_)), cache.typ(typ), - abbrev.map(cache.term(_))) + abbrev.map(cache.term(_)), + propositional, + primrec_types.map(cache.string(_))) } def read_consts(provider: Export.Provider): List[Const] = provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.CONST, tree) - val (syntax, (args, (typ, abbrev))) = + val (syntax, (args, (typ, (abbrev, (propositional, primrec_types))))) = { import XML.Decode._ - pair(decode_syntax, pair(list(string), - pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body) + pair(decode_syntax, + pair(list(string), + pair(Term_XML.Decode.typ, + pair(option(Term_XML.Decode.term), pair(bool, list(string))))))(body) } - Const(entity, syntax, args, typ, abbrev) + Const(entity, syntax, args, typ, abbrev, propositional, primrec_types) })