# HG changeset patch # User ballarin # Date 1228916715 -3600 # Node ID df1113d916db73bcdc8f2b6a62da441fdce905f6 # Parent b0a0843dfd9905648a7823e1a5eadf7d8c55ae92# Parent 501780b0bcae45f2940ae3fef15ad9ef094a72b7 Merged. diff -r 501780b0bcae -r df1113d916db src/FOL/ex/NewLocaleSetup.thy --- a/src/FOL/ex/NewLocaleSetup.thy Wed Dec 10 10:28:16 2008 +0100 +++ b/src/FOL/ex/NewLocaleSetup.thy Wed Dec 10 14:45:15 2008 +0100 @@ -16,7 +16,7 @@ val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; val locale_val = - Expression.parse_expression -- + SpecParse.locale_expression -- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || Scan.repeat1 SpecParse.context_element >> pair ([], []); @@ -27,7 +27,9 @@ (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin >> (fn ((name, (expr, elems)), begin) => (begin ? Toplevel.print) o Toplevel.begin_local_theory begin - (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin))); + (Expression.add_locale_cmd name name expr elems #> + (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes)))); val _ = OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag @@ -42,7 +44,7 @@ val _ = OuterSyntax.command "interpretation" "prove interpretation of locale expression in theory" K.thy_goal - (P.!!! Expression.parse_expression + (P.!!! SpecParse.locale_expression >> (fn expr => Toplevel.print o Toplevel.theory_to_proof (Expression.interpretation_cmd expr))); @@ -50,7 +52,7 @@ OuterSyntax.command "interpret" "prove interpretation of locale expression in proof context" (K.tag_proof K.prf_goal) - (P.!!! Expression.parse_expression + (P.!!! SpecParse.locale_expression >> (fn expr => Toplevel.print o Toplevel.proof' (fn int => Expression.interpret_cmd expr int))); diff -r 501780b0bcae -r df1113d916db src/FOL/ex/NewLocaleTest.thy --- a/src/FOL/ex/NewLocaleTest.thy Wed Dec 10 10:28:16 2008 +0100 +++ b/src/FOL/ex/NewLocaleTest.thy Wed Dec 10 14:45:15 2008 +0100 @@ -113,6 +113,12 @@ print_locale! use_decl thm use_decl_def +text {* Foundational versions of theorems *} + +thm logic.assoc +thm logic.lor_def + + text {* Defines *} locale logic_def = @@ -124,12 +130,45 @@ defines "x || y == --(-- x && -- y)" begin +thm lor_def +(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *) + +lemma "x || y = --(-- x && --y)" + by (unfold lor_def) (rule refl) + +end + +(* Inheritance of defines *) + +locale logic_def2 = logic_def +begin + lemma "x || y = --(-- x && --y)" by (unfold lor_def) (rule refl) end +text {* Notes *} + +(* A somewhat arcane homomorphism example *) + +definition semi_hom where + "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))" + +lemma semi_hom_mult: + "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))" + by (simp add: semi_hom_def) + +locale semi_hom_loc = prod: semi prod + sum: semi sum + for prod and sum and h + + assumes semi_homh: "semi_hom(prod, sum, h)" + notes semi_hom_mult = semi_hom_mult [OF semi_homh] + +lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" + by (rule semi_hom_mult) + + text {* Theorem statements *} lemma (in lgrp) lcancel: diff -r 501780b0bcae -r df1113d916db src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Dec 10 10:28:16 2008 +0100 +++ b/src/Pure/Isar/class.ML Wed Dec 10 14:45:15 2008 +0100 @@ -394,7 +394,8 @@ end; fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] + intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE + Locale.intro_locales_tac true ctxt [] | default_intro_tac _ _ = no_tac; fun default_tac rules ctxt facts = diff -r 501780b0bcae -r df1113d916db src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Dec 10 10:28:16 2008 +0100 +++ b/src/Pure/Isar/expression.ML Wed Dec 10 14:45:15 2008 +0100 @@ -19,9 +19,11 @@ (* Declaring locales *) val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory -> - string * Proof.context + (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) * + Proof.context val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory -> - string * Proof.context + (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) * + Proof.context (* Interpretation *) val sublocale_cmd: string -> expression -> theory -> Proof.state; @@ -30,10 +32,6 @@ val interpretation: expression_i -> theory -> Proof.state; val interpret_cmd: expression -> bool -> Proof.state -> Proof.state; val interpret: expression_i -> bool -> Proof.state -> Proof.state; - - (* Debugging and development *) - val parse_expression: OuterParse.token list -> expression * OuterParse.token list - (* FIXME to spec_parse.ML *) end; @@ -55,63 +53,6 @@ type expression_i = term expr * (Binding.T * typ option * mixfix) list; -(** Parsing and printing **) - -local - -structure P = OuterParse; - -val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || - P.$$$ "defines" || P.$$$ "notes"; -fun plus1_unless test scan = - scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)); - -val prefix = P.name --| P.$$$ ":"; -val named = P.name -- (P.$$$ "=" |-- P.term); -val position = P.maybe P.term; -val instance = P.$$$ "where" |-- P.and_list1 named >> Named || - Scan.repeat1 position >> Positional; - -in - -val parse_expression = - let - fun expr2 x = P.xname x; - fun expr1 x = (Scan.optional prefix "" -- expr2 -- - Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; - fun expr0 x = (plus1_unless loc_keyword expr1) x; - in expr0 -- P.for_fixes end; - -end; - -fun pretty_expr thy expr = - let - fun pretty_pos NONE = Pretty.str "_" - | pretty_pos (SOME x) = Pretty.str x; - fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=", - Pretty.brk 1, Pretty.str y] |> Pretty.block; - fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |> - map pretty_pos |> Pretty.breaks - | pretty_ren (Named []) = [] - | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 :: - (ps |> map pretty_named |> Pretty.separate "and"); - fun pretty_rename (loc, ("", ren)) = - Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) - | pretty_rename (loc, (prfx, ren)) = - Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) :: - Pretty.brk 1 :: pretty_ren ren); - in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end; - -fun err_in_expr thy msg expr = - let - val err_msg = - if null expr then msg - else msg ^ "\n" ^ Pretty.string_of (Pretty.block - [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1, - pretty_expr thy expr]) - in error err_msg end; - - (** Internalise locale names in expr **) fun intern thy instances = map (apfst (NewLocale.intern thy)) instances; @@ -133,6 +74,13 @@ end; fun match_bind (n, b) = (n = Binding.base_name b); + fun parm_eq ((b1, mx1), (b2, mx2)) = + (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *) + (Binding.base_name b1 = Binding.base_name b2) andalso + (if mx1 = mx2 then true + else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^ + " in expression.")); + fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2); (* FIXME: cannot compare bindings for equality. *) @@ -164,12 +112,7 @@ val (is', ps') = fold_map (fn i => fn ps => let val (ps', i') = params_inst i; - val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) => - (* FIXME: should check for bindings being the same. - Instead we check for equal name and syntax. *) - if mx1 = mx2 then mx1 - else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^ - " in expression.")) (ps, ps') + val ps'' = distinct parm_eq (ps @ ps'); in (i', ps'') end) is [] in (ps', is') end; @@ -329,21 +272,18 @@ val norm_term = Envir.beta_norm oo Term.subst_atomic; -fun abstract_thm thy eq = - Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; - -fun bind_def ctxt eq (xs, env, ths) = +fun bind_def ctxt eq (xs, env, eqs) = let + val _ = LocalDefs.cert_def ctxt eq; val ((y, T), b) = LocalDefs.abs_def eq; val b' = norm_term env b; - val th = abstract_thm (ProofContext.theory_of ctxt) eq; fun err msg = error (msg ^ ": " ^ quote y); in exists (fn (x, _) => x = y) xs andalso err "Attempt to define previously specified variable"; exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso err "Attempt to redefine variable"; - (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) + (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) end; fun eval_text _ _ (Fixes _) text = text @@ -494,8 +434,7 @@ env: list of term pairs encoding substitutions, where the first term is a free variable; substitutions represent defines elements and the rhs is normalised wrt. the previous env - defs: theorems representing the substitutions from defines elements - (thms are normalised wrt. env). + defs: the equations from the defines elements elems is an updated version of raw_elems: - type info added to Fixes and modified in Constrains - axiom and definition statement replaced by corresponding one @@ -548,7 +487,6 @@ NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps; val ((elems', _), _) = activate elems (ProofContext.set_stmt true context'); in ((fixed, deps, elems'), (parms, spec, defs)) end; - (* FIXME check if defs used somewhere *) in @@ -583,7 +521,6 @@ val export = Variable.export_morphism goal_ctxt context; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; -(* val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *) val exp_term = Drule.term_rule thy (singleton exp_fact); val exp_typ = Logic.type_map exp_term; val export' = @@ -687,6 +624,8 @@ fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy = let + val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs; + val (a_pred, a_intro, a_axioms, thy'') = if null exts then (NONE, NONE, [], thy) else @@ -694,7 +633,7 @@ val aname = if null ints then pname else pname ^ "_" ^ axiomsN; val ((statement, intro, axioms), thy') = thy - |> def_pred aname parms defs exts exts'; + |> def_pred aname parms defs' exts exts'; val (_, thy'') = thy' |> Sign.add_path aname @@ -709,7 +648,7 @@ let val ((statement, intro, axioms), thy''') = thy'' - |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred); + |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val (_, thy'''') = thy''' |> Sign.add_path pname @@ -734,15 +673,10 @@ |> apfst (curry Notes Thm.assumptionK) | assumes_to_notes e axms = (e, axms); -fun defines_to_notes thy (Defines defs) defns = - let - val defs' = map (fn (_, (def, _)) => def) defs - val notes = map (fn (a, (def, _)) => - (a, [([Assumption.assume (cterm_of thy def)], [])])) defs - in - (Notes (Thm.definitionK, notes), defns @ defs') - end - | defines_to_notes _ e defns = (e, defns); +fun defines_to_notes thy (Defines defs) = + Notes (Thm.definitionK, map (fn (a, (def, _)) => + (a, [([Assumption.assume (cterm_of thy def)], [])])) defs) + | defines_to_notes _ e = e; fun gen_add_locale prep_decl bname predicate_name raw_imprt raw_body thy = @@ -751,7 +685,7 @@ val _ = NewLocale.test_locale thy name andalso error ("Duplicate definition of locale " ^ quote name); - val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), _)) = + val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) = prep_decl raw_imprt raw_body (ProofContext.init thy); val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_name text thy; @@ -760,29 +694,39 @@ val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ quote bname); - val satisfy = Element.satisfy_morphism b_axioms; + val a_satisfy = Element.satisfy_morphism a_axioms; + val b_satisfy = Element.satisfy_morphism b_axioms; val params = fixed @ (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat); val asm = if is_some b_statement then b_statement else a_statement; - val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems []; - val notes = body_elems' |> + + (* These are added immediately. *) + val notes = + if is_some asm + then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []), + [([Assumption.assume (cterm_of thy' (the asm))], + [(Attrib.internal o K) NewLocale.witness_attrib])])])] + else []; + + (* These will be added in the local theory. *) + val notes' = body_elems |> + map (defines_to_notes thy') |> + map (Element.morph_ctxt a_satisfy) |> (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |> - fst |> map (Element.morph_ctxt satisfy) |> - map_filter (fn Notes notes => SOME notes | _ => NONE) |> - (if is_some asm - then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []), - [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])]) - else I); + fst |> + map (Element.morph_ctxt b_satisfy) |> + map_filter (fn Notes notes => SOME notes | _ => NONE); - val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps; + val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; val loc_ctxt = thy' |> NewLocale.register_locale bname (extraTs, params) - (asm, defns) ([], []) + (asm, rev defs) ([], []) (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |> - NewLocale.init name - in (name, loc_ctxt) end; + NewLocale.init name; + + in ((name, notes'), loc_ctxt) end; in diff -r 501780b0bcae -r df1113d916db src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Dec 10 10:28:16 2008 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Dec 10 14:45:15 2008 +0100 @@ -401,7 +401,7 @@ val _ = OuterSyntax.command "sublocale" "prove sublocale relation between a locale and a locale expression" K.thy_goal - (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! Expression.parse_expression + (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! SpecParse.locale_expression >> (fn (loc, expr) => Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)))); diff -r 501780b0bcae -r df1113d916db src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Wed Dec 10 10:28:16 2008 +0100 +++ b/src/Pure/Isar/new_locale.ML Wed Dec 10 14:45:15 2008 +0100 @@ -39,7 +39,6 @@ Proof.context -> Proof.context val activate_global_facts: string * Morphism.morphism -> theory -> theory val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context -(* val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *) val init: string -> theory -> Proof.context (* Reasoning about locales *) diff -r 501780b0bcae -r df1113d916db src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Wed Dec 10 10:28:16 2008 +0100 +++ b/src/Pure/Isar/spec_parse.ML Wed Dec 10 14:45:15 2008 +0100 @@ -26,6 +26,7 @@ val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list val class_expr: token list -> string list * token list val locale_expr: token list -> Locale.expr * token list + val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list val locale_keyword: token list -> string * token list val context_element: token list -> Element.context * token list val statement: token list -> (Attrib.binding * (string * string list) list) list * token list @@ -103,6 +104,12 @@ val rename = P.name -- Scan.option P.mixfix; +val prefix = P.name --| P.$$$ ":"; +val named = P.name -- (P.$$$ "=" |-- P.term); +val position = P.maybe P.term; +val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named || + Scan.repeat1 position >> Expression.Positional; + in val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || @@ -117,6 +124,14 @@ and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x; in expr0 end; +val locale_expression = + let + fun expr2 x = P.xname x; + fun expr1 x = (Scan.optional prefix "" -- expr2 -- + Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; + fun expr0 x = (plus1_unless locale_keyword expr1) x; + in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end; + val context_element = P.group "context element" loc_element; end;