author ballarin Sat, 25 Jun 2011 12:19:54 +0200 changeset 43543 eb8b4851b039 parent 43538 de5c79682b56 child 43544 6b95bcc5c2da
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
--- a/doc-src/Locales/Locales/Examples2.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -3,7 +3,7 @@
begin
text {* \vspace{-5ex} *}
interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::int) y = (x < y)"
+    where "int.less x y = (x < y)"
proof -
txt {* \normalsize The goals are now:
@{subgoals [display]}
@@ -12,7 +12,7 @@
by unfold_locales auto
txt {* \normalsize The second goal is shown by unfolding the
definition of @{term "partial_order.less"}. *}
-    show "partial_order.less op \<le> (x::int) y = (x < y)"
+    show "partial_order.less op \<le> x y = (x < y)"
unfolding partial_order.less_def [OF partial_order op \<le>]
by auto
qed
--- a/doc-src/Locales/Locales/Examples3.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -17,12 +17,12 @@
repeat the example from the previous section to illustrate this. *}

interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::int) y = (x < y)"
+    where "int.less x y = (x < y)"
proof -
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
by unfold_locales auto
then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
-    show "partial_order.less op \<le> (x::int) y = (x < y)"
+    show "int.less x y = (x < y)"
unfolding int.less_def by auto
qed

@@ -47,8 +47,8 @@
so they can be used in a later example.  *}

interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where int_min_eq: "lattice.meet op \<le> (x::int) y = min x y"
-      and int_max_eq: "lattice.join op \<le> (x::int) y = max x y"
+    where int_min_eq: "int.meet x y = min x y"
+      and int_max_eq: "int.join x y = max x y"
proof -
show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
txt {* \normalsize We have already shown that this is a partial
@@ -69,9 +69,9 @@
in a situation where the lattice theorems can be used in a
convenient way. *}
then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
-    show "lattice.meet op \<le> (x::int) y = min x y"
+    show "int.meet x y = min x y"
by (bestsimp simp: int.meet_def int.is_inf_def)
-    show "lattice.join op \<le> (x::int) y = max x y"
+    show "int.join x y = max x y"
by (bestsimp simp: int.join_def int.is_sup_def)
qed

--- a/doc-src/Locales/Locales/document/Examples2.tex	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Sat Jun 25 12:19:54 2011 +0200
@@ -30,7 +30,7 @@
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}int{\isaliteral{2C}{\isacharcomma}}\ int{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}less\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isaliteral{2D}{\isacharminus}}%
\begin{isamarkuptxt}%
@@ -52,7 +52,7 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
--- a/doc-src/Locales/Locales/document/Examples3.tex	Thu Jun 23 23:12:00 2011 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Sat Jun 25 12:19:54 2011 +0200
@@ -49,7 +49,7 @@
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}less\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
@@ -61,7 +61,7 @@
\ int{\isaliteral{3A}{\isacharcolon}}\ partial{\isaliteral{5F}{\isacharunderscore}}order\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}int{\isaliteral{2C}{\isacharcomma}}\ int{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}partial{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{2E}{\isachardot}}less\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}less\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ int{\isaliteral{2E}{\isachardot}}less{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
@@ -108,8 +108,8 @@
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ int{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isakeyword{where}\ int{\isaliteral{5F}{\isacharunderscore}}min{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}meet\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ int{\isaliteral{5F}{\isacharunderscore}}max{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}join\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isakeyword{where}\ int{\isaliteral{5F}{\isacharunderscore}}min{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}meet\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ int{\isaliteral{5F}{\isacharunderscore}}max{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}join\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
@@ -157,11 +157,11 @@
\ int{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}meet\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}meet\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ min\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}bestsimp\ simp{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2E}{\isachardot}}meet{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}inf{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}lattice{\isaliteral{2E}{\isachardot}}join\ op\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}int{\isaliteral{2E}{\isachardot}}join\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ max\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}bestsimp\ simp{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2E}{\isachardot}}join{\isaliteral{5F}{\isacharunderscore}}def\ int{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}sup{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -499,7 +499,7 @@
end

interpretation x: logic_o "op &" "Not"
-  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+  where bool_logic_o: "x.lor_o(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"
--- a/src/Pure/Isar/expression.ML	Thu Jun 23 23:12:00 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Jun 25 12:19:54 2011 +0200
@@ -797,6 +797,14 @@

(*** Interpretation ***)

+fun read_with_extended_syntax parse_prop deps ctxt props =
+  let
+    val deps_ctxt = fold Locale.activate_declarations deps ctxt;
+  in
+    map (parse_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
+      |> Variable.export_terms deps_ctxt ctxt
+  end;
+
(** Interpretation in theories and proof contexts **)

local
@@ -825,8 +833,8 @@
let
val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
|> prep_expr expression;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;

-    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
@@ -845,8 +853,8 @@
val theory = Proof_Context.theory_of ctxt;

val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;

-    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
@@ -904,8 +912,8 @@
val target = intern thy raw_target;
val target_ctxt = Named_Target.init before_exit target thy;
val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
+    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;

-    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
val attrss = 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;