Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Port to Isabelle 2020 (tested with Isabelle 2020 RC4).

This commit is contained in:
Achim D. Brucker 2020-04-08 13:12:17 +01:00
parent 6ec427e716
commit 0c41ee46bb
12 changed files with 94 additions and 67 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -14,7 +14,6 @@
(*<*)
theory TR_MyCommentedIsabelle
imports "Isabelle_DOF.technical_report"
(*imports "../../../ontologies/technical_report"*)
begin
@ -784,9 +783,9 @@ Theory.setup: (theory -> theory) -> unit; (* The thing to extend the table of "
Theory.get_markup: theory -> Markup.T;
Theory.axiom_table: theory -> term Name_Space.table;
Theory.axiom_space: theory -> Name_Space.T;
Theory.axioms_of: theory -> (string * term) list;
Theory.all_axioms_of: theory -> (string * term) list;
Theory.defs_of: theory -> Defs.T;
Theory.join_theory: theory list -> theory;
Theory.at_begin: (theory -> theory option) -> theory -> theory;
Theory.at_end: (theory -> theory option) -> theory -> theory;
Theory.begin_theory: string * Position.T -> theory list -> theory;
@ -1016,7 +1015,7 @@ fun derive_thm name term lthy =
[] (* local assumption context *)
(term) (* parsed goal *)
(fn _ => simp_tac lthy 1) (* proof tactic *)
|> Thm.close_derivation (* some cleanups *);
|> Thm.close_derivation \<^here> (* some cleanups *);
val thm111_intern = derive_thm "thm111" tt @{context} (* just for fun at the ML level *)
@ -1035,7 +1034,7 @@ text\<open>Converting a local theory transformation into a global one:\<close>
setup\<open>SimpleSampleProof.prove_n_store\<close>
text\<open>... and there it is in the global (Isar) context:\<close>
thm thm111
thm "thm111"
@ -2038,7 +2037,7 @@ text\<open>The heart of the LaTeX generator is to be found in the structure @{ML
\<close>
ML\<open>
local
local
open Latex

2
src/DOF/Assert.thy
View File

@ -48,7 +48,7 @@ fun assert_cmd some_name modes raw_t ctxt (* state*) =
val ty' = Term.type_of t';
val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Variable.auto_fixes t' ctxt;
val ctxt' = Proof_Context.augment t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();

17
src/ROOT
View File

@ -2,15 +2,32 @@ session "Isabelle_DOF" = "Functional-Automata" +
options [document = pdf, document_output = "output"]
sessions
"Regular-Sets"
directories
"DOF"
"ontologies"
"ontologies/CENELEC_50128"
"ontologies/Conceptual"
"ontologies/math_exam"
"ontologies/math_paper"
"ontologies/scholarly_paper"
"ontologies/small_math"
"ontologies/technical_report"
theories
"DOF/Isa_DOF"
"ontologies/ontologies"
(*
session "Isabelle_DOF-tests" = "Isabelle_DOF" +
options [document = false]
directories
tests
theories
"tests/AssnsLemmaThmEtc"
"tests/Concept_ExampleInvariant"
"tests/Concept_Example"
"tests/InnerSyntaxAntiquotations"
"tests/Attributes"
*)

1
src/ROOTS Normal file
View File

@ -0,0 +1 @@
tests

54
src/patches/thy_output.orig19.ML → src/patches/thy_output.Isabelle2020.ML
View File

@ -175,30 +175,30 @@ end;
(* presentation tokens *)
datatype token =
Ignore_Token
| Basic_Token of Token.T
| Markup_Token of string * Input.source
| Markup_Env_Token of string * Input.source
| Raw_Token of Input.source;
Ignore
| Token of Token.T
| Heading of string * Input.source
| Body of string * Input.source
| Raw of Input.source;
fun basic_token pred (Basic_Token tok) = pred tok
| basic_token _ _ = false;
fun token_with pred (Token tok) = pred tok
| token_with _ _ = false;
val white_token = basic_token Document_Source.is_white;
val white_comment_token = basic_token Document_Source.is_white_comment;
val blank_token = basic_token Token.is_blank;
val newline_token = basic_token Token.is_newline;
val white_token = token_with Document_Source.is_white;
val white_comment_token = token_with Document_Source.is_white_comment;
val blank_token = token_with Token.is_blank;
val newline_token = token_with Token.is_newline;
fun present_token ctxt tok =
(case tok of
Ignore_Token => []
| Basic_Token tok => output_token ctxt tok
| Markup_Token (cmd, source) =>
Ignore => []
| Token tok => output_token ctxt tok
| Heading (cmd, source) =>
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
(output_document ctxt {markdown = false} source)
| Markup_Env_Token (cmd, source) =>
| Body (cmd, source) =>
[Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
| Raw_Token source =>
| Raw source =>
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
@ -367,7 +367,7 @@ fun present_thy options thy (segments: segment list) =
(* tokens *)
val ignored = Scan.state --| ignore
>> (fn d => (NONE, (Ignore_Token, ("", d))));
>> (fn d => (NONE, (Ignore, ("", d))));
fun markup pred mk flag = Scan.peek (fn d =>
Document_Source.improper |--
@ -384,29 +384,29 @@ fun present_thy options thy (segments: segment list) =
Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
Scan.one Token.is_command --| Document_Source.annotation
>> (fn (cmd_mod, cmd) =>
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @
[(SOME (Token.content_of cmd, Token.pos_of cmd),
(Basic_Token cmd, (markup_false, d)))]));
(Token cmd, (markup_false, d)))]));
val cmt = Scan.peek (fn d =>
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d)))));
val tokens =
(ignored ||
markup Keyword.is_document_heading Markup_Token markup_true ||
markup Keyword.is_document_body Markup_Env_Token markup_true ||
markup Keyword.is_document_raw (Raw_Token o #2) "") >> single ||
markup Keyword.is_document_heading Heading markup_true ||
markup Keyword.is_document_body Body markup_true ||
markup Keyword.is_document_raw (Raw o #2) "") >> single ||
command ||
(cmt || other) >> single;
(* spans *)
val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false;
val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof;
val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false;
val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof;
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
@ -466,7 +466,7 @@ end;
(* pretty printing *)
fun pretty_term ctxt t =
Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
Syntax.pretty_term (Proof_Context.augment t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;

56
src/patches/thy_output.ML
View File

@ -2,6 +2,8 @@
Author: Makarius
Theory document output.
This is a modified/patched version that supports Isabelle/DOF.
*)
signature THY_OUTPUT =
@ -176,32 +178,32 @@ end;
(* presentation tokens *)
datatype token =
Ignore_Token
| Basic_Token of Token.T
| Markup_Token of string * string * Input.source
| Markup_Env_Token of string * string * Input.source
| Raw_Token of Input.source;
Ignore
| Token of Token.T
| Heading of string * string * Input.source
| Body of string * string * Input.source
| Raw of Input.source;
fun basic_token pred (Basic_Token tok) = pred tok
| basic_token _ _ = false;
fun token_with pred (Token tok) = pred tok
| token_with _ _ = false;
val white_token = basic_token Document_Source.is_white;
val white_comment_token = basic_token Document_Source.is_white_comment;
val blank_token = basic_token Token.is_blank;
val newline_token = basic_token Token.is_newline;
val white_token = token_with Document_Source.is_white;
val white_comment_token = token_with Document_Source.is_white_comment;
val blank_token = token_with Token.is_blank;
val newline_token = token_with Token.is_newline;
fun present_token ctxt tok =
(case tok of
Ignore_Token => []
| Basic_Token tok => output_token ctxt tok
| Markup_Token (cmd, meta_args, source) =>
Ignore => []
| Token tok => output_token ctxt tok
| Heading (cmd, meta_args, source) =>
Latex.enclose_body ("%\n\\isamarkup" ^ cmd (* ^ meta_args *) ^ "{") "%\n}\n"
(output_document ctxt {markdown = false} source)
| Markup_Env_Token (cmd, meta_args, source) =>
| Body (cmd, meta_args, source) =>
[Latex.environment_block
("isamarkup" ^ cmd (* ^ meta_args*))
(Latex.string meta_args :: output_document ctxt {markdown = true} source)]
| Raw_Token source =>
| Raw source =>
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
@ -376,7 +378,7 @@ fun present_thy options thy (segments: segment list) =
(* tokens *)
val ignored = Scan.state --| ignore
>> (fn d => (NONE, (Ignore_Token, ("", d))));
>> (fn d => (NONE, (Ignore, ("", d))));
fun markup pred mk flag = Scan.peek (fn d =>
Document_Source.improper
@ -399,29 +401,29 @@ fun present_thy options thy (segments: segment list) =
Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
Scan.one Token.is_command --| Document_Source.annotation
>> (fn (cmd_mod, cmd) =>
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @
[(SOME (Token.content_of cmd, Token.pos_of cmd),
(Basic_Token cmd, (markup_false, d)))]));
(Token cmd, (markup_false, d)))]));
val cmt = Scan.peek (fn d =>
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d)))));
val tokens =
(ignored ||
markup Keyword.is_document_heading Markup_Token markup_true ||
markup Keyword.is_document_body Markup_Env_Token markup_true ||
markup Keyword.is_document_raw (Raw_Token o #3) "") >> single ||
markup Keyword.is_document_heading Heading markup_true ||
markup Keyword.is_document_body Body markup_true ||
markup Keyword.is_document_raw (Raw o #3) "") >> single ||
command ||
(cmt || other) >> single;
(* spans *)
val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false;
val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof;
val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false;
val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof;
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
@ -488,7 +490,7 @@ end;
(* pretty printing *)
fun pretty_term ctxt t =
Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
Syntax.pretty_term (Proof_Context.augment t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;

4
src/tests/AssnsLemmaThmEtc.thy
View File

@ -14,8 +14,8 @@
theory
AssnsLemmaThmEtc
imports
"../ontologies/Conceptual/Conceptual"
"../ontologies/math_paper/math_paper"
"Isabelle_DOF.Conceptual"
"Isabelle_DOF.math_paper"
begin
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>

2
src/tests/Attributes.thy
View File

@ -14,7 +14,7 @@
theory
Attributes
imports
"../ontologies/Conceptual/Conceptual"
"Isabelle_DOF.Conceptual"
begin
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>

4
src/tests/Concept_Example.thy
View File

@ -16,10 +16,10 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
theory
Concept_Example
imports
"../ontologies/Conceptual/Conceptual" (* we use the generic "Conceptual" ontology *)
"Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
begin
text\<open>@{theory "Isabelle_DOF-tests.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure.
text\<open>@{theory "Isabelle_DOF.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure.
Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is
enabled for.\<close>
open_monitor*[struct::M]

2
src/tests/Concept_ExampleInvariant.thy
View File

@ -16,7 +16,7 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
theory
Concept_ExampleInvariant
imports
"../ontologies/Conceptual/Conceptual" (* we use the generic "Conceptual" ontology *)
"Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
begin
section\<open>Example: Standard Class Invariant\<close>

2
src/tests/InnerSyntaxAntiquotations.thy
View File

@ -16,7 +16,7 @@ chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
theory
InnerSyntaxAntiquotations
imports
"../ontologies/Conceptual/Conceptual"
"Isabelle_DOF.Conceptual"
begin
text\<open>Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring

8
src/tests/ROOT Normal file
View File

@ -0,0 +1,8 @@
session "Isabelle_DOF-tests" = "Isabelle_DOF" +
options [document = false]
theories
"AssnsLemmaThmEtc"
"Concept_ExampleInvariant"
"Concept_Example"
"InnerSyntaxAntiquotations"
"Attributes"