merged
authorwenzelm
Sun Nov 15 14:40:07 2015 +0100 (2015-11-15)
changeset 6168379514e0f60eb
parent 61679 1335462046e8
parent 61682 f2c69a221055
child 61684 048ba34613bb
merged
     1.1 --- a/NEWS	Sun Nov 15 14:38:29 2015 +0100
     1.2 +++ b/NEWS	Sun Nov 15 14:40:07 2015 +0100
     1.3 @@ -537,10 +537,14 @@
     1.4  * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
     1.5  command. Minor INCOMPATIBILITY, use 'function' instead.
     1.6  
     1.7 +* Inductive definitions ('inductive', 'coinductive', etc.) expose
     1.8 +low-level facts of the internal construction only if the option
     1.9 +"inductive_defs" is enabled. This refers to the internal predicate
    1.10 +definition and its monotonicity result. Rare INCOMPATIBILITY.
    1.11 +
    1.12  * Recursive function definitions ('fun', 'function', 'partial_function')
    1.13 -no longer expose the low-level "_def" facts of the internal
    1.14 -construction. INCOMPATIBILITY, enable option "function_defs" in the
    1.15 -context for rare situations where these facts are really needed.
    1.16 +expose low-level facts of the internal construction only if the option
    1.17 +"function_defs" is enabled. Rare INCOMPATIBILITY.
    1.18  
    1.19  * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.20  
     2.1 --- a/src/HOL/BNF_Def.thy	Sun Nov 15 14:38:29 2015 +0100
     2.2 +++ b/src/HOL/BNF_Def.thy	Sun Nov 15 14:40:07 2015 +0100
     2.3 @@ -24,8 +24,6 @@
     2.4    "R1 a c \<Longrightarrow> rel_sum R1 R2 (Inl a) (Inl c)"
     2.5  | "R2 b d \<Longrightarrow> rel_sum R1 R2 (Inr b) (Inr d)"
     2.6  
     2.7 -hide_fact rel_sum_def
     2.8 -
     2.9  definition
    2.10    rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    2.11  where
     3.1 --- a/src/HOL/Basic_BNFs.thy	Sun Nov 15 14:38:29 2015 +0100
     3.2 +++ b/src/HOL/Basic_BNFs.thy	Sun Nov 15 14:40:07 2015 +0100
     3.3 @@ -102,8 +102,6 @@
     3.4  where
     3.5    "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
     3.6  
     3.7 -hide_fact rel_prod_def
     3.8 -
     3.9  lemma rel_prod_apply [code, simp]:
    3.10    "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    3.11    by (auto intro: rel_prod.intros elim: rel_prod.cases)
     4.1 --- a/src/HOL/Finite_Set.thy	Sun Nov 15 14:38:29 2015 +0100
     4.2 +++ b/src/HOL/Finite_Set.thy	Sun Nov 15 14:40:07 2015 +0100
     4.3 @@ -11,11 +11,17 @@
     4.4  
     4.5  subsection \<open>Predicate for finite sets\<close>
     4.6  
     4.7 +context
     4.8 +  notes [[inductive_defs]]
     4.9 +begin
    4.10 +
    4.11  inductive finite :: "'a set \<Rightarrow> bool"
    4.12    where
    4.13      emptyI [simp, intro!]: "finite {}"
    4.14    | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
    4.15  
    4.16 +end
    4.17 +
    4.18  simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
    4.19  
    4.20  declare [[simproc del: finite_Collect]]
     5.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Sun Nov 15 14:38:29 2015 +0100
     5.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Sun Nov 15 14:40:07 2015 +0100
     5.3 @@ -64,6 +64,10 @@
     5.4  abbreviation HLD_nxt (infixr "\<cdot>" 65) where
     5.5    "s \<cdot> P \<equiv> HLD s aand nxt P"
     5.6  
     5.7 +context
     5.8 +  notes [[inductive_defs]]
     5.9 +begin
    5.10 +
    5.11  inductive ev for \<phi> where
    5.12  base: "\<phi> xs \<Longrightarrow> ev \<phi> xs"
    5.13  |
    5.14 @@ -78,6 +82,8 @@
    5.15  |
    5.16  step: "\<lbrakk>\<phi> xs; (\<phi> until \<psi>) (stl xs)\<rbrakk> \<Longrightarrow> (\<phi> until \<psi>) xs"
    5.17  
    5.18 +end
    5.19 +
    5.20  lemma holds_mono:
    5.21  assumes holds: "holds P xs" and 0: "\<And> x. P x \<Longrightarrow> Q x"
    5.22  shows "holds Q xs"
    5.23 @@ -587,12 +593,18 @@
    5.24  
    5.25  text \<open>Strong until\<close>
    5.26  
    5.27 +context
    5.28 +  notes [[inductive_defs]]
    5.29 +begin
    5.30 +
    5.31  inductive suntil (infix "suntil" 60) for \<phi> \<psi> where
    5.32    base: "\<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
    5.33  | step: "\<phi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
    5.34  
    5.35  inductive_simps suntil_Stream: "(\<phi> suntil \<psi>) (x ## s)"
    5.36  
    5.37 +end
    5.38 +
    5.39  lemma suntil_induct_strong[consumes 1, case_names base step]:
    5.40    "(\<phi> suntil \<psi>) x \<Longrightarrow>
    5.41      (\<And>\<omega>. \<psi> \<omega> \<Longrightarrow> P \<omega>) \<Longrightarrow>
     6.1 --- a/src/HOL/Library/Stream.thy	Sun Nov 15 14:38:29 2015 +0100
     6.2 +++ b/src/HOL/Library/Stream.thy	Sun Nov 15 14:40:07 2015 +0100
     6.3 @@ -68,12 +68,18 @@
     6.4  
     6.5  subsection \<open>set of streams with elements in some fixed set\<close>
     6.6  
     6.7 +context
     6.8 +  notes [[inductive_defs]]
     6.9 +begin
    6.10 +
    6.11  coinductive_set
    6.12    streams :: "'a set \<Rightarrow> 'a stream set"
    6.13    for A :: "'a set"
    6.14  where
    6.15    Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
    6.16  
    6.17 +end
    6.18 +
    6.19  lemma in_streams: "stl s \<in> streams S \<Longrightarrow> shd s \<in> S \<Longrightarrow> s \<in> streams S"
    6.20    by (cases s) auto
    6.21  
     7.1 --- a/src/HOL/List.thy	Sun Nov 15 14:38:29 2015 +0100
     7.2 +++ b/src/HOL/List.thy	Sun Nov 15 14:40:07 2015 +0100
     7.3 @@ -5573,7 +5573,12 @@
     7.4    Author: Andreas Lochbihler
     7.5  \<close>
     7.6  
     7.7 -context ord begin
     7.8 +context ord
     7.9 +begin
    7.10 +
    7.11 +context
    7.12 +  notes [[inductive_defs]]
    7.13 +begin
    7.14  
    7.15  inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    7.16  where
    7.17 @@ -5582,6 +5587,8 @@
    7.18  | Cons_eq:
    7.19    "\<lbrakk> \<not> x < y; \<not> y < x; lexordp xs ys \<rbrakk> \<Longrightarrow> lexordp (x # xs) (y # ys)"
    7.20  
    7.21 +end
    7.22 +
    7.23  lemma lexordp_simps [simp]:
    7.24    "lexordp [] ys = (ys \<noteq> [])"
    7.25    "lexordp xs [] = False"
    7.26 @@ -5636,7 +5643,8 @@
    7.27  lemma lexord_code [code, code_unfold]: "lexordp = ord.lexordp less"
    7.28  unfolding lexordp_def ord.lexordp_def ..
    7.29  
    7.30 -context order begin
    7.31 +context order
    7.32 +begin
    7.33  
    7.34  lemma lexordp_antisym:
    7.35    assumes "lexordp xs ys" "lexordp ys xs"
     8.1 --- a/src/HOL/Nitpick.thy	Sun Nov 15 14:38:29 2015 +0100
     8.2 +++ b/src/HOL/Nitpick.thy	Sun Nov 15 14:40:07 2015 +0100
     8.3 @@ -238,7 +238,7 @@
     8.4  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
     8.5  
     8.6  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
     8.7 -  card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
     8.8 +  card'_def setsum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
     8.9    size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    8.10    num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
    8.11    number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
     9.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sun Nov 15 14:38:29 2015 +0100
     9.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Sun Nov 15 14:40:07 2015 +0100
     9.3 @@ -886,9 +886,15 @@
     9.4               intro!: setsum.mono_neutral_cong_left arg_cong2[where f=measure])
     9.5  qed
     9.6  
     9.7 +context
     9.8 +  notes [[inductive_defs]]
     9.9 +begin
    9.10 +
    9.11  inductive integrable for M f where
    9.12    "has_bochner_integral M f x \<Longrightarrow> integrable M f"
    9.13  
    9.14 +end
    9.15 +
    9.16  definition lebesgue_integral ("integral\<^sup>L") where
    9.17    "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)"
    9.18  
    10.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 15 14:38:29 2015 +0100
    10.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 15 14:40:07 2015 +0100
    10.3 @@ -71,6 +71,7 @@
    10.4  signature INDUCTIVE =
    10.5  sig
    10.6    include BASIC_INDUCTIVE
    10.7 +  val inductive_defs: bool Config.T
    10.8    val select_disj_tac: Proof.context -> int -> int -> int -> tactic
    10.9    type add_ind_def =
   10.10      inductive_flags ->
   10.11 @@ -121,6 +122,8 @@
   10.12  
   10.13  (** misc utilities **)
   10.14  
   10.15 +val inductive_defs = Attrib.setup_config_bool @{binding inductive_defs} (K false);
   10.16 +
   10.17  fun message quiet_mode s = if quiet_mode then () else writeln s;
   10.18  
   10.19  fun clean_message ctxt quiet_mode s =
   10.20 @@ -836,17 +839,21 @@
   10.21  
   10.22      (* add definition of recursive predicates to theory *)
   10.23  
   10.24 -    val rec_name =
   10.25 +    val rec_binding =
   10.26        if Binding.is_empty alt_name then
   10.27          Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
   10.28        else alt_name;
   10.29 +    val rec_name = Binding.name_of rec_binding;
   10.30  
   10.31 -    val is_auxiliary = length cs >= 2; 
   10.32 +    val inductive_defs = Config.get lthy inductive_defs;
   10.33 +    val is_auxiliary = length cs >= 2;
   10.34 +
   10.35      val ((rec_const, (_, fp_def)), lthy') = lthy
   10.36        |> is_auxiliary ? Proof_Context.concealed
   10.37        |> Local_Theory.define
   10.38 -        ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
   10.39 -         ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
   10.40 +        ((rec_binding, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
   10.41 +         ((if inductive_defs then Thm.def_binding rec_binding else Binding.empty,
   10.42 +           @{attributes [nitpick_unfold]}),
   10.43             fold_rev lambda params
   10.44               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   10.45        ||> Proof_Context.restore_naming lthy;
   10.46 @@ -854,18 +861,18 @@
   10.47        Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
   10.48          (Thm.cterm_of lthy' (list_comb (rec_const, params)));
   10.49      val specs =
   10.50 -      if length cs < 2 then []
   10.51 -      else
   10.52 +      if is_auxiliary then
   10.53          map_index (fn (i, (name_mx, c)) =>
   10.54            let
   10.55              val Ts = arg_types_of (length params) c;
   10.56              val xs =
   10.57                map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
   10.58            in
   10.59 -            (name_mx, (apfst Binding.concealed Attrib.empty_binding, fold_rev lambda (params @ xs)
   10.60 +            (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
   10.61                (list_comb (rec_const, params @ make_bool_args' bs i @
   10.62                  make_args argTs (xs ~~ Ts)))))
   10.63 -          end) (cnames_syn ~~ cs);
   10.64 +          end) (cnames_syn ~~ cs)
   10.65 +      else [];
   10.66      val (consts_defs, lthy'') = lthy'
   10.67        |> fold_map Local_Theory.define specs;
   10.68      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
   10.69 @@ -873,11 +880,14 @@
   10.70      val (_, ctxt'') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
   10.71      val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt'';
   10.72      val (_, lthy''') = lthy''
   10.73 -      |> Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
   10.74 -        Proof_Context.export ctxt'' lthy'' [mono]);
   10.75 +      |> Local_Theory.note
   10.76 +        ((if inductive_defs
   10.77 +          then Binding.qualify true rec_name (Binding.name "mono")
   10.78 +          else Binding.empty, []),
   10.79 +          Proof_Context.export ctxt'' lthy'' [mono]);
   10.80    in
   10.81      (lthy''', Proof_Context.transfer (Proof_Context.theory_of lthy''') ctxt'',
   10.82 -      rec_name, mono, fp_def', map (#2 o #2) consts_defs,
   10.83 +      rec_binding, mono, fp_def', map (#2 o #2) consts_defs,
   10.84        list_comb (rec_const, params), preds, argTs, bs, xs)
   10.85    end;
   10.86  
   10.87 @@ -974,7 +984,7 @@
   10.88      val ((intr_names, intr_atts), intr_ts) =
   10.89        apfst split_list (split_list (map (check_rule lthy cs params) intros));
   10.90  
   10.91 -    val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
   10.92 +    val (lthy1, lthy2, rec_binding, mono, fp_def, rec_preds_defs, rec_const, preds,
   10.93        argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
   10.94          monos params cnames_syn lthy;
   10.95  
   10.96 @@ -1003,7 +1013,7 @@
   10.97      val intrs' = map (rulify lthy1) intrs;
   10.98  
   10.99      val (intrs'', elims'', eqs', induct, inducts, lthy3) =
  10.100 -      declare_rules rec_name coind no_ind
  10.101 +      declare_rules rec_binding coind no_ind
  10.102          cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1;
  10.103  
  10.104      val result =
    11.1 --- a/src/HOL/Transitive_Closure.thy	Sun Nov 15 14:38:29 2015 +0100
    11.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Nov 15 14:40:07 2015 +0100
    11.3 @@ -20,6 +20,10 @@
    11.4    operands to be atomic.
    11.5  \<close>
    11.6  
    11.7 +context
    11.8 +  notes [[inductive_defs]]
    11.9 +begin
   11.10 +
   11.11  inductive_set
   11.12    rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"   ("(_^*)" [1000] 999)
   11.13    for r :: "('a \<times> 'a) set"
   11.14 @@ -39,6 +43,8 @@
   11.15          trancl_def [nitpick_unfold del]
   11.16          tranclp_def [nitpick_unfold del]
   11.17  
   11.18 +end
   11.19 +
   11.20  notation
   11.21    rtranclp  ("(_^**)" [1000] 1000) and
   11.22    tranclp  ("(_^++)" [1000] 1000)
    12.1 --- a/src/Tools/jEdit/src/session_build.scala	Sun Nov 15 14:38:29 2015 +0100
    12.2 +++ b/src/Tools/jEdit/src/session_build.scala	Sun Nov 15 14:40:07 2015 +0100
    12.3 @@ -174,7 +174,7 @@
    12.4        progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
    12.5  
    12.6        if (rc == 0) Isabelle_Logic.session_start()
    12.7 -      else progress.echo("Build failed -- prover remains inactive!")
    12.8 +      else progress.echo("Session build failed -- prover process remains inactive!")
    12.9  
   12.10        return_code(rc)
   12.11      }