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