<commit_before>(*  Title:      Pure/Isar/isar_thy.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>

Derived theory operations.

TODO:
  - pure_thy.ML: add_constdefs (atomic!);
  - 'methods' section (proof macros, ML method defs) (!?);
  - next_block: ProofHistory open / close (!?);
*)

signature ISAR_THY =
sig
  val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
  val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
  val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
    -> theory -> theory
  val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list
    -> theory -> theory
  val have_facts: (string * Args.src list) * (string * Args.src list) list
    -> ProofHistory.T -> ProofHistory.T
  val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
  val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
  val theorem: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
  val lemma: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
  val assume: string -> Args.src list -> (string * string list) list
    -> ProofHistory.T -> ProofHistory.T
  val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
  val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
  val chain: ProofHistory.T -> ProofHistory.T
  val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
  val begin_block: ProofHistory.T -> ProofHistory.T
  val next_block: ProofHistory.T -> ProofHistory.T
  val end_block: ProofHistory.T -> ProofHistory.T
  val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
  val qed: ProofHistory.T -> theory
  val kill_proof: ProofHistory.T -> theory
  val tac: Method.text -> ProofHistory.T -> ProofHistory.T
  val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
  val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
  val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
  val trivial_proof: ProofHistory.T -> ProofHistory.T
  val default_proof: ProofHistory.T -> ProofHistory.T
  val use_mltext: string -> theory option -> theory option
  val use_mltext_theory: string -> theory -> theory
  val use_setup: string -> theory -> theory
  val parse_ast_translation: string -> theory -> theory
  val parse_translation: string -> theory -> theory
  val print_translation: string -> theory -> theory
  val typed_print_translation: string -> theory -> theory
  val print_ast_translation: string -> theory -> theory
  val token_translation: string -> theory -> theory
  val add_oracle: bstring * string -> theory -> theory
  val the_theory: string -> unit -> theory
  val begin_theory: string * string list -> unit -> theory
  val end_theory: theory -> unit
end;

structure IsarThy: ISAR_THY =
struct


(** derived theory and proof operations **)

(* axioms and defs *)

fun add_axms f args thy =
  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;

val add_axioms = add_axms PureThy.add_axioms;
val add_defs = add_axms PureThy.add_defs;

<commit_msg>add_text, add_chapter etc.: dummy;<commit_after>(*  Title:      Pure/Isar/isar_thy.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>

Derived theory operations.

TODO:
  - pure_thy.ML: add_constdefs (atomic!);
  - 'methods' section (proof macros, ML method defs) (!?);
  - next_block: ProofHistory open / close (!?);
*)

signature ISAR_THY =
sig
  val add_text: string -> theory -> theory
  val add_chapter: string -> theory -> theory
  val add_section: string -> theory -> theory
  val add_subsection: string -> theory -> theory
  val add_subsubsection: string -> theory -> theory
  val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
  val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
  val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
    -> theory -> theory
  val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list
    -> theory -> theory
  val have_facts: (string * Args.src list) * (string * Args.src list) list
    -> ProofHistory.T -> ProofHistory.T
  val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
  val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
  val theorem: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
  val lemma: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
  val assume: string -> Args.src list -> (string * string list) list
    -> ProofHistory.T -> ProofHistory.T
  val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
  val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
  val chain: ProofHistory.T -> ProofHistory.T
  val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
  val begin_block: ProofHistory.T -> ProofHistory.T
  val next_block: ProofHistory.T -> ProofHistory.T
  val end_block: ProofHistory.T -> ProofHistory.T
  val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
  val qed: ProofHistory.T -> theory
  val kill_proof: ProofHistory.T -> theory
  val tac: Method.text -> ProofHistory.T -> ProofHistory.T
  val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
  val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
  val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
  val trivial_proof: ProofHistory.T -> ProofHistory.T
  val default_proof: ProofHistory.T -> ProofHistory.T
  val use_mltext: string -> theory option -> theory option
  val use_mltext_theory: string -> theory -> theory
  val use_setup: string -> theory -> theory
  val parse_ast_translation: string -> theory -> theory
  val parse_translation: string -> theory -> theory
  val print_translation: string -> theory -> theory
  val typed_print_translation: string -> theory -> theory
  val print_ast_translation: string -> theory -> theory
  val token_translation: string -> theory -> theory
  val add_oracle: bstring * string -> theory -> theory
  val the_theory: string -> unit -> theory
  val begin_theory: string * string list -> unit -> theory
  val end_theory: theory -> unit
end;

structure IsarThy: ISAR_THY =
struct


(** derived theory and proof operations **)

(* formal comments *)	(* FIXME dummy *)

fun add_text (txt:string) (thy:theory) = thy;
val add_chapter = add_text;
val add_section = add_text;
val add_subsection = add_text;
val add_subsubsection = add_text;


(* axioms and defs *)

fun add_axms f args thy =
  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;

val add_axioms = add_axms PureThy.add_axioms;
val add_defs = add_axms PureThy.add_defs;


{'fraction_non_alphanumeric': 0.1203450754852624, 'fraction_numerical': 0.0, 'mean_word_length': 3.473311897106109, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 177, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1972444', 'n_tokens_mistral': 2254, 'n_tokens_neox': 2171, 'n_words': 697}