--- 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