some meagure hints concerning reification
authorhaftmann
Sun Jun 02 09:10:53 2013 +0200 (2013-06-02)
changeset 522877e54c4d964e7
parent 52286 8170e5327c02
child 52288 ca4932dad084
some meagure hints concerning reification
src/Doc/Codegen/Evaluation.thy
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Sun Jun 02 07:46:40 2013 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sun Jun 02 09:10:53 2013 +0200
     1.3 @@ -192,6 +192,56 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Preprocessing HOL terms into evaluable shape *}
     1.8 +
     1.9 +text {*
    1.10 +  When integration decision procedures developed inside HOL into HOL itself,
    1.11 +  it is necessary to somehow get from the Isabelle/ML representation to
    1.12 +  the representation used by the decision procedure itself (``reification'').
    1.13 +  One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}).
    1.14 +  Another option is to use pre-existing infrastructure in HOL:
    1.15 +  @{ML "Reification.conv"} and @{ML "Reification.tac"}
    1.16 +
    1.17 +  An simplistic example:
    1.18 +*}
    1.19 +
    1.20 +datatype %quote form_ord = T | F | Less nat nat
    1.21 +  | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
    1.22 +
    1.23 +primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
    1.24 +where
    1.25 +  "interp T vs \<longleftrightarrow> True"
    1.26 +| "interp F vs \<longleftrightarrow> False"
    1.27 +| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
    1.28 +| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
    1.29 +| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
    1.30 +| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
    1.31 +
    1.32 +text {*
    1.33 +  The datatype @{type form_ord} represents formulae whose semantics is given by
    1.34 +  @{const interp}.  Note that values are represented by variable indices (@{typ nat})
    1.35 +  whose concrete values are given in list @{term vs}.
    1.36 +*}
    1.37 +
    1.38 +ML (*<*) {* *}
    1.39 +schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P"
    1.40 +ML_prf 
    1.41 +(*>*) {* val thm =
    1.42 +  Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"} *} (*<*)
    1.43 +by (tactic {* ALLGOALS (rtac thm) *})
    1.44 +(*>*) 
    1.45 +
    1.46 +text {*
    1.47 +  By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
    1.48 +  which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
    1.49 +  to @{const interp} does not contain any free variables and can this be evaluated
    1.50 +  using evaluation.
    1.51 +
    1.52 +  A less meager example can be found in the AFP, session @{text "Regular-Sets"},
    1.53 +  theory @{text Regexp_Method}.
    1.54 +*}
    1.55 +
    1.56 +
    1.57  subsection {* Intimate connection between logic and system runtime *}
    1.58  
    1.59  text {*
    1.60 @@ -201,7 +251,7 @@
    1.61  *}
    1.62  
    1.63  
    1.64 -subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation *}
    1.65 +subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq} *}
    1.66  
    1.67  text {*
    1.68    The @{text code} antiquotation allows to include constants from