1.1 --- a/src/FOL/ex/NewLocaleSetup.thy	Wed Dec 10 10:11:18 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleSetup.thy	Wed Dec 10 10:12:44 2008 +0100
     1.3 @@ -27,7 +27,9 @@
     1.4      (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
     1.5        >> (fn ((name, (expr, elems)), begin) =>
     1.6            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     1.7 -            (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin)));
     1.8 +            (Expression.add_locale_cmd name name expr elems #>
     1.9 +              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
    1.10 +                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
    1.11  
    1.12  val _ =
    1.13    OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag

     2.1 --- a/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 10:11:18 2008 +0100
     2.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 10:12:44 2008 +0100
     2.3 @@ -113,6 +113,12 @@
     2.4  print_locale! use_decl thm use_decl_def
     2.5  
     2.6  
     2.7 +text {* Foundational versions of theorems *}
     2.8 +
     2.9 +thm logic.assoc
    2.10 +thm logic.lor_def
    2.11 +
    2.12 +
    2.13  text {* Defines *}
    2.14  
    2.15  locale logic_def =
    2.16 @@ -121,7 +127,20 @@
    2.17      and lnot ("-- _" [60] 60)
    2.18    assumes assoc: "(x && y) && z = x && (y && z)"
    2.19      and notnot: "-- (-- x) = x"
    2.20 -  defines lor_def: (* FIXME *) "x || y == --(-- x && -- y)"
    2.21 +  defines "x || y == --(-- x && -- y)"
    2.22 +begin
    2.23 +
    2.24 +thm lor_def
    2.25 +(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *)
    2.26 +
    2.27 +lemma "x || y = --(-- x && --y)"
    2.28 +  by (unfold lor_def) (rule refl)
    2.29 +
    2.30 +end
    2.31 +
    2.32 +(* Inheritance of defines *)
    2.33 +
    2.34 +locale logic_def2 = logic_def
    2.35  begin
    2.36  
    2.37  lemma "x || y = --(-- x && --y)"
    2.38 @@ -129,7 +148,6 @@
    2.39  
    2.40  end
    2.41  
    2.42 -
    2.43  text {* Theorem statements *}
    2.44  
    2.45  lemma (in lgrp) lcancel:

     3.1 --- a/src/Pure/Isar/class.ML	Wed Dec 10 10:11:18 2008 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Wed Dec 10 10:12:44 2008 +0100
     3.3 @@ -394,7 +394,8 @@
     3.4    end;
     3.5  
     3.6  fun default_intro_tac ctxt [] =
     3.7 -      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
     3.8 +      intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE
     3.9 +      Locale.intro_locales_tac true ctxt []
    3.10    | default_intro_tac _ _ = no_tac;
    3.11  
    3.12  fun default_tac rules ctxt facts =

     4.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 10 10:11:18 2008 +0100
     4.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 10:12:44 2008 +0100
     4.3 @@ -19,9 +19,11 @@
     4.4  
     4.5    (* Declaring locales *)
     4.6    val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
     4.7 -    string * Proof.context
     4.8 +    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
     4.9 +    Proof.context
    4.10    val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    4.11 -    string * Proof.context
    4.12 +    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
    4.13 +    Proof.context
    4.14  
    4.15    (* Interpretation *)
    4.16    val sublocale_cmd: string -> expression -> theory -> Proof.state;
    4.17 @@ -72,6 +74,13 @@
    4.18        end;
    4.19  
    4.20      fun match_bind (n, b) = (n = Binding.base_name b);
    4.21 +    fun parm_eq ((b1, mx1), (b2, mx2)) =
    4.22 +      (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
    4.23 +      (Binding.base_name b1 = Binding.base_name b2) andalso
    4.24 +      (if mx1 = mx2 then true
    4.25 +      else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^
    4.26 +                    " in expression."));
    4.27 +      
    4.28      fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
    4.29        (* FIXME: cannot compare bindings for equality. *)
    4.30  
    4.31 @@ -103,12 +112,7 @@
    4.32              val (is', ps') = fold_map (fn i => fn ps =>
    4.33                let
    4.34                  val (ps', i') = params_inst i;
    4.35 -                val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
    4.36 -                  (* FIXME: should check for bindings being the same.
    4.37 -                     Instead we check for equal name and syntax. *)
    4.38 -                  if mx1 = mx2 then mx1
    4.39 -                  else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^
    4.40 -                    " in expression.")) (ps, ps')
    4.41 +                val ps'' = distinct parm_eq (ps @ ps');
    4.42                in (i', ps'') end) is []
    4.43            in (ps', is') end;
    4.44  
    4.45 @@ -268,21 +272,18 @@
    4.46  
    4.47  val norm_term = Envir.beta_norm oo Term.subst_atomic;
    4.48  
    4.49 -fun abstract_thm thy eq =
    4.50 -  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
    4.51 -
    4.52 -fun bind_def ctxt eq (xs, env, ths) =
    4.53 +fun bind_def ctxt eq (xs, env, eqs) =
    4.54    let
    4.55 +    val _ = LocalDefs.cert_def ctxt eq;
    4.56      val ((y, T), b) = LocalDefs.abs_def eq;
    4.57      val b' = norm_term env b;
    4.58 -    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
    4.59      fun err msg = error (msg ^ ": " ^ quote y);
    4.60    in
    4.61      exists (fn (x, _) => x = y) xs andalso
    4.62        err "Attempt to define previously specified variable";
    4.63      exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
    4.64        err "Attempt to redefine variable";
    4.65 -    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
    4.66 +    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
    4.67    end;
    4.68  
    4.69  fun eval_text _ _ (Fixes _) text = text
    4.70 @@ -317,8 +318,11 @@
    4.71          (case elem of
    4.72            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
    4.73              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
    4.74 -        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
    4.75 -            (a, (#2 (LocalDefs.cert_def ctxt (close_frees t)), no_binds ps))))
    4.76 +        | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
    4.77 +            let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
    4.78 +            in
    4.79 +              ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps))
    4.80 +            end))
    4.81          | e => e)
    4.82        end;
    4.83  
    4.84 @@ -430,8 +434,7 @@
    4.85           env: list of term pairs encoding substitutions, where the first term
    4.86             is a free variable; substitutions represent defines elements and
    4.87             the rhs is normalised wrt. the previous env
    4.88 -         defs: theorems representing the substitutions from defines elements
    4.89 -           (thms are normalised wrt. env).
    4.90 +         defs: the equations from the defines elements
    4.91         elems is an updated version of raw_elems:
    4.92           - type info added to Fixes and modified in Constrains
    4.93           - axiom and definition statement replaced by corresponding one
    4.94 @@ -519,7 +522,6 @@
    4.95  
    4.96      val export = Variable.export_morphism goal_ctxt context;
    4.97      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
    4.98 -(*    val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *)
    4.99      val exp_term = Drule.term_rule thy (singleton exp_fact);
   4.100      val exp_typ = Logic.type_map exp_term;
   4.101      val export' =
   4.102 @@ -623,6 +625,8 @@
   4.103  
   4.104  fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
   4.105    let
   4.106 +    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
   4.107 +
   4.108      val (a_pred, a_intro, a_axioms, thy'') =
   4.109        if null exts then (NONE, NONE, [], thy)
   4.110        else
   4.111 @@ -630,7 +634,7 @@
   4.112            val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
   4.113            val ((statement, intro, axioms), thy') =
   4.114              thy
   4.115 -            |> def_pred aname parms defs exts exts';
   4.116 +            |> def_pred aname parms defs' exts exts';
   4.117            val (_, thy'') =
   4.118              thy'
   4.119              |> Sign.add_path aname
   4.120 @@ -645,7 +649,7 @@
   4.121          let
   4.122            val ((statement, intro, axioms), thy''') =
   4.123              thy''
   4.124 -            |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
   4.125 +            |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
   4.126            val (_, thy'''') =
   4.127              thy'''
   4.128              |> Sign.add_path pname
   4.129 @@ -670,15 +674,10 @@
   4.130        |> apfst (curry Notes Thm.assumptionK)
   4.131    | assumes_to_notes e axms = (e, axms);
   4.132  
   4.133 -fun defines_to_notes thy (Defines defs) defns =
   4.134 -    let
   4.135 -      val defs' = map (fn (_, (def, _)) => def) defs
   4.136 -      val notes = map (fn (a, (def, _)) =>
   4.137 -        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs
   4.138 -    in
   4.139 -      (Notes (Thm.definitionK, notes), defns @ defs')
   4.140 -    end
   4.141 -  | defines_to_notes _ e defns = (e, defns);
   4.142 +fun defines_to_notes thy (Defines defs) =
   4.143 +      Notes (Thm.definitionK, map (fn (a, (def, _)) =>
   4.144 +        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs)
   4.145 +  | defines_to_notes _ e = e;
   4.146  
   4.147  fun gen_add_locale prep_decl
   4.148      bname predicate_name raw_imprt raw_body thy =
   4.149 @@ -687,7 +686,7 @@
   4.150      val _ = NewLocale.test_locale thy name andalso
   4.151        error ("Duplicate definition of locale " ^ quote name);
   4.152  
   4.153 -    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), _)) =
   4.154 +    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
   4.155        prep_decl raw_imprt raw_body (ProofContext.init thy);
   4.156      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   4.157        define_preds predicate_name text thy;
   4.158 @@ -701,24 +700,30 @@
   4.159      val params = fixed @
   4.160        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   4.161      val asm = if is_some b_statement then b_statement else a_statement;
   4.162 -    val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
   4.163 -    val notes = body_elems' |>
   4.164 -      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   4.165 -      fst |> map (Element.morph_ctxt satisfy) |>
   4.166 -      map_filter (fn Notes notes => SOME notes | _ => NONE) |>
   4.167 -      (if is_some asm
   4.168 -        then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
   4.169 -          [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
   4.170 -        else I);
   4.171 +    val body_elems' = map (defines_to_notes thy') body_elems;
   4.172 +
   4.173 +    val notes =
   4.174 +        if is_some asm
   4.175 +        then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
   4.176 +          [([Assumption.assume (cterm_of thy' (the asm))],
   4.177 +            [(Attrib.internal o K) NewLocale.witness_attrib])])])]
   4.178 +        else [];
   4.179  
   4.180      val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
   4.181  
   4.182      val loc_ctxt = thy' |>
   4.183        NewLocale.register_locale bname (extraTs, params)
   4.184 -        (asm, defns) ([], [])
   4.185 +        (asm, rev defs) ([], [])
   4.186          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
   4.187 -      NewLocale.init name
   4.188 -  in (name, loc_ctxt) end;
   4.189 +      NewLocale.init name;
   4.190 +
   4.191 +    (* These will be added in the local theory. *)
   4.192 +    val notes' = body_elems' |>
   4.193 +      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   4.194 +      fst |> map (Element.morph_ctxt satisfy) |>
   4.195 +      map_filter (fn Notes notes => SOME notes | _ => NONE);
   4.196 +
   4.197 +  in ((name, notes'), loc_ctxt) end;
   4.198  
   4.199  in
   4.200  

     5.1 --- a/src/Pure/Isar/new_locale.ML	Wed Dec 10 10:11:18 2008 +0100
     5.2 +++ b/src/Pure/Isar/new_locale.ML	Wed Dec 10 10:12:44 2008 +0100
     5.3 @@ -39,7 +39,6 @@
     5.4      Proof.context -> Proof.context
     5.5    val activate_global_facts: string * Morphism.morphism -> theory -> theory
     5.6    val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
     5.7 -(*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
     5.8    val init: string -> theory -> Proof.context
     5.9  
    5.10    (* Reasoning about locales *)