# HG changeset patch # User wenzelm # Date 1346870173 -7200 # Node ID bf6f727cb3627b0f29e79c556260173869771115 # Parent 937a0fadddfb13c9a9c2b26ad259d9b02a9992c5# Parent 3d7a695385f1e4bf908829e6a650aa794a7e691b merged diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Nominal/Examples/Crary.thy --- a/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Nominal/Examples/Crary.thy Wed Sep 05 20:36:13 2012 +0200 @@ -225,7 +225,7 @@ assumes a: "x\\" shows "\ = Var x" using a -by (induct \ arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm) +by (induct \ arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm) lemma psubst_subst_propagate: assumes "x\\" @@ -529,7 +529,7 @@ lemma alg_path_equiv_implies_valid: shows "\ \ s \ t : T \ valid \" and "\ \ s \ t : T \ valid \" -by (induct rule : alg_equiv_alg_path_equiv.inducts, auto) +by (induct rule : alg_equiv_alg_path_equiv.inducts) auto lemma algorithmic_symmetry: shows "\ \ s \ t : T \ \ \ t \ s : T" diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Sep 05 20:36:13 2012 +0200 @@ -140,12 +140,12 @@ lemma finite_vrs: shows "finite (tyvrs_of x)" and "finite (vrs_of x)" -by (nominal_induct rule:binding.strong_induct, auto) +by (nominal_induct rule:binding.strong_induct) auto lemma finite_doms: shows "finite (ty_dom \)" and "finite (trm_dom \)" -by (induct \, auto simp add: finite_vrs) +by (induct \) (auto simp add: finite_vrs) lemma ty_dom_supp: shows "(supp (ty_dom \)) = (ty_dom \)" @@ -155,13 +155,13 @@ lemma ty_dom_inclusion: assumes a: "(TVarB X T)\set \" shows "X\(ty_dom \)" -using a by (induct \, auto) +using a by (induct \) (auto) lemma ty_binding_existence: assumes "X \ (tyvrs_of a)" shows "\T.(TVarB X T=a)" using assms -by (nominal_induct a rule: binding.strong_induct, auto) +by (nominal_induct a rule: binding.strong_induct) (auto) lemma ty_dom_existence: assumes a: "X\(ty_dom \)" @@ -176,7 +176,7 @@ lemma doms_append: shows "ty_dom (\@\) = ((ty_dom \) \ (ty_dom \))" and "trm_dom (\@\) = ((trm_dom \) \ (trm_dom \))" - by (induct \, auto) + by (induct \) (auto) lemma ty_vrs_prm_simp: fixes pi::"vrs prm" @@ -1069,7 +1069,7 @@ lemma typing_ok: assumes "\ \ t : T" shows "\ \ ok" -using assms by (induct, auto) +using assms by (induct) (auto) nominal_inductive typing by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh @@ -1208,7 +1208,7 @@ lemma ty_dom_cons: shows "ty_dom (\@[VarB X Q]@\) = ty_dom (\@\)" -by (induct \, auto) +by (induct \) (auto) lemma closed_in_cons: assumes "S closed_in (\ @ VarB X Q # \)" @@ -1251,7 +1251,7 @@ lemma ty_dom_vrs: shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)" -by (induct G, auto) +by (induct G) (auto) lemma valid_cons': assumes "\ (\ @ VarB x Q # \) ok" diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Nominal/Examples/SOS.thy --- a/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Nominal/Examples/SOS.thy Wed Sep 05 20:36:13 2012 +0200 @@ -321,7 +321,7 @@ proof (nominal_induct e e\<^isub>1 avoiding: e\<^isub>2 rule: big.strong_induct) case (b_Lam x e t\<^isub>2) have "Lam [x].e \ t\<^isub>2" by fact - thus "Lam [x].e = t\<^isub>2" by (cases, simp_all add: trm.inject) + thus "Lam [x].e = t\<^isub>2" by cases (simp_all add: trm.inject) next case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2) have ih1: "\t. e\<^isub>1 \ t \ Lam [x].e\<^isub>1' = t" by fact diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 05 20:36:13 2012 +0200 @@ -527,7 +527,7 @@ |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name, - coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} + coind = false, no_elim = true, no_ind = false, skip_mono = true} (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] @@ -1484,7 +1484,7 @@ |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, - coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} + coind = false, no_elim = false, no_ind = false, skip_mono = true} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Sep 05 20:36:13 2012 +0200 @@ -178,7 +178,7 @@ |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, - coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} + coind = false, no_elim = true, no_ind = false, skip_mono = true} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] ||> Sign.restore_naming thy1 diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Sep 05 20:36:13 2012 +0200 @@ -145,7 +145,7 @@ |> Sign.map_naming Name_Space.conceal |> Inductive.add_inductive_global {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name', - coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false} + coind = false, no_elim = false, no_ind = true, skip_mono = true} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Wed Sep 05 20:36:13 2012 +0200 @@ -439,8 +439,7 @@ coind = false, no_elim = false, no_ind = false, - skip_mono = true, - fork_mono = false} + skip_mono = true} [binding] (* relation *) [] (* no parameters *) (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Tools/inductive.ML Wed Sep 05 20:36:13 2012 +0200 @@ -39,7 +39,7 @@ thm list list * local_theory type inductive_flags = {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, - no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool} + no_elim: bool, no_ind: bool, skip_mono: bool} val add_inductive_i: inductive_flags -> ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> @@ -358,10 +358,10 @@ (* prove monotonicity *) -fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt = - (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono) +fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt = + (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty) " Proving monotonicity ..."; - (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt + (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt [] [] (HOLogic.mk_Trueprop (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) @@ -746,8 +746,7 @@ (** specification of (co)inductive predicates **) -fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind - cs intr_ts monos params cnames_syn lthy = +fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy = let val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; @@ -841,7 +840,7 @@ val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy''; - val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'''; + val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy'''; val (_, lthy'''') = Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, Proof_Context.export lthy''' lthy'' [mono]) lthy''; @@ -912,7 +911,7 @@ type inductive_flags = {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, - no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}; + no_elim: bool, no_ind: bool, skip_mono: bool}; type add_ind_def = inductive_flags -> @@ -920,7 +919,7 @@ term list -> (binding * mixfix) list -> local_theory -> inductive_result * local_theory; -fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono} cs intros monos params cnames_syn lthy = let val _ = null cnames_syn andalso error "No inductive predicates given"; @@ -933,7 +932,7 @@ 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, - argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts + argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy; val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs) @@ -983,7 +982,7 @@ (* external interfaces *) fun gen_add_inductive_i mk_def - (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}) + (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}) cnames_syn pnames spec monos lthy = let val thy = Proof_Context.theory_of lthy; @@ -1047,8 +1046,9 @@ |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs; val (cs, ps) = chop (length cnames_syn) vars; val monos = Attrib.eval_thms lthy raw_monos; - val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty, - coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int}; + val flags = + {quiet_mode = false, verbose = verbose, alt_name = Binding.empty, + coind = coind, no_elim = false, no_ind = false, skip_mono = false}; in lthy |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Sep 05 20:36:13 2012 +0200 @@ -355,7 +355,7 @@ val (ind_info, thy3') = thy2 |> Inductive.add_inductive_global {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, - no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} + no_elim = false, no_ind = false, skip_mono = false} rlzpreds rlzparams (map (fn (rintr, intr) => ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), subst_atomic rlzpreds' (Logic.unvarify_global rintr))) diff -r 937a0fadddfb -r bf6f727cb362 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed Sep 05 19:58:09 2012 +0200 +++ b/src/HOL/Tools/inductive_set.ML Wed Sep 05 20:36:13 2012 +0200 @@ -417,7 +417,7 @@ (**** definition of inductive sets ****) fun add_ind_set_def - {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} + {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono} cs intros monos params cnames_syn lthy = let val thy = Proof_Context.theory_of lthy; @@ -490,8 +490,7 @@ val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) = Inductive.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty, - coind = coind, no_elim = no_elim, no_ind = no_ind, - skip_mono = skip_mono, fork_mono = fork_mono} + coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} cs' intros' monos' params1 cnames_syn' lthy; (* define inductive sets using previously defined predicates *) diff -r 937a0fadddfb -r bf6f727cb362 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 05 19:58:09 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 05 20:36:13 2012 +0200 @@ -92,9 +92,9 @@ private val subexp_include = Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP, Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY, - Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, - Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, - Isabelle_Markup.DOC_SOURCE) + Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, + Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, + Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE) def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] = { @@ -190,8 +190,8 @@ Isabelle_Markup.DOC_SOURCE -> "document source") private val tooltip_elements = - Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING) ++ - tooltips.keys + Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING, + Isabelle_Markup.PATH) ++ tooltips.keys private def string_of_typing(kind: String, body: XML.Body): String = Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)), @@ -208,6 +208,10 @@ { case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) => add(prev, r, (true, kind + " " + quote(name))) + case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _))) + if Path.is_ok(name) => + val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name)) + add(prev, r, (true, "file " + quote(jedit_file))) case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) => add(prev, r, (true, string_of_typing("::", body))) case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>