Equations in interpretation as goals.
--- a/src/FOL/ex/NewLocaleSetup.thy Thu Dec 11 17:56:34 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy Fri Dec 12 12:31:00 2008 +0100
@@ -45,8 +45,7 @@
OuterSyntax.command "interpretation"
"prove interpretation of locale expression in theory" K.thy_goal
(P.!!! SpecParse.locale_expression --
- Scan.optional (P.$$$ "where" |-- P.and_list1 (P.alt_string >> Facts.Fact ||
- P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named)) []
+ 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)));
--- a/src/FOL/ex/NewLocaleTest.thy Thu Dec 11 17:56:34 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Fri Dec 12 12:31:00 2008 +0100
@@ -421,16 +421,15 @@
end
-lemma bool_logic_o: "PROP logic_o(op &, Not)"
- by unfold_locales fast+
+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
-lemma bool_lor_eq: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
- by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
-
-interpretation x: logic_o "op &" "Not" where bool_lor_eq
- by (rule bool_logic_o)
-
-thm x.lor_o_def
+thm x.lor_o_def bool_logic_o
lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
--- a/src/Pure/Isar/expression.ML Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/expression.ML Fri Dec 12 12:31:00 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 -> Facts.ref list -> theory -> Proof.state;
- val interpretation: expression_i -> thm list -> 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;
@@ -786,41 +786,63 @@
local
-fun gen_interpretation prep_expr prep_thms
+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 eqns = equations |> prep_thms ctxt |>
- map (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt);
- val eq_morph =
- Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
- Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
-
- val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
+ val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
+
+ 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) =
- let
- val morph' = morph $> Element.satisfy_morphism thms;
- in
- NewLocale.add_global_registration (name, (morph', export)) #>
- NewLocale.amend_global_registration (name, morph') eq_morph #>
- NewLocale.activate_global_facts (name, morph' $> eq_morph $> export)
- end;
+ 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
- (fn ctxt => map (ProofContext.get_fact ctxt) #> flat) x;
-fun interpretation x = gen_interpretation cert_goal_expression (K I) x;
+ 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 Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Fri Dec 12 12:31:00 2008 +0100
@@ -50,7 +50,7 @@
(* Registrations *)
val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
theory -> theory
- val amend_global_registration: (string * Morphism.morphism) -> Morphism.morphism ->
+ val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
theory -> theory
val get_global_registrations: theory -> (string * Morphism.morphism) list
@@ -471,7 +471,7 @@
fun add_global_registration reg =
(Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
-fun amend_global_registration (name, base_morph) morph thy =
+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;