# HG changeset patch # User wenzelm # Date 1447587591 -3600 # Node ID ca53150406c91589751beffec5fe1294e4fc362a # Parent f7c00119e6e7ca655a668b0d0abf8e1902a92d73 option "inductive_defs" controls exposure of def and mono facts; diff -r f7c00119e6e7 -r ca53150406c9 NEWS --- 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. diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/BNF_Def.thy --- 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 \ rel_sum R1 R2 (Inl a) (Inl c)" | "R2 b d \ rel_sum R1 R2 (Inr b) (Inr d)" -hide_fact rel_sum_def - definition rel_fun :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" where diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Basic_BNFs.thy --- 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 "\R1 a b; R2 c d\ \ 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) \ R1 a c \ R2 b d" by (auto intro: rel_prod.intros elim: rel_prod.cases) diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Finite_Set.thy --- 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 \Predicate for finite sets\ +context + notes [[inductive_defs]] +begin + inductive finite :: "'a set \ bool" where emptyI [simp, intro!]: "finite {}" | insertI [simp, intro!]: "finite A \ finite (insert a A)" +end + simproc_setup finite_Collect ("finite (Collect P)") = \K Set_Comprehension_Pointfree.simproc\ declare [[simproc del: finite_Collect]] diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy --- 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 "\" 65) where "s \ P \ HLD s aand nxt P" +context + notes [[inductive_defs]] +begin + inductive ev for \ where base: "\ xs \ ev \ xs" | @@ -78,6 +82,8 @@ | step: "\\ xs; (\ until \) (stl xs)\ \ (\ until \) xs" +end + lemma holds_mono: assumes holds: "holds P xs" and 0: "\ x. P x \ Q x" shows "holds Q xs" @@ -587,12 +593,18 @@ text \Strong until\ +context + notes [[inductive_defs]] +begin + inductive suntil (infix "suntil" 60) for \ \ where base: "\ \ \ (\ suntil \) \" | step: "\ \ \ (\ suntil \) (stl \) \ (\ suntil \) \" inductive_simps suntil_Stream: "(\ suntil \) (x ## s)" +end + lemma suntil_induct_strong[consumes 1, case_names base step]: "(\ suntil \) x \ (\\. \ \ \ P \) \ diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Library/Stream.thy --- 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 \set of streams with elements in some fixed set\ +context + notes [[inductive_defs]] +begin + coinductive_set streams :: "'a set \ 'a stream set" for A :: "'a set" where Stream[intro!, simp, no_atp]: "\a \ A; s \ streams A\ \ a ## s \ streams A" +end + lemma in_streams: "stl s \ streams S \ shd s \ S \ s \ streams S" by (cases s) auto diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/List.thy --- 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 \ -context ord begin +context ord +begin + +context + notes [[inductive_defs]] +begin inductive lexordp :: "'a list \ 'a list \ bool" where @@ -5582,6 +5587,8 @@ | Cons_eq: "\ \ x < y; \ y < x; lexordp xs ys \ \ lexordp (x # xs) (y # ys)" +end + lemma lexordp_simps [simp]: "lexordp [] ys = (ys \ [])" "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" diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Nitpick.thy --- 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 diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Probability/Bochner_Integration.thy --- 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 \ integrable M f" +end + definition lebesgue_integral ("integral\<^sup>L") where "integral\<^sup>L M f = (if \x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)" diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Tools/inductive.ML --- 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 = diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Transitive_Closure.thy --- 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. \ +context + notes [[inductive_defs]] +begin + inductive_set rtrancl :: "('a \ 'a) set \ ('a \ 'a) set" ("(_^*)" [1000] 999) for r :: "('a \ '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)