# HG changeset patch # User ballarin # Date 1228900364 -3600 # Node ID 3dc51c01f9f31ed50884335beb47e1de4d451cd8 # Parent 721529248e31482a6d30fe1bd3db6da85e4ba098# Parent 3ad4cf50070dc993caac437fac06eb437badea13 Merged. diff -r 721529248e31 -r 3dc51c01f9f3 src/FOL/ex/NewLocaleSetup.thy --- a/src/FOL/ex/NewLocaleSetup.thy Wed Dec 10 10:11:18 2008 +0100 +++ b/src/FOL/ex/NewLocaleSetup.thy Wed Dec 10 10:12:44 2008 +0100 @@ -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 diff -r 721529248e31 -r 3dc51c01f9f3 src/FOL/ex/NewLocaleTest.thy --- a/src/FOL/ex/NewLocaleTest.thy Wed Dec 10 10:11:18 2008 +0100 +++ b/src/FOL/ex/NewLocaleTest.thy Wed Dec 10 10:12:44 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 = @@ -121,7 +127,20 @@ and lnot ("-- _" [60] 60) assumes assoc: "(x && y) && z = x && (y && z)" and notnot: "-- (-- x) = x" - defines lor_def: (* FIXME *) "x || y == --(-- x && -- y)" + 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)" @@ -129,7 +148,6 @@ end - text {* Theorem statements *} lemma (in lgrp) lcancel: diff -r 721529248e31 -r 3dc51c01f9f3 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Dec 10 10:11:18 2008 +0100 +++ b/src/Pure/Isar/class.ML Wed Dec 10 10:12:44 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 721529248e31 -r 3dc51c01f9f3 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Dec 10 10:11:18 2008 +0100 +++ b/src/Pure/Isar/expression.ML Wed Dec 10 10:12:44 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; @@ -72,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. *) @@ -103,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; @@ -268,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 @@ -317,8 +318,11 @@ (case elem of Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) - | Defines defs => Defines (defs |> map (fn (a, (t, ps)) => - (a, (#2 (LocalDefs.cert_def ctxt (close_frees t)), no_binds ps)))) + | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => + let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t) + in + ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps)) + end)) | e => e) end; @@ -430,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 @@ -519,7 +522,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' = @@ -623,6 +625,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 @@ -630,7 +634,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 @@ -645,7 +649,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 @@ -670,15 +674,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 = @@ -687,7 +686,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; @@ -701,24 +700,30 @@ 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' |> - (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); + val body_elems' = map (defines_to_notes thy') body_elems; + + 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 []; val deps' = map (fn (l, morph) => (l, morph $> 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; + + (* These will be added in the local theory. *) + val notes' = body_elems' |> + (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); + + in ((name, notes'), loc_ctxt) end; in diff -r 721529248e31 -r 3dc51c01f9f3 src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Wed Dec 10 10:11:18 2008 +0100 +++ b/src/Pure/Isar/new_locale.ML Wed Dec 10 10:12:44 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 *)