diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 97df321..b4d9720 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -45,7 +45,7 @@ text\ While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation. This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated - "The Isabelle Cookbook" in \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader + "The Isabelle Cookbook" in \<^url>\https://nms.kcl.ac.uk/christian.urban/Cookbook/\. The reader is encouraged not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jedit in order to make experiments on the running code. This text is written itself in Isabelle/Isar using a specific document ontology for technical reports. It is @@ -554,7 +554,41 @@ text\ Type inference eliminates also joker-types such as @{ML dummyT} and it produces a certifiable term. \ ML\ Type_Infer_Context.infer_types: Proof.context -> term list -> term list \ - +subsection*[t237::technical]\Constructing Terms without Type-Inference\ +text\Using @{ML "Type_Infer_Context.infer_types"} is not quite unproblematic: since the type +inference can construct types for largely underspecified terms, it may happen that under +some circumstances, tactics and proof-attempts fail since just some internal term representation +was too general. A more defensive strategy is already sketched --- but neither explicitely +mentioned nor worked out in the interface in @{ML_structure HOLogic}. The idea is to have +advanced term constructors that construct the right term from the leaves, which were by convention +fully type-annotated (so: this does not work for terms with dangling @(ML Bound)'s). + +Operations like @{ML "HOLogic.mk_prod"} or @{ML "HOLogic.mk_fst"} or @{ML "HOLogic.mk_eq"} do +exactly this by using an internal pure bottom-up type-inference @{ML "fastype_of"}. +The following routines are written in the same style complement the existing API +@{ML_structure HOLogic}. +\ + +ML\ +fun mk_None ty = let val none = \<^const_name>\Option.option.None\ + val none_ty = ty --> Type(\<^type_name>\option\,[ty]) + in Const(none, none_ty) + end; +fun mk_Some t = let val some = \<^const_name>\Option.option.Some\ + val ty = fastype_of t + val some_ty = ty --> Type(\<^type_name>\option\,[ty]) + in Const(some, some_ty) $ t + end; + +fun mk_undefined (@{typ "unit"}) = Const (\<^const_name>\Product_Type.Unity\, \<^typ>\unit\) + |mk_undefined t = Const (\<^const_name>\HOL.undefined\, t) + +fun meta_eq_const T = Const (\<^const_name>\Pure.eq\, T --> T --> propT); + +fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u; + +\ + subsection*[t233::technical]\ Theories and the Signature API\ ML\ Sign.tsig_of : theory -> Type.tsig; @@ -713,6 +747,79 @@ Theory.at_end: (theory -> theory option) -> theory -> theory; Theory.begin_theory: string * Position.T -> theory list -> theory; Theory.end_theory: theory -> theory;\ +section*[t26::technical]\Advanced Specification Constructs\ +text\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 +--- rather than inside as in the Coq kernel that foresees, for example, data-types +and primitive recursors already in the basic $\lambda$-term language. +Therefore, records, definitions, type-definitions, recursive function definitions +are supported by packages that belong to the \<^emph>\components\ strata. +With the exception of the @{ML "Specification.axiomatization"} construct, they +are all-together built as composition of conservative extensions. + +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"} +exist) for definitions and axiomatizations is here: +\ + + +ML\ +local open Specification + val _= definition: (binding * typ option * mixfix) option -> + (binding * typ option * mixfix) list -> term list -> Attrib.binding * term -> + local_theory -> (term * (string * thm)) * local_theory + val _= definition': (binding * typ option * mixfix) option -> + (binding * typ option * mixfix) list -> term list -> Attrib.binding * term -> + bool -> local_theory -> (term * (string * thm)) * local_theory + val _= definition_cmd: (binding * string option * mixfix) option -> + (binding * string option * mixfix) list -> string list -> Attrib.binding * string -> + bool -> local_theory -> (term * (string * thm)) * local_theory + val _= axiomatization: (binding * typ option * mixfix) list -> + (binding * typ option * mixfix) list -> term list -> + (Attrib.binding * term) list -> theory -> (term list * thm list) * theory + val _= axiomatization_cmd: (binding * string option * mixfix) list -> + (binding * string option * mixfix) list -> string list -> + (Attrib.binding * string) list -> theory -> (term list * thm list) * theory + val _= axiom: Attrib.binding * term -> theory -> thm * theory + val _= abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> + (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory + val _= abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> + (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory +in val _ = () end +\ + +text\Note that the interface is mostly based on @{ML_type "local_theory"}, which is a synonym to +@{ML_type "Proof.context"}. Need to lift this to a global system transition ? +Don't worry, @{ML "Named_Target.theory_map: (local_theory -> local_theory) -> theory -> theory"} +does the trick. +\ + +subsection*[t261::example]\Example\ + +text\Suppose that we want do \definition I :: "'a \ 'a" where "I x = x"\ at the ML-level. +We construct our defining equation and embed it as a @{typ "prop"} into Pure. +\ +ML\ val ty = @{typ "'a"} + val term = HOLogic.mk_eq (Free("I",ty -->ty) $ Free("x", ty), Free("x", ty)); + val term_prop = HOLogic.mk_Trueprop term\ +text\Recall the notes on defensive term construction wrt. typing in @{docitem "t237"}. +Then the trick is done by:\ + +setup\ +let +fun mk_def name p = + let val nameb = Binding.make(name,p) + val ty_global = ty -->ty + val args = (((SOME(nameb,SOME ty_global,NoSyn),(Binding.empty_atts,term_prop)),[]),[]) + val cmd = (fn (((decl, spec), prems), params) => + #2 oo Specification.definition' decl params prems spec) + in cmd args true + end; +in Named_Target.theory_map (mk_def "I" @{here} ) +end\ + +thm I_def +text\Voilà.\ section*[t24::technical]\Backward Proofs: Tactics, Tacticals and Goal-States\