nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

stiluebungen am PML

This commit is contained in:
Burkhart Wolff 2020-09-21 21:24:08 +02:00
parent 6f36efae7f
commit ad6ba9e302
1 changed files with 58 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -780,9 +780,9 @@ figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
text\<open>Note that the transfer rule: text\<open>Note that the transfer rule:
\[ \[
\begin{prooftree} \begin{prooftree}
\Gamma \vdash_\theta \phi \qquad \qquad \theta \sqsubseteq \theta' \<open>\<Gamma> \<turnstile>\<^sub>\<theta> \<phi>\<close> \qquad \qquad \<open>\<theta> \<sqsubseteq> \<theta>'\<close>
\justifies \justifies
\Gamma \vdash_{\theta'} \phi \qquad \qquad \<open>\<Gamma> \<turnstile>\<^sub>\<theta>\<^sub>' \<phi>\<close> \qquad \qquad
\end{prooftree} \end{prooftree}
\] \]
which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design
@ -822,11 +822,15 @@ subsection*[t235::technical]\<open> \<^ML_structure>\<open>Theory\<close>'s \<cl
text \<open> This structure yields the abstract datatype \<^ML_structure>\<open>Theory\<close> which becomes the content of text \<open> This structure yields the abstract datatype \<^ML_structure>\<open>Theory\<close> which becomes the content of
\<^ML_type>\<open>Context.theory\<close>. In a way, the LCF-Kernel registers itself into the Nano-Kernel, \<^ML_type>\<open>Context.theory\<close>. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
which inspired me (bu) to this naming. \<close> which inspired me (bu) to this naming. However, not that this is a mental model: the Nano-Kernel
offers ab initio many operations directly linked to its main purpose: incommodating the
micro-kernel and its management of local and global contexts.
\<close>
ML\<open> text\<open>
@{theory_text [display]
(* intern Theory.Thy; \<open>
intern Theory.Thy;
datatype thy = Thy of datatype thy = Thy of
{pos: Position.T, {pos: Position.T,
@ -834,75 +838,73 @@ datatype thy = Thy of
axioms: term Name_Space.table, axioms: term Name_Space.table,
defs: Defs.T, defs: Defs.T,
wrappers: wrapper list * wrapper list}; wrappers: wrapper list * wrapper list};
\<close>}
*) \<^item> \<^ML>\<open>Theory.check: {long: bool} -> Proof.context -> string * Position.T -> theory\<close>
\<^item> \<^ML>\<open>Theory.local_setup: (Proof.context -> Proof.context) -> unit\<close>
Theory.check: {long: bool} -> Proof.context -> string * Position.T -> theory; \<^item> \<^ML>\<open>Theory.setup: (theory -> theory) -> unit\<close> (* The thing to extend the table of "command"s with parser - callbacks. *)
\<^item> \<^ML>\<open>Theory.get_markup: theory -> Markup.T\<close>
Theory.local_setup: (Proof.context -> Proof.context) -> unit; \<^item> \<^ML>\<open>Theory.axiom_table: theory -> term Name_Space.table\<close>
Theory.setup: (theory -> theory) -> unit; (* The thing to extend the table of "command"s with parser - callbacks. *) \<^item> \<^ML>\<open>Theory.axiom_space: theory -> Name_Space.T\<close>
Theory.get_markup: theory -> Markup.T; \<^item> \<^ML>\<open>Theory.all_axioms_of: theory -> (string * term) list\<close>
Theory.axiom_table: theory -> term Name_Space.table; \<^item> \<^ML>\<open>Theory.defs_of: theory -> Defs.T\<close>
Theory.axiom_space: theory -> Name_Space.T; \<^item> \<^ML>\<open>Theory.join_theory: theory list -> theory\<close>
Theory.all_axioms_of: theory -> (string * term) list; \<^item> \<^ML>\<open>Theory.at_begin: (theory -> theory option) -> theory -> theory\<close>
Theory.defs_of: theory -> Defs.T; \<^item> \<^ML>\<open>Theory.at_end: (theory -> theory option) -> theory -> theory\<close>
Theory.join_theory: theory list -> theory; \<^item> \<^ML>\<open>Theory.begin_theory: string * Position.T -> theory list -> theory\<close>
Theory.at_begin: (theory -> theory option) -> theory -> theory; \<^item> \<^ML>\<open>Theory.end_theory: theory -> theory\<close>
Theory.at_end: (theory -> theory option) -> theory -> theory; \<close>
Theory.begin_theory: string * Position.T -> theory list -> theory;
Theory.end_theory: theory -> theory;\<close>
section*[t26::technical]\<open>Advanced Specification Constructs\<close> section*[t26::technical]\<open>Advanced Specification Constructs\<close>
text\<open>Isabelle is built around the idea that system components were built on top text\<open>Isabelle is built around the idea that system components were built on top
of the kernel in order to give the user high-level specification constructs of the kernel in order to give the user high-level specification constructs
--- rather than inside as in the Coq kernel that foresees, for example, data-types --- rather than inside as in the Coq kernel that foresees, for example, data-types
and primitive recursors already in the basic $\lambda$-term language. and primitive recursors already in the basic \<open>\<lambda>\<close>-term language.
Therefore, records, definitions, type-definitions, recursive function definitions Therefore, records, definitions, type-definitions, recursive function definitions
are supported by packages that belong to the \<^emph>\<open>components\<close> strata. are supported by packages that belong to the \<^emph>\<open>components\<close> strata.
With the exception of the @{ML "Specification.axiomatization"} construct, they With the exception of the \<^ML>\<open>Specification.axiomatization\<close> construct, they
are all-together built as composition of conservative extensions. are all-together built as composition of conservative extensions.
The components are a bit scattered in the architecture. A relatively recent and The components are a bit scattered in the architecture. A relatively recent and
high-level component (more low-level components such as @{ML "Global_Theory.add_defs"} high-level component (more low-level components such as \<^ML>\<open>Global_Theory.add_defs\<close>
exist) for definitions and axiomatizations is here: exist) for definitions and axiomatizations is here:
\<close> \<close>
ML\<open> text\<open>
local open Specification \<^item> \<^ML>\<open>Specification.definition: (binding * typ option * mixfix) option ->
val _= definition: (binding * typ option * mixfix) option ->
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term -> (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
local_theory -> (term * (string * thm)) * local_theory local_theory -> (term * (string * thm)) * local_theory\<close>
val _= definition': (binding * typ option * mixfix) option -> \<^item> \<^ML>\<open>Specification.definition': (binding * typ option * mixfix) option ->
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term -> (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
bool -> local_theory -> (term * (string * thm)) * local_theory bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
val _= definition_cmd: (binding * string option * mixfix) option -> \<^item> \<^ML>\<open>Specification.definition_cmd: (binding * string option * mixfix) option ->
(binding * string option * mixfix) list -> string list -> Attrib.binding * string -> (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
bool -> local_theory -> (term * (string * thm)) * local_theory bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
val _= axiomatization: (binding * typ option * mixfix) list -> \<^item> \<^ML>\<open>Specification.axiomatization: (binding * typ option * mixfix) list ->
(binding * typ option * mixfix) list -> term list -> (binding * typ option * mixfix) list -> term list ->
(Attrib.binding * term) list -> theory -> (term list * thm list) * theory (Attrib.binding * term) list -> theory -> (term list * thm list) * theory\<close>
val _= axiomatization_cmd: (binding * string option * mixfix) list -> \<^item> \<^ML>\<open>Specification.axiomatization_cmd: (binding * string option * mixfix) list ->
(binding * string option * mixfix) list -> string list -> (binding * string option * mixfix) list -> string list ->
(Attrib.binding * string) list -> theory -> (term list * thm list) * theory (Attrib.binding * string) list -> theory -> (term list * thm list) * theory\<close>
val _= axiom: Attrib.binding * term -> theory -> thm * theory \<^item> \<^ML>\<open>Specification.axiom: Attrib.binding * term -> theory -> thm * theory\<close>
val _= abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> \<^item> \<^ML>\<open>Specification.abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
(binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory\<close>
val _= abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> \<^item> \<^ML>\<open>Specification.abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
(binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory\<close>
in val _ = () end
\<close> \<close>
text\<open>Note that the interface is mostly based on @{ML_type "local_theory"}, which is a synonym to text\<open>
@{ML_type "Proof.context"}. Need to lift this to a global system transition ? Note that the interface is mostly based on \<^ML_type>\<open>local_theory\<close>, which is a synonym to
Don't worry, @{ML "Named_Target.theory_map: (local_theory -> local_theory) -> theory -> theory"} \<^ML_type>\<open>Proof.context\<close>. Need to lift this to a global system transition ?
Don't worry, \<^ML>\<open>Named_Target.theory_map: (local_theory -> local_theory) -> theory -> theory\<close>
does the trick. does the trick.
\<close> \<close>
subsection*[t261::example]\<open>Example\<close> subsection*[t261::example]\<open>Example\<close>
text\<open>Suppose that we want do \<open>definition I :: "'a \<Rightarrow> 'a" where "I x = x"\<close> at the ML-level. text\<open>Suppose that we want do \<^theory_text>\<open>definition I :: "'a \<Rightarrow> 'a" where "I x = x"\<close> at the ML-level.
We construct our defining equation and embed it as a @{typ "prop"} into Pure. We construct our defining equation and embed it as a \<^typ>\<open>prop\<close> into Pure.
\<close> \<close>
ML\<open> val ty = @{typ "'a"} ML\<open> val ty = @{typ "'a"}
val term = HOLogic.mk_eq (Free("I",ty -->ty) $ Free("x", ty), Free("x", ty)); val term = HOLogic.mk_eq (Free("I",ty -->ty) $ Free("x", ty), Free("x", ty));
@ -931,18 +933,18 @@ section*[t24::technical]\<open>Backward Proofs: Tactics, Tacticals and Goal-Stat
text\<open>At this point, we leave the Pure-Kernel and start to describe the first layer on top text\<open>At this point, we leave the Pure-Kernel and start to describe the first layer on top
of it, involving support for specific styles of reasoning and automation of reasoning.\<close> of it, involving support for specific styles of reasoning and automation of reasoning.\<close>
text\<open> \<^verbatim>\<open>tactic\<close>'s are in principle \<^emph>\<open>relations\<close> on theorems @{ML_type "thm"}; this gives a natural way text\<open> \<^ML_type>\<open>tactic\<close>'s are in principle \<^emph>\<open>relations\<close> on theorems \<^ML_type>\<open>thm\<close>; this gives a
to represent the fact that HO-Unification (and therefore the mechanism of rule-instantiation) natural way to represent the fact that HO-Unification (and therefore the mechanism of rule-instan-
are non-deterministic in principle. Heuristics may choose particular preferences between tiation) are non-deterministic in principle. Heuristics may choose particular preferences between
the theorems in the range of this relation, but the Isabelle Design accepts this fundamental the theorems in the range of this relation, but the Isabelle Design accepts this fundamental
fact reflected at this point in the prover architecture. fact reflected at this point in the prover architecture.
This potentially infinite relation is implemented by a function of theorems to lazy lists This potentially infinite relation is implemented by a function of theorems to lazy lists
over theorems, which gives both sufficient structure for heuristic over theorems, which gives both sufficient structure for heuristic
considerations as well as a nice algebra, called \<^verbatim>\<open>TACTICAL\<close>'s, providing a bottom element considerations as well as a nice algebra, called \<^ML_structure>\<open>Tactical\<close>'s, providing a bottom element
@{ML "no_tac"} (the function that always fails), the top-element @{ML "all_tac"} \<^ML>\<open>no_tac\<close> (the function that always fails), the top-element \<^ML>\<open>all_tac\<close>
(the function that never fails), sequential composition @{ML "op THEN"}, (serialized) (the function that never fails), sequential composition \<^ML>\<open>op THEN\<close>, (serialized)
non-deterministic composition @{ML "op ORELSE"}, conditionals, repetitions over lists, etc. non-deterministic composition \<^ML>\<open>op ORELSE\<close>, conditionals, repetitions over lists, etc.
The following is an excerpt of @{file "~~/src/Pure/tactical.ML"}:\<close> The following is an excerpt of \<^file>\<open>~~/src/Pure/tactical.ML\<close>:\<close>
ML\<open> ML\<open>
signature TACTICAL = signature TACTICAL =