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