1.1 --- a/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 19:58:09 2012 +0200
1.2 +++ b/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 20:36:13 2012 +0200
1.3 @@ -225,7 +225,7 @@
1.4 assumes a: "x\<sharp>\<theta>"
1.5 shows "\<theta><Var x> = Var x"
1.6 using a
1.7 -by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
1.8 +by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm)
1.9
1.10 lemma psubst_subst_propagate:
1.11 assumes "x\<sharp>\<theta>"
1.12 @@ -529,7 +529,7 @@
1.13 lemma alg_path_equiv_implies_valid:
1.14 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
1.15 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
1.16 -by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
1.17 +by (induct rule : alg_equiv_alg_path_equiv.inducts) auto
1.18
1.19 lemma algorithmic_symmetry:
1.20 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T"
2.1 --- a/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 19:58:09 2012 +0200
2.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 20:36:13 2012 +0200
2.3 @@ -140,12 +140,12 @@
2.4 lemma finite_vrs:
2.5 shows "finite (tyvrs_of x)"
2.6 and "finite (vrs_of x)"
2.7 -by (nominal_induct rule:binding.strong_induct, auto)
2.8 +by (nominal_induct rule:binding.strong_induct) auto
2.9
2.10 lemma finite_doms:
2.11 shows "finite (ty_dom \<Gamma>)"
2.12 and "finite (trm_dom \<Gamma>)"
2.13 -by (induct \<Gamma>, auto simp add: finite_vrs)
2.14 +by (induct \<Gamma>) (auto simp add: finite_vrs)
2.15
2.16 lemma ty_dom_supp:
2.17 shows "(supp (ty_dom \<Gamma>)) = (ty_dom \<Gamma>)"
2.18 @@ -155,13 +155,13 @@
2.19 lemma ty_dom_inclusion:
2.20 assumes a: "(TVarB X T)\<in>set \<Gamma>"
2.21 shows "X\<in>(ty_dom \<Gamma>)"
2.22 -using a by (induct \<Gamma>, auto)
2.23 +using a by (induct \<Gamma>) (auto)
2.24
2.25 lemma ty_binding_existence:
2.26 assumes "X \<in> (tyvrs_of a)"
2.27 shows "\<exists>T.(TVarB X T=a)"
2.28 using assms
2.29 -by (nominal_induct a rule: binding.strong_induct, auto)
2.30 +by (nominal_induct a rule: binding.strong_induct) (auto)
2.31
2.32 lemma ty_dom_existence:
2.33 assumes a: "X\<in>(ty_dom \<Gamma>)"
2.34 @@ -176,7 +176,7 @@
2.35 lemma doms_append:
2.36 shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
2.37 and "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
2.38 - by (induct \<Gamma>, auto)
2.39 + by (induct \<Gamma>) (auto)
2.40
2.41 lemma ty_vrs_prm_simp:
2.42 fixes pi::"vrs prm"
2.43 @@ -1069,7 +1069,7 @@
2.44 lemma typing_ok:
2.45 assumes "\<Gamma> \<turnstile> t : T"
2.46 shows "\<turnstile> \<Gamma> ok"
2.47 -using assms by (induct, auto)
2.48 +using assms by (induct) (auto)
2.49
2.50 nominal_inductive typing
2.51 by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
2.52 @@ -1208,7 +1208,7 @@
2.53
2.54 lemma ty_dom_cons:
2.55 shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
2.56 -by (induct \<Gamma>, auto)
2.57 +by (induct \<Gamma>) (auto)
2.58
2.59 lemma closed_in_cons:
2.60 assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
2.61 @@ -1251,7 +1251,7 @@
2.62
2.63 lemma ty_dom_vrs:
2.64 shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
2.65 -by (induct G, auto)
2.66 +by (induct G) (auto)
2.67
2.68 lemma valid_cons':
2.69 assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
3.1 --- a/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 19:58:09 2012 +0200
3.2 +++ b/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 20:36:13 2012 +0200
3.3 @@ -321,7 +321,7 @@
3.4 proof (nominal_induct e e\<^isub>1 avoiding: e\<^isub>2 rule: big.strong_induct)
3.5 case (b_Lam x e t\<^isub>2)
3.6 have "Lam [x].e \<Down> t\<^isub>2" by fact
3.7 - thus "Lam [x].e = t\<^isub>2" by (cases, simp_all add: trm.inject)
3.8 + thus "Lam [x].e = t\<^isub>2" by cases (simp_all add: trm.inject)
3.9 next
3.10 case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2)
3.11 have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact
4.1 --- a/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 19:58:09 2012 +0200
4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 20:36:13 2012 +0200
4.3 @@ -527,7 +527,7 @@
4.4 |> Sign.map_naming Name_Space.conceal
4.5 |> Inductive.add_inductive_global
4.6 {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
4.7 - coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
4.8 + coind = false, no_elim = true, no_ind = false, skip_mono = true}
4.9 (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
4.10 (rep_set_names' ~~ recTs'))
4.11 [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
4.12 @@ -1484,7 +1484,7 @@
4.13 |> Sign.map_naming Name_Space.conceal
4.14 |> Inductive.add_inductive_global
4.15 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
4.16 - coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
4.17 + coind = false, no_elim = false, no_ind = false, skip_mono = true}
4.18 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
4.19 (map dest_Free rec_fns)
4.20 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
5.1 --- a/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 19:58:09 2012 +0200
5.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 20:36:13 2012 +0200
5.3 @@ -178,7 +178,7 @@
5.4 |> Sign.map_naming Name_Space.conceal
5.5 |> Inductive.add_inductive_global
5.6 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
5.7 - coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
5.8 + coind = false, no_elim = true, no_ind = false, skip_mono = true}
5.9 (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
5.10 (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
5.11 ||> Sign.restore_naming thy1
6.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 19:58:09 2012 +0200
6.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 20:36:13 2012 +0200
6.3 @@ -145,7 +145,7 @@
6.4 |> Sign.map_naming Name_Space.conceal
6.5 |> Inductive.add_inductive_global
6.6 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
6.7 - coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
6.8 + coind = false, no_elim = false, no_ind = true, skip_mono = true}
6.9 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
6.10 (map dest_Free rec_fns)
6.11 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
7.1 --- a/src/HOL/Tools/Function/function_core.ML Wed Sep 05 19:58:09 2012 +0200
7.2 +++ b/src/HOL/Tools/Function/function_core.ML Wed Sep 05 20:36:13 2012 +0200
7.3 @@ -439,8 +439,7 @@
7.4 coind = false,
7.5 no_elim = false,
7.6 no_ind = false,
7.7 - skip_mono = true,
7.8 - fork_mono = false}
7.9 + skip_mono = true}
7.10 [binding] (* relation *)
7.11 [] (* no parameters *)
7.12 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
8.1 --- a/src/HOL/Tools/inductive.ML Wed Sep 05 19:58:09 2012 +0200
8.2 +++ b/src/HOL/Tools/inductive.ML Wed Sep 05 20:36:13 2012 +0200
8.3 @@ -39,7 +39,7 @@
8.4 thm list list * local_theory
8.5 type inductive_flags =
8.6 {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
8.7 - no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
8.8 + no_elim: bool, no_ind: bool, skip_mono: bool}
8.9 val add_inductive_i:
8.10 inductive_flags -> ((binding * typ) * mixfix) list ->
8.11 (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
8.12 @@ -358,10 +358,10 @@
8.13
8.14 (* prove monotonicity *)
8.15
8.16 -fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
8.17 - (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
8.18 +fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
8.19 + (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
8.20 " Proving monotonicity ...";
8.21 - (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
8.22 + (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt
8.23 [] []
8.24 (HOLogic.mk_Trueprop
8.25 (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
8.26 @@ -746,8 +746,7 @@
8.27
8.28 (** specification of (co)inductive predicates **)
8.29
8.30 -fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
8.31 - cs intr_ts monos params cnames_syn lthy =
8.32 +fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
8.33 let
8.34 val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
8.35
8.36 @@ -841,7 +840,7 @@
8.37 val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
8.38
8.39 val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
8.40 - val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
8.41 + val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
8.42 val (_, lthy'''') =
8.43 Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
8.44 Proof_Context.export lthy''' lthy'' [mono]) lthy'';
8.45 @@ -912,7 +911,7 @@
8.46
8.47 type inductive_flags =
8.48 {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
8.49 - no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
8.50 + no_elim: bool, no_ind: bool, skip_mono: bool};
8.51
8.52 type add_ind_def =
8.53 inductive_flags ->
8.54 @@ -920,7 +919,7 @@
8.55 term list -> (binding * mixfix) list ->
8.56 local_theory -> inductive_result * local_theory;
8.57
8.58 -fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
8.59 +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
8.60 cs intros monos params cnames_syn lthy =
8.61 let
8.62 val _ = null cnames_syn andalso error "No inductive predicates given";
8.63 @@ -933,7 +932,7 @@
8.64 apfst split_list (split_list (map (check_rule lthy cs params) intros));
8.65
8.66 val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
8.67 - argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
8.68 + argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
8.69 monos params cnames_syn lthy;
8.70
8.71 val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
8.72 @@ -983,7 +982,7 @@
8.73 (* external interfaces *)
8.74
8.75 fun gen_add_inductive_i mk_def
8.76 - (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
8.77 + (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
8.78 cnames_syn pnames spec monos lthy =
8.79 let
8.80 val thy = Proof_Context.theory_of lthy;
8.81 @@ -1047,8 +1046,9 @@
8.82 |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
8.83 val (cs, ps) = chop (length cnames_syn) vars;
8.84 val monos = Attrib.eval_thms lthy raw_monos;
8.85 - val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
8.86 - coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
8.87 + val flags =
8.88 + {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
8.89 + coind = coind, no_elim = false, no_ind = false, skip_mono = false};
8.90 in
8.91 lthy
8.92 |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
9.1 --- a/src/HOL/Tools/inductive_realizer.ML Wed Sep 05 19:58:09 2012 +0200
9.2 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Sep 05 20:36:13 2012 +0200
9.3 @@ -355,7 +355,7 @@
9.4 val (ind_info, thy3') = thy2 |>
9.5 Inductive.add_inductive_global
9.6 {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
9.7 - no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
9.8 + no_elim = false, no_ind = false, skip_mono = false}
9.9 rlzpreds rlzparams (map (fn (rintr, intr) =>
9.10 ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
9.11 subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
10.1 --- a/src/HOL/Tools/inductive_set.ML Wed Sep 05 19:58:09 2012 +0200
10.2 +++ b/src/HOL/Tools/inductive_set.ML Wed Sep 05 20:36:13 2012 +0200
10.3 @@ -417,7 +417,7 @@
10.4 (**** definition of inductive sets ****)
10.5
10.6 fun add_ind_set_def
10.7 - {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
10.8 + {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
10.9 cs intros monos params cnames_syn lthy =
10.10 let
10.11 val thy = Proof_Context.theory_of lthy;
10.12 @@ -490,8 +490,7 @@
10.13 val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
10.14 Inductive.add_ind_def
10.15 {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
10.16 - coind = coind, no_elim = no_elim, no_ind = no_ind,
10.17 - skip_mono = skip_mono, fork_mono = fork_mono}
10.18 + coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
10.19 cs' intros' monos' params1 cnames_syn' lthy;
10.20
10.21 (* define inductive sets using previously defined predicates *)
11.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 05 19:58:09 2012 +0200
11.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 05 20:36:13 2012 +0200
11.3 @@ -92,9 +92,9 @@
11.4 private val subexp_include =
11.5 Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
11.6 Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
11.7 - Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
11.8 - Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
11.9 - Isabelle_Markup.DOC_SOURCE)
11.10 + Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
11.11 + Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
11.12 + Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
11.13
11.14 def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
11.15 {
11.16 @@ -190,8 +190,8 @@
11.17 Isabelle_Markup.DOC_SOURCE -> "document source")
11.18
11.19 private val tooltip_elements =
11.20 - Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING) ++
11.21 - tooltips.keys
11.22 + Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
11.23 + Isabelle_Markup.PATH) ++ tooltips.keys
11.24
11.25 private def string_of_typing(kind: String, body: XML.Body): String =
11.26 Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
11.27 @@ -208,6 +208,10 @@
11.28 {
11.29 case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
11.30 add(prev, r, (true, kind + " " + quote(name)))
11.31 + case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
11.32 + if Path.is_ok(name) =>
11.33 + val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
11.34 + add(prev, r, (true, "file " + quote(jedit_file)))
11.35 case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
11.36 add(prev, r, (true, string_of_typing("::", body)))
11.37 case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>