# HG changeset patch # User Andreas Lochbihler # Date 1349880079 -7200 # Node ID 3fc6b3289c31a2204748fe04fb219a140ada5a2e # Parent 53f14f62cca2c10c218fbd47c4e3ab05dc2b35a5# Parent acb6fa98e310b75894ae104e623ad30e2e4d39d8 merged diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Cube/Cube.thy Wed Oct 10 16:41:19 2012 +0200 @@ -10,6 +10,15 @@ setup Pure_Thy.old_appl_syntax_setup +ML {* + structure Rules = Named_Thms + ( + val name = @{binding rules} + val description = "Cube inference rules" + ) +*} +setup Rules.setup + typedecl "term" typedecl "context" typedecl typing @@ -72,8 +81,7 @@ beta: "Abs(A, f)^a == f(a)" -lemmas simple = s_b strip_s strip_b app lam_ss pi_ss -lemmas rules = simple +lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss lemma imp_elim: assumes "f:A\B" and "a:A" and "f^a:B ==> PROP P" @@ -90,7 +98,7 @@ ==> Abs(A,f) : Prod(A,B)" begin -lemmas rules = simple lam_bs pi_bs +lemmas [rules] = lam_bs pi_bs end @@ -102,7 +110,7 @@ ==> Abs(A,f) : Prod(A,B)" begin -lemmas rules = simple lam_bb pi_bb +lemmas [rules] = lam_bb pi_bb end @@ -113,7 +121,7 @@ ==> Abs(A,f) : Prod(A,B)" begin -lemmas rules = simple lam_sb pi_sb +lemmas [rules] = lam_sb pi_sb end @@ -121,7 +129,7 @@ locale LP2 = LP + L2 begin -lemmas rules = simple lam_bs pi_bs lam_sb pi_sb +lemmas [rules] = lam_bs pi_bs lam_sb pi_sb end @@ -129,7 +137,7 @@ locale Lomega2 = L2 + Lomega begin -lemmas rules = simple lam_bs pi_bs lam_bb pi_bb +lemmas [rules] = lam_bs pi_bs lam_bb pi_bb end @@ -137,7 +145,7 @@ locale LPomega = LP + Lomega begin -lemmas rules = simple lam_bb pi_bb lam_sb pi_sb +lemmas [rules] = lam_bb pi_bb lam_sb pi_sb end @@ -145,7 +153,7 @@ locale CC = L2 + LP + Lomega begin -lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb +lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb end diff -r 53f14f62cca2 -r 3fc6b3289c31 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 16:41:19 2012 +0200 @@ -104,7 +104,7 @@ end print_locale! logic -locale use_decl = logic + semi "op ||" +locale use_decl = l: logic + semi "op ||" print_locale! use_decl thm use_decl_def locale extra_type = diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/Cardinals/Wellorder_Embedding_Base.thy --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 16:41:19 2012 +0200 @@ -273,7 +273,7 @@ lemma embed_underS: -assumes WELL: "Well_order r" and WELL: "Well_order r'" and +assumes WELL: "Well_order r" and WELL': "Well_order r'" and EMB: "embed r r' f" and IN: "a \ Field r" shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))" proof- diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 16:41:19 2012 +0200 @@ -452,7 +452,7 @@ assumes between_less: "less x y \ less x (between x y) \ less (between x y) y" and between_same: "between x x = x" -sublocale constr_dense_linorder < dense_linorder +sublocale constr_dense_linorder < dlo: dense_linorder apply unfold_locales using gt_ex lt_ex between_less apply auto diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/Finite_Set.thy Wed Oct 10 16:41:19 2012 +0200 @@ -1757,7 +1757,7 @@ locale folding_image_simple_idem = folding_image_simple + assumes idem: "x * x = x" -sublocale folding_image_simple_idem < semilattice proof +sublocale folding_image_simple_idem < semilattice: semilattice proof qed (fact idem) context folding_image_simple_idem @@ -1898,7 +1898,7 @@ locale folding_one_idem = folding_one + assumes idem: "x * x = x" -sublocale folding_one_idem < semilattice proof +sublocale folding_one_idem < semilattice: semilattice proof qed (fact idem) context folding_one_idem diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/Library/Univ_Poly.thy --- a/src/HOL/Library/Univ_Poly.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/Library/Univ_Poly.thy Wed Oct 10 16:41:19 2012 +0200 @@ -414,7 +414,6 @@ apply (auto simp add: poly_exp poly_mult) done -lemma (in semiring_1) one_neq_zero[simp]: "1 \ 0" using zero_neq_one by blast lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \ poly []" apply (simp add: fun_eq) apply (rule_tac x = "minus one a" in exI) diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/NthRoot.thy Wed Oct 10 16:41:19 2012 +0200 @@ -398,9 +398,9 @@ lemma DERIV_real_root_generic: assumes "0 < n" and "x \ 0" - and even: "\ even n ; 0 < x \ \ D = inverse (real n * root n x ^ (n - Suc 0))" - and even: "\ even n ; x < 0 \ \ D = - inverse (real n * root n x ^ (n - Suc 0))" - and odd: "odd n \ D = inverse (real n * root n x ^ (n - Suc 0))" + and "\ even n ; 0 < x \ \ D = inverse (real n * root n x ^ (n - Suc 0))" + and "\ even n ; x < 0 \ \ D = - inverse (real n * root n x ^ (n - Suc 0))" + and "odd n \ D = inverse (real n * root n x ^ (n - Suc 0))" shows "DERIV (root n) x :> D" using assms by (cases "even n", cases "0 < x", auto intro: DERIV_real_root[THEN DERIV_cong] diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 16:41:19 2012 +0200 @@ -84,7 +84,7 @@ later use and is automatically propagated to all its interpretations. Here is another example: *} -statespace 'a varsX = vars [n=N, b=B] + vars + x::'a +statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a text {* \noindent The state space @{text "varsX"} imports two copies of the state space @{text "vars"}, where one has the variables renamed @@ -179,7 +179,7 @@ qed -statespace 'a dup = 'a foo [f=F, a=A] + 'a foo + +statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo + x::int lemma (in dup) diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/Statespace/state_space.ML Wed Oct 10 16:41:19 2012 +0200 @@ -21,18 +21,18 @@ val define_statespace : string list -> string -> - (string list * bstring * (string * string) list) list -> + ((string * bool) * (string list * bstring * (string * string) list)) list -> (string * string) list -> theory -> theory val define_statespace_i : string option -> string list -> string -> - (typ list * bstring * (string * string) list) list -> + ((string * bool) * (typ list * bstring * (string * string) list)) list -> (string * typ) list -> theory -> theory val statespace_decl : ((string list * bstring) * - ((string list * xstring * (bstring * bstring) list) list * + (((string * bool) * (string list * xstring * (bstring * bstring) list)) list * (bstring * string) list)) parser @@ -355,7 +355,7 @@ val inst = map fst args ~~ Ts; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val parent_comps = - maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents; + maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents; val all_comps = rename renaming (parent_comps @ map (apsnd subst) components); in all_comps end; @@ -369,8 +369,8 @@ val components' = map (fn (n,T) => (n,(T,full_name))) components; val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; - fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs)); - (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *) + fun parent_expr (prefix, (_, n, rs)) = + (suffix namespaceN n, (prefix, Expression.Positional rs)); val parents_expr = map parent_expr parents; fun distinct_types Ts = let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty; @@ -386,14 +386,14 @@ fun projectT T = valueT --> T; fun injectT T = T --> valueT; val locinsts = map (fn T => (project_injectL, - (("",false),Expression.Positional + ((encode_type T,false),Expression.Positional [SOME (Free (project_name T,projectT T)), SOME (Free ((inject_name T,injectT T)))]))) Ts; val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn), (Binding.name (inject_name T),NONE,NoSyn)]) Ts; val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts; - fun interprete_parent_valuetypes (Ts, pname, _) thy = + fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy = let val {args,types,...} = the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname); @@ -402,15 +402,15 @@ val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types; val expr = ([(suffix valuetypesN name, - (("",false),Expression.Positional (map SOME pars)))],[]); + (prefix, Expression.Positional (map SOME pars)))],[]); in prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of) (suffix valuetypesN name, expr) thy end; - fun interprete_parent (_, pname, rs) = + fun interprete_parent (prefix, (_, pname, rs)) = let - val expr = ([(pname, (("",false), Expression.Positional rs))],[]) + val expr = ([(pname, (prefix, Expression.Positional rs))],[]) in prove_interpretation_in (fn ctxt => Locale.intro_locales_tac false ctxt []) (full_name, expr) end; @@ -449,7 +449,7 @@ |> namespace_definition (suffix namespaceN name) nameT (parents_expr,[]) (map fst parent_comps) (map fst components) - |> Context.theory_map (add_statespace full_name args parents components []) + |> Context.theory_map (add_statespace full_name args (map snd parents) components []) |> add_locale (suffix valuetypesN name) (locinsts,locs) [] |> Proof_Context.theory_of |> fold interprete_parent_valuetypes parents @@ -495,8 +495,13 @@ val ctxt = Proof_Context.init_global thy; - fun add_parent (Ts,pname,rs) env = + fun add_parent (prefix, (Ts, pname, rs)) env = let + val prefix' = + (case prefix of + ("", mandatory) => (pname, mandatory) + | _ => prefix); + val full_pname = Sign.full_bname thy pname; val {args,components,...} = (case get_statespace (Context.Theory thy) full_pname of @@ -526,8 +531,9 @@ val rs' = map (AList.lookup (op =) rs o fst) components; val errs =err_insts @ err_dup_renamings @ err_rename_unknowns - in if null errs then ((Ts',full_pname,rs'),env') - else error (cat_lines (errs @ ["in parent statespace " ^ quote pname])) + in + if null errs then ((prefix', (Ts', full_pname, rs')), env') + else error (cat_lines (errs @ ["in parent statespace " ^ quote pname])) end; val (parents',env) = fold_map add_parent parents []; @@ -562,7 +568,7 @@ fun fst_eq ((x:string,_),(y,_)) = x = y; fun snd_eq ((_,t:typ),(_,u)) = t = u; - val raw_parent_comps = maps (parent_components thy) parents'; + val raw_parent_comps = maps (parent_components thy o snd) parents'; fun check_type (n,T) = (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of [] => [] @@ -687,8 +693,9 @@ val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) []; val parent = + Parse_Spec.locale_prefix false -- ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames - >> (fn ((insts, name), renames) => (insts,name, renames)); + >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames))); in diff -r 53f14f62cca2 -r 3fc6b3289c31 src/HOL/ex/Tarski.thy --- a/src/HOL/ex/Tarski.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/HOL/ex/Tarski.thy Wed Oct 10 16:41:19 2012 +0200 @@ -119,7 +119,7 @@ locale CL = S + assumes cl_co: "cl : CompleteLattice" -sublocale CL < PO +sublocale CL < po: PO apply (simp_all add: A_def r_def) apply unfold_locales using cl_co unfolding CompleteLattice_def by auto @@ -130,7 +130,7 @@ assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*) defines P_def: "P == fix f A" -sublocale CLF < CL +sublocale CLF < cl: CL apply (simp_all add: A_def r_def) apply unfold_locales using f_cl unfolding CLF_set_def by auto diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/Isar/element.ML Wed Oct 10 16:41:19 2012 +0200 @@ -493,9 +493,9 @@ | init (Defines defs) = Context.map_proof (fn ctxt => let val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs; - val asms = defs' |> map (fn ((name, atts), (t, ps)) => - let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) - in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end); + val asms = defs' |> map (fn (b, (t, ps)) => + let val (_, t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) + in (t', (b, [(t', ps)])) end); val (_, ctxt') = ctxt |> fold Variable.auto_fixes (map #1 asms) |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms); @@ -507,7 +507,13 @@ fun activate_i elem ctxt = let - val elem' = map_ctxt_attrib Args.assignable elem; + val elem' = + (case map_ctxt_attrib Args.assignable elem of + Defines defs => + Defines (defs |> map (fn ((a, atts), (t, ps)) => + ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts), + (t, ps)))) + | e => e); val ctxt' = Context.proof_map (init elem') ctxt; in (map_ctxt_attrib Args.closure elem', ctxt') end; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/Isar/expression.ML Wed Oct 10 16:41:19 2012 +0200 @@ -527,11 +527,11 @@ val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in - case filter (fn (Free (y', _), _) => y = y' | _ => false) env of - [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) | - dups => if forall (fn (_, b'') => b' aconv b'') dups - then (xs, env, eqs) - else err "Attempt to redefine variable" + (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of + [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) + | dups => + if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs) + else err "Attempt to redefine variable") end; (* text has the following structure: diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/Isar/local_defs.ML Wed Oct 10 16:41:19 2012 +0200 @@ -89,16 +89,14 @@ fun add_defs defs ctxt = let val ((xs, mxs), specs) = defs |> split_list |>> split_list; - val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; - val names = map2 Thm.def_binding_optional xs bfacts; + val (bs, rhss) = specs |> split_list; val eqs = mk_def ctxt (xs ~~ rhss); val lhss = map (fst o Logic.dest_equals) eqs; in ctxt |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 |> fold Variable.declare_term eqs - |> Proof_Context.add_assms_i def_export - (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs) + |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs) |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss end; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/Isar/parse_spec.ML Wed Oct 10 16:41:19 2012 +0200 @@ -24,8 +24,9 @@ val locale_fixes: (binding * string option * mixfix) list parser val locale_insts: (string option list * (Attrib.binding * string) list) parser val class_expression: string list parser + val locale_prefix: bool -> (string * bool) parser + val locale_keyword: string parser val locale_expression: bool -> Expression.expression parser - val locale_keyword: string parser val context_element: Element.context parser val statement: (Attrib.binding * (string * string list) list) list parser val general_statement: (Element.context list * Element.statement) parser @@ -113,17 +114,19 @@ fun plus1_unless test scan = scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); -fun prefix mandatory = - Parse.name -- - (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| - Parse.$$$ ":"; - val instance = Parse.where_ |-- Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; in +fun locale_prefix mandatory = + Scan.optional + (Parse.name -- + (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| + Parse.$$$ ":") + ("", false); + val locale_keyword = Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" || Parse.$$$ "defines" || Parse.$$$ "notes"; @@ -133,7 +136,7 @@ fun locale_expression mandatory = let val expr2 = Parse.position Parse.xname; - val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 -- + val expr1 = locale_prefix mandatory -- expr2 -- Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); val expr0 = plus1_unless locale_keyword expr1; in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/Isar/proof.ML Wed Oct 10 16:41:19 2012 +0200 @@ -643,7 +643,11 @@ |>> map (fn (x, _, mx) => (x, mx)) |-> (fn vars => map_context_result (prep_binds false (map swap raw_rhss)) - #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss))))) + #-> (fn rhss => + let + val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) => + ((x, mx), ((Thm.def_binding_optional x a, atts), rhs))); + in map_context_result (Local_Defs.add_defs defs) end)) |-> (set_facts o map (#2 o #2)) end; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Oct 10 16:41:19 2012 +0200 @@ -938,8 +938,8 @@ local fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b)) - | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts - (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd); + | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts + (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd); in @@ -952,12 +952,12 @@ val (res, ctxt') = fold_map app facts ctxt; val thms = Global_Theory.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; - in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end); + in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end); -fun put_thms do_props thms ctxt = ctxt +fun put_thms index thms ctxt = ctxt |> map_naming (K Name_Space.local_naming) |> Context_Position.set_visible false - |> update_thms do_props (apfst Binding.name thms) + |> update_thms {strict = false, index = index} (apfst Binding.name thms) |> Context_Position.restore_visible ctxt |> restore_naming ctxt; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/facts.ML --- a/src/Pure/facts.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/facts.ML Wed Oct 10 16:41:19 2012 +0200 @@ -32,8 +32,8 @@ val props: T -> thm list val could_unify: T -> term -> thm list val merge: T * T -> T - val add_global: Context.generic -> binding * thm list -> T -> string * T - val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T + val add_static: Context.generic -> {strict: bool, index: bool} -> + binding * thm list -> T -> string * T val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T val del: string -> T -> T val hide: bool -> string -> T -> T @@ -188,26 +188,15 @@ (* add static entries *) -local - -fun add context strict do_props (b, ths) (Facts {facts, props}) = +fun add_static context {strict, index} (b, ths) (Facts {facts, props}) = let val (name, facts') = if Binding.is_empty b then ("", facts) else Name_Space.define context strict (b, Static ths) facts; - val props' = - if do_props - then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props - else props; + val props' = props + |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths; in (name, make_facts facts' props') end; -in - -fun add_global context = add context true false; -fun add_local context = add context false; - -end; - (* add dynamic entries *) diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Pure/global_theory.ML Wed Oct 10 16:41:19 2012 +0200 @@ -134,7 +134,8 @@ val name = Sign.full_name thy b; val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs; val thms'' = map (Thm.transfer thy') thms'; - val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd); + val thy'' = thy' |> Data.map + (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd); in (thms'', thy'') end; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/Tools/induct.ML --- a/src/Tools/induct.ML Wed Oct 10 16:18:27 2012 +0200 +++ b/src/Tools/induct.ML Wed Oct 10 16:41:19 2012 +0200 @@ -705,15 +705,15 @@ fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt) | add (SOME (SOME x, (t, _))) ctxt = let val ([(lhs, (_, th))], ctxt') = - Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt + Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt in ((SOME lhs, [th]), ctxt') end | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) | add (SOME (NONE, (t, _))) ctxt = let val (s, _) = Name.variant "x" (Variable.names_of ctxt); - val ([(lhs, (_, th))], ctxt') = - Local_Defs.add_defs [((Binding.name s, NoSyn), - (Thm.empty_binding, t))] ctxt + val x = Binding.name s; + val ([(lhs, (_, th))], ctxt') = ctxt + |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))]; in ((SOME lhs, [th]), ctxt') end | add NONE ctxt = ((NONE, []), ctxt); in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; diff -r 53f14f62cca2 -r 3fc6b3289c31 src/ZF/ex/Group.thy --- a/src/ZF/ex/Group.thy Wed Oct 10 16:18:27 2012 +0200 +++ b/src/ZF/ex/Group.thy Wed Oct 10 16:41:19 2012 +0200 @@ -203,11 +203,11 @@ qed lemma (in group) inv_comm: - assumes inv: "x \ y = \" + assumes "x \ y = \" and G: "x \ carrier(G)" "y \ carrier(G)" shows "y \ x = \" proof - - from G have "x \ y \ x = x \ \" by (auto simp add: inv) + from G have "x \ y \ x = x \ \" by (auto simp add: assms) with G show ?thesis by (simp del: r_one add: m_assoc) qed @@ -490,11 +490,12 @@ lemma (in group) subgroupI: assumes subset: "H \ carrier(G)" and non_empty: "H \ 0" - and inv: "!!a. a \ H ==> inv a \ H" - and mult: "!!a b. [|a \ H; b \ H|] ==> a \ b \ H" + and "!!a. a \ H ==> inv a \ H" + and "!!a b. [|a \ H; b \ H|] ==> a \ b \ H" shows "subgroup(H,G)" proof (simp add: subgroup_def assms) - show "\ \ H" by (rule one_in_subset) (auto simp only: assms) + show "\ \ H" + by (rule one_in_subset) (auto simp only: assms) qed @@ -595,7 +596,7 @@ "set_inv\<^bsub>G\<^esub> H == \h\H. {inv\<^bsub>G\<^esub> h}" -locale normal = subgroup + group + +locale normal = subgroup: subgroup + group + assumes coset_eq: "(\x \ carrier(G). H #> x = x <# H)" notation