src/HOL/Datatype_Benchmark/Instructions.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45860 93eda35a8377
child 58305 57752a91eec4
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Datatype_Benchmark/Instructions.thy
     2 
     3 Example from Konrad: 68000 instruction set.
     4 *)
     5 
     6 theory Instructions imports Main begin
     7 
     8 datatype Size = Byte | Word | Long
     9 
    10 datatype DataRegister
    11               = RegD0
    12               | RegD1
    13               | RegD2
    14               | RegD3
    15               | RegD4
    16               | RegD5
    17               | RegD6
    18               | RegD7
    19 
    20 datatype AddressRegister
    21               = RegA0
    22               | RegA1
    23               | RegA2
    24               | RegA3
    25               | RegA4
    26               | RegA5
    27               | RegA6
    28               | RegA7
    29 
    30 datatype DataOrAddressRegister
    31               = data DataRegister
    32               | address AddressRegister
    33 
    34 datatype Condition
    35               = Hi
    36               | Ls
    37               | Cc
    38               | Cs
    39               | Ne
    40               | Eq
    41               | Vc
    42               | Vs
    43               | Pl
    44               | Mi
    45               | Ge
    46               | Lt
    47               | Gt
    48               | Le
    49 
    50 datatype AddressingMode
    51         = immediate nat
    52         | direct DataOrAddressRegister
    53         | indirect AddressRegister
    54         | postinc AddressRegister
    55         | predec AddressRegister
    56         | indirectdisp nat AddressRegister
    57         | indirectindex nat AddressRegister DataOrAddressRegister Size
    58         | absolute nat
    59         | pcdisp nat
    60         | pcindex nat DataOrAddressRegister Size
    61 
    62 datatype M68kInstruction
    63     = ABCD AddressingMode AddressingMode
    64     | ADD Size AddressingMode AddressingMode
    65     | ADDA Size AddressingMode AddressRegister
    66     | ADDI Size nat AddressingMode
    67     | ADDQ Size nat AddressingMode
    68     | ADDX Size AddressingMode AddressingMode
    69     | AND Size AddressingMode AddressingMode
    70     | ANDI Size nat AddressingMode
    71     | ANDItoCCR nat
    72     | ANDItoSR nat
    73     | ASL Size AddressingMode DataRegister
    74     | ASLW AddressingMode
    75     | ASR Size AddressingMode DataRegister
    76     | ASRW AddressingMode
    77     | Bcc Condition Size nat
    78     | BTST Size AddressingMode AddressingMode
    79     | BCHG Size AddressingMode AddressingMode
    80     | BCLR Size AddressingMode AddressingMode
    81     | BSET Size AddressingMode AddressingMode
    82     | BRA Size nat
    83     | BSR Size nat
    84     | CHK AddressingMode DataRegister
    85     | CLR Size AddressingMode
    86     | CMP Size AddressingMode DataRegister
    87     | CMPA Size AddressingMode AddressRegister
    88     | CMPI Size nat AddressingMode
    89     | CMPM Size AddressRegister AddressRegister
    90     | DBT DataRegister nat
    91     | DBF DataRegister nat
    92     | DBcc Condition DataRegister nat
    93     | DIVS AddressingMode DataRegister
    94     | DIVU AddressingMode DataRegister
    95     | EOR Size DataRegister AddressingMode
    96     | EORI Size nat AddressingMode
    97     | EORItoCCR nat
    98     | EORItoSR nat
    99     | EXG DataOrAddressRegister DataOrAddressRegister
   100     | EXT Size DataRegister
   101     | ILLEGAL
   102     | JMP AddressingMode
   103     | JSR AddressingMode
   104     | LEA AddressingMode AddressRegister
   105     | LINK AddressRegister nat
   106     | LSL Size AddressingMode DataRegister
   107     | LSLW AddressingMode
   108     | LSR Size AddressingMode DataRegister
   109     | LSRW AddressingMode
   110     | MOVE Size AddressingMode AddressingMode
   111     | MOVEtoCCR AddressingMode
   112     | MOVEtoSR AddressingMode
   113     | MOVEfromSR AddressingMode
   114     | MOVEtoUSP AddressingMode
   115     | MOVEfromUSP AddressingMode
   116     | MOVEA Size AddressingMode AddressRegister
   117     | MOVEMto Size AddressingMode "DataOrAddressRegister list"
   118     | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
   119     | MOVEP Size AddressingMode AddressingMode
   120     | MOVEQ nat DataRegister
   121     | MULS AddressingMode DataRegister
   122     | MULU AddressingMode DataRegister
   123     | NBCD AddressingMode
   124     | NEG Size AddressingMode
   125     | NEGX Size AddressingMode
   126     | NOP
   127     | NOT Size AddressingMode
   128     | OR Size AddressingMode AddressingMode
   129     | ORI Size nat AddressingMode
   130     | ORItoCCR nat
   131     | ORItoSR nat
   132     | PEA AddressingMode
   133     | RESET
   134     | ROL Size AddressingMode DataRegister
   135     | ROLW AddressingMode
   136     | ROR Size AddressingMode DataRegister
   137     | RORW AddressingMode
   138     | ROXL Size AddressingMode DataRegister
   139     | ROXLW AddressingMode
   140     | ROXR Size AddressingMode DataRegister
   141     | ROXRW AddressingMode
   142     | RTE
   143     | RTR
   144     | RTS
   145     | SBCD AddressingMode AddressingMode
   146     | ST AddressingMode
   147     | SF AddressingMode
   148     | Scc Condition AddressingMode
   149     | STOP nat
   150     | SUB Size AddressingMode AddressingMode
   151     | SUBA Size AddressingMode AddressingMode
   152     | SUBI Size nat AddressingMode
   153     | SUBQ Size nat AddressingMode
   154     | SUBX Size AddressingMode AddressingMode
   155     | SWAP DataRegister
   156     | TAS AddressingMode
   157     | TRAP nat
   158     | TRAPV
   159     | TST Size AddressingMode
   160     | UNLK AddressRegister
   161 
   162 end