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