Merged.
--- a/src/FOL/ex/NewLocaleTest.thy Tue Dec 16 15:09:12 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Tue Dec 16 15:09:37 2008 +0100
@@ -167,6 +167,13 @@
lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
by (rule semi_hom_mult)
+(* Referring to facts from within a context specification *)
+
+lemma
+ assumes x: "P <-> P"
+ notes y = x
+ shows True ..
+
section {* Theorem statements *}
--- a/src/Pure/Isar/element.ML Tue Dec 16 15:09:12 2008 +0100
+++ b/src/Pure/Isar/element.ML Tue Dec 16 15:09:37 2008 +0100
@@ -23,6 +23,10 @@
val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
(Attrib.binding * ('fact * Attrib.src list) list) list ->
(Attrib.binding * ('c * Attrib.src list) list) list
+ val map_ctxt': {binding: Binding.T -> Binding.T,
+ var: Binding.T * mixfix -> Binding.T * mixfix,
+ typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
+ attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
val map_ctxt: {binding: Binding.T -> Binding.T,
var: Binding.T * mixfix -> Binding.T * mixfix,
typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
@@ -74,10 +78,8 @@
val generalize_facts: Proof.context -> Proof.context ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
(Attrib.binding * (thm list * Attrib.src list) list) list
- val activate: (typ, term, Facts.ref) ctxt list -> Proof.context ->
- (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
- val activate_i: context_i list -> Proof.context ->
- (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
+ val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
+ val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
end;
structure Element: ELEMENT =
@@ -109,18 +111,22 @@
fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
-fun map_ctxt {binding, var, typ, term, fact, attrib} =
+fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} =
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
- ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
+ ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
- ((binding a, map attrib atts), (term t, map term ps))))
+ ((binding a, map attrib atts), (term t, map pat ps))))
| Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
+fun map_ctxt {binding, var, typ, term, fact, attrib} =
+ map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term,
+ fact = fact, attrib = attrib}
+
fun map_ctxt_attrib attrib =
map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
@@ -536,9 +542,9 @@
local
fun activate_elem (Fixes fixes) ctxt =
- ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
+ ctxt |> ProofContext.add_fixes_i fixes |> snd
| activate_elem (Constrains _) ctxt =
- ([], ctxt)
+ ctxt
| activate_elem (Assumes asms) ctxt =
let
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
@@ -546,7 +552,7 @@
val (_, ctxt') =
ctxt |> fold Variable.auto_fixes ts
|> ProofContext.add_assms_i Assumption.presume_export asms';
- in ([], ctxt') end
+ in ctxt' end
| activate_elem (Defines defs) ctxt =
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
@@ -556,19 +562,20 @@
val (_, ctxt') =
ctxt |> fold (Variable.auto_fixes o #1) asms
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
- in ([], ctxt') end
+ in ctxt' end
| activate_elem (Notes (kind, facts)) ctxt =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
- in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
+ in ctxt' end;
fun gen_activate prep_facts raw_elems ctxt =
let
- val elems = map (map_ctxt_attrib Args.assignable o prep_facts ctxt) raw_elems;
- val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
- val elems' = elems |> map (map_ctxt_attrib Args.closure);
- in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
+ fun activate elem ctxt =
+ let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
+ in (elem', activate_elem elem' ctxt) end
+ val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
+ in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
fun check_name name =
if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
--- a/src/Pure/Isar/expression.ML Tue Dec 16 15:09:12 2008 +0100
+++ b/src/Pure/Isar/expression.ML Tue Dec 16 15:09:37 2008 +0100
@@ -184,12 +184,15 @@
(** Parsing **)
fun parse_elem prep_typ prep_term ctxt elem =
- Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt,
- term = prep_term ctxt, fact = I, attrib = I} elem;
+ Element.map_ctxt' {binding = I, var = I, typ = prep_typ ctxt,
+ term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt), (* FIXME ?? *)
+ pat = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
+ fact = I, attrib = I} elem;
fun parse_concl prep_term ctxt concl =
(map o map) (fn (t, ps) =>
- (prep_term ctxt, map (prep_term ctxt) ps)) concl;
+ (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t, (* FIXME ?? *)
+ map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
(** Simultaneous type inference: instantiations + elements + conclusion **)
@@ -398,14 +401,12 @@
let
val ctxt' = declare_elem prep_vars raw_elem ctxt;
val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
- (* FIXME term bindings *)
val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
in (insts, elems', ctxt') end;
fun prep_concl raw_concl (insts, elems, ctxt) =
let
- val concl = (map o map) (fn (t, ps) =>
- (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl;
+ val concl = parse_concl parse_prop ctxt raw_concl;
in check_autofix insts elems concl ctxt end;
val fors = prep_vars fixed context |> fst;
@@ -485,7 +486,7 @@
val context' = context |>
ProofContext.add_fixes_i fixed |> snd |>
fold NewLocale.activate_local_facts deps;
- val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
+ val (elems', _) = activate elems (ProofContext.set_stmt true context');
in ((fixed, deps, elems'), (parms, spec, defs)) end;
in
--- a/src/Pure/Isar/new_locale.ML Tue Dec 16 15:09:12 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Tue Dec 16 15:09:37 2008 +0100
@@ -287,18 +287,19 @@
fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
end;
-fun activate_notes activ_elem thy (name, morph) input =
+fun activate_notes activ_elem transfer thy (name, morph) input =
let
val Loc {notes, ...} = the_locale thy name;
fun activate ((kind, facts), _) input =
let
- val facts' = facts |> Element.facts_map (Element.morph_ctxt morph)
+ val facts' = facts |> Element.facts_map (Element.morph_ctxt
+ (Morphism.thm_morphism (transfer input) $> morph))
in activ_elem (Notes (kind, facts')) input end;
in
fold_rev activate notes input
end;
-fun activate_all name thy activ_elem (marked, input) =
+fun activate_all name thy activ_elem transfer (marked, input) =
let
val Loc {parameters = (_, params), spec = (asm, defs), ...} =
the_locale thy name;
@@ -310,7 +311,7 @@
(if not (null defs)
then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
else I) |>
- pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
+ pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
end;
@@ -354,15 +355,18 @@
roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
fun activate_global_facts dep thy =
- roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
+ roundup thy (activate_notes init_global_elem transfer) dep (get_global_idents thy, thy) |>
uncurry put_global_idents;
fun activate_local_facts dep ctxt =
- roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep
+ roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem
+ (transfer o ProofContext.theory_of)) dep
(get_local_idents ctxt, ctxt) |>
uncurry put_local_idents;
-fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
+fun init name thy =
+ activate_all name thy init_local_elem (transfer o ProofContext.theory_of)
+ (empty, ProofContext.init thy) |>
uncurry put_local_idents;
fun print_locale thy show_facts name =
@@ -371,7 +375,7 @@
val ctxt = init name' thy
in
Pretty.big_list "locale elements:"
- (activate_all name' thy (cons_elem show_facts) (empty, []) |> snd |> rev |>
+ (activate_all name' thy (cons_elem show_facts) (K I) (empty, []) |> snd |> rev |>
map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
end
@@ -420,7 +424,7 @@
fun add_thmss loc kind args ctxt =
let
- val (([Notes args'], _), ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+ val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
val ctxt'' = ctxt' |> ProofContext.theory (
change_locale loc
(fn (parameters, spec, decls, notes, dependencies) =>