--- 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 =
--- 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
--- 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 "\<And>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 "\<And>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 \<and> (R1 ===> R2) s s \<and>
- (rep1 ---> abs2) r = (rep1 ---> abs2) s)"
+ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" for r s
proof -
-
have "(R1 ===> R2) r s \<Longrightarrow> (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 \<Longrightarrow> (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 \<open>unfold Quotient3_def, metis\<close>)
moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s) \<Longrightarrow> (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 \<open>unfold Quotient3_def, metis map_fun_apply\<close>)
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:
--- 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
--- 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)
--- 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
--- 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
--- 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;
--- 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;
--- 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
--- 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
--- 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]))
--- 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 =
--- 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>\<open>The\<close> then
@@ -513,7 +506,7 @@
if card = Inf orelse card = Fin_or_Inf then
spec_rules ()
else
- [(Spec_Rules.Equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
+ [(Spec_Rules.equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
[Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]))]
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
--- 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;
--- 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
--- 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 *)
--- 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 *)
--- 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);
--- 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], [])])];
--- 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;
--- 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
--- 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)
})