--- a/NEWS Mon Sep 20 20:24:43 2021 +0200
+++ b/NEWS Tue Sep 21 16:23:33 2021 +0200
@@ -9,6 +9,12 @@
*** General ***
+* Commands 'syntax' and 'no_syntax' now work in a local theory context,
+but there is no proper way to refer to local entities --- in contrast to
+'notation' and 'no_notation'. Local syntax works well with 'bundle',
+e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
+Isabelle/HOL.
+
* Configuration option "show_results" controls output of final results
in commands like 'definition' or 'theorem'. Output is normally enabled
in interactive mode, but it could occasionally cause unnecessary
@@ -128,6 +134,11 @@
*** HOL ***
+* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
+"lattice_syntax": it can be used in a local context via 'include' or in
+a global theory via 'unbundle'. The opposite declarations are bundled as
+"no_lattice_syntax".
+
* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
use explict expression instead. Minor INCOMPATIBILITY.
@@ -251,6 +262,10 @@
* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
corresponding ML values, notably as arguments for Thm.instantiate etc.
+* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
+corresponding functions for the object-logic of the ML compilation
+context. This supersedes older mk_Trueprop / dest_Trueprop operations.
+
* ML antiquotations for type constructors and term constants:
\<^Type>\<open>c\<close>
--- a/etc/symbols Mon Sep 20 20:24:43 2021 +0200
+++ b/etc/symbols Tue Sep 21 16:23:33 2021 +0200
@@ -456,6 +456,8 @@
\<^ctyp> argument: cartouche
\<^keyword> argument: cartouche
\<^locale> argument: cartouche
+\<^make_judgment>
+\<^dest_judgment>
\<^make_string>
\<^method> argument: cartouche
\<^named_theorems> argument: cartouche
--- a/lib/texinputs/isabellesym.sty Mon Sep 20 20:24:43 2021 +0200
+++ b/lib/texinputs/isabellesym.sty Tue Sep 21 16:23:33 2021 +0200
@@ -446,6 +446,8 @@
\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
+\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}}
+\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}
\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Sep 21 16:23:33 2021 +0200
@@ -1077,8 +1077,8 @@
text \<open>
\begin{tabular}{rcll}
@{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def "syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def "no_syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
+ @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
--- a/src/Doc/Main/Main_Doc.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Doc/Main/Main_Doc.thy Tue Sep 21 16:23:33 2021 +0200
@@ -89,7 +89,7 @@
\subsubsection*{Syntax}
-Available by loading theory \<open>Lattice_Syntax\<close> in directory \<open>Library\<close>.
+Available via \<^theory_text>\<open>unbundle lattice_syntax\<close>.
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
@{text[source]"x \<sqsubseteq> y"} & \<^term>\<open>x \<le> y\<close>\\
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Tue Sep 21 16:23:33 2021 +0200
@@ -1,7 +1,9 @@
theory Setup
-imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
+imports Complex_Main "HOL-Library.Multiset"
begin
+unbundle lattice_syntax
+
ML_file \<open>../antiquote_setup.ML\<close>
ML_file \<open>../more_antiquote.ML\<close>
--- a/src/FOL/IFOL.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/FOL/IFOL.thy Tue Sep 21 16:23:33 2021 +0200
@@ -527,7 +527,7 @@
structure Hypsubst = Hypsubst
(
val dest_eq = FOLogic.dest_eq
- val dest_Trueprop = FOLogic.dest_Trueprop
+ val dest_Trueprop = \<^dest_judgment>
val dest_imp = FOLogic.dest_imp
val eq_reflection = @{thm eq_reflection}
val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
--- a/src/FOL/fologic.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/FOL/fologic.ML Tue Sep 21 16:23:33 2021 +0200
@@ -6,8 +6,6 @@
signature FOLOGIC =
sig
- val mk_Trueprop: term -> term
- val dest_Trueprop: term -> term
val mk_conj: term * term -> term
val mk_disj: term * term -> term
val mk_imp: term * term -> term
@@ -24,10 +22,6 @@
structure FOLogic: FOLOGIC =
struct
-fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
-
-val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
-
fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
--- a/src/HOL/Complete_Lattices.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Complete_Lattices.thy Tue Sep 21 16:23:33 2021 +0200
@@ -15,10 +15,10 @@
subsection \<open>Syntactic infimum and supremum operations\<close>
class Inf =
- fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>")
+ fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter> _" [900] 900)
class Sup =
- fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>")
+ fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion> _" [900] 900)
syntax
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
--- a/src/HOL/Examples/Knaster_Tarski.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Examples/Knaster_Tarski.thy Tue Sep 21 16:23:33 2021 +0200
@@ -7,9 +7,11 @@
section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
theory Knaster_Tarski
- imports Main "HOL-Library.Lattice_Syntax"
+ imports Main
begin
+unbundle lattice_syntax
+
subsection \<open>Prose version\<close>
--- a/src/HOL/Library/Combine_PER.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Library/Combine_PER.thy Tue Sep 21 16:23:33 2021 +0200
@@ -3,9 +3,11 @@
section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
theory Combine_PER
- imports Main Lattice_Syntax
+ imports Main
begin
+unbundle lattice_syntax
+
definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
--- a/src/HOL/Library/Complete_Partial_Order2.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Tue Sep 21 16:23:33 2021 +0200
@@ -5,9 +5,11 @@
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
- Main Lattice_Syntax
+ Main
begin
+unbundle lattice_syntax
+
lemma chain_transfer [transfer_rule]:
includes lifting_syntax
shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
--- a/src/HOL/Library/Lattice_Syntax.thy Mon Sep 20 20:24:43 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-section \<open>Pretty syntax for lattice operations\<close>
-
-theory Lattice_Syntax
-imports Main
-begin
-
-notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter> _" [900] 900) and
- Sup ("\<Squnion> _" [900] 900)
-
-syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-end
--- a/src/HOL/Library/Library.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Library/Library.thy Tue Sep 21 16:23:33 2021 +0200
@@ -46,7 +46,6 @@
IArray
Landau_Symbols
Lattice_Algebras
- Lattice_Syntax
Lattice_Constructions
Linear_Temporal_Logic_on_Streams
ListVector
--- a/src/HOL/Library/Option_ord.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Library/Option_ord.thy Tue Sep 21 16:23:33 2021 +0200
@@ -8,20 +8,7 @@
imports Main
begin
-notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter> _" [900] 900) and
- Sup ("\<Squnion> _" [900] 900)
-
-syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
+unbundle lattice_syntax
instantiation option :: (preorder) preorder
begin
@@ -462,19 +449,6 @@
instance option :: (complete_linorder) complete_linorder ..
-
-no_notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter> _" [900] 900) and
- Sup ("\<Squnion> _" [900] 900)
-
-no_syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+unbundle no_lattice_syntax
end
--- a/src/HOL/Library/code_lazy.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Tue Sep 21 16:23:33 2021 +0200
@@ -91,7 +91,7 @@
val lthy' = (snd o Local_Theory.begin_nested) lthy
val ((t, (_, thm)), lthy') = Specification.definition NONE [] []
((Thm.def_binding (Binding.name name), []), def) lthy'
- val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
+ val lthy' = Local_Theory.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
val lthy = Local_Theory.end_nested lthy'
val def_thm = singleton (Proof_Context.export lthy' lthy) thm
in
--- a/src/HOL/Main.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/HOL/Main.thy Tue Sep 21 16:23:33 2021 +0200
@@ -19,7 +19,7 @@
GCD
begin
-text \<open>Namespace cleanup\<close>
+subsection \<open>Namespace cleanup\<close>
hide_const (open)
czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
@@ -29,15 +29,9 @@
hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
-text \<open>Syntax cleanup\<close>
+subsection \<open>Syntax cleanup\<close>
no_notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>") and
- Sup ("\<Squnion>") and
ordLeq2 (infix "<=o" 50) and
ordLeq3 (infix "\<le>o" 50) and
ordLess2 (infix "<o" 50) and
@@ -48,7 +42,9 @@
BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
-bundle cardinal_syntax begin
+bundle cardinal_syntax
+begin
+
notation
ordLeq2 (infix "<=o" 50) and
ordLeq3 (infix "\<le>o" 50) and
@@ -63,8 +59,42 @@
alias czero = BNF_Cardinal_Arithmetic.czero
alias cone = BNF_Cardinal_Arithmetic.cone
alias ctwo = BNF_Cardinal_Arithmetic.ctwo
+
end
+
+subsection \<open>Lattice syntax\<close>
+
+bundle lattice_syntax
+begin
+
+notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter> _" [900] 900) and
+ Sup ("\<Squnion> _" [900] 900)
+
+syntax
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+end
+
+bundle no_lattice_syntax
+begin
+
+no_notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter> _" [900] 900) and
+ Sup ("\<Squnion> _" [900] 900)
+
no_syntax
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
@@ -72,3 +102,7 @@
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
end
+
+unbundle no_lattice_syntax
+
+end
--- a/src/Pure/Isar/local_theory.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/Isar/local_theory.ML Tue Sep 21 16:23:33 2021 +0200
@@ -60,8 +60,15 @@
val pretty: local_theory -> Pretty.T list
val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
val set_defsort: sort -> local_theory -> local_theory
+ val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+ local_theory -> local_theory
+ val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
+ local_theory -> local_theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
+ val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
+ local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+ val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val type_alias: binding -> string -> local_theory -> local_theory
val const_alias: binding -> string -> local_theory -> local_theory
val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
@@ -297,11 +304,30 @@
(K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
+(* syntax *)
+
+fun gen_syntax prep_type add mode raw_args lthy =
+ let
+ val args = map (fn (c, T, mx) => (c, prep_type lthy T, mx)) raw_args;
+ val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
+ val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
+ in
+ declaration {syntax = true, pervasive = false}
+ (fn _ => Proof_Context.generic_syntax add mode args') lthy
+ end;
+
+val syntax = gen_syntax (K I);
+val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;
+
+
(* notation *)
-fun type_notation add mode raw_args lthy =
+local
+
+fun gen_type_notation prep_type add mode raw_args lthy =
let
- val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
+ val prepare = prep_type lthy #> Logic.type_map (Assumption.export_term lthy (target_of lthy));
+ val args = map (apfst prepare) raw_args;
val args' = map (apsnd Mixfix.reset_pos) args;
val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
in
@@ -309,9 +335,10 @@
(Proof_Context.generic_type_notation add mode args') lthy
end;
-fun notation add mode raw_args lthy =
+fun gen_notation prep_const add mode raw_args lthy =
let
- val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
+ val prepare = prep_const lthy #> Assumption.export_term lthy (target_of lthy);
+ val args = map (apfst prepare) raw_args;
val args' = map (apsnd Mixfix.reset_pos) args;
val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
in
@@ -319,6 +346,17 @@
(Proof_Context.generic_notation add mode args') lthy
end;
+in
+
+val type_notation = gen_type_notation (K I);
+val type_notation_cmd =
+ gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
+
+val notation = gen_notation (K I);
+val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
+
+end;
+
(* name space aliases *)
--- a/src/Pure/Isar/object_logic.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/Isar/object_logic.ML Tue Sep 21 16:23:33 2021 +0200
@@ -11,6 +11,7 @@
val add_judgment: binding * typ * mixfix -> theory -> theory
val add_judgment_cmd: binding * string * mixfix -> theory -> theory
val judgment_name: Proof.context -> string
+ val judgment_const: Proof.context -> string * typ
val is_judgment: Proof.context -> term -> bool
val drop_judgment: Proof.context -> term -> term
val fixed_judgment: Proof.context -> string -> term
@@ -91,10 +92,9 @@
let
val c = Sign.full_name thy b;
val thy' = thy |> add_consts [(b, T, mx)];
- val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
in
thy'
- |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
+ |> Theory.add_deps_const c
|> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
if is_some judgment then error "Attempt to redeclare object-logic judgment"
else (base_sort, SOME c, atomize_rulify))
@@ -115,6 +115,13 @@
SOME name => name
| _ => raise TERM ("Unknown object-logic judgment", []));
+fun judgment_const ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val c = judgment_name ctxt;
+ val T = Sign.the_const_type thy c;
+ in (c, T) end;
+
fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
| is_judgment _ _ = false;
--- a/src/Pure/Isar/proof_context.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 21 16:23:33 2021 +0200
@@ -155,6 +155,11 @@
val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
val check_case: Proof.context -> bool ->
string * Position.T -> binding option list -> Rule_Cases.T
+ val check_syntax_const: Proof.context -> string * Position.T -> string
+ val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+ Proof.context -> Proof.context
+ val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+ Context.generic -> Context.generic
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 generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -1123,6 +1128,20 @@
end;
+(* syntax *)
+
+fun check_syntax_const ctxt (c, pos) =
+ if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
+ else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
+
+fun syntax add mode args ctxt =
+ let val args' = map (pair Local_Syntax.Const) args
+ in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
+
+fun generic_syntax add mode args =
+ Context.mapping (Sign.syntax add mode args) (syntax add mode args);
+
+
(* notation *)
local
@@ -1138,9 +1157,9 @@
| NONE => NONE)
| const_syntax _ _ = NONE;
-fun gen_notation syntax add mode args ctxt =
+fun gen_notation make_syntax add mode args ctxt =
ctxt |> map_syntax_idents
- (Local_Syntax.update_modesyntax ctxt add mode (map_filter (syntax ctxt) args));
+ (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args));
in
--- a/src/Pure/Isar/specification.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/Isar/specification.ML Tue Sep 21 16:23:33 2021 +0200
@@ -46,11 +46,6 @@
val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
val type_alias: binding * string -> local_theory -> local_theory
val type_alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
- val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
- val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
- local_theory -> local_theory
- val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
- val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
(Attrib.binding * Attrib.thms) list ->
(binding * typ option * mixfix) list ->
@@ -334,28 +329,6 @@
gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
-(* notation *)
-
-local
-
-fun gen_type_notation prep_type add mode args lthy =
- lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
-
-fun gen_notation prep_const add mode args lthy =
- lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
-
-in
-
-val type_notation = gen_type_notation (K I);
-val type_notation_cmd =
- gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
-
-val notation = gen_notation (K I);
-val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
-
-end;
-
-
(* fact statements *)
local
--- a/src/Pure/ML/ml_antiquotations1.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML Tue Sep 21 16:23:33 2021 +0200
@@ -4,7 +4,13 @@
Miscellaneous ML antiquotations: part 1.
*)
-structure ML_Antiquotations1: sig end =
+signature ML_ANTIQUOTATIONS1 =
+sig
+ val make_judgment: Proof.context -> term -> term
+ val dest_judgment: Proof.context -> term -> term
+end;
+
+structure ML_Antiquotations1: ML_ANTIQUOTATIONS1 =
struct
(* ML support *)
@@ -171,10 +177,8 @@
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
- if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
- then ML_Syntax.print_string c
- else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+ ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close>
(Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
@@ -192,6 +196,22 @@
in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
+(* object-logic judgment *)
+
+fun make_judgment ctxt t = Const (Object_Logic.judgment_const ctxt) $ t;
+
+fun dest_judgment ctxt t =
+ if Object_Logic.is_judgment ctxt t
+ then Object_Logic.drop_judgment ctxt t
+ else raise TERM ("dest_judgment", [t]);
+
+val _ = Theory.setup
+ (ML_Antiquotation.value \<^binding>\<open>make_judgment\<close>
+ (Scan.succeed "ML_Antiquotations1.make_judgment ML_context") #>
+ ML_Antiquotation.value \<^binding>\<open>dest_judgment\<close>
+ (Scan.succeed "ML_Antiquotations1.dest_judgment ML_context"));
+
+
(* type/term constructors *)
local
--- a/src/Pure/Proof/proof_syntax.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Sep 21 16:23:33 2021 +0200
@@ -46,7 +46,7 @@
|> Sign.add_nonterminals_global
[Binding.make ("param", \<^here>),
Binding.make ("params", \<^here>)]
- |> Sign.add_syntax Syntax.mode_default
+ |> Sign.syntax true Syntax.mode_default
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
--- a/src/Pure/Pure.thy Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/Pure.thy Tue Sep 21 16:23:33 2021 +0200
@@ -384,14 +384,14 @@
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
val _ =
- Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
+ Outer_Syntax.local_theory \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
(Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
- >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
+ >> uncurry (Local_Theory.syntax_cmd true));
val _ =
- Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
+ Outer_Syntax.local_theory \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
(Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
- >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
+ >> uncurry (Local_Theory.syntax_cmd false));
val trans_pat =
Scan.optional
@@ -499,25 +499,25 @@
Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
"add concrete syntax for type constructors"
(Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
- >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+ >> (fn (mode, args) => Local_Theory.type_notation_cmd true mode args));
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>no_type_notation\<close>
"delete concrete syntax for type constructors"
(Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
- >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+ >> (fn (mode, args) => Local_Theory.type_notation_cmd false mode args));
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>notation\<close>
"add concrete syntax for constants / fixed variables"
(Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
- >> (fn (mode, args) => Specification.notation_cmd true mode args));
+ >> (fn (mode, args) => Local_Theory.notation_cmd true mode args));
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>no_notation\<close>
"delete concrete syntax for constants / fixed variables"
(Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
- >> (fn (mode, args) => Specification.notation_cmd false mode args));
+ >> (fn (mode, args) => Local_Theory.notation_cmd false mode args));
in end\<close>
--- a/src/Pure/System/isabelle_system.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML Tue Sep 21 16:23:33 2021 +0200
@@ -180,6 +180,7 @@
fun isabelle_name () = getenv_strict "ISABELLE_NAME";
-fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading ();
+fun identification () =
+ "Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading ();
end;
--- a/src/Pure/System/isabelle_system.scala Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Sep 21 16:23:33 2021 +0200
@@ -139,7 +139,8 @@
def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
- def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
+ def identification(): String =
+ "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading()
/** file-system operations **/
--- a/src/Pure/pure_thy.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/pure_thy.ML Tue Sep 21 16:23:33 2021 +0200
@@ -29,18 +29,6 @@
fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
-fun add_deps_type c thy =
- let
- val n = Sign.arity_number thy c;
- val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
- in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end
-
-fun add_deps_const c thy =
- let
- val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
- val typargs = Sign.const_typargs thy (c, T);
- in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end;
-
(* application syntax variants *)
@@ -68,8 +56,8 @@
val old_appl_syntax_setup =
Old_Appl_Syntax.put true #>
- Sign.del_syntax Syntax.mode_default applC_syntax #>
- Sign.add_syntax Syntax.mode_default appl_syntax;
+ Sign.syntax false Syntax.mode_default applC_syntax #>
+ Sign.syntax true Syntax.mode_default appl_syntax;
(* main content *)
@@ -86,11 +74,11 @@
(Binding.make ("itself", \<^here>), 1, NoSyn),
(Binding.make ("dummy", \<^here>), 0, NoSyn),
(qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)]
- #> add_deps_type "fun"
- #> add_deps_type "prop"
- #> add_deps_type "itself"
- #> add_deps_type "dummy"
- #> add_deps_type "Pure.proof"
+ #> Theory.add_deps_type "fun"
+ #> Theory.add_deps_type "prop"
+ #> Theory.add_deps_type "itself"
+ #> Theory.add_deps_type "dummy"
+ #> Theory.add_deps_type "Pure.proof"
#> Sign.add_nonterminals_global
(map (fn name => Binding.make (name, \<^here>))
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -100,8 +88,8 @@
"tvar_position", "id_position", "longid_position", "var_position",
"str_position", "string_position", "cartouche_position", "type_name",
"class_name"]))
- #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
- #> Sign.add_syntax Syntax.mode_default
+ #> Sign.syntax true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
+ #> Sign.syntax true Syntax.mode_default
[("", typ "prop' \<Rightarrow> prop", Mixfix.mixfix "_"),
("", typ "logic \<Rightarrow> any", Mixfix.mixfix "_"),
("", typ "prop' \<Rightarrow> any", Mixfix.mixfix "_"),
@@ -197,8 +185,8 @@
("_sort_constraint", typ "type \<Rightarrow> prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic \<Rightarrow> prop", Mixfix.mixfix "TERM _"),
(const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
- #> Sign.add_syntax Syntax.mode_default applC_syntax
- #> Sign.add_syntax (Print_Mode.ASCII, true)
+ #> Sign.syntax true Syntax.mode_default applC_syntax
+ #> Sign.syntax true (Print_Mode.ASCII, true)
[(tycon "fun", typ "type \<Rightarrow> type \<Rightarrow> type", mixfix ("(_/ => _)", [1, 0], 0)),
("_bracket", typ "types \<Rightarrow> type \<Rightarrow> type", mixfix ("([_]/ => _)", [0, 0], 0)),
("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3)),
@@ -208,7 +196,7 @@
("_DDDOT", typ "aprop", Mixfix.mixfix "..."),
("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Mixfix.mixfix "...")]
- #> Sign.add_syntax ("", false)
+ #> Sign.syntax true ("", false)
[(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))]
#> Sign.add_consts
[(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)),
@@ -225,11 +213,11 @@
(qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
(qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
(qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
- #> add_deps_const "Pure.eq"
- #> add_deps_const "Pure.imp"
- #> add_deps_const "Pure.all"
- #> add_deps_const "Pure.type"
- #> add_deps_const "Pure.dummy_pattern"
+ #> Theory.add_deps_const "Pure.eq"
+ #> Theory.add_deps_const "Pure.imp"
+ #> Theory.add_deps_const "Pure.all"
+ #> Theory.add_deps_const "Pure.type"
+ #> Theory.add_deps_const "Pure.dummy_pattern"
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
--- a/src/Pure/sign.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/sign.ML Tue Sep 21 16:23:33 2021 +0200
@@ -72,10 +72,8 @@
val add_nonterminals: Proof.context -> binding list -> theory -> theory
val add_nonterminals_global: binding list -> theory -> theory
val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
- val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
- val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
- val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
- val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+ val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
@@ -369,19 +367,15 @@
(* modify syntax *)
-fun gen_syntax change_gram parse_typ mode args thy =
+fun gen_syntax parse_typ add mode args thy =
let
val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
- in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
-
-fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
+ in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end;
-val add_syntax = gen_add_syntax (K I);
-val add_syntax_cmd = gen_add_syntax Syntax.read_typ;
-val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I);
-val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
+val syntax = gen_syntax (K I);
+val syntax_cmd = gen_syntax Syntax.read_typ;
fun type_notation add mode args =
let
@@ -397,7 +391,7 @@
SOME T => SOME (Lexicon.mark_const c, T, mx)
| NONE => NONE)
| const_syntax _ = NONE;
- in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
+ in syntax add mode (map_filter const_syntax args) thy end;
(* add constants *)
@@ -418,7 +412,7 @@
in
thy
|> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
- |> add_syntax Syntax.mode_default (map #2 args)
+ |> syntax true Syntax.mode_default (map #2 args)
|> pair (map #3 args)
end;
--- a/src/Pure/theory.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/Pure/theory.ML Tue Sep 21 16:23:33 2021 +0200
@@ -30,6 +30,8 @@
val type_dep: string * typ list -> Defs.entry
val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
+ val add_deps_const: string -> theory -> theory
+ val add_deps_type: string -> theory -> theory
val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
val specify_const: (binding * typ) * mixfix -> theory -> term * theory
val check_overloading: Proof.context -> bool -> string * typ -> unit
@@ -270,6 +272,16 @@
fun add_deps_global a x y thy =
add_deps (Defs.global_context thy) a x y thy;
+fun add_deps_const c thy =
+ let val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
+ in thy |> add_deps_global "" (const_dep thy (c, T)) [] end;
+
+fun add_deps_type c thy =
+ let
+ val n = Sign.arity_number thy c;
+ val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+ in thy |> add_deps_global "" (type_dep (c, args)) [] end
+
fun specify_const decl thy =
let val (t, thy') = Sign.declare_const_global decl thy;
in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
--- a/src/ZF/Tools/datatype_package.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Sep 21 16:23:33 2021 +0200
@@ -270,7 +270,7 @@
(*Each equation has the form
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
- FOLogic.mk_Trueprop
+ \<^make_judgment>
(FOLogic.mk_eq
(case_tm $
(list_comb (Const (Sign.intern_const thy1 name,T),
@@ -320,7 +320,7 @@
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
constructor argument.*)
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
- FOLogic.mk_Trueprop
+ \<^make_judgment>
(FOLogic.mk_eq
(recursor_tm $
(list_comb (Const (Sign.intern_const thy2 name,T),
--- a/src/ZF/Tools/ind_cases.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/Tools/ind_cases.ML Tue Sep 21 16:23:33 2021 +0200
@@ -33,7 +33,7 @@
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
- val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
+ val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (\<^dest_judgment>
(Logic.strip_imp_concl A)))))) handle TERM _ => err "";
in
(case Symtab.lookup (IndCasesData.get thy) c of
--- a/src/ZF/Tools/induct_tacs.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue Sep 21 16:23:33 2021 +0200
@@ -72,7 +72,7 @@
fun find_tname ctxt var As =
let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
- val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
+ val pairs = map_filter (try (mk_pair o \<^dest_judgment>)) As
val x =
(case try (dest_Free o Syntax.read_term ctxt) var of
SOME (x, _) => x
@@ -101,7 +101,7 @@
val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
(case Thm.prems_of rule of
[] => error "induction is not available for this datatype"
- | major::_ => FOLogic.dest_Trueprop major)
+ | major::_ => \<^dest_judgment> major)
in
Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
end
@@ -124,9 +124,9 @@
Syntax.string_of_term_global thy eqn);
val constructors =
- map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
+ map (head_of o const_of o \<^dest_judgment> o Thm.prop_of) case_eqns;
- val \<^Const_>\<open>mem for _ data\<close> = FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
+ val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.prems_of elim));
val Const(big_rec_name, _) = head_of data;
--- a/src/ZF/Tools/inductive_package.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Sep 21 16:23:33 2021 +0200
@@ -185,7 +185,7 @@
val dummy = writeln " Proving monotonicity...";
val bnd_mono0 =
- Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
+ Goal.prove_global thy1 [] [] (\<^make_judgment> (Fp.bnd_mono $ dom_sum $ fp_abs))
(fn {context = ctxt, ...} => EVERY
[resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
@@ -300,7 +300,7 @@
prem is a premise of an intr rule*)
fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
(case AList.lookup (op aconv) ind_alist X of
- SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
+ SOME pred => prem :: \<^make_judgment> (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
let fun mk_sb (rec_tm,pred) =
(rec_tm, \<^Const>\<open>Collect\<close> $ rec_tm $ pred)
@@ -314,7 +314,7 @@
(Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr
val (SOME pred) = AList.lookup (op aconv) ind_alist X
- val concl = FOLogic.mk_Trueprop (pred $ t)
+ val concl = \<^make_judgment> (pred $ t)
in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end
handle Bind => error"Recursion term not found in conclusion";
@@ -349,7 +349,7 @@
val quant_induct =
Goal.prove_global thy4 [] ind_prems
- (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
+ (\<^make_judgment> (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
(fn {context = ctxt, prems} => EVERY
[rewrite_goals_tac ctxt part_rec_defs,
resolve_tac ctxt [@{thm impI} RS @{thm allI}] 1,
@@ -404,14 +404,14 @@
(*To instantiate the main induction rule*)
val induct_concl =
- FOLogic.mk_Trueprop
+ \<^make_judgment>
(Ind_Syntax.mk_all_imp
(big_rec_tm,
Abs("z", \<^Type>\<open>i\<close>,
Balanced_Tree.make FOLogic.mk_conj
(ListPair.map mk_rec_imp (rec_tms, preds)))))
and mutual_induct_concl =
- FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
+ \<^make_judgment> (Balanced_Tree.make FOLogic.mk_conj qconcls);
val dummy = if !Ind_Syntax.trace then
(writeln ("induct_concl = " ^
--- a/src/ZF/Tools/primrec_package.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Sep 21 16:23:33 2021 +0200
@@ -18,7 +18,7 @@
exception RecError of string;
(*Remove outer Trueprop and equality sign*)
-val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
+val dest_eqn = FOLogic.dest_eq o \<^dest_judgment>;
fun primrec_err s = error ("Primrec definition error:\n" ^ s);
--- a/src/ZF/arith_data.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/arith_data.ML Tue Sep 21 16:23:33 2021 +0200
@@ -53,15 +53,13 @@
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
-fun is_eq_thm th =
- can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
+fun is_eq_thm th = can FOLogic.dest_eq (\<^dest_judgment> (Thm.prop_of th));
fun prove_conv name tacs ctxt prems (t,u) =
if t aconv u then NONE
else
let val prems' = filter_out is_eq_thm prems
- val goal = Logic.list_implies (map Thm.prop_of prems',
- FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
+ val goal = Logic.list_implies (map Thm.prop_of prems', \<^make_judgment> (mk_eq_iff (t, u)));
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
handle ERROR msg =>
(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
--- a/src/ZF/ind_syntax.ML Mon Sep 20 20:24:43 2021 +0200
+++ b/src/ZF/ind_syntax.ML Tue Sep 21 16:23:33 2021 +0200
@@ -79,9 +79,8 @@
let
fun mk_intr ((id,T,syn), name, args, prems) =
Logic.list_implies
- (map FOLogic.mk_Trueprop prems,
- FOLogic.mk_Trueprop
- (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
+ (map \<^make_judgment> prems,
+ \<^make_judgment> (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
in map mk_intr constructs end;
fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);