Package arm-decomp: ARM decompilation support

Information

name	arm-decomp
version	1.0
description	ARM decompilation support
author	HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
license	MIT
checksum	1de1f2458fef14b888a26aae5b5183d900f80551
requires	base arm-model arm-prog
show	Data.Bool Data.Pair HOL4

Files

Package tarball arm-decomp-1.0.tgz
Theory source file arm-decomp.thy (included in the package tarball)

Defined Constant

HOL4
- arm_decomp
  - arm_decomp.arm_OK

Theorem

⊦ ∀mode.
arm_decomp.arm_OK mode =
arm_prog.arm_CONFIG (arm.VFPv3, arm.ARMv7_A, ⊥, ⊥, mode)

External Type Operators

→
bool
Data
- Pair
  - ×
- Unit
  - Data.Unit.unit
HOL4
- arm
  - arm.Architecture
  - arm.VFPExtension
- arm_prog
  - arm_prog.arm_component
  - arm_prog.arm_data
- fcp
  - fcp.bit0
  - fcp.bit1
  - fcp.cart

External Constants

=
Data
- Bool
  - ∀
  - ⊥
  - ⊤
- Pair
  - ,
HOL4
- arm
  - arm.ARMv7_A
  - arm.VFPv3
- arm_prog
  - arm_prog.arm_CONFIG

Assumptions

⊦ ⊤

⊦ (∀) = λP. P = λx. ⊤