diff --git a/src/HOL/SMT_Examples/SMT_Word_Examples.thy b/src/HOL/SMT_Examples/SMT_Word_Examples.thy --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy @@ -1,69 +1,69 @@ (* Title: HOL/SMT_Examples/SMT_Word_Examples.thy Author: Sascha Boehme, TU Muenchen *) section \Word examples for for SMT binding\ theory SMT_Word_Examples -imports "HOL-Word.Word" "HOL-Word.Traditional_Syntax" +imports "HOL-Word.Word" begin declare [[smt_oracle = true]] declare [[z3_extensions = true]] declare [[smt_certificates = "SMT_Word_Examples.certs"]] declare [[smt_read_only_certificates = true]] text \ Currently, there is no proof reconstruction for words. All lemmas are proved using the oracle mechanism. \ section \Bitvector numbers\ lemma "(27 :: 4 word) = -5" by smt lemma "(27 :: 4 word) = 11" by smt lemma "23 < (27::8 word)" by smt lemma "27 + 11 = (6::5 word)" by smt lemma "7 * 3 = (21::8 word)" by smt lemma "11 - 27 = (-16::8 word)" by smt lemma "- (- 11) = (11::5 word)" by smt lemma "-40 + 1 = (-39::7 word)" by smt lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt lemma "x = (5 :: 4 word) \ 4 * x = 4" by smt section \Bit-level logic\ lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" by smt lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt -lemma "0b10011 << 2 = (0b1001100::8 word)" by smt -lemma "0b11001 >> 2 = (0b110::8 word)" by smt -lemma "0b10011 >>> 2 = (0b100::8 word)" by smt +lemma "push_bit 2 0b10011 = (0b1001100::8 word)" by smt +lemma "drop_bit 2 0b11001 = (0b110::8 word)" by smt +lemma "signed_drop_bit 2 0b10011 = (0b100::8 word)" by smt lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt lemma "w < 256 \ (w :: 16 word) AND 0x00FF = w" by smt section \Combined integer-bitvector properties\ lemma assumes "bv2int 0 = 0" and "bv2int 1 = 1" and "bv2int 2 = 2" and "bv2int 3 = 3" and "\x::2 word. bv2int x > 0" shows "\i::int. i < 0 \ (\x::2 word. bv2int x > i)" using assms by smt lemma "P (0 \ (a :: 4 word)) = P True" by smt end diff --git a/src/HOL/SPARK/Manual/Reference.thy b/src/HOL/SPARK/Manual/Reference.thy --- a/src/HOL/SPARK/Manual/Reference.thy +++ b/src/HOL/SPARK/Manual/Reference.thy @@ -1,327 +1,330 @@ (*<*) theory Reference -imports "HOL-SPARK.SPARK" "HOL-Word.Bits_Int" +imports "HOL-SPARK.SPARK" begin +lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n" for x :: int + by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod) + syntax (my_constrain output) "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) (*>*) chapter \HOL-\SPARK{} Reference\ text \ \label{sec:spark-reference} This section is intended as a quick reference for the HOL-\SPARK{} verification environment. In \secref{sec:spark-commands}, we give a summary of the commands provided by the HOL-\SPARK{}, while \secref{sec:spark-types} contains a description of how particular types of \SPARK{} and FDL are modelled in Isabelle. \ section \Commands\ text \ \label{sec:spark-commands} This section describes the syntax and effect of each of the commands provided by HOL-\SPARK{}. \<^rail>\ @'spark_open' name ('(' name ')')? \ Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs. Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}. The corresponding \texttt{*.fdl} and \texttt{*.rls} files must reside in the same directory as the file given as an argument to the command. This command also generates records and datatypes for the types specified in the \texttt{*.fdl} file, unless they have already been associated with user-defined Isabelle types (see below). Since the full package name currently cannot be determined from the files generated by the \SPARK{} Examiner, the command also allows to specify an optional package prefix in the format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several packages, this is necessary in order for the verification environment to be able to map proof functions and types defined in Isabelle to their \SPARK{} counterparts. \<^rail>\ @'spark_proof_functions' ((name '=' term)+) \ Associates a proof function with the given name to a term. The name should be the full name of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix. This command can be used both inside and outside a verification environment. The latter variant is useful for introducing proof functions that are shared by several procedures or packages, whereas the former allows the given term to refer to the types generated by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the \texttt{*.fdl} file. \<^rail>\ @'spark_types' ((name '=' type (mapping?))+) ; mapping: '('((name '=' name)+',')')' \ Associates a \SPARK{} type with the given name with an Isabelle type. This command can only be used outside a verification environment. The given type must be either a record or a datatype, where the names of fields or constructors must either match those of the corresponding \SPARK{} types (modulo casing), or a mapping from \SPARK{} to Isabelle names has to be provided. This command is useful when having to define proof functions referring to record or enumeration types that are shared by several procedures or packages. First, the types required by the proof functions can be introduced using Isabelle's commands for defining records or datatypes. Having introduced the types, the proof functions can be defined in Isabelle. Finally, both the proof functions and the types can be associated with their \SPARK{} counterparts. \<^rail>\ @'spark_status' (('(proved)' | '(unproved)')?) \ Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved). The output can be restricted to the proved or unproved VCs by giving the corresponding option to the command. \<^rail>\ @'spark_vc' name \ Initiates the proof of the VC with the given name. Similar to the standard \isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command must be followed by a sequence of proof commands. The command introduces the hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers \texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC. \<^rail>\ @'spark_end' '(incomplete)'? \ Closes the current verification environment. Unless the \texttt{incomplete} option is given, all VCs must have been proved, otherwise the command issues an error message. As a side effect, the command generates a proof review (\texttt{*.prv}) file to inform POGS of the proved VCs. \ section \Types\ text \ \label{sec:spark-types} The main types of FDL are integers, enumeration types, records, and arrays. In the following sections, we describe how these types are modelled in Isabelle. \ subsection \Integers\ text \ The FDL type \texttt{integer} is modelled by the Isabelle type \<^typ>\int\. While the FDL \texttt{mod} operator behaves in the same way as its Isabelle counterpart, this is not the case for the \texttt{div} operator. As has already been mentioned in \secref{sec:proving-vcs}, the \texttt{div} operator of \SPARK{} always truncates towards zero, whereas the \div\ operator of Isabelle truncates towards minus infinity. Therefore, the FDL \texttt{div} operator is mapped to the \sdiv\ operator in Isabelle. The characteristic theorems of \sdiv\, in particular those describing the relationship with the standard \div\ operator, are shown in \figref{fig:sdiv-properties} \begin{figure} \begin{center} \small \begin{tabular}{ll} \sdiv_def\: & @{thm sdiv_def} \\ \sdiv_minus_dividend\: & @{thm sdiv_minus_dividend} \\ \sdiv_minus_divisor\: & @{thm sdiv_minus_divisor} \\ \sdiv_pos_pos\: & @{thm [mode=no_brackets] sdiv_pos_pos} \\ \sdiv_pos_neg\: & @{thm [mode=no_brackets] sdiv_pos_neg} \\ \sdiv_neg_pos\: & @{thm [mode=no_brackets] sdiv_neg_pos} \\ \sdiv_neg_neg\: & @{thm [mode=no_brackets] sdiv_neg_neg} \\ \end{tabular} \end{center} \caption{Characteristic properties of \sdiv\} \label{fig:sdiv-properties} \end{figure} \begin{figure} \begin{center} \small \begin{tabular}{ll} \AND_lower\: & @{thm [mode=no_brackets] AND_lower} \\ \OR_lower\: & @{thm [mode=no_brackets] OR_lower} \\ \XOR_lower\: & @{thm [mode=no_brackets] XOR_lower} \\ \AND_upper1\: & @{thm [mode=no_brackets] AND_upper1} \\ \AND_upper2\: & @{thm [mode=no_brackets] AND_upper2} \\ \OR_upper\: & @{thm [mode=no_brackets] OR_upper} \\ \XOR_upper\: & @{thm [mode=no_brackets] XOR_upper} \\ \AND_mod\: & @{thm [mode=no_brackets] AND_mod} \end{tabular} \end{center} \caption{Characteristic properties of bitwise operators} \label{fig:bitwise} \end{figure} The bitwise logical operators of \SPARK{} and FDL are modelled by the operators \AND\, \OR\ and \XOR\ from Isabelle's \Word\ library, all of which have type \<^typ>\int \ int \ int\. A list of properties of these operators that are useful in proofs about \SPARK{} programs are shown in \figref{fig:bitwise} \ subsection \Enumeration types\ text \ The FDL enumeration type \begin{alltt} type \(t\) = (\(e\sb{1}\), \(e\sb{2}\), \dots, \(e\sb{n}\)); \end{alltt} is modelled by the Isabelle datatype \begin{isabelle} \normalsize \isacommand{datatype}\ $t$\ =\ $e_1$\ $\mid$\ $e_2$\ $\mid$\ \dots\ $\mid$\ $e_n$ \end{isabelle} The HOL-\SPARK{} environment defines a type class \<^class>\spark_enum\ that captures the characteristic properties of all enumeration types. It provides the following polymorphic functions and constants for all types \'a\ of this type class: \begin{flushleft} @{term_type [mode=my_constrain] pos} \\ @{term_type [mode=my_constrain] val} \\ @{term_type [mode=my_constrain] succ} \\ @{term_type [mode=my_constrain] pred} \\ @{term_type [mode=my_constrain] first_el} \\ @{term_type [mode=my_constrain] last_el} \end{flushleft} In addition, \<^class>\spark_enum\ is a subclass of the \<^class>\linorder\ type class, which allows the comparison operators \<\ and \\\ to be used on enumeration types. The polymorphic operations shown above enjoy a number of generic properties that hold for all enumeration types. These properties are listed in \figref{fig:enum-generic-properties}. Moreover, \figref{fig:enum-specific-properties} shows a list of properties that are specific to each enumeration type $t$, such as the characteristic equations for \<^term>\val\ and \<^term>\pos\. \begin{figure}[t] \begin{center} \small \begin{tabular}{ll} \range_pos\: & @{thm range_pos} \\ \less_pos\: & @{thm less_pos} \\ \less_eq_pos\: & @{thm less_eq_pos} \\ \val_def\: & @{thm val_def} \\ \succ_def\: & @{thm succ_def} \\ \pred_def\: & @{thm pred_def} \\ \first_el_def\: & @{thm first_el_def} \\ \last_el_def\: & @{thm last_el_def} \\ \inj_pos\: & @{thm inj_pos} \\ \val_pos\: & @{thm val_pos} \\ \pos_val\: & @{thm pos_val} \\ \first_el_smallest\: & @{thm first_el_smallest} \\ \last_el_greatest\: & @{thm last_el_greatest} \\ \pos_succ\: & @{thm pos_succ} \\ \pos_pred\: & @{thm pos_pred} \\ \succ_val\: & @{thm succ_val} \\ \pred_val\: & @{thm pred_val} \end{tabular} \end{center} \caption{Generic properties of functions on enumeration types} \label{fig:enum-generic-properties} \end{figure} \begin{figure}[t] \begin{center} \small \begin{tabular}{ll@ {\hspace{2cm}}ll} \texttt{$t$\_val}: & \isa{val\ $0$\ =\ $e_1$} & \texttt{$t$\_pos}: & pos\ $e_1$\ =\ $0$ \\ & \isa{val\ $1$\ =\ $e_2$} & & pos\ $e_2$\ =\ $1$ \\ & \hspace{1cm}\vdots & & \hspace{1cm}\vdots \\ & \isa{val\ $(n-1)$\ =\ $e_n$} & & pos\ $e_n$\ =\ $n-1$ \end{tabular} \\[3ex] \begin{tabular}{ll} \texttt{$t$\_card}: & \isa{card($t$)\ =\ $n$} \\ \texttt{$t$\_first\_el}: & \isa{first\_el\ =\ $e_1$} \\ \texttt{$t$\_last\_el}: & \isa{last\_el\ =\ $e_n$} \end{tabular} \end{center} \caption{Type-specific properties of functions on enumeration types} \label{fig:enum-specific-properties} \end{figure} \ subsection \Records\ text \ The FDL record type \begin{alltt} type \(t\) = record \(f\sb{1}\) : \(t\sb{1}\); \(\vdots\) \(f\sb{n}\) : \(t\sb{n}\) end; \end{alltt} is modelled by the Isabelle record type \begin{isabelle} \normalsize \isacommand{record}\ t\ = \isanewline \ \ $f_1$\ ::\ $t_1$ \isanewline \ \ \ \vdots \isanewline \ \ $f_n$\ ::\ $t_n$ \end{isabelle} Records are constructed using the notation \isa{\isasymlparr$f_1$\ =\ $v_1$,\ $\ldots$,\ $f_n$\ =\ $v_n$\isasymrparr}, a field $f_i$ of a record $r$ is selected using the notation $f_i~r$, and the fields $f$ and $f'$ of a record $r$ can be updated using the notation \mbox{\isa{$r$\ \isasymlparr$f$\ :=\ $v$,\ $f'$\ :=\ $v'$\isasymrparr}}. \ subsection \Arrays\ text \ The FDL array type \begin{alltt} type \(t\) = array [\(t\sb{1}\), \(\ldots\), \(t\sb{n}\)] of \(u\); \end{alltt} is modelled by the Isabelle function type $t_1 \times \cdots \times t_n \Rightarrow u$. Array updates are written as \isa{$A$($x_1$\ := $y_1$,\ \dots,\ $x_n$\ :=\ $y_n$)}. To allow updating an array at a set of indices, HOL-\SPARK{} provides the notation \isa{\dots\ [:=]\ \dots}, which can be combined with \isa{\dots\ :=\ \dots} and has the properties @{thm [display,mode=no_brackets] fun_upds_in fun_upds_notin upds_singleton} Thus, we can write expressions like @{term [display] "(A::int\int) ({0..9} [:=] 42, 15 := 99, {20..29} [:=] 0)"} that would be cumbersome to write using single updates. \ section \User-defined proof functions and types\ text \ To illustrate the interplay between the commands for introducing user-defined proof functions and types mentioned in \secref{sec:spark-commands}, we now discuss a larger example involving the definition of proof functions on complex types. Assume we would like to define an array type, whose elements are records that themselves contain arrays. Moreover, assume we would like to initialize all array elements and record fields of type \texttt{Integer} in an array of this type with the value \texttt{0}. The specification of package \texttt{Complex\_Types} containing the definition of the array type, which we call \texttt{Array\_Type2}, is shown in \figref{fig:complex-types}. It also contains the declaration of a proof function \texttt{Initialized} that is used to express that the array has been initialized. The two other proof functions \texttt{Initialized2} and \texttt{Initialized3} are used to reason about the initialization of the inner array. Since the array types and proof functions may be used by several packages, such as the one shown in \figref{fig:complex-types-app}, it is advantageous to define the proof functions in a central theory that can be included by other theories containing proofs about packages using \texttt{Complex\_Types}. We show this theory in \figref{fig:complex-types-thy}. Since the proof functions refer to the enumeration and record types defined in \texttt{Complex\_Types}, we need to define the Isabelle counterparts of these types using the \isa{\isacommand{datatype}} and \isa{\isacommand{record}} commands in order to be able to write down the definition of the proof functions. These types are linked to the corresponding \SPARK{} types using the \isa{\isacommand{spark\_types}} command. Note that we have to specify the full name of the \SPARK{} functions including the package prefix. Using the logic of Isabelle, we can then define functions involving the enumeration and record types introduced above, and link them to the corresponding \SPARK{} proof functions. It is important that the \isa{\isacommand{definition}} commands are preceeded by the \isa{\isacommand{spark\_types}} command, since the definition of \initialized3\ uses the \val\ function for enumeration types that is only available once that \day\ has been declared as a \SPARK{} type. \begin{figure} \lstinputlisting{complex_types.ads} \caption{Nested array and record types} \label{fig:complex-types} \end{figure} \begin{figure} \lstinputlisting{complex_types_app.ads} \lstinputlisting{complex_types_app.adb} \caption{Application of \texttt{Complex\_Types} package} \label{fig:complex-types-app} \end{figure} \begin{figure} \input{Complex_Types} \caption{Theory defining proof functions for complex types} \label{fig:complex-types-thy} \end{figure} \ (*<*) end (*>*) diff --git a/src/HOL/Word/Tools/smt_word.ML b/src/HOL/Word/Tools/smt_word.ML --- a/src/HOL/Word/Tools/smt_word.ML +++ b/src/HOL/Word/Tools/smt_word.ML @@ -1,158 +1,158 @@ (* Title: HOL/Word/Tools/smt_word.ML Author: Sascha Boehme, TU Muenchen SMT setup for words. *) signature SMT_WORD = sig val add_word_shift': term * string -> Context.generic -> Context.generic end structure SMT_Word : SMT_WORD = struct open Word_Lib (* SMT-LIB logic *) (* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers. Better set the logic to "" and make at least Z3 happy. *) fun smtlib_logic ts = if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE (* SMT-LIB builtins *) local val smtlibC = SMTLIB_Interface.smtlibC val wordT = \<^typ>\'a::len word\ fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")" fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")" fun word_typ (Type (\<^type_name>\word\, [T])) = Option.map (rpair [] o index1 "BitVec") (try dest_binT T) | word_typ _ = NONE fun word_num (Type (\<^type_name>\word\, [T])) k = Option.map (index1 ("bv" ^ string_of_int k)) (try dest_binT T) | word_num _ _ = NONE fun if_fixed pred m n T ts = let val (Us, U) = Term.strip_type T in if pred (U, Us) then SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) else NONE end fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m fun add_word_fun f (t, n) = let val (m, _) = Term.dest_Const t in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end val mk_nat = HOLogic.mk_number \<^typ>\nat\ + fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t + | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts) + + fun shift m n T ts = + let val U = Term.domain_type (Term.range_type T) + in + (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of + (true, SOME i) => + SOME (n, 2, [hd (tl ts), HOLogic.mk_number U i], mk_shift (m, T)) + | _ => NONE) (* FIXME: also support non-numerical shifts *) + end + fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u)) | mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts) fun shift' m n T ts = let val U = Term.domain_type T in (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of (true, SOME i) => SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T)) | _ => NONE) (* FIXME: also support non-numerical shifts *) end - fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t - | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts) - - fun shift m n T ts = - let val U = Term.domain_type T - in - (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of - (true, SOME i) => - SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T)) - | _ => NONE) (* FIXME: also support non-numerical shifts *) - end - fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts) fun extract m n T ts = let val U = Term.range_type (Term.range_type T) in (case (try (snd o HOLogic.dest_number o hd) ts, try dest_wordT U) of (SOME lb, SOME i) => SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb) | _ => NONE) end fun mk_extend c ts = Term.list_comb (Const c, ts) fun extend m n T ts = let val (U1, U2) = Term.dest_funT T in (case (try dest_wordT U1, try dest_wordT U2) of (SOME i, SOME j) => if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T)) else NONE | _ => NONE) end fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts) fun rotate m n T ts = let val U = Term.domain_type (Term.range_type T) in (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i) | _ => NONE) end in val setup_builtins = SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #> fold (add_word_fun if_fixed_all) [ (\<^term>\uminus :: 'a::len word \ _\, "bvneg"), (\<^term>\plus :: 'a::len word \ _\, "bvadd"), (\<^term>\minus :: 'a::len word \ _\, "bvsub"), (\<^term>\times :: 'a::len word \ _\, "bvmul"), (\<^term>\NOT :: 'a::len word \ _\, "bvnot"), (\<^term>\(AND) :: 'a::len word \ _\, "bvand"), (\<^term>\(OR) :: 'a::len word \ _\, "bvor"), (\<^term>\(XOR) :: 'a::len word \ _\, "bvxor"), (\<^term>\word_cat :: 'a::len word \ _\, "concat") ] #> fold (add_word_fun shift) [ (\<^term>\push_bit :: nat \ 'a::len word \ _ \, "bvshl"), (\<^term>\drop_bit :: nat \ 'a::len word \ _\, "bvlshr"), (\<^term>\signed_drop_bit :: nat \ 'a::len word \ _\, "bvashr") ] #> add_word_fun extract (\<^term>\slice :: _ \ 'a::len word \ _\, "extract") #> fold (add_word_fun extend) [ (\<^term>\ucast :: 'a::len word \ _\, "zero_extend"), (\<^term>\scast :: 'a::len word \ _\, "sign_extend") ] #> fold (add_word_fun rotate) [ (\<^term>\word_rotl\, "rotate_left"), (\<^term>\word_rotr\, "rotate_right") ] #> fold (add_word_fun if_fixed_args) [ (\<^term>\less :: 'a::len word \ _\, "bvult"), (\<^term>\less_eq :: 'a::len word \ _\, "bvule"), (\<^term>\word_sless\, "bvslt"), (\<^term>\word_sle\, "bvsle") ] val add_word_shift' = add_word_fun shift' end (* setup *) val _ = Theory.setup (Context.theory_map ( SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins)) end; diff --git a/src/HOL/Word/Traditional_Syntax.thy b/src/HOL/Word/Traditional_Syntax.thy --- a/src/HOL/Word/Traditional_Syntax.thy +++ b/src/HOL/Word/Traditional_Syntax.thy @@ -1,534 +1,526 @@ (* Author: Jeremy Dawson, NICTA *) section \Operation variants with traditional syntax\ theory Traditional_Syntax imports Word begin class semiring_bit_syntax = semiring_bit_shifts begin definition test_bit :: \'a \ nat \ bool\ (infixl "!!" 100) where test_bit_eq_bit: \test_bit = bit\ definition shiftl :: \'a \ nat \ 'a\ (infixl "<<" 55) where shiftl_eq_push_bit: \a << n = push_bit n a\ definition shiftr :: \'a \ nat \ 'a\ (infixl ">>" 55) where shiftr_eq_drop_bit: \a >> n = drop_bit n a\ end instance word :: (len) semiring_bit_syntax .. context includes lifting_syntax begin lemma test_bit_word_transfer [transfer_rule]: \(pcr_word ===> (=)) (\k n. n < LENGTH('a) \ bit k n) (test_bit :: 'a::len word \ _)\ by (unfold test_bit_eq_bit) transfer_prover lemma shiftl_word_transfer [transfer_rule]: \(pcr_word ===> (=) ===> pcr_word) (\k n. push_bit n k) shiftl\ by (unfold shiftl_eq_push_bit) transfer_prover lemma shiftr_word_transfer [transfer_rule]: \(pcr_word ===> (=) ===> pcr_word) (\k n. (drop_bit n \ take_bit LENGTH('a)) k) (shiftr :: 'a::len word \ _)\ by (unfold shiftr_eq_drop_bit) transfer_prover end lemma test_bit_word_eq: \test_bit = (bit :: 'a::len word \ _)\ by (fact test_bit_eq_bit) lemma shiftl_word_eq: \w << n = push_bit n w\ for w :: \'a::len word\ by (fact shiftl_eq_push_bit) lemma shiftr_word_eq: \w >> n = drop_bit n w\ for w :: \'a::len word\ by (fact shiftr_eq_drop_bit) lemma test_bit_eq_iff: "test_bit u = test_bit v \ u = v" for u v :: "'a::len word" by (simp add: bit_eq_iff test_bit_eq_bit fun_eq_iff) lemma test_bit_size: "w !! n \ n < size w" for w :: "'a::len word" by transfer simp lemma word_eq_iff: "x = y \ (\n?P \ ?Q\) for x y :: "'a::len word" by transfer (auto simp add: bit_eq_iff bit_take_bit_iff) lemma word_eqI: "(\n. n < size u \ u !! n = v !! n) \ u = v" for u :: "'a::len word" by (simp add: word_size word_eq_iff) lemma word_eqD: "u = v \ u !! x = v !! x" for u v :: "'a::len word" by simp lemma test_bit_bin': "w !! n \ n < size w \ bit (uint w) n" by transfer (simp add: bit_take_bit_iff) lemmas test_bit_bin = test_bit_bin' [unfolded word_size] lemma word_test_bit_def: \test_bit a = bit (uint a)\ by transfer (simp add: fun_eq_iff bit_take_bit_iff) lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] lemma word_test_bit_transfer [transfer_rule]: "(rel_fun pcr_word (rel_fun (=) (=))) (\x n. n < LENGTH('a) \ bit x n) (test_bit :: 'a::len word \ _)" by (simp only: test_bit_eq_bit) transfer_prover lemma test_bit_wi [simp]: "(word_of_int x :: 'a::len word) !! n \ n < LENGTH('a) \ bit x n" by transfer simp lemma word_ops_nth_size: "n < size x \ (x OR y) !! n = (x !! n | y !! n) \ (x AND y) !! n = (x !! n \ y !! n) \ (x XOR y) !! n = (x !! n \ y !! n) \ (NOT x) !! n = (\ x !! n)" for x :: "'a::len word" by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff) lemma word_ao_nth: "(x OR y) !! n = (x !! n | y !! n) \ (x AND y) !! n = (x !! n \ y !! n)" for x :: "'a::len word" by transfer (auto simp add: bit_or_iff bit_and_iff) lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]] lemmas msb1 = msb0 [where i = 0] lemma test_bit_numeral [simp]: "(numeral w :: 'a::len word) !! n \ n < LENGTH('a) \ bit (numeral w :: int) n" by transfer (rule refl) lemma test_bit_neg_numeral [simp]: "(- numeral w :: 'a::len word) !! n \ n < LENGTH('a) \ bit (- numeral w :: int) n" by transfer (rule refl) lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \ n = 0" by transfer (auto simp add: bit_1_iff) lemma nth_0 [simp]: "\ (0 :: 'a::len word) !! n" by transfer simp lemma nth_minus1 [simp]: "(-1 :: 'a::len word) !! n \ n < LENGTH('a)" by transfer simp lemma shiftl1_code [code]: \shiftl1 w = push_bit 1 w\ by transfer (simp add: ac_simps) lemma uint_shiftr_eq: \uint (w >> n) = uint w div 2 ^ n\ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv) lemma shiftr1_code [code]: \shiftr1 w = drop_bit 1 w\ by transfer (simp add: drop_bit_Suc) lemma shiftl_def: \w << n = (shiftl1 ^^ n) w\ proof - have \push_bit n = (((*) 2 ^^ n) :: int \ int)\ for n by (induction n) (simp_all add: fun_eq_iff funpow_swap1, simp add: ac_simps) then show ?thesis by transfer simp qed lemma shiftr_def: \w >> n = (shiftr1 ^^ n) w\ proof - have \shiftr1 ^^ n = (drop_bit n :: 'a word \ 'a word)\ apply (induction n) apply simp apply (simp only: shiftr1_eq_div_2 [abs_def] drop_bit_eq_div [abs_def] funpow_Suc_right) apply (use div_exp_eq [of _ 1, where ?'a = \'a word\] in simp) done then show ?thesis by (simp add: shiftr_eq_drop_bit) qed lemma bit_shiftl_word_iff: \bit (w << m) n \ m \ n \ n < LENGTH('a) \ bit w (n - m)\ for w :: \'a::len word\ by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) lemma bit_shiftr_word_iff: \bit (w >> m) n \ bit w (m + n)\ for w :: \'a::len word\ by (simp add: shiftr_word_eq bit_drop_bit_eq) lift_definition sshiftr :: \'a::len word \ nat \ 'a word\ (infixl \>>>\ 55) is \\k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))\ by (simp flip: signed_take_bit_decr_length_iff) lemma sshiftr_eq [code]: \w >>> n = signed_drop_bit n w\ by transfer simp lemma sshiftr_eq_funpow_sshiftr1: \w >>> n = (sshiftr1 ^^ n) w\ apply (rule sym) apply (simp add: sshiftr1_eq_signed_drop_bit_Suc_0 sshiftr_eq) apply (induction n) apply simp_all done lemma uint_sshiftr_eq: \uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\ for w :: \'a::len word\ by transfer (simp flip: drop_bit_eq_div) lemma sshift1_code [code]: \sshiftr1 w = signed_drop_bit 1 w\ by transfer (simp add: drop_bit_Suc) lemma sshiftr_0 [simp]: "0 >>> n = 0" by transfer simp lemma sshiftr_n1 [simp]: "-1 >>> n = -1" by transfer simp lemma bit_sshiftr_word_iff: \bit (w >>> m) n \ bit w (if LENGTH('a) - m \ n \ n < LENGTH('a) then LENGTH('a) - 1 else (m + n))\ for w :: \'a::len word\ apply transfer apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le simp flip: bit_Suc) using le_less_Suc_eq apply fastforce using le_less_Suc_eq apply fastforce done lemma nth_sshiftr : "(w >>> m) !! n = (n < size w \ (if n + m \ size w then w !! (size w - 1) else w !! (n + m)))" apply transfer apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le ac_simps) using le_less_Suc_eq apply fastforce using le_less_Suc_eq apply fastforce done lemma sshiftr_numeral [simp]: \(numeral k >>> numeral n :: 'a::len word) = word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k)))\ apply (rule word_eqI) apply (cases \LENGTH('a)\) apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps) done lemma revcast_down_us [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = ucast (w >>> n)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_revcast_iff bit_ucast_iff bit_sshiftr_word_iff ac_simps) done lemma revcast_down_ss [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = scast (w >>> n)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_revcast_iff bit_word_scast_iff bit_sshiftr_word_iff ac_simps) done lemma sshiftr_div_2n: "sint (w >>> n) = sint w div 2 ^ n" using sint_signed_drop_bit_eq [of n w] by (simp add: drop_bit_eq_div sshiftr_eq) lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]] lemma nth_sint: fixes w :: "'a::len word" defines "l \ LENGTH('a)" shows "bit (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" unfolding sint_uint l_def by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def) lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \ m = n \ m < LENGTH('a)" by transfer (auto simp add: bit_exp_iff) lemma nth_w2p: "((2::'a::len word) ^ n) !! m \ m = n \ m < LENGTH('a::len)" by transfer (auto simp add: bit_exp_iff) lemma bang_is_le: "x !! m \ 2 ^ m \ x" for x :: "'a::len word" apply (rule xtrans(3)) apply (rule_tac [2] y = "x" in le_word_or2) apply (rule word_eqI) apply (auto simp add: word_ao_nth nth_w2p word_size) done lemma mask_eq: \mask n = (1 << n) - (1 :: 'a::len word)\ by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \ n < LENGTH('a))" by transfer (simp add: bit_take_bit_iff ac_simps) lemma shiftl_0 [simp]: "(0::'a::len word) << n = 0" by transfer simp lemma shiftr_0 [simp]: "(0::'a::len word) >> n = 0" by transfer simp lemma nth_shiftl1: "shiftl1 w !! n \ n < size w \ n > 0 \ w !! (n - 1)" by transfer (auto simp add: bit_double_iff) lemma nth_shiftl': "(w << m) !! n \ n < size w \ n >= m \ w !! (n - m)" for w :: "'a::len word" by transfer (auto simp add: bit_push_bit_iff) lemmas nth_shiftl = nth_shiftl' [unfolded word_size] lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n" by transfer (auto simp add: bit_take_bit_iff simp flip: bit_Suc) lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)" for w :: "'a::len word" apply (unfold shiftr_def) apply (induct "m" arbitrary: n) apply (auto simp add: nth_shiftr1) done lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)" apply transfer apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc) using le_less_Suc_eq apply fastforce using le_less_Suc_eq apply fastforce done lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n" by (fact uint_shiftr_eq) lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)" by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev) lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)" by (simp add: shiftl_rev) lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)" by (simp add: rev_shiftl) lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)" by (simp add: shiftr_rev) lemma shiftl_numeral [simp]: \numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)\ by (fact shiftl_word_eq) lemma shiftl_zero_size: "size x \ n \ x << n = 0" for x :: "'a::len word" apply transfer apply (simp add: take_bit_push_bit) done lemma shiftl_t2n: "shiftl w n = 2 ^ n * w" for w :: "'a::len word" by (induct n) (auto simp: shiftl_def shiftl1_2t) lemma shiftr_numeral [simp]: \(numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)\ by (fact shiftr_word_eq) lemma nth_mask [simp]: \(mask n :: 'a::len word) !! i \ i < n \ i < size (mask n :: 'a word)\ by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff) lemma slice_shiftr: "slice n w = ucast (w >> n)" apply (rule bit_word_eqI) apply (cases \n \ LENGTH('b)\) apply (auto simp add: bit_slice_iff bit_ucast_iff bit_shiftr_word_iff ac_simps dest: bit_imp_le_length) done lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n) \ m < LENGTH('a))" by (simp add: slice_shiftr nth_ucast nth_shiftr) lemma revcast_down_uu [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = ucast (w >> n)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_revcast_iff bit_ucast_iff bit_shiftr_word_iff ac_simps) done lemma revcast_down_su [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = scast (w >> n)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_revcast_iff bit_word_scast_iff bit_shiftr_word_iff ac_simps) done lemma cast_down_rev [OF refl]: "uc = ucast \ source_size uc = target_size uc + n \ uc w = revcast (w << n)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff) done lemma revcast_up [OF refl]: "rc = revcast \ source_size rc + n = target_size rc \ rc w = (ucast w :: 'a::len word) << n" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff) apply auto apply (metis add.commute add_diff_cancel_right) apply (metis diff_add_inverse2 diff_diff_add) done lemmas rc1 = revcast_up [THEN revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]] lemmas rc2 = revcast_down_uu [THEN revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]] lemmas ucast_up = rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]] lemmas ucast_down = rc2 [simplified rev_shiftr revcast_ucast [symmetric]] \ \problem posed by TPHOLs referee: criterion for overflow of addition of signed integers\ lemma sofl_test: \sint x + sint y = sint (x + y) \ (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\ for x y :: \'a::len word\ proof - obtain n where n: \LENGTH('a) = Suc n\ by (cases \LENGTH('a)\) simp_all have *: \sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \ sint x + sint y \ - (2 ^ n)\ \signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \ 2 ^ n > sint x + sint y\ using signed_take_bit_int_greater_eq [of \sint x + sint y\ n] signed_take_bit_int_less_eq [of n \sint x + sint y\] by (auto intro: ccontr) have \sint x + sint y = sint (x + y) \ (sint (x + y) < 0 \ sint x < 0) \ (sint (x + y) < 0 \ sint y < 0)\ using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y] signed_take_bit_int_eq_self [of \LENGTH('a) - 1\ \sint x + sint y\] apply (auto simp add: not_less) apply (unfold sint_word_ariths) apply (subst signed_take_bit_int_eq_self) prefer 4 apply (subst signed_take_bit_int_eq_self) prefer 7 apply (subst signed_take_bit_int_eq_self) prefer 10 apply (subst signed_take_bit_int_eq_self) apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *) done then show ?thesis apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff) apply (simp add: bit_last_iff) done qed lemma shiftr_zero_size: "size x \ n \ x >> n = 0" for x :: "'a :: len word" by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size) lemma test_bit_cat [OF refl]: "wc = word_cat a b \ wc !! n = (n < size wc \ (if n < size b then b !! n else a !! (n - size b)))" apply (simp add: word_size not_less; transfer) apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff) done \ \keep quantifiers for use in simplification\ lemma test_bit_split': "word_split c = (a, b) \ (\n m. b !! n = (n < size b \ c !! n) \ a !! m = (m < size a \ c !! (m + size b)))" by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size bit_drop_bit_eq ac_simps exp_eq_zero_iff dest: bit_imp_le_length) lemma test_bit_split: "word_split c = (a, b) \ (\n::nat. b !! n \ n < size b \ c !! n) \ (\m::nat. a !! m \ m < size a \ c !! (m + size b))" by (simp add: test_bit_split') lemma test_bit_split_eq: "word_split c = (a, b) \ ((\n::nat. b !! n = (n < size b \ c !! n)) \ (\m::nat. a !! m = (m < size a \ c !! (m + size b))))" apply (rule_tac iffI) apply (rule_tac conjI) apply (erule test_bit_split [THEN conjunct1]) apply (erule test_bit_split [THEN conjunct2]) apply (case_tac "word_split c") apply (frule test_bit_split) apply (erule trans) apply (fastforce intro!: word_eqI simp add: word_size) done lemma test_bit_rcat: "sw = size (hd wl) \ rc = word_rcat wl \ rc !! n = (n < size rc \ n div sw < size wl \ (rev wl) ! (n div sw) !! (n mod sw))" for wl :: "'a::len word list" by (simp add: word_size word_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff) (simp add: test_bit_eq_bit) lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong] lemma max_test_bit: "(max_word::'a::len word) !! n \ n < LENGTH('a)" by (fact nth_minus1) lemma shiftr_x_0 [iff]: "x >> 0 = x" for x :: "'a::len word" by transfer simp lemma shiftl_x_0 [simp]: "x << 0 = x" for x :: "'a::len word" by (simp add: shiftl_t2n) lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n" by (simp add: shiftl_t2n) lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)" by (induct n) (auto simp: shiftr_def) lemma map_nth_0 [simp]: "map ((!!) (0::'a::len word)) xs = replicate (length xs) False" by (induct xs) auto lemma word_and_1: "n AND 1 = (if n !! 0 then 1 else 0)" for n :: "_ word" by (rule bit_word_eqI) (auto simp add: bit_and_iff test_bit_eq_bit bit_1_iff intro: gr0I) lemma test_bit_1' [simp]: "(1 :: 'a :: len word) !! n \ 0 < LENGTH('a) \ n = 0" by simp lemma shiftl0: "x << 0 = (x :: 'a :: len word)" by (fact shiftl_x_0) -setup \ - Context.theory_map (fold SMT_Word.add_word_shift' [ - (\<^term>\shiftl :: 'a::len word \ _\, "bvshl"), - (\<^term>\shiftr :: 'a::len word \ _\, "bvlshr"), - (\<^term>\sshiftr :: 'a::len word \ _\, "bvashr") - ]) -\ - end