(*Generated by Lem from machine_word.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_numTheory lem_basic_classesTheory lem_showTheory lem_functionTheory wordsTheory wordsLib bitstringTheory integer_wordTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_machine_word"



(*open import Bool Num Basic_classes Show Function*)

(*open import {isabelle} `~~/src/HOL/Word/Word`*)
(*open import {hol} `wordsTheory` `wordsLib` `bitstringTheory` `integer_wordTheory`*)

(*type mword 'a*)

(*class (Size 'a)
  val size : nat
end*)

(*val native_size : forall 'a. nat*)

(*val ocaml_inject : forall 'a. nat * natural -> mword 'a*)

(* A singleton type family that can be used to carry a size as the type parameter *)

(*type itself 'a*)

(*val the_value : forall 'a. itself 'a*)

(*val size_itself : forall 'a. Size 'a => itself 'a -> nat*)
val _ = Define `
 ((size_itself:'a itself -> num) x=  (dimindex (the_value : 'a itself)))`;


(*******************************************************************)
(* Fixed bitwidths extracted from Anthony's models.                *)
(*                                                                 *)
(* If you need a size N that is not included here, put the lines   *)
(*                                                                 *)
(* type tyN                                                        *)
(* instance (Size tyN) let size = N end                            *)
(* declare isabelle target_rep type tyN = `N`                      *)
(* declare hol target_rep type tyN = `N`                           *)
(*                                                                 *)
(* in your project, replacing N in each line.                      *)
(*******************************************************************)

(*type ty1*)
(*type ty2*)
(*type ty3*)
(*type ty4*)
(*type ty5*)
(*type ty6*)
(*type ty7*)
(*type ty8*)
(*type ty9*)
(*type ty10*)
(*type ty11*)
(*type ty12*)
(*type ty13*)
(*type ty14*)
(*type ty15*)
(*type ty16*)
(*type ty17*)
(*type ty18*)
(*type ty19*)
(*type ty20*)
(*type ty21*)
(*type ty22*)
(*type ty23*)
(*type ty24*)
(*type ty25*)
(*type ty26*)
(*type ty27*)
(*type ty28*)
(*type ty29*)
(*type ty30*)
(*type ty31*)
(*type ty32*)
(*type ty33*)
(*type ty34*)
(*type ty35*)
(*type ty36*)
(*type ty37*)
(*type ty38*)
(*type ty39*)
(*type ty40*)
(*type ty41*)
(*type ty42*)
(*type ty43*)
(*type ty44*)
(*type ty45*)
(*type ty46*)
(*type ty47*)
(*type ty48*)
(*type ty49*)
(*type ty50*)
(*type ty51*)
(*type ty52*)
(*type ty53*)
(*type ty54*)
(*type ty55*)
(*type ty56*)
(*type ty57*)
(*type ty58*)
(*type ty59*)
(*type ty60*)
(*type ty61*)
(*type ty62*)
(*type ty63*)
(*type ty64*)
(*type ty65*)
(*type ty66*)
(*type ty67*)
(*type ty68*)
(*type ty69*)
(*type ty70*)
(*type ty71*)
(*type ty72*)
(*type ty73*)
(*type ty74*)
(*type ty75*)
(*type ty76*)
(*type ty77*)
(*type ty78*)
(*type ty79*)
(*type ty80*)
(*type ty81*)
(*type ty82*)
(*type ty83*)
(*type ty84*)
(*type ty85*)
(*type ty86*)
(*type ty87*)
(*type ty88*)
(*type ty89*)
(*type ty90*)
(*type ty91*)
(*type ty92*)
(*type ty93*)
(*type ty94*)
(*type ty95*)
(*type ty96*)
(*type ty97*)
(*type ty98*)
(*type ty99*)
(*type ty100*)
(*type ty101*)
(*type ty102*)
(*type ty103*)
(*type ty104*)
(*type ty105*)
(*type ty106*)
(*type ty107*)
(*type ty108*)
(*type ty109*)
(*type ty110*)
(*type ty111*)
(*type ty112*)
(*type ty113*)
(*type ty114*)
(*type ty115*)
(*type ty116*)
(*type ty117*)
(*type ty118*)
(*type ty119*)
(*type ty120*)
(*type ty121*)
(*type ty122*)
(*type ty123*)
(*type ty124*)
(*type ty125*)
(*type ty126*)
(*type ty127*)
(*type ty128*)
(*type ty129*)
(*type ty130*)
(*type ty131*)
(*type ty132*)
(*type ty133*)
(*type ty134*)
(*type ty135*)
(*type ty136*)
(*type ty137*)
(*type ty138*)
(*type ty139*)
(*type ty140*)
(*type ty141*)
(*type ty142*)
(*type ty143*)
(*type ty144*)
(*type ty145*)
(*type ty146*)
(*type ty147*)
(*type ty148*)
(*type ty149*)
(*type ty150*)
(*type ty151*)
(*type ty152*)
(*type ty153*)
(*type ty154*)
(*type ty155*)
(*type ty156*)
(*type ty157*)
(*type ty158*)
(*type ty159*)
(*type ty160*)
(*type ty161*)
(*type ty162*)
(*type ty163*)
(*type ty164*)
(*type ty165*)
(*type ty166*)
(*type ty167*)
(*type ty168*)
(*type ty169*)
(*type ty170*)
(*type ty171*)
(*type ty172*)
(*type ty173*)
(*type ty174*)
(*type ty175*)
(*type ty176*)
(*type ty177*)
(*type ty178*)
(*type ty179*)
(*type ty180*)
(*type ty181*)
(*type ty182*)
(*type ty183*)
(*type ty184*)
(*type ty185*)
(*type ty186*)
(*type ty187*)
(*type ty188*)
(*type ty189*)
(*type ty190*)
(*type ty191*)
(*type ty192*)
(*type ty193*)
(*type ty194*)
(*type ty195*)
(*type ty196*)
(*type ty197*)
(*type ty198*)
(*type ty199*)
(*type ty200*)
(*type ty201*)
(*type ty202*)
(*type ty203*)
(*type ty204*)
(*type ty205*)
(*type ty206*)
(*type ty207*)
(*type ty208*)
(*type ty209*)
(*type ty210*)
(*type ty211*)
(*type ty212*)
(*type ty213*)
(*type ty214*)
(*type ty215*)
(*type ty216*)
(*type ty217*)
(*type ty218*)
(*type ty219*)
(*type ty220*)
(*type ty221*)
(*type ty222*)
(*type ty223*)
(*type ty224*)
(*type ty225*)
(*type ty226*)
(*type ty227*)
(*type ty228*)
(*type ty229*)
(*type ty230*)
(*type ty231*)
(*type ty232*)
(*type ty233*)
(*type ty234*)
(*type ty235*)
(*type ty236*)
(*type ty237*)
(*type ty238*)
(*type ty239*)
(*type ty240*)
(*type ty241*)
(*type ty242*)
(*type ty243*)
(*type ty244*)
(*type ty245*)
(*type ty246*)
(*type ty247*)
(*type ty248*)
(*type ty249*)
(*type ty250*)
(*type ty251*)
(*type ty252*)
(*type ty253*)
(*type ty254*)
(*type ty255*)
(*type ty256*)
(*type ty257*)

(*val word_length : forall 'a. mword 'a -> nat*)

(******************************************************************)
(* Conversions                                                    *)
(******************************************************************)

(*val signedIntegerFromWord : forall 'a. mword 'a -> integer*)

(*val unsignedIntegerFromWord : forall 'a. mword 'a -> integer*)

(* Version without typeclass constraint so that we can derive operations
   in Lem for one of the theorem provers without requiring it. *)
(*val proverWordFromInteger : forall 'a. integer -> mword 'a*)

(*val wordFromInteger : forall 'a. Size 'a => integer -> mword 'a*)
(* The OCaml version is defined after the arithmetic operations, below. *)

(*val naturalFromWord : forall 'a. mword 'a -> natural*)

(*val wordFromNatural : forall 'a. Size 'a => natural -> mword 'a*)

(*val wordToHex : forall 'a. mword 'a -> string*)

val _ = Define `
((instance_Show_Show_Machine_word_mword_dict:('a words$word)Show_class)= (<|

  show_method := words$word_to_hex_string|>))`;


(*val wordFromBitlist : forall 'a. Size 'a => list bool -> mword 'a*)

(*val bitlistFromWord : forall 'a. mword 'a -> list bool*)


(*val size_test_fn : forall 'a. Size 'a => mword 'a -> nat*)
val _ = Define `
 ((size_test_fn:'a words$word -> num) _=  (dimindex (the_value : 'a itself)))`;


(******************************************************************)
(* Comparisons                                                    *)
(******************************************************************)

(*val mwordEq : forall 'a. mword 'a -> mword 'a -> bool*)

(*val signedLess : forall 'a. mword 'a -> mword 'a -> bool*)

(*val signedLessEq : forall 'a. mword 'a -> mword 'a -> bool*)

(*val unsignedLess : forall 'a. mword 'a -> mword 'a -> bool*)

(*val unsignedLessEq : forall 'a. mword 'a -> mword 'a -> bool*)

(* Comparison tests are below, after the definition of wordFromInteger *)

(******************************************************************)
(* Appending, splitting and probing words                         *)
(******************************************************************)

(*val word_concat : forall 'a 'b 'c. mword 'a -> mword 'b -> mword 'c*)

(* Note that we assume the result type has the correct size, especially
   for Isabelle. *)
(*val word_extract : forall 'a 'b. nat -> nat -> mword 'a -> mword 'b*)

(*  Needs to be in the prover because we'd end up with unknown sizes in the
   types in Lem.
*)
(*val word_update : forall 'a 'b. mword 'a -> nat -> nat -> mword 'b -> mword 'a*)

(*val setBit : forall 'a. mword 'a -> nat -> bool -> mword 'a*)

(*val getBit : forall 'a. mword 'a -> nat -> bool*)

(*val msb : forall 'a. mword 'a -> bool*)

(*val lsb : forall 'a. mword 'a -> bool*)

(******************************************************************)
(* Bitwise operations, shifts, etc.                               *)
(******************************************************************)

(*val shiftLeft  : forall 'a. mword 'a -> nat -> mword 'a*)

(*val shiftRight : forall 'a. mword 'a -> nat -> mword 'a*)

(*val arithShiftRight : forall 'a. mword 'a -> nat -> mword 'a*)

(*val lAnd       : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val lOr        : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val lXor       : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val lNot       : forall 'a. mword 'a -> mword 'a*)

(*val rotateRight : forall 'a. nat -> mword 'a -> mword 'a*)

(*val rotateLeft : forall 'a. nat -> mword 'a -> mword 'a*)

(*val zeroExtend : forall 'a 'b. Size 'b => mword 'a -> mword 'b*)

(*val signExtend : forall 'a 'b. Size 'b => mword 'a -> mword 'b*)

(* Sign extension tests are below, after the definition of wordFromInteger *)

(*****************************************************************)
(* Arithmetic                                                    *)
(*****************************************************************)

(*val plus   : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val minus  : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val uminus : forall 'a. mword 'a -> mword 'a*)

(*val times : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val unsignedDivide : forall 'a. mword 'a -> mword 'a -> mword 'a*)
(*val signedDivide : forall 'a. mword 'a -> mword 'a -> mword 'a*)

(*val modulo : forall 'a. mword 'a -> mword 'a -> mword 'a*)
val _ = export_theory()