diff --git a/src/Pure/Isar/bundle.ML b/src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML +++ b/src/Pure/Isar/bundle.ML @@ -1,247 +1,222 @@ (* Title: Pure/Isar/bundle.ML Author: Makarius Bundled declarations (notes etc.). *) signature BUNDLE = sig val check: Proof.context -> xstring * Position.T -> string val get: Proof.context -> string -> Attrib.thms val read: Proof.context -> xstring * Position.T -> Attrib.thms val print_bundles: bool -> Proof.context -> unit val bundle: binding * Attrib.thms -> (binding * typ option * mixfix) list -> local_theory -> local_theory val bundle_cmd: binding * (Facts.ref * Token.src list) list -> (binding * string option * mixfix) list -> local_theory -> local_theory val init: binding -> theory -> local_theory val unbundle: string list -> local_theory -> local_theory val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory val includes: string list -> Proof.context -> Proof.context val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context val include_: string list -> Proof.state -> Proof.state val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state val including: string list -> Proof.state -> Proof.state val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state - val context: string list -> Element.context_i list -> - local_theory -> Binding.scope * local_theory - val context_cmd: (xstring * Position.T) list -> Element.context list -> - local_theory -> Binding.scope * local_theory - val begin_nested_target: Context.generic -> local_theory - val end_nested_target: local_theory -> Context.generic end; structure Bundle: BUNDLE = struct (** context data **) structure Data = Generic_Data ( type T = Attrib.thms Name_Space.table * Attrib.thms option; val empty : T = (Name_Space.empty_table "bundle", NONE); val extend = I; fun merge ((tab1, target1), (tab2, target2)) = (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2)); ); (* bundles *) val get_all_generic = #1 o Data.get; val get_all = get_all_generic o Context.Proof; fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt); val get = Name_Space.get o get_all_generic o Context.Proof; fun read ctxt = get ctxt o check ctxt; fun define_bundle (b, bundle) context = let val bundle' = Attrib.trim_context_thms bundle; val (name, bundles') = Name_Space.define context true (b, bundle') (get_all_generic context); val context' = (Data.map o apfst o K) bundles' context; in (name, context') end; (* target -- bundle under construction *) fun the_target thy = (case #2 (Data.get (Context.Theory thy)) of SOME thms => thms | NONE => error "Missing bundle target"); val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms; fun augment_target thms = Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); (* print bundles *) fun pretty_bundle ctxt (markup_name, bundle) = let val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; fun prt_thm_attribs atts th = Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts)); fun prt_thms (ths, []) = map prt_thm ths | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths; in Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle))) end; fun print_bundles verbose ctxt = Pretty.writeln_chunks (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt))); (** define bundle **) fun transform_bundle phi = map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); (* command *) local fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy = let val (_, ctxt') = add_fixes raw_fixes lthy; val bundle0 = raw_bundle |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); val bundle = Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat |> transform_bundle (Proof_Context.export_morphism ctxt' lthy); in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle)) end; in val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes; val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; end; (* target *) local fun bad_operation _ = error "Not possible in bundle target"; fun conclude invisible binding = Local_Theory.background_theory_result (fn thy => thy |> invisible ? Context_Position.set_visible_global false |> Context.Theory |> define_bundle (binding, the_target thy) ||> (Context.the_theory #> invisible ? Context_Position.restore_visible_global thy #> reset_target)); fun pretty binding lthy = let val bundle = the_target (Proof_Context.theory_of lthy); val (name, lthy') = lthy |> Local_Theory.raw_theory (Context_Position.set_visible_global false) |> conclude true binding; val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy'); val markup_name = Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_all thy_ctxt')) name; in [pretty_bundle lthy' (markup_name, bundle)] end; fun bundle_notes kind facts lthy = let val bundle = facts |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms); in lthy |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle) |> Generic_Target.standard_notes (op <>) kind facts |> Attrib.local_notes kind facts end; fun bundle_declaration decl lthy = lthy |> (augment_target o Attrib.internal_declaration) (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl) |> Generic_Target.standard_declaration (K true) decl; in fun init binding thy = thy |> Generic_Target.init {background_naming = Sign.naming_of thy, setup = set_target [] #> Proof_Context.init_global, conclude = conclude false binding #> #2} {define = bad_operation, notes = bundle_notes, abbrev = bad_operation, declaration = K bundle_declaration, theory_registration = bad_operation, locale_dependency = bad_operation, pretty = pretty binding} end; (** activate bundles **) local fun gen_activate notes prep_bundle args ctxt = let val decls = maps (prep_bundle ctxt) args in ctxt |> Context_Position.set_visible false |> notes [(Binding.empty_atts, decls)] |> #2 |> Context_Position.restore_visible ctxt end; fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle; -fun gen_context prep_bundle prep_decl raw_incls raw_elems lthy = - lthy - |> gen_includes prep_bundle raw_incls - |> prep_decl ([], []) I raw_elems - |> (#4 o fst) - |> Local_Theory.begin_nested; - in val unbundle = gen_activate Local_Theory.notes get; val unbundle_cmd = gen_activate Local_Theory.notes read; val includes = gen_includes get; val includes_cmd = gen_includes read; fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts; fun include_cmd bs = Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts; fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); -val context = gen_context get Expression.cert_declaration; - -val context_cmd = gen_context read Expression.read_declaration; - -val begin_nested_target = - Context.cases Named_Target.theory_init Local_Theory.assert; - -fun end_nested_target lthy = - if Named_Target.is_theory lthy - then Context.Theory (Local_Theory.exit_global lthy) - else Context.Proof lthy; - end; end; diff --git a/src/Pure/Isar/named_target.ML b/src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML +++ b/src/Pure/Isar/named_target.ML @@ -1,162 +1,143 @@ (* Title: Pure/Isar/named_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Targets for theory, locale, class -- at the bottom of the nested structure. *) signature NAMED_TARGET = sig val is_theory: local_theory -> bool val locale_of: local_theory -> string option val bottom_locale_of: local_theory -> string option val class_of: local_theory -> string option val init: string -> theory -> local_theory val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} -> string -> theory -> local_theory val theory_init: theory -> local_theory val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory - val begin: xstring * Position.T -> theory -> local_theory - val exit: local_theory -> theory - val switch: (xstring * Position.T) option -> Context.generic -> - (local_theory -> Context.generic) * local_theory + val reinit: local_theory -> theory -> local_theory end; structure Named_Target: NAMED_TARGET = struct (* context data *) datatype target = Theory | Locale of string | Class of string; fun target_of_ident _ "" = Theory | target_of_ident thy ident = if Locale.defined thy ident then (if Class.is_class thy ident then Class else Locale) ident else error ("No such locale: " ^ quote ident); fun ident_of_target Theory = "" | ident_of_target (Locale locale) = locale | ident_of_target (Class class) = class; fun target_is_theory (SOME Theory) = true | target_is_theory _ = false; fun locale_of_target (SOME (Locale locale)) = SOME locale | locale_of_target (SOME (Class locale)) = SOME locale | locale_of_target _ = NONE; fun class_of_target (SOME (Class class)) = SOME class | class_of_target _ = NONE; structure Data = Proof_Data ( type T = target option; fun init _ = NONE; ); val get_bottom_target = Data.get; fun get_target lthy = if Local_Theory.level lthy = 1 then get_bottom_target lthy else NONE; fun ident_of lthy = case get_target lthy of NONE => error "Not in a named target" | SOME target => ident_of_target target; val is_theory = target_is_theory o get_target; val locale_of = locale_of_target o get_target; val bottom_locale_of = locale_of_target o get_bottom_target; val class_of = class_of_target o get_target; (* operations *) fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun class_foundation class (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params #> pair (lhs, def)); fun operations Theory = {define = Generic_Target.define Generic_Target.theory_target_foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.theory_abbrev, declaration = fn _ => Generic_Target.theory_declaration, theory_registration = Generic_Target.theory_registration, locale_dependency = fn _ => error "Not possible in theory target", pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} | operations (Locale locale) = {define = Generic_Target.define (locale_foundation locale), notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), abbrev = Generic_Target.locale_abbrev locale, declaration = Generic_Target.locale_declaration locale, theory_registration = fn _ => error "Not possible in locale target", locale_dependency = Generic_Target.locale_dependency locale, pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} | operations (Class class) = {define = Generic_Target.define (class_foundation class), notes = Generic_Target.notes (Generic_Target.locale_target_notes class), abbrev = Class.abbrev class, declaration = Generic_Target.locale_declaration class, theory_registration = fn _ => error "Not possible in class target", locale_dependency = Generic_Target.locale_dependency class, pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class}; fun setup_context Theory = Proof_Context.init_global | setup_context (Locale locale) = Locale.init locale | setup_context (Class class) = Class.init class; fun init' {setup, conclude} ident thy = let val target = target_of_ident thy ident; in thy |> Generic_Target.init {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), setup = setup_context target #> setup, conclude = conclude} (operations target) end; fun init ident thy = init' {setup = Data.put (SOME (target_of_ident thy ident)), conclude = I} ident thy; val theory_init = init ""; fun theory_map g = theory_init #> g #> Local_Theory.exit_global; fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; - -(* toplevel interaction *) - -fun begin ("-", _) thy = theory_init thy - | begin target thy = init (Locale.check thy target) thy; - -val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global; - -fun switch NONE (Context.Theory thy) = - (Context.Theory o exit, theory_init thy) - | switch (SOME name) (Context.Theory thy) = - (Context.Theory o exit, begin name thy) - | switch NONE (Context.Proof lthy) = - (Context.Proof o Local_Theory.reset, lthy) - | switch (SOME name) (Context.Proof lthy) = - (Context.Proof o init (ident_of lthy) o exit, - (begin name o exit o Local_Theory.assert_nonbrittle) lthy); +fun reinit lthy = init (ident_of lthy); end; diff --git a/src/Pure/Isar/target_context.ML b/src/Pure/Isar/target_context.ML new file mode 100644 --- /dev/null +++ b/src/Pure/Isar/target_context.ML @@ -0,0 +1,55 @@ +(* Title: Pure/Isar/target_context.ML + Author: Florian Haftmann + +Handling of named and nested targets at the Isar toplevel via context begin / end blocks. +*) + +signature TARGET_CONTEXT = +sig + val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory + val end_named_cmd: local_theory -> theory + val switch_named_cmd: (xstring * Position.T) option -> Context.generic -> + (local_theory -> Context.generic) * local_theory + val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list -> + Context.generic -> local_theory + val end_nested_cmd: local_theory -> Context.generic +end; + +structure Target_Context: TARGET_CONTEXT = +struct + +fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy + | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy; + +val end_named_cmd = Local_Theory.assert_bottom #> Local_Theory.exit_global; + +fun switch_named_cmd NONE (Context.Theory thy) = + (Context.Theory o end_named_cmd, Named_Target.theory_init thy) + | switch_named_cmd (SOME name) (Context.Theory thy) = + (Context.Theory o end_named_cmd, context_begin_named_cmd name thy) + | switch_named_cmd NONE (Context.Proof lthy) = + (Context.Proof o Local_Theory.reset, lthy) + | switch_named_cmd (SOME name) (Context.Proof lthy) = + (Context.Proof o Named_Target.reinit lthy o end_named_cmd, + (context_begin_named_cmd name o end_named_cmd o Local_Theory.assert_nonbrittle) lthy); + +fun includes raw_incls lthy = + Bundle.includes (map (Bundle.check lthy) raw_incls) lthy; + +fun context_begin_nested_cmd raw_incls raw_elems gthy = + gthy + |> Context.cases Named_Target.theory_init Local_Theory.assert + |> includes raw_incls + |> Expression.read_declaration ([], []) I raw_elems + |> (#4 o fst) + |> Local_Theory.begin_nested + |> snd; + +fun end_nested_cmd lthy = + if Named_Target.is_theory lthy + then Context.Theory (Local_Theory.exit_global lthy) + else Context.Proof lthy; + +end; + +structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end; diff --git a/src/Pure/Isar/toplevel.ML b/src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML +++ b/src/Pure/Isar/toplevel.ML @@ -1,793 +1,793 @@ (* Title: Pure/Isar/toplevel.ML Author: Markus Wenzel, TU Muenchen Isabelle/Isar toplevel transactions. *) signature TOPLEVEL = sig exception UNDEF type state val init_toplevel: unit -> state val theory_toplevel: theory -> state val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool val is_skipped_proof: state -> bool val level: state -> int val previous_theory_of: state -> theory option val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory val proof_of: state -> Proof.state val proof_position_of: state -> int val is_end_theory: state -> bool val end_theory: Position.T -> state -> theory val presentation_context: state -> Proof.context val presentation_state: Proof.context -> state val pretty_context: state -> Pretty.T list val pretty_state: state -> Pretty.T list val string_of_state: state -> string val pretty_abstract: state -> Pretty.T type transition val empty: transition val name_of: transition -> string val pos_of: transition -> Position.T val timing_of: transition -> Time.time val type_error: transition -> string val name: string -> transition -> transition val position: Position.T -> transition -> transition val markers: Input.source list -> transition -> transition val timing: Time.time -> transition -> transition val init_theory: (unit -> theory) -> transition -> transition val is_init: transition -> bool val modify_init: (unit -> theory) -> transition -> transition val exit: transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val keep_proof: (state -> unit) -> transition -> transition val ignored: Position.T -> transition val is_ignored: transition -> bool val malformed: Position.T -> string -> transition val generic_theory: (generic_theory -> generic_theory) -> transition -> transition val theory': (bool -> theory -> theory) -> transition -> transition val theory: (theory -> theory) -> transition -> transition val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition val end_main_target: transition -> transition - val begin_nested_target: (local_theory -> local_theory) -> transition -> transition + val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition val end_nested_target: transition -> transition val local_theory': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> local_theory) -> transition -> transition val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> local_theory) -> transition -> transition val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> transition -> transition val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> Proof.state) -> transition -> transition val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> Proof.state) -> transition -> transition val theory_to_proof: (theory -> Proof.state) -> transition -> transition val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition val forget_proof: transition -> transition val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (unit -> unit) -> transition -> transition val skip_proof_open: transition -> transition val skip_proof_close: transition -> transition val exec_id: Document_ID.exec -> transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> state * (exn * string) option val command_errors: bool -> transition -> state -> Runtime.error list * state option val command_exception: bool -> transition -> state -> state val reset_theory: state -> state option val reset_proof: state -> state option val reset_notepad: state -> state option val fork_presentation: transition -> transition * transition type result val join_results: result -> (transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state end; structure Toplevel: TOPLEVEL = struct (** toplevel state **) exception UNDEF = Runtime.UNDEF; (* datatype node *) datatype node = Toplevel (*toplevel outside of theory body*) | Theory of generic_theory (*global or local theory*) | Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) (*proof node, finish, original theory*) | Skipped_Proof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) val theory_node = fn Theory gthy => SOME gthy | _ => NONE; val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; fun cases_node f _ _ Toplevel = f () | cases_node _ g _ (Theory gthy) = g gthy | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf) | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy; fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h; val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of); (* datatype state *) type node_presentation = node * Proof.context; fun init_presentation () = Proof_Context.init_global (Theory.get_pure_bootstrap ()); fun node_presentation node = (node, cases_node init_presentation Context.proof_of Proof.context_of node); datatype state = State of node_presentation * theory option; (*current node with presentation context, previous theory*) fun node_of (State ((node, _), _)) = node; fun previous_theory_of (State (_, prev_thy)) = prev_thy; fun init_toplevel () = State (node_presentation Toplevel, NONE); fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); fun level state = (case node_of state of Toplevel => 0 | Theory _ => 0 | Proof (prf, _) => Proof.level (Proof_Node.current prf) | Skipped_Proof (d, _) => d + 1); (*different notion of proof depth!*) fun str_of_state state = (case node_of state of Toplevel => (case previous_theory_of state of NONE => "at top level" | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy)) | Theory (Context.Theory _) => "in theory mode" | Theory (Context.Proof _) => "in local theory mode" | Proof _ => "in proof mode" | Skipped_Proof _ => "in skipped proof mode"); (* current node *) fun is_toplevel state = (case node_of state of Toplevel => true | _ => false); fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state; fun proper_node_case f g state = cases_proper_node f g (proper_node_of state); val context_of = proper_node_case Context.proof_of Proof.context_of; val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of); val theory_of = proper_node_case Context.theory_of Proof.theory_of; val proof_of = proper_node_case (fn _ => error "No proof state") I; fun proof_position_of state = (case proper_node_of state of Proof (prf, _) => Proof_Node.position prf | _ => ~1); fun is_end_theory (State ((Toplevel, _), SOME _)) = true | is_end_theory _ = false; fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy | end_theory pos _ = error ("Malformed theory" ^ Position.here pos); (* presentation context *) structure Presentation_State = Proof_Data ( type T = state option; fun init _ = NONE; ); fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt; fun presentation_context (state as State (current, _)) = presentation_context0 state |> Presentation_State.put (SOME (State (current, NONE))); fun presentation_state ctxt = (case Presentation_State.get ctxt of NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE) | SOME state => state); (* print state *) fun pretty_context state = if is_toplevel state then [] else let val gthy = (case node_of state of Toplevel => raise Match | Theory gthy => gthy | Proof (_, (_, gthy)) => gthy | Skipped_Proof (_, (_, gthy)) => gthy); val lthy = Context.cases Named_Target.theory_init I gthy; in Local_Theory.pretty lthy end; fun pretty_state state = (case node_of state of Toplevel => [] | Theory _ => [] | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf) | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of; fun pretty_abstract state = Pretty.str (""); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract); (** toplevel transitions **) (* primitive transitions *) datatype trans = (*init theory*) Init of unit -> theory | (*formal exit of theory*) Exit | (*peek at state*) Keep of bool -> state -> unit | (*node transaction and presentation*) Transaction of (bool -> node -> node_presentation) * (state -> unit); local exception FAILURE of state * exn; fun apply f g node = let val node_pr = node_presentation node; val context = cases_proper_node I (Context.Proof o Proof.context_of) node; fun state_error e node_pr' = (State (node_pr', get_theory node), e); val (result, err) = node |> Runtime.controlled_execution (SOME context) f |> state_error NONE handle exn => state_error (SOME exn) node_pr; in (case err of NONE => tap g result | SOME exn => raise FAILURE (result, exn)) end; fun apply_tr int trans state = (case (trans, node_of state) of (Init f, Toplevel) => Runtime.controlled_execution NONE (fn () => State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = node |> apply (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) (K ()); in State ((Toplevel, pr_ctxt), get_theory node') end | (Keep f, node) => Runtime.controlled_execution (try generic_theory_of state) (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () | (Transaction _, Toplevel) => raise UNDEF | (Transaction (f, g), node) => apply (fn x => f int x) g node | _ => raise UNDEF); fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = apply_union int trs state handle Runtime.UNDEF => apply_tr int tr state | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state | exn as FAILURE _ => raise exn | exn => raise FAILURE (state, exn); fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) = let val state' = Runtime.controlled_execution (try generic_theory_of state) (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) (); in (state', NONE) end handle exn => (state, SOME exn); in fun apply_trans int name markers trans state = (apply_union int trans state |> apply_markers name markers) handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); end; (* datatype transition *) datatype transition = Transition of {name: string, (*command name*) pos: Position.T, (*source position*) markers: Input.source list, (*semantic document markers*) timing: Time.time, (*prescient timing information*) trans: trans list}; (*primitive transitions (union)*) fun make_transition (name, pos, markers, timing, trans) = Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans}; fun map_transition f (Transition {name, pos, markers, timing, trans}) = make_transition (f (name, pos, markers, timing, trans)); val empty = make_transition ("", Position.none, [], Time.zeroTime, []); (* diagnostics *) fun name_of (Transition {name, ...}) = name; fun pos_of (Transition {pos, ...}) = pos; fun timing_of (Transition {timing, ...}) = timing; fun command_msg msg tr = msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^ Position.here (pos_of tr); fun at_command tr = command_msg "At " tr; fun type_error tr = command_msg "Bad context for " tr; (* modify transitions *) fun name name = map_transition (fn (_, pos, markers, timing, trans) => (name, pos, markers, timing, trans)); fun position pos = map_transition (fn (name, _, markers, timing, trans) => (name, pos, markers, timing, trans)); fun markers markers = map_transition (fn (name, pos, _, timing, trans) => (name, pos, markers, timing, trans)); fun timing timing = map_transition (fn (name, pos, markers, _, trans) => (name, pos, markers, timing, trans)); fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) => (name, pos, markers, timing, tr :: trans)); val reset_trans = map_transition (fn (name, pos, markers, timing, _) => (name, pos, markers, timing, [])); (* basic transitions *) fun init_theory f = add_trans (Init f); fun is_init (Transition {trans = [Init _], ...}) = true | is_init _ = false; fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; val exit = add_trans Exit; val keep' = add_trans o Keep; fun present_transaction f g = add_trans (Transaction (f, g)); fun transaction f = present_transaction f (K ()); fun transaction0 f = present_transaction (node_presentation oo f) (K ()); fun keep f = add_trans (Keep (fn _ => f)); fun keep_proof f = keep (fn st => if is_proof st then f st else if is_skipped_proof st then () else warning "No proof state"); fun ignored pos = empty |> name "" |> position pos |> keep (fn _ => ()); fun is_ignored tr = name_of tr = ""; fun malformed pos msg = empty |> name "" |> position pos |> keep (fn _ => error msg); (* theory transitions *) fun generic_theory f = transaction (fn _ => (fn Theory gthy => node_presentation (Theory (f gthy)) | _ => raise UNDEF)); fun theory' f = transaction (fn int => (fn Theory (Context.Theory thy) => let val thy' = thy |> Sign.new_group |> f int |> Sign.reset_group; in node_presentation (Theory (Context.Theory thy')) end | _ => raise UNDEF)); fun theory f = theory' (K f); fun begin_main_target begin f = transaction (fn _ => (fn Theory (Context.Theory thy) => let val lthy = f thy; - val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy); + val gthy = + if begin + then Context.Proof lthy + else Context.Theory (Target_Context.end_named_cmd lthy); val _ = (case Local_Theory.pretty lthy of [] => () | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); in (Theory gthy, lthy) end | _ => raise UNDEF)); val end_main_target = transaction (fn _ => - (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Named_Target.exit lthy)), lthy) + (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Target_Context.end_named_cmd lthy)), lthy) | _ => raise UNDEF)); fun begin_nested_target f = transaction0 (fn _ => (fn Theory gthy => let - val lthy = Bundle.begin_nested_target gthy; - val lthy' = f lthy + val lthy' = f gthy; in Theory (Context.Proof lthy') end | _ => raise UNDEF)); val end_nested_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (case try Local_Theory.end_nested lthy of SOME lthy' => - let val gthy' = Bundle.end_nested_target lthy' + let val gthy' = Target_Context.end_nested_cmd lthy' in (Theory gthy', lthy) end | NONE => raise UNDEF) | _ => raise UNDEF)); fun restricted_context (SOME (strict, scope)) = Proof_Context.map_naming (Name_Space.restricted strict scope) | restricted_context NONE = I; fun local_theory' restricted target f = present_transaction (fn int => (fn Theory gthy => let - val (finish, lthy) = Named_Target.switch target gthy; + val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val lthy' = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int |> Local_Theory.reset_group; in (Theory (finish lthy'), lthy') end | _ => raise UNDEF)) (K ()); fun local_theory restricted target f = local_theory' restricted target (K f); fun present_local_theory target = present_transaction (fn _ => (fn Theory gthy => - let val (finish, lthy) = Named_Target.switch target gthy; + let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; in (Theory (finish lthy), lthy) end | _ => raise UNDEF)); (* proof transitions *) fun end_proof f = transaction (fn int => (fn Proof (prf, (finish, _)) => let val state = Proof_Node.current prf in if can (Proof.assert_bottom true) state then let val ctxt' = f int state; val gthy' = finish ctxt'; in (Theory gthy', ctxt') end else raise UNDEF end | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy) | _ => raise UNDEF)); local fun begin_proof init_proof = transaction0 (fn int => (fn Theory gthy => let val (finish, prf) = init_proof int gthy; val document = Options.default_string "document"; val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled (); val schematic_goal = try Proof.schematic_goal prf; val _ = if skip andalso schematic_goal = SOME true then warning "Cannot skip proof of schematic goal statement" else (); in if skip andalso schematic_goal = SOME false then Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); in fun local_theory_to_proof' restricted target f = begin_proof (fn int => fn gthy => let - val (finish, lthy) = Named_Target.switch target gthy; + val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val prf = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int; in (finish o Local_Theory.reset_group, prf) end); fun local_theory_to_proof restricted target f = local_theory_to_proof' restricted target (K f); fun theory_to_proof f = begin_proof (fn _ => fn gthy => (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, (case gthy of Context.Theory thy => f (Sign.new_group thy) | _ => raise UNDEF))); end; val forget_proof = transaction0 (fn _ => (fn Proof (prf, (_, orig_gthy)) => if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF else Theory orig_gthy | Skipped_Proof (_, (_, orig_gthy)) => Theory orig_gthy | _ => raise UNDEF)); fun proofs' f = transaction0 (fn int => (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) | skip as Skipped_Proof _ => skip | _ => raise UNDEF)); fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); val proofs = proofs' o K; val proof = proof' o K; (* skipped proofs *) fun actual_proof f = transaction0 (fn _ => (fn Proof (prf, x) => Proof (f prf, x) | _ => raise UNDEF)); fun skip_proof f = transaction0 (fn _ => (fn skip as Skipped_Proof _ => (f (); skip) | _ => raise UNDEF)); val skip_proof_open = transaction0 (fn _ => (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x) | _ => raise UNDEF)); val skip_proof_close = transaction0 (fn _ => (fn Skipped_Proof (0, (gthy, _)) => Theory gthy | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x) | _ => raise UNDEF)); (** toplevel transactions **) (* runtime position *) fun exec_id id (tr as Transition {pos, ...}) = position (Position.put_id (Document_ID.print id) pos) tr; fun setmp_thread_position (Transition {pos, ...}) f x = Position.setmp_thread_data pos f x; (* post-transition hooks *) local val hooks = Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); in fun add_hook hook = Synchronized.change hooks (cons hook); fun get_hooks () = Synchronized.value hooks; end; (* apply transitions *) local fun app int (tr as Transition {name, markers, trans, ...}) = setmp_thread_position tr (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans) ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)); in fun transition int tr st = let val (st', opt_err) = Context.setmp_generic_context (try (Context.Proof o presentation_context0) st) (fn () => app int tr st) (); val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ())); in (st', opt_err') end; end; (* managed commands *) fun command_errors int tr st = (case transition int tr st of (st', NONE) => ([], SOME st') | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE)); fun command_exception int tr st = (case transition int tr st of (st', NONE) => st' | (_, SOME (exn, info)) => if Exn.is_interrupt exn then Exn.reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)); val command = command_exception false; (* reset state *) local fun reset_state check trans st = if check st then NONE else #2 (command_errors false (trans empty) st); in val reset_theory = reset_state is_theory forget_proof; val reset_proof = reset_state is_proof (transaction0 (fn _ => (fn Theory gthy => Skipped_Proof (0, (gthy, gthy)) | _ => raise UNDEF))); val reset_notepad = reset_state (fn st => (case try proof_of st of SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state | NONE => true)) (proof Proof.reset_notepad); end; (* scheduled proof result *) datatype result = Result of transition * state | Result_List of result list | Result_Future of result future; fun join_results (Result x) = [x] | join_results (Result_List xs) = maps join_results xs | join_results (Result_Future x) = join_results (Future.join x); local structure Result = Proof_Data ( type T = result; fun init _ = Result_List []; ); val get_result = Result.get o Proof.context_of; val put_result = Proof.map_context o Result.put; fun timing_estimate elem = let val trs = tl (Thy_Element.flat_element elem) in fold (fn tr => fn t => timing_of tr + t) trs Time.zeroTime end; fun future_proofs_enabled estimate st = (case try proof_of st of NONE => false | SOME state => not (Proofterm.proofs_enabled ()) andalso not (Proof.is_relevant state) andalso (if can (Proof.assert_bottom true) state then Future.proofs_enabled 1 else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate)); val empty_markers = markers []; val empty_trans = reset_trans #> keep (K ()); in fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans); fun atom_result keywords tr st = let val st' = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then let val (tr1, tr2) = fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} (fn () => command tr1 st); in command tr2 st end else command tr st; in (Result (tr, st'), st') end; fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st = let val (head_result, st') = atom_result keywords head_tr st; val (body_elems, end_tr) = element_rest; val estimate = timing_estimate elem; in if not (future_proofs_enabled estimate st') then let val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr]; val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; in (Result_List (head_result :: proof_results), st'') end else let val (end_tr1, end_tr2) = fork_presentation end_tr; val finish = Context.Theory o Proof_Context.theory_of; val future_proof = Proof.future_proof (fn state => Execution.fork {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} (fn () => let val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st'; val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy)); val (results, result_state) = State (node_presentation node', prev_thy) |> fold_map (element_result keywords) body_elems ||> command end_tr1; in (Result_List results, presentation_context0 result_state) end)) #> (fn (res, state') => state' |> put_result (Result_Future res)); val forked_proof = proof (future_proof #> (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o end_proof (fn _ => future_proof #> (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); val st'' = st' |> command (head_tr |> reset_trans |> forked_proof); val end_st = st'' |> command end_tr2; val end_result = Result (end_tr, end_st); val result = Result_List [head_result, Result.get (presentation_context0 st''), end_result]; in (result, end_st) end end; end; end; - -structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end; diff --git a/src/Pure/Pure.thy b/src/Pure/Pure.thy --- a/src/Pure/Pure.thy +++ b/src/Pure/Pure.thy @@ -1,1503 +1,1504 @@ (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" "obtains" "shows" "when" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias" "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn and "axiomatization" :: thy_stmt and "external_file" "bibtex_file" :: thy_load and "generate_file" :: thy_decl and "export_generated_files" :: diag and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix" and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "ML_val" "ML_command" :: diag % "ML" and "simproc_setup" :: thy_decl % "ML" and "setup" "local_setup" "attribute_setup" "method_setup" "declaration" "syntax_declaration" "parse_ast_translation" "parse_translation" "print_translation" "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" and "bundle" :: thy_decl_block and "unbundle" :: thy_decl and "include" "including" :: prf_decl and "print_bundles" :: diag and "context" "locale" "experiment" :: thy_decl_block and "interpret" :: prf_goal % "proof" and "interpretation" "global_interpretation" "sublocale" :: thy_goal and "class" :: thy_decl_block and "subclass" :: thy_goal and "instantiation" :: thy_decl_block and "instance" :: thy_goal and "overloading" :: thy_decl_block and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt and "schematic_goal" :: thy_goal_stmt and "notepad" :: thy_decl_block and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" and "show" :: prf_asm_goal % "proof" and "thus" :: prf_asm_goal % "proof" and "then" "from" "with" :: prf_chain % "proof" and "note" :: prf_decl % "proof" and "supply" :: prf_script % "proof" and "using" "unfolding" :: prf_decl % "proof" and "fix" "assume" "presume" "define" :: prf_asm % "proof" and "consider" :: prf_goal % "proof" and "obtain" :: prf_asm_goal % "proof" and "guess" :: prf_script_asm_goal % "proof" and "let" "write" :: prf_decl % "proof" and "case" :: prf_asm % "proof" and "{" :: prf_open % "proof" and "}" :: prf_close % "proof" and "next" :: next_block % "proof" and "qed" :: qed_block % "proof" and "by" ".." "." "sorry" "\" :: "qed" % "proof" and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof" and "apply_end" :: prf_script % "proof" and "subgoal" :: prf_script_goal % "proof" and "proof" :: prf_block % "proof" and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" and "help" "print_commands" "print_options" "print_context" "print_theory" "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" "print_antiquotations" "print_ML_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings" "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag and "print_state" :: diag and "welcome" :: diag and "end" :: thy_end and "realizers" :: thy_decl and "realizability" :: thy_decl and "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl abbrevs "\\tag" = "\<^marker>\tag \" and "===>" = "===>" (*prevent replacement of very long arrows*) and "--->" = "\\" and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = "" and "hence" = "then have" and "thus" = "then show" begin section \Isar commands\ subsection \Other files\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\external_file\ "formal dependency on external file" (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files))); val _ = Outer_Syntax.command \<^command_keyword>\bibtex_file\ "check bibtex database file in Prover IDE" (Resources.provide_parse_files "bibtex_file" >> (fn files => Toplevel.theory (fn thy => let val ([{lines, pos, ...}], thy') = files thy; val _ = Bibtex.check_database_output pos (cat_lines lines); in thy' end))); val _ = Outer_Syntax.local_theory \<^command_keyword>\generate_file\ "generate source file, with antiquotations" (Parse.path_binding -- (\<^keyword>\=\ |-- Parse.embedded_input) >> Generated_Files.generate_file_cmd); val files_in_theory = (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- Scan.option (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.theory_name --| \<^keyword>\)\)); val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ "export generated files from given theories" (Parse.and_list1 files_in_theory >> (fn args => Toplevel.keep (fn st => Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))); val base_dir = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.position Parse.path --| \<^keyword>\)\)) ("", Position.none); val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir; val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false; val executable = \<^keyword>\(\ |-- Parse.!!! (exe --| \<^keyword>\)\) >> SOME || Scan.succeed NONE; val export_files = Scan.repeat1 Parse.path_binding -- executable; val _ = Outer_Syntax.command \<^command_keyword>\compile_generated_files\ "compile generated files and export results" (Parse.and_list files_in_theory -- Scan.optional (\<^keyword>\external_files\ |-- Parse.!!! (Parse.and_list1 external_files)) [] -- Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("", Position.none) -- (Parse.where_ |-- Parse.!!! Parse.ML_source) >> (fn ((((args, external), export), export_prefix), source) => Toplevel.keep (fn st => Generated_Files.compile_generated_files_cmd (Toplevel.context_of st) args external export export_prefix source))); in end\ subsection \Embedded ML text\ ML \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\ML_file\ "read and evaluate Isabelle/ML file" (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_debug\ "read and evaluate Isabelle/ML file (with debugger information)" (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_no_debug\ "read and evaluate Isabelle/ML file (no debugger information)" (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file\ "read and evaluate Standard ML file" (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_debug\ "read and evaluate Standard ML file (with debugger information)" (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_no_debug\ "read and evaluate Standard ML file (no debugger information)" (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_export\ "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_export, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.theory (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) end)); val _ = Outer_Syntax.command \<^command_keyword>\SML_import\ "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_import, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> Local_Theory.propagate_ml_env) end)); val _ = Outer_Syntax.command ("ML_export", \<^here>) "ML text within theory or local theory, and export to bootstrap environment" (Parse.ML_source >> (fn source => Toplevel.generic_theory (fn context => context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> Proof.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_val\ "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true); val _ = Outer_Syntax.command \<^command_keyword>\ML_command\ "diagnostic ML text (silent)" (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = Outer_Syntax.command \<^command_keyword>\setup\ "ML setup for global theory" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = Outer_Syntax.local_theory \<^command_keyword>\local_setup\ "ML setup for local theory" (Parse.ML_source >> Isar_Cmd.local_setup); val _ = Outer_Syntax.command \<^command_keyword>\oracle\ "declare oracle" (Parse.range Parse.name -- (\<^keyword>\=\ |-- Parse.ML_source) >> (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); val _ = Outer_Syntax.local_theory \<^command_keyword>\attribute_setup\ "define attribute in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\method_setup\ "define proof method in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\declaration\ "generic ML declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\syntax_declaration\ "generic ML syntax declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" (Parse.name_position -- (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\ --| \<^keyword>\=\) -- Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); in end\ subsection \Theory commands\ subsubsection \Sorts and types\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\default_sort\ "declare default sort for explicit type variables" (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); val _ = Outer_Syntax.local_theory \<^command_keyword>\typedecl\ "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_synonym\ "declare type abbreviation" (Parse.type_args -- Parse.binding -- (\<^keyword>\=\ |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); in end\ subsubsection \Consts\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\judgment\ "declare object-logic judgment" (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\consts\ "declare constants" (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); in end\ subsubsection \Syntax and translations\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\nonterminal\ "declare syntactic type constructors (grammar nonterminal symbols)" (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); val _ = Outer_Syntax.command \<^command_keyword>\syntax\ "add raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\no_syntax\ "delete raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); val trans_pat = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\)\)) "logic" -- Parse.inner_syntax Parse.string; fun trans_arrow toks = ((\<^keyword>\\\ || \<^keyword>\=>\) >> K Syntax.Parse_Rule || (\<^keyword>\\\ || \<^keyword>\<=\) >> K Syntax.Print_Rule || (\<^keyword>\\\ || \<^keyword>\==\) >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) >> (fn (left, (arr, right)) => arr (left, right)); val _ = Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); in end\ subsubsection \Translation functions\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\parse_ast_translation\ "install parse ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); val _ = Outer_Syntax.command \<^command_keyword>\parse_translation\ "install parse translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_translation\ "install print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\typed_print_translation\ "install typed print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_ast_translation\ "install print ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); in end\ subsubsection \Specifications\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\definition\ "constant definition" (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => #2 oo Specification.definition_cmd decl params prems spec)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\abbreviation\ "constant abbreviation" (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); val axiomatization = Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); val _ = Outer_Syntax.command \<^command_keyword>\axiomatization\ "axiomatic constant specification" (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); val _ = Outer_Syntax.local_theory \<^command_keyword>\alias\ "name-space alias for constant" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.alias_cmd); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_alias\ "name-space alias for type constructor" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.type_alias_cmd); in end\ subsubsection \Notation\ ML \ local val _ = 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)); 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)); 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)); 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)); in end\ subsubsection \Theorems\ ML \ local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); fun theorem spec schematic descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl))); val _ = theorem \<^command_keyword>\theorem\ false "theorem"; val _ = theorem \<^command_keyword>\lemma\ false "lemma"; val _ = theorem \<^command_keyword>\corollary\ false "corollary"; val _ = theorem \<^command_keyword>\proposition\ false "proposition"; val _ = theorem \<^command_keyword>\schematic_goal\ true "schematic goal"; in end\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas\ "define theorems" (Parse_Spec.name_facts -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\declare\ "declare theorems" (Parse.and_list1 Parse.thms1 -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes)); val _ = Outer_Syntax.local_theory \<^command_keyword>\named_theorems\ "declare named collection of theorems" (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); in end\ subsubsection \Hide names\ ML \ local fun hide_names command_keyword what hide parse prep = Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) => (Toplevel.theory (fn thy => let val ctxt = Proof_Context.init_global thy in fold (hide fully o prep ctxt) args thy end)))); val _ = hide_names \<^command_keyword>\hide_class\ "classes" Sign.hide_class Parse.class Proof_Context.read_class; val _ = hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_fact\ "facts" Global_Theory.hide_fact Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of); in end\ subsection \Bundled declarations\ ML \ local val _ = Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\bundle\ "define bundle of declarations" ((Parse.binding --| \<^keyword>\=\) -- Parse.thms1 -- Parse.for_fixes >> (uncurry Bundle.bundle_cmd)) (Parse.binding --| Parse.begin >> Bundle.init); val _ = Outer_Syntax.local_theory \<^command_keyword>\unbundle\ "activate declarations from bundle in local theory" (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd); val _ = Outer_Syntax.command \<^command_keyword>\include\ "activate declarations from bundle in proof body" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\including\ "activate declarations from bundle in goal refinement" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\print_bundles\ "print bundles of declarations" (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); in end\ subsection \Local theory specifications\ subsubsection \Specification context\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\context\ "begin local theory context" - ((Parse.name_position >> (Toplevel.begin_main_target true o Named_Target.begin) || + ((Parse.name_position + >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd name)) || Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element - >> (fn (incls, elems) => Toplevel.begin_nested_target (#2 o Bundle.context_cmd incls elems))) + >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems))) --| Parse.begin); val _ = Outer_Syntax.command \<^command_keyword>\end\ "end context" (Scan.succeed (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o Toplevel.end_proof (K Proof.end_notepad))); in end\ subsubsection \Locales and interpretation\ ML \ local val locale_val = Parse_Spec.locale_expression -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || Scan.repeat1 Parse_Spec.context_element >> pair ([], []); val _ = Outer_Syntax.command \<^command_keyword>\locale\ "define named specification context" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin >> (fn ((name, (expr, elems)), begin) => Toplevel.begin_main_target begin (Expression.add_locale_cmd name Binding.empty expr elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\experiment\ "open private specification context" (Scan.repeat Parse_Spec.context_element --| Parse.begin >> (fn elems => Toplevel.begin_main_target true (Experiment.experiment_cmd elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\interpret\ "prove interpretation of locale expression in proof context" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.proof (Interpretation.interpret_cmd expr))); val interpretation_args_with_defs = Parse.!!! Parse_Spec.locale_expression -- (Scan.optional (\<^keyword>\defines\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term))) ([])); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\global_interpretation\ "prove interpretation of locale expression into global theory" (interpretation_args_with_defs >> (fn (expr, defs) => Interpretation.global_interpretation_cmd expr defs)); val _ = Outer_Syntax.command \<^command_keyword>\sublocale\ "prove sublocale relation between a locale and a locale expression" ((Parse.name_position --| (\<^keyword>\\\ || \<^keyword>\<\) -- interpretation_args_with_defs >> (fn (loc, (expr, defs)) => Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs))) || interpretation_args_with_defs >> (fn (expr, defs) => Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs))); val _ = Outer_Syntax.command \<^command_keyword>\interpretation\ "prove interpretation of locale expression in local theory or into global theory" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr))); in end\ subsubsection \Type classes\ ML \ local val class_val = Parse_Spec.class_expression -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || Scan.repeat1 Parse_Spec.context_element >> pair []; val _ = Outer_Syntax.command \<^command_keyword>\class\ "define type class" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- class_val) ([], []) -- Parse.opt_begin >> (fn ((name, (supclasses, elems)), begin) => Toplevel.begin_main_target begin (Class_Declaration.class_cmd name supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\subclass\ "prove a subclass relation" (Parse.class >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command \<^command_keyword>\instantiation\ "instantiate and prove type arity" (Parse.multi_arity --| Parse.begin >> (fn arities => Toplevel.begin_main_target true (Class.instantiation_cmd arities))); val _ = Outer_Syntax.command \<^command_keyword>\instance\ "prove type arity or subclass relation" ((Parse.class -- ((\<^keyword>\\\ || \<^keyword>\<\) |-- Parse.!!! Parse.class) >> Class.classrel_cmd || Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof || Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); in end\ subsubsection \Arbitrary overloading\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\overloading\ "overloaded definitions" (Scan.repeat1 (Parse.name --| (\<^keyword>\==\ || \<^keyword>\\\) -- Parse.term -- Scan.optional (\<^keyword>\(\ |-- (\<^keyword>\unchecked\ >> K false) --| \<^keyword>\)\) true >> Scan.triple1) --| Parse.begin >> (fn operations => Toplevel.begin_main_target true (Overloading.overloading_cmd operations))); in end\ subsection \Proof commands\ ML \ local val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\notepad\ "begin proof context" (Parse.begin >> K Proof.begin_notepad); in end\ subsubsection \Statements\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\have\ "state local goal" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\show\ "state local goal, to refine pending subgoals" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\hence\ "old-style alias of \"then have\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\thus\ "old-style alias of \"then show\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); in end\ subsubsection \Local facts\ ML \ local val facts = Parse.and_list1 Parse.thms1; val _ = Outer_Syntax.command \<^command_keyword>\then\ "forward chaining" (Scan.succeed (Toplevel.proof Proof.chain)); val _ = Outer_Syntax.command \<^command_keyword>\from\ "forward chaining from given facts" (facts >> (Toplevel.proof o Proof.from_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\with\ "forward chaining from given and current facts" (facts >> (Toplevel.proof o Proof.with_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\note\ "define facts" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\supply\ "define facts during goal refinement (unstructured)" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\using\ "augment goal facts" (facts >> (Toplevel.proof o Proof.using_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\unfolding\ "unfold definitions in goal and facts" (facts >> (Toplevel.proof o Proof.unfolding_cmd)); in end\ subsubsection \Proof context\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\fix\ "fix local variables (Skolem constants)" (Parse.vars >> (Toplevel.proof o Proof.fix_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\assume\ "assume propositions" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\presume\ "assume propositions, to be established later" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\define\ "local definition (non-polymorphic)" ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); val _ = Outer_Syntax.command \<^command_keyword>\consider\ "state cases rule" (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\obtain\ "generalized elimination" (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\let\ "bind text variables" (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\=\ |-- Parse.term)) >> (Toplevel.proof o Proof.let_bind_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\write\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); val _ = Outer_Syntax.command \<^command_keyword>\case\ "invoke local context" (Parse_Spec.opt_thm_name ":" -- (\<^keyword>\(\ |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding) --| \<^keyword>\)\) || Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); in end\ subsubsection \Proof structure\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\{\ "begin explicit proof block" (Scan.succeed (Toplevel.proof Proof.begin_block)); val _ = Outer_Syntax.command \<^command_keyword>\}\ "end explicit proof block" (Scan.succeed (Toplevel.proof Proof.end_block)); val _ = Outer_Syntax.command \<^command_keyword>\next\ "enter next proof block" (Scan.succeed (Toplevel.proof Proof.next_block)); in end\ subsubsection \End proof\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\qed\ "conclude proof" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m))); val _ = Outer_Syntax.command \<^command_keyword>\by\ "terminal backward proof" (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2)))); val _ = Outer_Syntax.command \<^command_keyword>\..\ "default proof" (Scan.succeed Isar_Cmd.default_proof); val _ = Outer_Syntax.command \<^command_keyword>\.\ "immediate proof" (Scan.succeed Isar_Cmd.immediate_proof); val _ = Outer_Syntax.command \<^command_keyword>\done\ "done proof" (Scan.succeed Isar_Cmd.done_proof); val _ = Outer_Syntax.command \<^command_keyword>\sorry\ "skip proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\\\ "dummy proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\oops\ "forget proof" (Scan.succeed Toplevel.forget_proof); in end\ subsubsection \Proof steps\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\defer\ "shuffle internal proof state" (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); val _ = Outer_Syntax.command \<^command_keyword>\prefer\ "shuffle internal proof state" (Parse.nat >> (Toplevel.proof o Proof.prefer)); val _ = Outer_Syntax.command \<^command_keyword>\apply\ "initial goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); val _ = Outer_Syntax.command \<^command_keyword>\apply_end\ "terminal goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); val _ = Outer_Syntax.command \<^command_keyword>\proof\ "backward proof step" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Toplevel.proof (fn state => let val state' = state |> Proof.proof m |> Seq.the_result ""; val _ = Output.information (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state')); in state' end)))) in end\ subsubsection \Subgoal focus\ ML \ local val opt_fact_binding = Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) Binding.empty_atts; val for_params = Scan.optional (\<^keyword>\for\ |-- Parse.!!! ((Scan.option Parse.dots >> is_some) -- (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) (false, []); val _ = Outer_Syntax.command \<^command_keyword>\subgoal\ "focus on first subgoal within backward refinement" (opt_fact_binding -- (Scan.option (\<^keyword>\premises\ |-- Parse.!!! opt_fact_binding)) -- for_params >> (fn ((a, b), c) => Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); in end\ subsubsection \Calculation\ ML \ local val calculation_args = Scan.option (\<^keyword>\(\ |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\)\))); val _ = Outer_Syntax.command \<^command_keyword>\also\ "combine calculation and current facts" (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\finally\ "combine calculation and current facts, exhibit result" (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\moreover\ "augment calculation by current facts" (Scan.succeed (Toplevel.proof' Calculation.moreover)); val _ = Outer_Syntax.command \<^command_keyword>\ultimately\ "augment calculation by current facts, exhibit result" (Scan.succeed (Toplevel.proof' Calculation.ultimately)); val _ = Outer_Syntax.command \<^command_keyword>\print_trans_rules\ "print transitivity rules" (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); in end\ subsubsection \Proof navigation\ ML \ local fun report_back () = Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]; val _ = Outer_Syntax.command \<^command_keyword>\back\ "explicit backtracking of proof command" (Scan.succeed (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o Toplevel.skip_proof report_back)); in end\ subsection \Diagnostic commands (for interactive mode only)\ ML \ local val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Outer_Syntax.command \<^command_keyword>\help\ "retrieve outer syntax commands according to name patterns" (Scan.repeat Parse.name >> (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); val _ = Outer_Syntax.command \<^command_keyword>\print_commands\ "print outer syntax commands" (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_options\ "print configuration options" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_context\ "print context of local theory target" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); val _ = Outer_Syntax.command \<^command_keyword>\print_theory\ "print logical theory contents" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_definitions\ "print dependencies of definitional theory content" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_syntax\ "print inner syntax of context" (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_defn_rules\ "print definitional rewrite rules of context" (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_abbrevs\ "print constant abbreviations of context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_theorems\ "print theorems of local theory or proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); val _ = Outer_Syntax.command \<^command_keyword>\print_locales\ "print locales of this theory" (Parse.opt_bang >> (fn verbose => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in Pretty.writeln (Locale.pretty_locales thy verbose) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_classes\ "print classes of this theory" (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_locale\ "print locale of this theory" (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_interps\ "print interpretations of locale for this theory or proof context" (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_attributes\ "print attributes of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_simpset\ "print context of Simplifier" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_rules\ "print intro/elim rules" (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_methods\ "print methods of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_antiquotations\ "print document antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_ML_antiquotations\ "print ML antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" (Scan.succeed (Toplevel.keep (Toplevel.theory_of #> (fn thy => Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |> Graph_Display.display_graph_old)))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ "print term bindings of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_facts\ "print facts of proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_cases\ "print cases of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_statement\ "print theorems as long statements" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts); val _ = Outer_Syntax.command \<^command_keyword>\thm\ "print theorems" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms); val _ = Outer_Syntax.command \<^command_keyword>\prf\ "print proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); val _ = Outer_Syntax.command \<^command_keyword>\full_prf\ "print full proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); val _ = Outer_Syntax.command \<^command_keyword>\prop\ "read and print proposition" (opt_modes -- Parse.term >> Isar_Cmd.print_prop); val _ = Outer_Syntax.command \<^command_keyword>\term\ "read and print term" (opt_modes -- Parse.term >> Isar_Cmd.print_term); val _ = Outer_Syntax.command \<^command_keyword>\typ\ "read and print type" (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\::\ |-- Parse.!!! Parse.sort)) >> Isar_Cmd.print_type); val _ = Outer_Syntax.command \<^command_keyword>\print_codesetup\ "print code generator setup" (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_state\ "print current proof state (if present)" (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); val _ = Outer_Syntax.command \<^command_keyword>\welcome\ "print welcome message" (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); in end\ subsection \Dependencies\ ML \ local val theory_bounds = Parse.theory_name >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\thy_deps\ "visualize theory dependencies" (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); val class_bounds = Parse.sort >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.sort --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\class_deps\ "visualize class dependencies" (Scan.option class_bounds -- Scan.option class_bounds >> (fn args => Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); val _ = Outer_Syntax.command \<^command_keyword>\thm_deps\ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ "print all oracles used in theorems (full graph of transitive dependencies)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val ctxt = Toplevel.context_of st; val thms = Attrib.eval_thms ctxt args; in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end))); val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name); val _ = Outer_Syntax.command \<^command_keyword>\unused_thms\ "find unused theorems" (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); val check = Theory.check {long = false} ctxt; in Thm_Deps.unused_thms_cmd (case opt_range of NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) | SOME (xs, SOME ys) => (map check xs, map check ys)) |> map pretty_thm |> Pretty.writeln_chunks end))); in end\ subsubsection \Find consts and theorems\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\find_consts\ "find constants by name / type patterns" (Find_Consts.query_parser >> (fn spec => Toplevel.keep (fn st => Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); val options = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) (NONE, true); val _ = Outer_Syntax.command \<^command_keyword>\find_theorems\ "find theorems meeting specified criteria" (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => Toplevel.keep (fn st => Pretty.writeln (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); in end\ subsection \Code generation\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\code_datatype\ "define set of code datatype constructors" (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd)); in end\ subsection \Extraction of programs from proofs\ ML \ local val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") []; val _ = Outer_Syntax.command \<^command_keyword>\realizers\ "specify realizers for primitive axioms / theorems, together with correctness proof" (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = Outer_Syntax.command \<^command_keyword>\realizability\ "add equations characterizing realizability" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract_type\ "add equations characterizing type of extracted program" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract\ "extract terms from proofs" (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); in end\ section \Auxiliary lemmas\ subsection \Meta-level connectives in assumptions\ lemma meta_mp: assumes "PROP P \ PROP Q" and "PROP P" shows "PROP Q" by (rule \PROP P \ PROP Q\ [OF \PROP P\]) lemmas meta_impE = meta_mp [elim_format] lemma meta_spec: assumes "\x. PROP P x" shows "PROP P x" by (rule \\x. PROP P x\) lemmas meta_allE = meta_spec [elim_format] lemma swap_params: "(\x y. PROP P x y) \ (\y x. PROP P x y)" .. lemma equal_allI: \(\x. PROP P x) \ (\x. PROP Q x)\ if \\x. PROP P x \ PROP Q x\ by (simp only: that) subsection \Meta-level conjunction\ lemma all_conjunction: "(\x. PROP A x &&& PROP B x) \ ((\x. PROP A x) &&& (\x. PROP B x))" proof assume conj: "\x. PROP A x &&& PROP B x" show "(\x. PROP A x) &&& (\x. PROP B x)" proof - fix x from conj show "PROP A x" by (rule conjunctionD1) from conj show "PROP B x" by (rule conjunctionD2) qed next assume conj: "(\x. PROP A x) &&& (\x. PROP B x)" fix x show "PROP A x &&& PROP B x" proof - show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) qed qed lemma imp_conjunction: "(PROP A \ PROP B &&& PROP C) \ ((PROP A \ PROP B) &&& (PROP A \ PROP C))" proof assume conj: "PROP A \ PROP B &&& PROP C" show "(PROP A \ PROP B) &&& (PROP A \ PROP C)" proof - assume "PROP A" from conj [OF \PROP A\] show "PROP B" by (rule conjunctionD1) from conj [OF \PROP A\] show "PROP C" by (rule conjunctionD2) qed next assume conj: "(PROP A \ PROP B) &&& (PROP A \ PROP C)" assume "PROP A" show "PROP B &&& PROP C" proof - from \PROP A\ show "PROP B" by (rule conj [THEN conjunctionD1]) from \PROP A\ show "PROP C" by (rule conj [THEN conjunctionD2]) qed qed lemma conjunction_imp: "(PROP A &&& PROP B \ PROP C) \ (PROP A \ PROP B \ PROP C)" proof assume r: "PROP A &&& PROP B \ PROP C" assume ab: "PROP A" "PROP B" show "PROP C" proof (rule r) from ab show "PROP A &&& PROP B" . qed next assume r: "PROP A \ PROP B \ PROP C" assume conj: "PROP A &&& PROP B" show "PROP C" proof (rule r) from conj show "PROP A" by (rule conjunctionD1) from conj show "PROP B" by (rule conjunctionD2) qed qed declare [[ML_write_global = false]] end diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,356 +1,357 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "System/distribution.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash_syntax.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; ML_file "ML/ml_pid.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/bundle.ML"; +ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala.ML"; ML_file "System/scala_compiler.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML"