# HG changeset patch # User wenzelm # Date 1632234213 -7200 # Node ID e0c072a1377121b008bdb93a649a034391e30b7a # Parent 949054d78a77d2f78639c43718467f4943d0d731# Parent 5d411d85da8cd87af6e922611e6787e97ae62db0 merged diff -r 949054d78a77 -r e0c072a13771 NEWS --- 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>\?'a::sort\ and \<^var>\?x::type\ 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>\c\ diff -r 949054d78a77 -r e0c072a13771 etc/symbols --- 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 diff -r 949054d78a77 -r e0c072a13771 lib/texinputs/isabellesym.sty --- 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}} diff -r 949054d78a77 -r e0c072a13771 src/Doc/Isar_Ref/Inner_Syntax.thy --- 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 \ \begin{tabular}{rcll} @{command_def "nonterminal"} & : & \theory \ theory\ \\ - @{command_def "syntax"} & : & \theory \ theory\ \\ - @{command_def "no_syntax"} & : & \theory \ theory\ \\ + @{command_def "syntax"} & : & \local_theory \ local_theory\ \\ + @{command_def "no_syntax"} & : & \local_theory \ local_theory\ \\ @{command_def "translations"} & : & \theory \ theory\ \\ @{command_def "no_translations"} & : & \theory \ theory\ \\ @{attribute_def syntax_ast_trace} & : & \attribute\ & default \false\ \\ diff -r 949054d78a77 -r e0c072a13771 src/Doc/Main/Main_Doc.thy --- 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 \Lattice_Syntax\ in directory \Library\. +Available via \<^theory_text>\unbundle lattice_syntax\. \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} @{text[source]"x \ y"} & \<^term>\x \ y\\\ diff -r 949054d78a77 -r e0c072a13771 src/Doc/Typeclass_Hierarchy/Setup.thy --- 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 \../antiquote_setup.ML\ ML_file \../more_antiquote.ML\ diff -r 949054d78a77 -r e0c072a13771 src/FOL/IFOL.thy --- 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} diff -r 949054d78a77 -r e0c072a13771 src/FOL/fologic.ML --- 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>\Trueprop for P\; - -val dest_Trueprop = \<^Const_fn>\Trueprop for P => P\; - fun mk_conj (t1, t2) = \<^Const>\conj for t1 t2\ and mk_disj (t1, t2) = \<^Const>\disj for t1 t2\ and mk_imp (t1, t2) = \<^Const>\imp for t1 t2\ diff -r 949054d78a77 -r e0c072a13771 src/HOL/Complete_Lattices.thy --- 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 \Syntactic infimum and supremum operations\ class Inf = - fixes Inf :: "'a set \ 'a" ("\") + fixes Inf :: "'a set \ 'a" ("\ _" [900] 900) class Sup = - fixes Sup :: "'a set \ 'a" ("\") + fixes Sup :: "'a set \ 'a" ("\ _" [900] 900) syntax "_INF1" :: "pttrns \ 'b \ 'b" ("(3INF _./ _)" [0, 10] 10) diff -r 949054d78a77 -r e0c072a13771 src/HOL/Examples/Knaster_Tarski.thy --- 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 \Textbook-style reasoning: the Knaster-Tarski Theorem\ theory Knaster_Tarski - imports Main "HOL-Library.Lattice_Syntax" + imports Main begin +unbundle lattice_syntax + subsection \Prose version\ diff -r 949054d78a77 -r e0c072a13771 src/HOL/Library/Combine_PER.thy --- 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 \A combinator to build partial equivalence relations from a predicate and an equivalence relation\ theory Combine_PER - imports Main Lattice_Syntax + imports Main begin +unbundle lattice_syntax + definition combine_per :: "('a \ bool) \ ('a \ 'a \ bool) \ 'a \ 'a \ bool" where "combine_per P R = (\x y. P x \ P y) \ R" diff -r 949054d78a77 -r e0c072a13771 src/HOL/Library/Complete_Partial_Order2.thy --- 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 \Formalisation of chain-complete partial orders, continuity and admissibility\ 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" diff -r 949054d78a77 -r e0c072a13771 src/HOL/Library/Lattice_Syntax.thy --- 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 \Pretty syntax for lattice operations\ - -theory Lattice_Syntax -imports Main -begin - -notation - bot ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\ _" [900] 900) and - Sup ("\ _" [900] 900) - -syntax - "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - -end diff -r 949054d78a77 -r e0c072a13771 src/HOL/Library/Library.thy --- 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 diff -r 949054d78a77 -r e0c072a13771 src/HOL/Library/Option_ord.thy --- 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 ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\ _" [900] 900) and - Sup ("\ _" [900] 900) - -syntax - "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [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 ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\ _" [900] 900) and - Sup ("\ _" [900] 900) - -no_syntax - "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) +unbundle no_lattice_syntax end diff -r 949054d78a77 -r e0c072a13771 src/HOL/Library/code_lazy.ML --- 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 diff -r 949054d78a77 -r e0c072a13771 src/HOL/Main.thy --- 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 \Namespace cleanup\ +subsection \Namespace cleanup\ 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 \Syntax cleanup\ +subsection \Syntax cleanup\ no_notation - bot ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\") and - Sup ("\") and ordLeq2 (infix "<=o" 50) and ordLeq3 (infix "\o" 50) and ordLess2 (infix "(_,/ _)\") -bundle cardinal_syntax begin +bundle cardinal_syntax +begin + notation ordLeq2 (infix "<=o" 50) and ordLeq3 (infix "\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 \Lattice syntax\ + +bundle lattice_syntax +begin + +notation + bot ("\") and + top ("\") and + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\ _" [900] 900) and + Sup ("\ _" [900] 900) + +syntax + "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) + "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) + "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) + "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) + +end + +bundle no_lattice_syntax +begin + +no_notation + bot ("\") and + top ("\") and + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\ _" [900] 900) and + Sup ("\ _" [900] 900) + no_syntax "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) @@ -72,3 +102,7 @@ "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) end + +unbundle no_lattice_syntax + +end diff -r 949054d78a77 -r e0c072a13771 src/Pure/Isar/local_theory.ML --- 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 *) diff -r 949054d78a77 -r e0c072a13771 src/Pure/Isar/object_logic.ML --- 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; diff -r 949054d78a77 -r e0c072a13771 src/Pure/Isar/proof_context.ML --- 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 diff -r 949054d78a77 -r e0c072a13771 src/Pure/Isar/specification.ML --- 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 diff -r 949054d78a77 -r e0c072a13771 src/Pure/ML/ml_antiquotations1.ML --- 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>\syntax_const\ - (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>\const\ (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>\make_judgment\ + (Scan.succeed "ML_Antiquotations1.make_judgment ML_context") #> + ML_Antiquotation.value \<^binding>\dest_judgment\ + (Scan.succeed "ML_Antiquotations1.dest_judgment ML_context")); + + (* type/term constructors *) local diff -r 949054d78a77 -r e0c072a13771 src/Pure/Proof/proof_syntax.ML --- 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>\_./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), diff -r 949054d78a77 -r e0c072a13771 src/Pure/Pure.thy --- 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>\syntax\ "add raw syntax clauses" + Outer_Syntax.local_theory \<^command_keyword>\syntax\ "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>\no_syntax\ "delete raw syntax clauses" + Outer_Syntax.local_theory \<^command_keyword>\no_syntax\ "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>\type_notation\ "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>\no_type_notation\ "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>\notation\ "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>\no_notation\ "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\ diff -r 949054d78a77 -r e0c072a13771 src/Pure/System/isabelle_system.ML --- 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; diff -r 949054d78a77 -r e0c072a13771 src/Pure/System/isabelle_system.scala --- 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 **/ diff -r 949054d78a77 -r e0c072a13771 src/Pure/pure_thy.ML --- 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' \ prop", Mixfix.mixfix "_"), ("", typ "logic \ any", Mixfix.mixfix "_"), ("", typ "prop' \ any", Mixfix.mixfix "_"), @@ -197,8 +185,8 @@ ("_sort_constraint", typ "type \ prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic \ prop", Mixfix.mixfix "TERM _"), (const "Pure.conjunction", typ "prop \ prop \ 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 \ type \ type", mixfix ("(_/ => _)", [1, 0], 0)), ("_bracket", typ "types \ type \ type", mixfix ("([_]/ => _)", [0, 0], 0)), ("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3)), @@ -208,7 +196,7 @@ ("_DDDOT", typ "aprop", Mixfix.mixfix "..."), ("_bigimpl", typ "asms \ prop \ prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), ("_DDDOT", typ "logic", Mixfix.mixfix "...")] - #> Sign.add_syntax ("", false) + #> Sign.syntax true ("", false) [(const "Pure.prop", typ "prop \ prop", mixfix ("_", [0], 0))] #> Sign.add_consts [(qualify (Binding.make ("eq", \<^here>)), typ "'a \ 'a \ prop", infix_ ("\", 2)), @@ -225,11 +213,11 @@ (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \ Pure.proof", NoSyn), (qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \ prop) \ 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 diff -r 949054d78a77 -r e0c072a13771 src/Pure/sign.ML --- 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; diff -r 949054d78a77 -r e0c072a13771 src/Pure/theory.ML --- 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; diff -r 949054d78a77 -r e0c072a13771 src/ZF/Tools/datatype_package.ML --- 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), diff -r 949054d78a77 -r e0c072a13771 src/ZF/Tools/ind_cases.ML --- 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 diff -r 949054d78a77 -r e0c072a13771 src/ZF/Tools/induct_tacs.ML --- 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_>\mem for \Free (v,_)\ A\ = (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_>\mem for \Var(ixn,_)\ _\ = (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_>\mem for _ data\ = FOLogic.dest_Trueprop (hd (Thm.prems_of elim)); + val \<^Const_>\mem for _ data\ = \<^dest_judgment> (hd (Thm.prems_of elim)); val Const(big_rec_name, _) = head_of data; diff -r 949054d78a77 -r e0c072a13771 src/ZF/Tools/inductive_package.ML --- 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_>\Trueprop for \\<^Const_>\mem for t X\\\, 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>\Collect\ $ 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>\i\, 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 = " ^ diff -r 949054d78a77 -r e0c072a13771 src/ZF/Tools/primrec_package.ML --- 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); diff -r 949054d78a77 -r e0c072a13771 src/ZF/arith_data.ML --- 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) diff -r 949054d78a77 -r e0c072a13771 src/ZF/ind_syntax.ML --- 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>\mem\ $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm)) + (map \<^make_judgment> prems, + \<^make_judgment> (\<^Const>\mem\ $ 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);