--- a/NEWS Sat Nov 14 18:37:49 2015 +0100
+++ b/NEWS Sun Nov 15 12:39:51 2015 +0100
@@ -529,10 +529,14 @@
* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
command. Minor INCOMPATIBILITY, use 'function' instead.
+* Inductive definitions ('inductive', 'coinductive', etc.) expose
+low-level facts of the internal construction only if the option
+"inductive_defs" is enabled. This refers to the internal predicate
+definition and its monotonicity result. Rare INCOMPATIBILITY.
+
* Recursive function definitions ('fun', 'function', 'partial_function')
-no longer expose the low-level "_def" facts of the internal
-construction. INCOMPATIBILITY, enable option "function_defs" in the
-context for rare situations where these facts are really needed.
+expose low-level facts of the internal construction only if the option
+"function_defs" is enabled. Rare INCOMPATIBILITY.
* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
--- a/src/HOL/BNF_Def.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/BNF_Def.thy Sun Nov 15 12:39:51 2015 +0100
@@ -24,8 +24,6 @@
"R1 a c \<Longrightarrow> rel_sum R1 R2 (Inl a) (Inl c)"
| "R2 b d \<Longrightarrow> rel_sum R1 R2 (Inr b) (Inr d)"
-hide_fact rel_sum_def
-
definition
rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
where
--- a/src/HOL/Basic_BNFs.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Basic_BNFs.thy Sun Nov 15 12:39:51 2015 +0100
@@ -102,8 +102,6 @@
where
"\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
-hide_fact rel_prod_def
-
lemma rel_prod_apply [code, simp]:
"rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
by (auto intro: rel_prod.intros elim: rel_prod.cases)
--- a/src/HOL/Finite_Set.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Finite_Set.thy Sun Nov 15 12:39:51 2015 +0100
@@ -11,11 +11,17 @@
subsection \<open>Predicate for finite sets\<close>
+context
+ notes [[inductive_defs]]
+begin
+
inductive finite :: "'a set \<Rightarrow> bool"
where
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
+end
+
simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
declare [[simproc del: finite_Collect]]
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Sun Nov 15 12:39:51 2015 +0100
@@ -64,6 +64,10 @@
abbreviation HLD_nxt (infixr "\<cdot>" 65) where
"s \<cdot> P \<equiv> HLD s aand nxt P"
+context
+ notes [[inductive_defs]]
+begin
+
inductive ev for \<phi> where
base: "\<phi> xs \<Longrightarrow> ev \<phi> xs"
|
@@ -78,6 +82,8 @@
|
step: "\<lbrakk>\<phi> xs; (\<phi> until \<psi>) (stl xs)\<rbrakk> \<Longrightarrow> (\<phi> until \<psi>) xs"
+end
+
lemma holds_mono:
assumes holds: "holds P xs" and 0: "\<And> x. P x \<Longrightarrow> Q x"
shows "holds Q xs"
@@ -587,12 +593,18 @@
text \<open>Strong until\<close>
+context
+ notes [[inductive_defs]]
+begin
+
inductive suntil (infix "suntil" 60) for \<phi> \<psi> where
base: "\<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
| step: "\<phi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
inductive_simps suntil_Stream: "(\<phi> suntil \<psi>) (x ## s)"
+end
+
lemma suntil_induct_strong[consumes 1, case_names base step]:
"(\<phi> suntil \<psi>) x \<Longrightarrow>
(\<And>\<omega>. \<psi> \<omega> \<Longrightarrow> P \<omega>) \<Longrightarrow>
--- a/src/HOL/Library/Stream.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Library/Stream.thy Sun Nov 15 12:39:51 2015 +0100
@@ -68,12 +68,18 @@
subsection \<open>set of streams with elements in some fixed set\<close>
+context
+ notes [[inductive_defs]]
+begin
+
coinductive_set
streams :: "'a set \<Rightarrow> 'a stream set"
for A :: "'a set"
where
Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
+end
+
lemma in_streams: "stl s \<in> streams S \<Longrightarrow> shd s \<in> S \<Longrightarrow> s \<in> streams S"
by (cases s) auto
--- a/src/HOL/List.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/List.thy Sun Nov 15 12:39:51 2015 +0100
@@ -5573,7 +5573,12 @@
Author: Andreas Lochbihler
\<close>
-context ord begin
+context ord
+begin
+
+context
+ notes [[inductive_defs]]
+begin
inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -5582,6 +5587,8 @@
| Cons_eq:
"\<lbrakk> \<not> x < y; \<not> y < x; lexordp xs ys \<rbrakk> \<Longrightarrow> lexordp (x # xs) (y # ys)"
+end
+
lemma lexordp_simps [simp]:
"lexordp [] ys = (ys \<noteq> [])"
"lexordp xs [] = False"
@@ -5636,7 +5643,8 @@
lemma lexord_code [code, code_unfold]: "lexordp = ord.lexordp less"
unfolding lexordp_def ord.lexordp_def ..
-context order begin
+context order
+begin
lemma lexordp_antisym:
assumes "lexordp xs ys" "lexordp ys xs"
--- a/src/HOL/Nitpick.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Nitpick.thy Sun Nov 15 12:39:51 2015 +0100
@@ -238,7 +238,7 @@
hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
- card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
+ card'_def setsum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
--- a/src/HOL/Probability/Bochner_Integration.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Sun Nov 15 12:39:51 2015 +0100
@@ -886,9 +886,15 @@
intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure])
qed
+context
+ notes [[inductive_defs]]
+begin
+
inductive integrable for M f where
"has_bochner_integral M f x \<Longrightarrow> integrable M f"
+end
+
definition lebesgue_integral ("integral\<^sup>L") where
"integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
--- a/src/HOL/Tools/inductive.ML Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Nov 15 12:39:51 2015 +0100
@@ -71,6 +71,7 @@
signature INDUCTIVE =
sig
include BASIC_INDUCTIVE
+ val inductive_defs: bool Config.T
val select_disj_tac: Proof.context -> int -> int -> int -> tactic
type add_ind_def =
inductive_flags ->
@@ -121,6 +122,8 @@
(** misc utilities **)
+val inductive_defs = Attrib.setup_config_bool @{binding inductive_defs} (K false);
+
fun message quiet_mode s = if quiet_mode then () else writeln s;
fun clean_message ctxt quiet_mode s =
@@ -836,17 +839,21 @@
(* add definition of recursive predicates to theory *)
- val rec_name =
+ val rec_binding =
if Binding.is_empty alt_name then
Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
else alt_name;
+ val rec_name = Binding.name_of rec_binding;
- val is_auxiliary = length cs >= 2;
+ val inductive_defs = Config.get lthy inductive_defs;
+ val is_auxiliary = length cs >= 2;
+
val ((rec_const, (_, fp_def)), lthy') = lthy
|> is_auxiliary ? Proof_Context.concealed
|> Local_Theory.define
- ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
- ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
+ ((rec_binding, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
+ ((if inductive_defs then Thm.def_binding rec_binding else Binding.empty,
+ @{attributes [nitpick_unfold]}),
fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
||> Proof_Context.restore_naming lthy;
@@ -854,18 +861,18 @@
Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
(Thm.cterm_of lthy' (list_comb (rec_const, params)));
val specs =
- if length cs < 2 then []
- else
+ if is_auxiliary then
map_index (fn (i, (name_mx, c)) =>
let
val Ts = arg_types_of (length params) c;
val xs =
map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
in
- (name_mx, (apfst Binding.concealed Attrib.empty_binding, fold_rev lambda (params @ xs)
+ (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
(list_comb (rec_const, params @ make_bool_args' bs i @
make_args argTs (xs ~~ Ts)))))
- end) (cnames_syn ~~ cs);
+ end) (cnames_syn ~~ cs)
+ else [];
val (consts_defs, lthy'') = lthy'
|> fold_map Local_Theory.define specs;
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
@@ -873,11 +880,14 @@
val (_, ctxt'') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt'';
val (_, lthy''') = lthy''
- |> Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
- Proof_Context.export ctxt'' lthy'' [mono]);
+ |> Local_Theory.note
+ ((if inductive_defs
+ then Binding.qualify true rec_name (Binding.name "mono")
+ else Binding.empty, []),
+ Proof_Context.export ctxt'' lthy'' [mono]);
in
(lthy''', Proof_Context.transfer (Proof_Context.theory_of lthy''') ctxt'',
- rec_name, mono, fp_def', map (#2 o #2) consts_defs,
+ rec_binding, mono, fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
@@ -974,7 +984,7 @@
val ((intr_names, intr_atts), intr_ts) =
apfst split_list (split_list (map (check_rule lthy cs params) intros));
- val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
+ val (lthy1, lthy2, rec_binding, mono, fp_def, rec_preds_defs, rec_const, preds,
argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
monos params cnames_syn lthy;
@@ -1003,7 +1013,7 @@
val intrs' = map (rulify lthy1) intrs;
val (intrs'', elims'', eqs', induct, inducts, lthy3) =
- declare_rules rec_name coind no_ind
+ declare_rules rec_binding coind no_ind
cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
val result =
--- a/src/HOL/Transitive_Closure.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Transitive_Closure.thy Sun Nov 15 12:39:51 2015 +0100
@@ -20,6 +20,10 @@
operands to be atomic.
\<close>
+context
+ notes [[inductive_defs]]
+begin
+
inductive_set
rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_^*)" [1000] 999)
for r :: "('a \<times> 'a) set"
@@ -39,6 +43,8 @@
trancl_def [nitpick_unfold del]
tranclp_def [nitpick_unfold del]
+end
+
notation
rtranclp ("(_^**)" [1000] 1000) and
tranclp ("(_^++)" [1000] 1000)