merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
--- a/Admin/update-keywords Sun Apr 01 23:09:36 2012 +0200
+++ b/Admin/update-keywords Sun Apr 01 23:21:54 2012 +0200
@@ -13,7 +13,7 @@
isabelle keywords \
"$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
"$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
- "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz"
+ "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
isabelle keywords -k ZF \
"$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
--- a/etc/isar-keywords.el Sun Apr 01 23:09:36 2012 +0200
+++ b/etc/isar-keywords.el Sun Apr 01 23:21:54 2012 +0200
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -108,7 +108,10 @@
"hide_const"
"hide_fact"
"hide_type"
+ "import_const_map"
+ "import_file"
"import_tptp"
+ "import_type_map"
"include"
"including"
"inductive"
@@ -491,7 +494,10 @@
"hide_const"
"hide_fact"
"hide_type"
+ "import_const_map"
+ "import_file"
"import_tptp"
+ "import_type_map"
"inductive"
"inductive_set"
"instantiation"
--- a/lib/scripts/getsettings Sun Apr 01 23:09:36 2012 +0200
+++ b/lib/scripts/getsettings Sun Apr 01 23:21:54 2012 +0200
@@ -92,7 +92,7 @@
#robust invocation via ISABELLE_JDK_HOME
function isabelle_jdk () {
[ -z "$ISABELLE_JDK_HOME" ] && \
- { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
+ { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; }
local PRG="$1"; shift
"$ISABELLE_JDK_HOME/bin/$PRG" "$@"
}
@@ -100,7 +100,7 @@
#robust invocation via SCALA_HOME
function isabelle_scala () {
[ -z "$SCALA_HOME" ] && \
- { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
+ { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; }
local PRG="$1"; shift
"$SCALA_HOME/bin/$PRG" "$@"
}
--- a/src/HOL/IsaMakefile Sun Apr 01 23:09:36 2012 +0200
+++ b/src/HOL/IsaMakefile Sun Apr 01 23:21:54 2012 +0200
@@ -548,7 +548,7 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
-## Import sessions
+## HOL-Import
HOL-Import: $(LOG)/HOL-Import.gz
@@ -561,6 +561,7 @@
Import/HOL_Light_Import.thy
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
+
## HOL-Number_Theory
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
@@ -1785,9 +1786,10 @@
@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \
$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \
$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz \
- $(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz \
- $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz \
- $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \
+ $(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-HOL_Light.gz \
+ $(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz \
+ $(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz \
+ $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \
$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \
$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz \
$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \
@@ -1817,18 +1819,17 @@
$(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz \
$(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz \
$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \
- $(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz \
- $(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \
- $(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base \
- $(OUT)/HOL-Boogie $(OUT)/HOL-IMP $(OUT)/HOL-Library \
+ $(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \
+ $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \
+ $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \
+ $(OUT)/HOL-HOL_Light $(OUT)/HOL-IMP $(OUT)/HOL-Library \
$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \
$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
$(OUT)/HOL-Probability $(OUT)/HOL-Proofs \
- $(OUT)/HOL-SPARK $(OUT)/HOL-Word \
- $(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz \
- $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz \
- $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz \
- $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
+ $(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/TLA \
+ $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
+ $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
+ $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \
$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz \
$(LOG)/HOL-Datatype_Benchmark.gz \
--- a/src/HOL/Library/Fraction_Field.thy Sun Apr 01 23:09:36 2012 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Sun Apr 01 23:21:54 2012 +0200
@@ -146,14 +146,15 @@
qed
lemma mult_fract_cancel:
- assumes "c \<noteq> 0"
+ assumes "c \<noteq> (0::'a)"
shows "Fract (c * a) (c * b) = Fract a b"
proof -
from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
then show ?thesis by (simp add: mult_fract [symmetric])
qed
-instance proof
+instance
+proof
fix q r s :: "'a fract" show "(q * r) * s = q * (r * s)"
by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps)
next
@@ -249,7 +250,8 @@
lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
by (simp add: divide_fract_def)
-instance proof
+instance
+proof
fix q :: "'a fract"
assume "q \<noteq> 0"
then show "inverse q * q = 1"
@@ -328,7 +330,8 @@
shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
by (simp add: less_fract_def less_le_not_le mult_ac assms)
-instance proof
+instance
+proof
fix q r s :: "'a fract"
assume "q \<le> r" and "r \<le> s" thus "q \<le> s"
proof (induct q, induct r, induct s)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Apr 01 23:21:54 2012 +0200
@@ -1420,14 +1420,12 @@
val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
(maps_modes result_thms)
val qname = #qname (dest_steps steps)
- (* FIXME !? *)
- val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
- (fn thm => Context.mapping (Code.add_eqn thm) I))))
+ val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)
val thy''' =
cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
[((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
- [attrib thy ])] thy))
+ [attrib])] thy))
result_thms' thy'' |> Theory.checkpoint)
in
thy'''
--- a/src/Pure/Isar/attrib.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Apr 01 23:21:54 2012 +0200
@@ -25,6 +25,12 @@
val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
+ val global_notes: string -> (binding * (thm list * src list) list) list ->
+ theory -> (string * thm list) list * theory
+ val local_notes: string -> (binding * (thm list * src list) list) list ->
+ Proof.context -> (string * thm list) list * Proof.context
+ val generic_notes: string -> (binding * (thm list * src list) list) list ->
+ Context.generic -> (string * thm list) list * Context.generic
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -138,6 +144,15 @@
(* fact expressions *)
+fun global_notes kind facts thy = thy |>
+ Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
+
+fun local_notes kind facts ctxt = ctxt |>
+ Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
+
+fun generic_notes kind facts context = context |>
+ Context.mapping_result (global_notes kind facts) (local_notes kind facts);
+
fun eval_thms ctxt srcs = ctxt
|> Proof_Context.note_thmss ""
(map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
--- a/src/Pure/Isar/bundle.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/bundle.ML Sun Apr 01 23:21:54 2012 +0200
@@ -15,12 +15,13 @@
(binding * string option * mixfix) list -> local_theory -> local_theory
val includes: string list -> Proof.context -> Proof.context
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
- val context_includes: string list -> generic_theory -> local_theory
- val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
val include_: string list -> Proof.state -> Proof.state
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val including: string list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+ val context: string list -> Element.context_i list -> generic_theory -> local_theory
+ val context_cmd: (xstring * Position.T) list -> Element.context list ->
+ generic_theory -> local_theory
val print_bundles: Proof.context -> unit
end;
@@ -87,29 +88,26 @@
local
fun gen_includes prep args ctxt =
- let
- val decls = maps (the_bundle ctxt o prep ctxt) args;
- val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
- val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
- in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
+ let val decls = maps (the_bundle ctxt o prep ctxt) args
+ in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
-fun gen_context prep args (Context.Theory thy) =
- Named_Target.theory_init thy
- |> Local_Theory.target (gen_includes prep args)
- |> Local_Theory.restore
- | gen_context prep args (Context.Proof lthy) =
- Named_Target.assert lthy
- |> gen_includes prep args
- |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy =
+ let
+ val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
+ val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd;
+ in
+ (case gthy of
+ Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
+ | Context.Proof _ =>
+ augment lthy |>
+ Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy))
+ end;
in
val includes = gen_includes (K I);
val includes_cmd = gen_includes check;
-val context_includes = gen_context (K I);
-val context_includes_cmd = gen_context check;
-
fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
fun include_cmd bs =
Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
@@ -117,6 +115,9 @@
fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
+val context = gen_context (K I) Expression.cert_statement;
+val context_cmd = gen_context check Expression.read_statement;
+
end;
--- a/src/Pure/Isar/class.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/class.ML Sun Apr 01 23:21:54 2012 +0200
@@ -320,7 +320,7 @@
lthy
|> Local_Theory.raw_theory f
|> Local_Theory.map_contexts
- (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class));
+ (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class)));
fun target_const class ((c, mx), (type_params, dict)) thy =
let
@@ -484,7 +484,7 @@
Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
##>> AxClass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
- ##> Local_Theory.map_contexts synchronize_inst_syntax;
+ ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
(case instantiation_param lthy b of
@@ -552,8 +552,7 @@
|> synchronize_inst_syntax
|> Local_Theory.init naming
{define = Generic_Target.define foundation,
- notes = Generic_Target.notes
- (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+ notes = Generic_Target.notes Generic_Target.theory_notes,
abbrev = Generic_Target.abbrev
(fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
Generic_Target.theory_abbrev prmode ((b, mx), t)),
--- a/src/Pure/Isar/element.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/element.ML Sun Apr 01 23:21:54 2012 +0200
@@ -51,8 +51,6 @@
val satisfy_morphism: witness list -> morphism
val eq_morphism: theory -> thm list -> morphism option
val transfer_morphism: theory -> morphism
- val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
- Context.generic -> (string * thm list) list * Context.generic
val init: context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -483,16 +481,6 @@
(* init *)
-fun generic_note_thmss kind facts context =
- let
- val facts' =
- Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
- in
- context |> Context.mapping_result
- (Global_Theory.note_thmss kind facts')
- (Proof_Context.note_thmss kind facts')
- end;
-
fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
| init (Constrains _) = I
| init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -514,7 +502,7 @@
|> fold Variable.auto_fixes (map #1 asms)
|> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
- | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
+ | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
(* activate *)
--- a/src/Pure/Isar/expression.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/expression.ML Sun Apr 01 23:21:54 2012 +0200
@@ -816,7 +816,7 @@
local
fun note_eqns_register deps witss attrss eqns export export' =
- Element.generic_note_thmss Thm.lemmaK
+ Attrib.generic_notes Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
#-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
#-> (fn eqns => fold (fn ((dep, morph), wits) =>
@@ -885,12 +885,10 @@
fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
-
val facts =
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
val eqns' = ctxt
- |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
+ |> Attrib.local_notes Thm.lemmaK facts
|-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
|> fst; (* FIXME duplication to add_thmss *)
in
--- a/src/Pure/Isar/generic_target.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Apr 01 23:21:54 2012 +0200
@@ -11,21 +11,26 @@
term list * term list -> local_theory -> (term * thm) * local_theory) ->
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
- val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+ val notes:
+ (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
(Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
(string * thm list) list * local_theory
+ val locale_notes: string -> string ->
+ (Attrib.binding * (thm list * Args.src list) list) list ->
+ (Attrib.binding * (thm list * Args.src list) list) list ->
+ local_theory -> local_theory
val abbrev: (string * bool -> binding * mixfix -> term * term ->
term list -> local_theory -> local_theory) ->
- string * bool -> (binding * mixfix) * term -> local_theory ->
- (term * term) * local_theory
-
+ string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
val background_declaration: declaration -> local_theory -> local_theory
val standard_declaration: declaration -> local_theory -> local_theory
-
+ val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
- val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+ val theory_notes: string ->
+ (Attrib.binding * (thm list * Args.src list) list) list ->
+ (Attrib.binding * (thm list * Args.src list) list) list ->
local_theory -> local_theory
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
end
@@ -95,6 +100,8 @@
(* notes *)
+local
+
fun import_export_proof ctxt (name, raw_th) =
let
val thy = Proof_Context.theory_of ctxt;
@@ -139,9 +146,13 @@
in (result'', result) end;
+fun standard_facts lthy ctxt =
+ Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+in
+
fun notes target_notes kind facts lthy =
let
- val thy = Proof_Context.theory_of lthy;
val facts' = facts
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
(Local_Theory.full_name lthy (fst a))) bs))
@@ -150,10 +161,23 @@
val global_facts = Global_Theory.map_facts #2 facts';
in
lthy
- |> target_notes kind global_facts local_facts
- |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
+ |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
+ |> Attrib.local_notes kind local_facts
end;
+fun locale_notes locale kind global_facts local_facts =
+ Local_Theory.background_theory
+ (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
+ (fn lthy => lthy |>
+ Local_Theory.target (fn ctxt => ctxt |>
+ Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
+ (fn lthy => lthy |>
+ Local_Theory.map_contexts (fn level => fn ctxt =>
+ if level = 0 orelse level = Local_Theory.level lthy then ctxt
+ else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd));
+
+end;
+
(* abbrev *)
@@ -191,9 +215,14 @@
fun standard_declaration decl =
background_declaration decl #>
- (fn lthy => Local_Theory.map_contexts (fn ctxt =>
+ (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt =>
Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
+fun locale_declaration locale syntax decl lthy = lthy
+ |> Local_Theory.target (fn ctxt => ctxt |>
+ Locale.add_declaration locale syntax
+ (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
+
(** primitive theory operations **)
@@ -209,15 +238,13 @@
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
-fun theory_notes kind global_facts lthy =
- let
- val thy = Proof_Context.theory_of lthy;
- val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
- in
- lthy
- |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
- end;
+fun theory_notes kind global_facts local_facts =
+ Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
+ (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
+ if level = Local_Theory.level lthy then ctxt
+ else
+ ctxt |> Attrib.local_notes kind
+ (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
fun theory_abbrev prmode ((b, mx), t) =
Local_Theory.background_theory
--- a/src/Pure/Isar/isar_syn.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Apr 01 23:21:54 2012 +0200
@@ -436,9 +436,10 @@
val _ =
Outer_Syntax.command ("context", Keyword.thy_decl) "begin local theory context"
- ((Parse_Spec.includes >> (Toplevel.open_target o Bundle.context_includes_cmd) ||
- Parse.position Parse.xname >> (fn name =>
- Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)))
+ ((Parse.position Parse.xname >> (fn name =>
+ Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
+ Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
+ >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
--| Parse.begin);
--- a/src/Pure/Isar/local_theory.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML Sun Apr 01 23:21:54 2012 +0200
@@ -10,12 +10,12 @@
signature LOCAL_THEORY =
sig
type operations
- val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
val assert: local_theory -> local_theory
val level: Proof.context -> int
val assert_bottom: bool -> local_theory -> local_theory
val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
val close_target: local_theory -> local_theory
+ val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
val naming_of: local_theory -> Name_Space.naming
val full_name: local_theory -> binding -> string
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
@@ -23,17 +23,16 @@
val new_group: local_theory -> local_theory
val reset_group: local_theory -> local_theory
val restore_naming: local_theory -> local_theory -> local_theory
- val target_of: local_theory -> Proof.context
+ val standard_morphism: local_theory -> Proof.context -> morphism
+ val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val background_theory: (theory -> theory) -> local_theory -> local_theory
- val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
+ val target_of: local_theory -> Proof.context
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
+ val target_morphism: local_theory -> morphism
val propagate_ml_env: generic_theory -> generic_theory
- val standard_morphism: local_theory -> Proof.context -> morphism
- val target_morphism: local_theory -> morphism
- val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val operations_of: local_theory -> operations
val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
@@ -98,21 +97,13 @@
fun init _ = [];
);
-fun map_contexts f =
- (Data.map o map) (fn {naming, operations, target} =>
- make_lthy (naming, operations,
- target
- |> Context_Position.set_visible false
- |> f
- |> Context_Position.restore_visible target))
- #> f;
-
fun assert lthy =
if null (Data.get lthy) then error "Missing local theory context" else lthy;
-val get_lthy = hd o Data.get o assert;
+val get_last_lthy = List.last o Data.get o assert;
+val get_first_lthy = hd o Data.get o assert;
-fun map_lthy f = assert #>
+fun map_first_lthy f = assert #>
Data.map (fn {naming, operations, target} :: parents =>
make_lthy (f (naming, operations, target)) :: parents);
@@ -137,13 +128,25 @@
fun close_target lthy =
assert_bottom false lthy |> Data.map tl;
+fun map_contexts f lthy =
+ let val n = level lthy in
+ lthy |> (Data.map o map_index) (fn (i, {naming, operations, target}) =>
+ make_lthy (naming, operations,
+ target
+ |> Context_Position.set_visible false
+ |> f (n - i - 1)
+ |> Context_Position.restore_visible target))
+ |> f n
+ end;
+
(* naming *)
-val naming_of = #naming o get_lthy;
+val naming_of = #naming o get_first_lthy;
val full_name = Name_Space.full_name o naming_of;
-fun map_naming f = map_lthy (fn (naming, operations, target) => (f naming, operations, target));
+fun map_naming f =
+ map_first_lthy (fn (naming, operations, target) => (f naming, operations, target));
val conceal = map_naming Name_Space.conceal;
val new_group = map_naming Name_Space.new_group;
@@ -152,19 +155,22 @@
val restore_naming = map_naming o K o naming_of;
-(* target *)
+(* standard morphisms *)
-val target_of = #target o get_lthy;
+fun standard_morphism lthy ctxt =
+ Proof_Context.norm_export_morphism lthy ctxt $>
+ Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
-fun map_target f = map_lthy (fn (naming, operations, target) => (naming, operations, f target));
+fun standard_form lthy ctxt x =
+ Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
-(* substructure mappings *)
+(* background theory *)
fun raw_theory_result f lthy =
let
val (res, thy') = f (Proof_Context.theory_of lthy);
- val lthy' = map_contexts (Proof_Context.transfer thy') lthy;
+ val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
in (res, lthy') end;
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
@@ -181,47 +187,37 @@
fun background_theory f = #2 o background_theory_result (f #> pair ());
-fun target_result f lthy =
+
+(* target contexts *)
+
+val target_of = #target o get_last_lthy;
+
+fun target f lthy =
let
- val target = target_of lthy;
- val (res, ctxt') = target
+ val ctxt = target_of lthy;
+ val ctxt' = ctxt
|> Context_Position.set_visible false
|> f
- ||> Context_Position.restore_visible target;
+ |> Context_Position.restore_visible ctxt;
val thy' = Proof_Context.theory_of ctxt';
- val lthy' = lthy
- |> map_target (K ctxt')
- |> map_contexts (Proof_Context.transfer thy');
- in (res, lthy') end;
+ in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
-fun target f = #2 o target_result (f #> pair ());
+fun target_morphism lthy = standard_morphism lthy (target_of lthy);
fun propagate_ml_env (context as Context.Proof lthy) =
let val inherit = ML_Env.inherit context in
lthy
|> background_theory (Context.theory_map inherit)
- |> map_contexts (Context.proof_map inherit)
+ |> map_contexts (K (Context.proof_map inherit))
|> Context.Proof
end
| propagate_ml_env context = context;
-(* morphisms *)
-
-fun standard_morphism lthy ctxt =
- Proof_Context.norm_export_morphism lthy ctxt $>
- Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
-
-fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-
-fun standard_form lthy ctxt x =
- Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
-
-
(** operations **)
-val operations_of = #operations o get_lthy;
+val operations_of = #operations o get_first_lthy;
(* primitives *)
@@ -252,13 +248,13 @@
fun type_notation add mode raw_args lthy =
let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in
declaration {syntax = true, pervasive = false}
- (Proof_Context.target_type_notation add mode args) lthy
+ (Proof_Context.generic_type_notation add mode args) lthy
end;
fun notation add mode raw_args lthy =
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in
declaration {syntax = true, pervasive = false}
- (Proof_Context.target_notation add mode args) lthy
+ (Proof_Context.generic_notation add mode args) lthy
end;
@@ -286,7 +282,7 @@
|> checkpoint;
fun restore lthy =
- let val {naming, operations, target} = get_lthy lthy
+ let val {naming, operations, target} = get_first_lthy lthy
in init naming operations target end;
--- a/src/Pure/Isar/locale.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/locale.ML Sun Apr 01 23:21:54 2012 +0200
@@ -49,8 +49,7 @@
(* Storing results *)
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
Proof.context -> Proof.context
- val add_declaration: string -> declaration -> Proof.context -> Proof.context
- val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
+ val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
(* Activation *)
val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -536,32 +535,34 @@
fun add_thmss _ _ [] ctxt = ctxt
| add_thmss loc kind facts ctxt =
ctxt
- |> Proof_Context.note_thmss kind
- (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
- |> snd
+ |> Attrib.local_notes kind facts |> snd
|> Proof_Context.background_theory
((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
(* Registrations *)
- (fn thy => fold_rev (fn (_, morph) =>
- let
- val facts' = facts
- |> Element.transform_facts morph
- |> Attrib.map_facts (map (Attrib.attribute_i thy));
- in snd o Global_Theory.note_thmss kind facts' end)
+ (fn thy =>
+ fold_rev (fn (_, morph) =>
+ snd o Attrib.global_notes kind (Element.transform_facts morph facts))
(registrations_of (Context.Theory thy) loc) thy));
(* Declarations *)
-fun add_declaration loc decl =
+local
+
+fun add_decl loc decl =
add_thmss loc ""
[((Binding.conceal Binding.empty,
[Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
[([Drule.dummy_thm], [])])];
-fun add_syntax_declaration loc decl =
- Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
- #> add_declaration loc decl;
+in
+
+fun add_declaration loc syntax decl =
+ syntax ?
+ Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+ #> add_decl loc decl;
+
+end;
(*** Reasoning about locales ***)
--- a/src/Pure/Isar/named_target.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/named_target.ML Sun Apr 01 23:21:54 2012 +0200
@@ -8,7 +8,6 @@
signature NAMED_TARGET =
sig
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
- val assert: local_theory -> local_theory
val init: (local_theory -> local_theory) -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val reinit: local_theory -> local_theory -> local_theory
@@ -44,35 +43,11 @@
Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
{target = target, is_locale = is_locale, is_class = is_class});
-fun assert lthy =
- if is_some (peek lthy) then lthy
- else error "Not in a named target (global theory, locale, class)";
-
-(* generic declarations *)
+(* consts in locale *)
-fun locale_declaration locale syntax decl lthy =
- let
- val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
- val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
- in
- lthy
- |> Local_Theory.target (add locale locale_decl)
- end;
-
-fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
- if target = "" then Generic_Target.standard_declaration decl lthy
- else
- lthy
- |> pervasive ? Generic_Target.background_declaration decl
- |> locale_declaration target syntax decl
- |> Context.proof_map (Morphism.form decl);
-
-
-(* consts in locales *)
-
-fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
- locale_declaration target true (fn phi =>
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+ Generic_Target.locale_declaration target true (fn phi =>
let
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
@@ -95,7 +70,7 @@
same_shape ?
(Context.mapping
(Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
- Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
+ Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)]))))
end);
@@ -121,21 +96,9 @@
(* notes *)
-fun locale_notes locale kind global_facts local_facts lthy =
- let
- val global_facts' = Attrib.map_facts (K []) global_facts;
- val local_facts' = local_facts
- |> Attrib.partial_evaluation lthy
- |> Element.transform_facts (Local_Theory.target_morphism lthy);
- in
- lthy
- |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
- end;
-
fun target_notes (Target {target, is_locale, ...}) =
- if is_locale then locale_notes target
- else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+ if is_locale then Generic_Target.locale_notes target
+ else Generic_Target.theory_notes;
(* abbrev *)
@@ -157,6 +120,19 @@
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+(* declaration *)
+
+fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
+ if target = "" then Generic_Target.standard_declaration decl lthy
+ else
+ lthy
+ |> pervasive ? Generic_Target.background_declaration decl
+ |> Generic_Target.locale_declaration target syntax decl
+ |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
+ if level = 0 then ctxt
+ else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
+
+
(* pretty *)
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
--- a/src/Pure/Isar/overloading.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/overloading.ML Sun Apr 01 23:21:54 2012 +0200
@@ -155,7 +155,7 @@
(Thm.def_binding_optional (Binding.name v) b_def,
Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
- ##> Local_Theory.map_contexts synchronize_syntax
+ ##> Local_Theory.map_contexts (K synchronize_syntax)
#-> (fn (_, def) => pair (Const (c, U), def));
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
@@ -203,8 +203,7 @@
|> synchronize_syntax
|> Local_Theory.init naming
{define = Generic_Target.define foundation,
- notes = Generic_Target.notes
- (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+ notes = Generic_Target.notes Generic_Target.theory_notes,
abbrev = Generic_Target.abbrev
(fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
Generic_Target.theory_abbrev prmode ((b, mx), t)),
--- a/src/Pure/Isar/proof_context.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Apr 01 23:21:54 2012 +0200
@@ -136,9 +136,9 @@
val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
- val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
+ val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
Context.generic -> Context.generic
- val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
+ val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
val class_alias: binding -> class -> Proof.context -> Proof.context
val type_alias: binding -> string -> Proof.context -> Proof.context
@@ -970,7 +970,7 @@
val type_notation = gen_notation (K type_syntax);
val notation = gen_notation const_syntax;
-fun target_type_notation add mode args phi =
+fun generic_type_notation add mode args phi =
let
val args' = args |> map_filter (fn (T, mx) =>
let
@@ -979,7 +979,7 @@
in if similar then SOME (T', mx) else NONE end);
in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
-fun target_notation add mode args phi =
+fun generic_notation add mode args phi =
let
val args' = args |> map_filter (fn (t, mx) =>
let val t' = Morphism.term phi t
--- a/src/Tools/interpretation_with_defs.ML Sun Apr 01 23:09:36 2012 +0200
+++ b/src/Tools/interpretation_with_defs.ML Sun Apr 01 23:21:54 2012 +0200
@@ -23,7 +23,7 @@
map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
maps snd;
in
- Element.generic_note_thmss Thm.lemmaK
+ Attrib.generic_notes Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
#-> (fn facts => `(fn context => meta_rewrite context facts))
#-> (fn eqns => fold (fn ((dep, morph), wits) =>