Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
--- a/src/FOL/ex/NewLocaleSetup.thy Fri Dec 12 12:14:02 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy Fri Dec 12 14:30:21 2008 +0100
@@ -44,9 +44,10 @@
val _ =
OuterSyntax.command "interpretation"
"prove interpretation of locale expression in theory" K.thy_goal
- (P.!!! SpecParse.locale_expression
- >> (fn expr => Toplevel.print o
- Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+ (P.!!! SpecParse.locale_expression --
+ Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
+ >> (fn (expr, mixin) => Toplevel.print o
+ Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin)));
val _ =
OuterSyntax.command "interpret"
--- a/src/FOL/ex/NewLocaleTest.thy Fri Dec 12 12:14:02 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Fri Dec 12 14:30:21 2008 +0100
@@ -10,7 +10,6 @@
ML_val {* set new_locales *}
ML_val {* set Toplevel.debug *}
-ML_val {* set show_hyps *}
typedecl int arities int :: "term"
@@ -24,7 +23,7 @@
int_minus: "(-x) + x = 0"
int_minus2: "-(-x) = x"
-text {* Inference of parameter types *}
+section {* Inference of parameter types *}
locale param1 = fixes p
print_locale! param1
@@ -44,7 +43,7 @@
print_locale! param4
-text {* Incremental type constraints *}
+subsection {* Incremental type constraints *}
locale constraint1 =
fixes prod (infixl "**" 65)
@@ -58,7 +57,7 @@
print_locale! constraint2
-text {* Inheritance *}
+section {* Inheritance *}
locale semi =
fixes prod (infixl "**" 65)
@@ -94,7 +93,7 @@
print_locale! pert_hom' thm pert_hom'_def
-text {* Syntax declarations *}
+section {* Syntax declarations *}
locale logic =
fixes land (infixl "&&" 55)
@@ -113,13 +112,13 @@
print_locale! use_decl thm use_decl_def
-text {* Foundational versions of theorems *}
+section {* Foundational versions of theorems *}
thm logic.assoc
thm logic.lor_def
-text {* Defines *}
+section {* Defines *}
locale logic_def =
fixes land (infixl "&&" 55)
@@ -149,7 +148,7 @@
end
-text {* Notes *}
+section {* Notes *}
(* A somewhat arcane homomorphism example *)
@@ -169,7 +168,7 @@
by (rule semi_hom_mult)
-text {* Theorem statements *}
+section {* Theorem statements *}
lemma (in lgrp) lcancel:
"x ** y = x ** z <-> y = z"
@@ -200,7 +199,7 @@
print_locale! rgrp
-text {* Patterns *}
+subsection {* Patterns *}
lemma (in rgrp)
assumes "y ** x = z ** x" (is ?a)
@@ -218,7 +217,7 @@
qed
-text {* Interpretation between locales: sublocales *}
+section {* Interpretation between locales: sublocales *}
sublocale lgrp < right: rgrp
print_facts
@@ -305,8 +304,7 @@
done
print_locale! order_with_def
-(* Note that decls come after theorems that make use of them.
- Appears to be harmless at least in this example. *)
+(* Note that decls come after theorems that make use of them. *)
(* locale with many parameters ---
@@ -359,7 +357,7 @@
print_locale! trivial (* No instance for y created (subsumed). *)
-text {* Sublocale, then interpretation in theory *}
+subsection {* Sublocale, then interpretation in theory *}
interpretation int: lgrp "op +" "0" "minus"
proof unfold_locales
@@ -374,7 +372,7 @@
(* the latter comes through the sublocale relation *)
-text {* Interpretation in theory, then sublocale *}
+subsection {* Interpretation in theory, then sublocale *}
interpretation (* fol: *) logic "op +" "minus"
(* FIXME declaration of qualified names *)
@@ -386,10 +384,12 @@
assumes assoc: "(x && y) && z = x && (y && z)"
and notnot: "-- (-- x) = x"
begin
-(* FIXME
+
+(* FIXME interpretation below fails
definition lor (infixl "||" 50) where
"x || y = --(-- x && -- y)"
*)
+
end
sublocale logic < two: logic2
@@ -398,7 +398,45 @@
thm two.assoc
-text {* Interpretation in proofs *}
+subsection {* Declarations and sublocale *}
+
+locale logic_a = logic
+locale logic_b = logic
+
+sublocale logic_a < logic_b
+ by unfold_locales
+
+
+subsection {* Equations *}
+
+locale logic_o =
+ fixes land (infixl "&&" 55)
+ and lnot ("-- _" [60] 60)
+ assumes assoc_o: "(x && y) && z <-> x && (y && z)"
+ and notnot_o: "-- (-- x) <-> x"
+begin
+
+definition lor_o (infixl "||" 50) where
+ "x || y <-> --(-- x && -- y)"
+
+end
+
+interpretation x: logic_o "op &" "Not"
+ where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+proof -
+ show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
+ show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+ by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
+qed
+
+thm x.lor_o_def bool_logic_o
+
+lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
+
+(* thm x.lor_triv *)
+
+
+subsection {* Interpretation in proofs *}
lemma True
proof
--- a/src/Pure/General/binding.ML Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/General/binding.ML Fri Dec 12 14:30:21 2008 +0100
@@ -59,8 +59,8 @@
val qualify = map_base o qualify_base;
(*FIXME should all operations on bare names move here from name_space.ML ?*)
-fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
- else (map_binding o apfst) (cons (prfx, sticky)) b;
+fun add_prefix sticky "" b = b
+ | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b;
fun map_prefix f (Binding ((prefix, name), pos)) =
f prefix (name_pos (name, pos));
--- a/src/Pure/IsaMakefile Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/IsaMakefile Fri Dec 12 14:30:21 2008 +0100
@@ -26,7 +26,8 @@
Concurrent/par_list_dummy.ML Concurrent/schedule.ML \
Concurrent/simple_thread.ML Concurrent/synchronized.ML \
Concurrent/task_queue.ML General/ROOT.ML General/alist.ML \
- General/balanced_tree.ML General/basics.ML General/buffer.ML \
+ General/balanced_tree.ML General/basics.ML General/binding.ML \
+ General/buffer.ML \
General/file.ML General/graph.ML General/heap.ML General/integer.ML \
General/lazy.ML General/markup.ML General/name_space.ML \
General/ord_list.ML General/output.ML General/path.ML \
--- a/src/Pure/Isar/expression.ML Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/Isar/expression.ML Fri Dec 12 14:30:21 2008 +0100
@@ -28,8 +28,8 @@
(* Interpretation *)
val sublocale_cmd: string -> expression -> theory -> Proof.state;
val sublocale: string -> expression_i -> theory -> Proof.state;
- val interpretation_cmd: expression -> theory -> Proof.state;
- val interpretation: expression_i -> theory -> Proof.state;
+ val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state;
+ val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state;
val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
val interpret: expression_i -> bool -> Proof.state -> Proof.state;
end;
@@ -175,7 +175,7 @@
val inst = Symtab.make insts'';
in
(Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
- Morphism.binding_morphism (Binding.qualify prfx), ctxt')
+ Morphism.binding_morphism (Binding.add_prefix false prfx), ctxt')
end;
@@ -410,7 +410,7 @@
val fors = prep_vars fixed context |> fst;
val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
- val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_local_idents ctxt);
+ val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], ctxt);
val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
@@ -484,7 +484,7 @@
(* Declare parameters and imported facts *)
val context' = context |>
ProofContext.add_fixes_i fixed |> snd |>
- NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
+ fold NewLocale.activate_local_facts deps;
val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
in ((fixed, deps, elems'), (parms, spec, defs)) end;
@@ -786,33 +786,63 @@
local
-fun gen_interpretation prep_expr
- expression thy =
+datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list;
+
+fun gen_interpretation prep_expr parse_prop prep_attr
+ expression equations thy =
let
val ctxt = ProofContext.init thy;
- val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
+ val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
- fun store_reg ((name, morph), thms) =
- let
- val morph' = morph $> Element.satisfy_morphism thms $> export;
- in
- NewLocale.add_global_registration (name, morph') #>
- NewLocale.activate_global_facts (name, morph')
- end;
+ val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
+ val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations;
+ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+ val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+
+ fun store (Reg (name, morph), thms) (regs, thy) =
+ let
+ val thms' = map (Element.morph_witness export') thms;
+ val morph' = morph $> Element.satisfy_morphism thms';
+ val add = NewLocale.add_global_registration (name, (morph', export));
+ in ((name, morph') :: regs, add thy) end
+ | store (Eqns [], []) (regs, thy) =
+ let val add = fold_rev (fn (name, morph) =>
+ NewLocale.activate_global_facts (name, morph $> export)) regs;
+ in (regs, add thy) end
+ | store (Eqns attns, thms) (regs, thy) =
+ let
+ val thms' = thms |> map (Element.conclude_witness #>
+ Morphism.thm (export' $> export) #>
+ LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+ Drule.abs_def);
+ val eq_morph =
+ Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
+ Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+ val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
+ val add =
+ fold_rev (fn (name, morph) =>
+ NewLocale.amend_global_registration eq_morph (name, morph) #>
+ NewLocale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
+ PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
+ snd
+ in (regs, add thy) end;
fun after_qed results =
- ProofContext.theory (fold store_reg (regs ~~ prep_result propss results));
+ ProofContext.theory (fn thy =>
+ fold store (map Reg regs @ [Eqns eq_attns] ~~
+ prep_result (propss @ [eqns]) results) ([], thy) |> snd);
in
goal_ctxt |>
- Proof.theorem_i NONE after_qed (prep_propp propss) |>
+ Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |>
Element.refine_witness |> Seq.hd
end;
in
-fun interpretation_cmd x = gen_interpretation read_goal_expression x;
-fun interpretation x = gen_interpretation cert_goal_expression x;
+fun interpretation_cmd x = gen_interpretation read_goal_expression
+ Syntax.parse_prop Attrib.intern_src x;
+fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
end;
--- a/src/Pure/Isar/new_locale.ML Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Fri Dec 12 14:30:21 2008 +0100
@@ -47,9 +47,11 @@
val unfold_attrib: attribute
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
- (* Identifiers and registrations *)
- val clear_local_idents: Proof.context -> Proof.context
- val add_global_registration: (string * Morphism.morphism) -> theory -> theory
+ (* Registrations *)
+ val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
+ theory -> theory
+ val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
+ theory -> theory
val get_global_registrations: theory -> (string * Morphism.morphism) list
(* Diagnostic *)
@@ -223,12 +225,10 @@
fun get_global_idents thy =
let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
-val clear_global_idents = put_global_idents empty;
fun get_local_idents ctxt =
let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
-val clear_local_idents = put_local_idents empty;
end;
@@ -457,7 +457,8 @@
(* FIXME only global variant needed *)
structure RegistrationsData = GenericDataFun
(
- type T = ((string * Morphism.morphism) * stamp) list;
+ type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
+(* FIXME mixins need to be stamped *)
(* registrations, in reverse order of declaration *)
val empty = [];
val extend = I;
@@ -465,9 +466,26 @@
(* FIXME consolidate with dependencies, consider one data slot only *)
);
-val get_global_registrations = map fst o RegistrationsData.get o Context.Theory;
+val get_global_registrations =
+ Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
fun add_global_registration reg =
(Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
+fun amend_global_registration morph (name, base_morph) thy =
+ let
+ val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
+ val base = instance_of thy name base_morph;
+ fun match (name', (morph', _)) =
+ name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
+ val i = find_index match (rev regs);
+ val _ = if i = ~1 then error ("No interpretation of locale " ^
+ quote (extern thy name) ^ " and parameter instantiation " ^
+ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
+ else ();
+ in
+ (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
+ (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
+ end;
+
end;
--- a/src/Pure/library.ML Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/library.ML Fri Dec 12 14:30:21 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/library.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Markus Wenzel, TU Muenchen
@@ -491,7 +490,7 @@
| split_last [x] = ([], x)
| split_last (x :: xs) = apfst (cons x) (split_last xs);
-(*find the position of an element in a list*)
+(*find position of first element satisfying a predicate*)
fun find_index pred =
let fun find (_: int) [] = ~1
| find n (x :: xs) = if pred x then n else find (n + 1) xs;