1.1 --- a/src/Cube/Cube.thy Wed Oct 10 16:18:27 2012 +0200
1.2 +++ b/src/Cube/Cube.thy Wed Oct 10 16:41:19 2012 +0200
1.3 @@ -10,6 +10,15 @@
1.4
1.5 setup Pure_Thy.old_appl_syntax_setup
1.6
1.7 +ML {*
1.8 + structure Rules = Named_Thms
1.9 + (
1.10 + val name = @{binding rules}
1.11 + val description = "Cube inference rules"
1.12 + )
1.13 +*}
1.14 +setup Rules.setup
1.15 +
1.16 typedecl "term"
1.17 typedecl "context"
1.18 typedecl typing
1.19 @@ -72,8 +81,7 @@
1.20
1.21 beta: "Abs(A, f)^a == f(a)"
1.22
1.23 -lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
1.24 -lemmas rules = simple
1.25 +lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
1.26
1.27 lemma imp_elim:
1.28 assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P"
1.29 @@ -90,7 +98,7 @@
1.30 ==> Abs(A,f) : Prod(A,B)"
1.31 begin
1.32
1.33 -lemmas rules = simple lam_bs pi_bs
1.34 +lemmas [rules] = lam_bs pi_bs
1.35
1.36 end
1.37
1.38 @@ -102,7 +110,7 @@
1.39 ==> Abs(A,f) : Prod(A,B)"
1.40 begin
1.41
1.42 -lemmas rules = simple lam_bb pi_bb
1.43 +lemmas [rules] = lam_bb pi_bb
1.44
1.45 end
1.46
1.47 @@ -113,7 +121,7 @@
1.48 ==> Abs(A,f) : Prod(A,B)"
1.49 begin
1.50
1.51 -lemmas rules = simple lam_sb pi_sb
1.52 +lemmas [rules] = lam_sb pi_sb
1.53
1.54 end
1.55
1.56 @@ -121,7 +129,7 @@
1.57 locale LP2 = LP + L2
1.58 begin
1.59
1.60 -lemmas rules = simple lam_bs pi_bs lam_sb pi_sb
1.61 +lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
1.62
1.63 end
1.64
1.65 @@ -129,7 +137,7 @@
1.66 locale Lomega2 = L2 + Lomega
1.67 begin
1.68
1.69 -lemmas rules = simple lam_bs pi_bs lam_bb pi_bb
1.70 +lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
1.71
1.72 end
1.73
1.74 @@ -137,7 +145,7 @@
1.75 locale LPomega = LP + Lomega
1.76 begin
1.77
1.78 -lemmas rules = simple lam_bb pi_bb lam_sb pi_sb
1.79 +lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
1.80
1.81 end
1.82
1.83 @@ -145,7 +153,7 @@
1.84 locale CC = L2 + LP + Lomega
1.85 begin
1.86
1.87 -lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
1.88 +lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
1.89
1.90 end
1.91
2.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 16:18:27 2012 +0200
2.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 16:41:19 2012 +0200
2.3 @@ -104,7 +104,7 @@
2.4 end
2.5 print_locale! logic
2.6
2.7 -locale use_decl = logic + semi "op ||"
2.8 +locale use_decl = l: logic + semi "op ||"
2.9 print_locale! use_decl thm use_decl_def
2.10
2.11 locale extra_type =
3.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 16:18:27 2012 +0200
3.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 16:41:19 2012 +0200
3.3 @@ -273,7 +273,7 @@
3.4
3.5
3.6 lemma embed_underS:
3.7 -assumes WELL: "Well_order r" and WELL: "Well_order r'" and
3.8 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
3.9 EMB: "embed r r' f" and IN: "a \<in> Field r"
3.10 shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
3.11 proof-
4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 16:18:27 2012 +0200
4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 16:41:19 2012 +0200
4.3 @@ -452,7 +452,7 @@
4.4 assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
4.5 and between_same: "between x x = x"
4.6
4.7 -sublocale constr_dense_linorder < dense_linorder
4.8 +sublocale constr_dense_linorder < dlo: dense_linorder
4.9 apply unfold_locales
4.10 using gt_ex lt_ex between_less
4.11 apply auto
5.1 --- a/src/HOL/Finite_Set.thy Wed Oct 10 16:18:27 2012 +0200
5.2 +++ b/src/HOL/Finite_Set.thy Wed Oct 10 16:41:19 2012 +0200
5.3 @@ -1757,7 +1757,7 @@
5.4 locale folding_image_simple_idem = folding_image_simple +
5.5 assumes idem: "x * x = x"
5.6
5.7 -sublocale folding_image_simple_idem < semilattice proof
5.8 +sublocale folding_image_simple_idem < semilattice: semilattice proof
5.9 qed (fact idem)
5.10
5.11 context folding_image_simple_idem
5.12 @@ -1898,7 +1898,7 @@
5.13 locale folding_one_idem = folding_one +
5.14 assumes idem: "x * x = x"
5.15
5.16 -sublocale folding_one_idem < semilattice proof
5.17 +sublocale folding_one_idem < semilattice: semilattice proof
5.18 qed (fact idem)
5.19
5.20 context folding_one_idem
6.1 --- a/src/HOL/Library/Univ_Poly.thy Wed Oct 10 16:18:27 2012 +0200
6.2 +++ b/src/HOL/Library/Univ_Poly.thy Wed Oct 10 16:41:19 2012 +0200
6.3 @@ -414,7 +414,6 @@
6.4 apply (auto simp add: poly_exp poly_mult)
6.5 done
6.6
6.7 -lemma (in semiring_1) one_neq_zero[simp]: "1 \<noteq> 0" using zero_neq_one by blast
6.8 lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []"
6.9 apply (simp add: fun_eq)
6.10 apply (rule_tac x = "minus one a" in exI)
7.1 --- a/src/HOL/NthRoot.thy Wed Oct 10 16:18:27 2012 +0200
7.2 +++ b/src/HOL/NthRoot.thy Wed Oct 10 16:41:19 2012 +0200
7.3 @@ -398,9 +398,9 @@
7.4
7.5 lemma DERIV_real_root_generic:
7.6 assumes "0 < n" and "x \<noteq> 0"
7.7 - and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
7.8 - and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
7.9 - and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
7.10 + and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
7.11 + and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
7.12 + and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
7.13 shows "DERIV (root n) x :> D"
7.14 using assms by (cases "even n", cases "0 < x",
7.15 auto intro: DERIV_real_root[THEN DERIV_cong]
8.1 --- a/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 16:18:27 2012 +0200
8.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 10 16:41:19 2012 +0200
8.3 @@ -84,7 +84,7 @@
8.4 later use and is automatically propagated to all its interpretations.
8.5 Here is another example: *}
8.6
8.7 -statespace 'a varsX = vars [n=N, b=B] + vars + x::'a
8.8 +statespace 'a varsX = NB: vars [n=N, b=B] + vars + x::'a
8.9
8.10 text {* \noindent The state space @{text "varsX"} imports two copies
8.11 of the state space @{text "vars"}, where one has the variables renamed
8.12 @@ -179,7 +179,7 @@
8.13 qed
8.14
8.15
8.16 -statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +
8.17 +statespace 'a dup = FA: 'a foo [f=F, a=A] + 'a foo +
8.18 x::int
8.19
8.20 lemma (in dup)
9.1 --- a/src/HOL/Statespace/state_space.ML Wed Oct 10 16:18:27 2012 +0200
9.2 +++ b/src/HOL/Statespace/state_space.ML Wed Oct 10 16:41:19 2012 +0200
9.3 @@ -21,18 +21,18 @@
9.4 val define_statespace :
9.5 string list ->
9.6 string ->
9.7 - (string list * bstring * (string * string) list) list ->
9.8 + ((string * bool) * (string list * bstring * (string * string) list)) list ->
9.9 (string * string) list -> theory -> theory
9.10 val define_statespace_i :
9.11 string option ->
9.12 string list ->
9.13 string ->
9.14 - (typ list * bstring * (string * string) list) list ->
9.15 + ((string * bool) * (typ list * bstring * (string * string) list)) list ->
9.16 (string * typ) list -> theory -> theory
9.17
9.18 val statespace_decl :
9.19 ((string list * bstring) *
9.20 - ((string list * xstring * (bstring * bstring) list) list *
9.21 + (((string * bool) * (string list * xstring * (bstring * bstring) list)) list *
9.22 (bstring * string) list)) parser
9.23
9.24
9.25 @@ -355,7 +355,7 @@
9.26 val inst = map fst args ~~ Ts;
9.27 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
9.28 val parent_comps =
9.29 - maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
9.30 + maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents;
9.31 val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
9.32 in all_comps end;
9.33
9.34 @@ -369,8 +369,8 @@
9.35 val components' = map (fn (n,T) => (n,(T,full_name))) components;
9.36 val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
9.37
9.38 - fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs));
9.39 - (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *)
9.40 + fun parent_expr (prefix, (_, n, rs)) =
9.41 + (suffix namespaceN n, (prefix, Expression.Positional rs));
9.42 val parents_expr = map parent_expr parents;
9.43 fun distinct_types Ts =
9.44 let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty;
9.45 @@ -386,14 +386,14 @@
9.46 fun projectT T = valueT --> T;
9.47 fun injectT T = T --> valueT;
9.48 val locinsts = map (fn T => (project_injectL,
9.49 - (("",false),Expression.Positional
9.50 + ((encode_type T,false),Expression.Positional
9.51 [SOME (Free (project_name T,projectT T)),
9.52 SOME (Free ((inject_name T,injectT T)))]))) Ts;
9.53 val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
9.54 (Binding.name (inject_name T),NONE,NoSyn)]) Ts;
9.55 val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
9.56
9.57 - fun interprete_parent_valuetypes (Ts, pname, _) thy =
9.58 + fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy =
9.59 let
9.60 val {args,types,...} =
9.61 the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
9.62 @@ -402,15 +402,15 @@
9.63 val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
9.64
9.65 val expr = ([(suffix valuetypesN name,
9.66 - (("",false),Expression.Positional (map SOME pars)))],[]);
9.67 + (prefix, Expression.Positional (map SOME pars)))],[]);
9.68 in
9.69 prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
9.70 (suffix valuetypesN name, expr) thy
9.71 end;
9.72
9.73 - fun interprete_parent (_, pname, rs) =
9.74 + fun interprete_parent (prefix, (_, pname, rs)) =
9.75 let
9.76 - val expr = ([(pname, (("",false), Expression.Positional rs))],[])
9.77 + val expr = ([(pname, (prefix, Expression.Positional rs))],[])
9.78 in prove_interpretation_in
9.79 (fn ctxt => Locale.intro_locales_tac false ctxt [])
9.80 (full_name, expr) end;
9.81 @@ -449,7 +449,7 @@
9.82 |> namespace_definition
9.83 (suffix namespaceN name) nameT (parents_expr,[])
9.84 (map fst parent_comps) (map fst components)
9.85 - |> Context.theory_map (add_statespace full_name args parents components [])
9.86 + |> Context.theory_map (add_statespace full_name args (map snd parents) components [])
9.87 |> add_locale (suffix valuetypesN name) (locinsts,locs) []
9.88 |> Proof_Context.theory_of
9.89 |> fold interprete_parent_valuetypes parents
9.90 @@ -495,8 +495,13 @@
9.91
9.92 val ctxt = Proof_Context.init_global thy;
9.93
9.94 - fun add_parent (Ts,pname,rs) env =
9.95 + fun add_parent (prefix, (Ts, pname, rs)) env =
9.96 let
9.97 + val prefix' =
9.98 + (case prefix of
9.99 + ("", mandatory) => (pname, mandatory)
9.100 + | _ => prefix);
9.101 +
9.102 val full_pname = Sign.full_bname thy pname;
9.103 val {args,components,...} =
9.104 (case get_statespace (Context.Theory thy) full_pname of
9.105 @@ -526,8 +531,9 @@
9.106
9.107 val rs' = map (AList.lookup (op =) rs o fst) components;
9.108 val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
9.109 - in if null errs then ((Ts',full_pname,rs'),env')
9.110 - else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
9.111 + in
9.112 + if null errs then ((prefix', (Ts', full_pname, rs')), env')
9.113 + else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
9.114 end;
9.115
9.116 val (parents',env) = fold_map add_parent parents [];
9.117 @@ -562,7 +568,7 @@
9.118 fun fst_eq ((x:string,_),(y,_)) = x = y;
9.119 fun snd_eq ((_,t:typ),(_,u)) = t = u;
9.120
9.121 - val raw_parent_comps = maps (parent_components thy) parents';
9.122 + val raw_parent_comps = maps (parent_components thy o snd) parents';
9.123 fun check_type (n,T) =
9.124 (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
9.125 [] => []
9.126 @@ -687,8 +693,9 @@
9.127 val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
9.128
9.129 val parent =
9.130 + Parse_Spec.locale_prefix false --
9.131 ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
9.132 - >> (fn ((insts, name), renames) => (insts,name, renames));
9.133 + >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
9.134
9.135 in
9.136
10.1 --- a/src/HOL/ex/Tarski.thy Wed Oct 10 16:18:27 2012 +0200
10.2 +++ b/src/HOL/ex/Tarski.thy Wed Oct 10 16:41:19 2012 +0200
10.3 @@ -119,7 +119,7 @@
10.4 locale CL = S +
10.5 assumes cl_co: "cl : CompleteLattice"
10.6
10.7 -sublocale CL < PO
10.8 +sublocale CL < po: PO
10.9 apply (simp_all add: A_def r_def)
10.10 apply unfold_locales
10.11 using cl_co unfolding CompleteLattice_def by auto
10.12 @@ -130,7 +130,7 @@
10.13 assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
10.14 defines P_def: "P == fix f A"
10.15
10.16 -sublocale CLF < CL
10.17 +sublocale CLF < cl: CL
10.18 apply (simp_all add: A_def r_def)
10.19 apply unfold_locales
10.20 using f_cl unfolding CLF_set_def by auto
11.1 --- a/src/Pure/Isar/element.ML Wed Oct 10 16:18:27 2012 +0200
11.2 +++ b/src/Pure/Isar/element.ML Wed Oct 10 16:41:19 2012 +0200
11.3 @@ -493,9 +493,9 @@
11.4 | init (Defines defs) = Context.map_proof (fn ctxt =>
11.5 let
11.6 val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
11.7 - val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
11.8 - let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
11.9 - in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
11.10 + val asms = defs' |> map (fn (b, (t, ps)) =>
11.11 + let val (_, t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
11.12 + in (t', (b, [(t', ps)])) end);
11.13 val (_, ctxt') = ctxt
11.14 |> fold Variable.auto_fixes (map #1 asms)
11.15 |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
11.16 @@ -507,7 +507,13 @@
11.17
11.18 fun activate_i elem ctxt =
11.19 let
11.20 - val elem' = map_ctxt_attrib Args.assignable elem;
11.21 + val elem' =
11.22 + (case map_ctxt_attrib Args.assignable elem of
11.23 + Defines defs =>
11.24 + Defines (defs |> map (fn ((a, atts), (t, ps)) =>
11.25 + ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
11.26 + (t, ps))))
11.27 + | e => e);
11.28 val ctxt' = Context.proof_map (init elem') ctxt;
11.29 in (map_ctxt_attrib Args.closure elem', ctxt') end;
11.30
12.1 --- a/src/Pure/Isar/expression.ML Wed Oct 10 16:18:27 2012 +0200
12.2 +++ b/src/Pure/Isar/expression.ML Wed Oct 10 16:41:19 2012 +0200
12.3 @@ -527,11 +527,11 @@
12.4 val b' = norm_term env b;
12.5 fun err msg = error (msg ^ ": " ^ quote y);
12.6 in
12.7 - case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
12.8 - [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) |
12.9 - dups => if forall (fn (_, b'') => b' aconv b'') dups
12.10 - then (xs, env, eqs)
12.11 - else err "Attempt to redefine variable"
12.12 + (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
12.13 + [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
12.14 + | dups =>
12.15 + if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
12.16 + else err "Attempt to redefine variable")
12.17 end;
12.18
12.19 (* text has the following structure:
13.1 --- a/src/Pure/Isar/local_defs.ML Wed Oct 10 16:18:27 2012 +0200
13.2 +++ b/src/Pure/Isar/local_defs.ML Wed Oct 10 16:41:19 2012 +0200
13.3 @@ -89,16 +89,14 @@
13.4 fun add_defs defs ctxt =
13.5 let
13.6 val ((xs, mxs), specs) = defs |> split_list |>> split_list;
13.7 - val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
13.8 - val names = map2 Thm.def_binding_optional xs bfacts;
13.9 + val (bs, rhss) = specs |> split_list;
13.10 val eqs = mk_def ctxt (xs ~~ rhss);
13.11 val lhss = map (fst o Logic.dest_equals) eqs;
13.12 in
13.13 ctxt
13.14 |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
13.15 |> fold Variable.declare_term eqs
13.16 - |> Proof_Context.add_assms_i def_export
13.17 - (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
13.18 + |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs)
13.19 |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
13.20 end;
13.21
14.1 --- a/src/Pure/Isar/parse_spec.ML Wed Oct 10 16:18:27 2012 +0200
14.2 +++ b/src/Pure/Isar/parse_spec.ML Wed Oct 10 16:41:19 2012 +0200
14.3 @@ -24,8 +24,9 @@
14.4 val locale_fixes: (binding * string option * mixfix) list parser
14.5 val locale_insts: (string option list * (Attrib.binding * string) list) parser
14.6 val class_expression: string list parser
14.7 + val locale_prefix: bool -> (string * bool) parser
14.8 + val locale_keyword: string parser
14.9 val locale_expression: bool -> Expression.expression parser
14.10 - val locale_keyword: string parser
14.11 val context_element: Element.context parser
14.12 val statement: (Attrib.binding * (string * string list) list) list parser
14.13 val general_statement: (Element.context list * Element.statement) parser
14.14 @@ -113,17 +114,19 @@
14.15 fun plus1_unless test scan =
14.16 scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
14.17
14.18 -fun prefix mandatory =
14.19 - Parse.name --
14.20 - (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
14.21 - Parse.$$$ ":";
14.22 -
14.23 val instance = Parse.where_ |--
14.24 Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
14.25 Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
14.26
14.27 in
14.28
14.29 +fun locale_prefix mandatory =
14.30 + Scan.optional
14.31 + (Parse.name --
14.32 + (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
14.33 + Parse.$$$ ":")
14.34 + ("", false);
14.35 +
14.36 val locale_keyword =
14.37 Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
14.38 Parse.$$$ "defines" || Parse.$$$ "notes";
14.39 @@ -133,7 +136,7 @@
14.40 fun locale_expression mandatory =
14.41 let
14.42 val expr2 = Parse.position Parse.xname;
14.43 - val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
14.44 + val expr1 = locale_prefix mandatory -- expr2 --
14.45 Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
14.46 val expr0 = plus1_unless locale_keyword expr1;
14.47 in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
15.1 --- a/src/Pure/Isar/proof.ML Wed Oct 10 16:18:27 2012 +0200
15.2 +++ b/src/Pure/Isar/proof.ML Wed Oct 10 16:41:19 2012 +0200
15.3 @@ -643,7 +643,11 @@
15.4 |>> map (fn (x, _, mx) => (x, mx))
15.5 |-> (fn vars =>
15.6 map_context_result (prep_binds false (map swap raw_rhss))
15.7 - #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
15.8 + #-> (fn rhss =>
15.9 + let
15.10 + val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
15.11 + ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
15.12 + in map_context_result (Local_Defs.add_defs defs) end))
15.13 |-> (set_facts o map (#2 o #2))
15.14 end;
15.15
16.1 --- a/src/Pure/Isar/proof_context.ML Wed Oct 10 16:18:27 2012 +0200
16.2 +++ b/src/Pure/Isar/proof_context.ML Wed Oct 10 16:41:19 2012 +0200
16.3 @@ -938,8 +938,8 @@
16.4 local
16.5
16.6 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
16.7 - | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
16.8 - (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
16.9 + | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
16.10 + (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
16.11
16.12 in
16.13
16.14 @@ -952,12 +952,12 @@
16.15 val (res, ctxt') = fold_map app facts ctxt;
16.16 val thms = Global_Theory.name_thms false false name (flat res);
16.17 val Mode {stmt, ...} = get_mode ctxt;
16.18 - in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
16.19 + in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
16.20
16.21 -fun put_thms do_props thms ctxt = ctxt
16.22 +fun put_thms index thms ctxt = ctxt
16.23 |> map_naming (K Name_Space.local_naming)
16.24 |> Context_Position.set_visible false
16.25 - |> update_thms do_props (apfst Binding.name thms)
16.26 + |> update_thms {strict = false, index = index} (apfst Binding.name thms)
16.27 |> Context_Position.restore_visible ctxt
16.28 |> restore_naming ctxt;
16.29
17.1 --- a/src/Pure/facts.ML Wed Oct 10 16:18:27 2012 +0200
17.2 +++ b/src/Pure/facts.ML Wed Oct 10 16:41:19 2012 +0200
17.3 @@ -32,8 +32,8 @@
17.4 val props: T -> thm list
17.5 val could_unify: T -> term -> thm list
17.6 val merge: T * T -> T
17.7 - val add_global: Context.generic -> binding * thm list -> T -> string * T
17.8 - val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
17.9 + val add_static: Context.generic -> {strict: bool, index: bool} ->
17.10 + binding * thm list -> T -> string * T
17.11 val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
17.12 val del: string -> T -> T
17.13 val hide: bool -> string -> T -> T
17.14 @@ -188,26 +188,15 @@
17.15
17.16 (* add static entries *)
17.17
17.18 -local
17.19 -
17.20 -fun add context strict do_props (b, ths) (Facts {facts, props}) =
17.21 +fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
17.22 let
17.23 val (name, facts') =
17.24 if Binding.is_empty b then ("", facts)
17.25 else Name_Space.define context strict (b, Static ths) facts;
17.26 - val props' =
17.27 - if do_props
17.28 - then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
17.29 - else props;
17.30 + val props' = props
17.31 + |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
17.32 in (name, make_facts facts' props') end;
17.33
17.34 -in
17.35 -
17.36 -fun add_global context = add context true false;
17.37 -fun add_local context = add context false;
17.38 -
17.39 -end;
17.40 -
17.41
17.42 (* add dynamic entries *)
17.43
18.1 --- a/src/Pure/global_theory.ML Wed Oct 10 16:18:27 2012 +0200
18.2 +++ b/src/Pure/global_theory.ML Wed Oct 10 16:41:19 2012 +0200
18.3 @@ -134,7 +134,8 @@
18.4 val name = Sign.full_name thy b;
18.5 val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
18.6 val thms'' = map (Thm.transfer thy') thms';
18.7 - val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
18.8 + val thy'' = thy' |> Data.map
18.9 + (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd);
18.10 in (thms'', thy'') end;
18.11
18.12
19.1 --- a/src/Tools/induct.ML Wed Oct 10 16:18:27 2012 +0200
19.2 +++ b/src/Tools/induct.ML Wed Oct 10 16:41:19 2012 +0200
19.3 @@ -705,15 +705,15 @@
19.4 fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
19.5 | add (SOME (SOME x, (t, _))) ctxt =
19.6 let val ([(lhs, (_, th))], ctxt') =
19.7 - Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
19.8 + Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
19.9 in ((SOME lhs, [th]), ctxt') end
19.10 | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
19.11 | add (SOME (NONE, (t, _))) ctxt =
19.12 let
19.13 val (s, _) = Name.variant "x" (Variable.names_of ctxt);
19.14 - val ([(lhs, (_, th))], ctxt') =
19.15 - Local_Defs.add_defs [((Binding.name s, NoSyn),
19.16 - (Thm.empty_binding, t))] ctxt
19.17 + val x = Binding.name s;
19.18 + val ([(lhs, (_, th))], ctxt') = ctxt
19.19 + |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
19.20 in ((SOME lhs, [th]), ctxt') end
19.21 | add NONE ctxt = ((NONE, []), ctxt);
19.22 in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
20.1 --- a/src/ZF/ex/Group.thy Wed Oct 10 16:18:27 2012 +0200
20.2 +++ b/src/ZF/ex/Group.thy Wed Oct 10 16:41:19 2012 +0200
20.3 @@ -203,11 +203,11 @@
20.4 qed
20.5
20.6 lemma (in group) inv_comm:
20.7 - assumes inv: "x \<cdot> y = \<one>"
20.8 + assumes "x \<cdot> y = \<one>"
20.9 and G: "x \<in> carrier(G)" "y \<in> carrier(G)"
20.10 shows "y \<cdot> x = \<one>"
20.11 proof -
20.12 - from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
20.13 + from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: assms)
20.14 with G show ?thesis by (simp del: r_one add: m_assoc)
20.15 qed
20.16
20.17 @@ -490,11 +490,12 @@
20.18
20.19 lemma (in group) subgroupI:
20.20 assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
20.21 - and inv: "!!a. a \<in> H ==> inv a \<in> H"
20.22 - and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
20.23 + and "!!a. a \<in> H ==> inv a \<in> H"
20.24 + and "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
20.25 shows "subgroup(H,G)"
20.26 proof (simp add: subgroup_def assms)
20.27 - show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
20.28 + show "\<one> \<in> H"
20.29 + by (rule one_in_subset) (auto simp only: assms)
20.30 qed
20.31
20.32
20.33 @@ -595,7 +596,7 @@
20.34 "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
20.35
20.36
20.37 -locale normal = subgroup + group +
20.38 +locale normal = subgroup: subgroup + group +
20.39 assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
20.40
20.41 notation