src/HOL/MicroJava/J/Value.thy

Prototype introiff option for find_theorems.

This feature was suggested by Jeremy Avigad / Tobias Nipkow.

It adds an introiff keyword for find_theorems that returns, in
addition to the usual results for intro, any theorems of the
form ([| ... |] ==> (P = Q)) where either P or Q matches the
conclusions of the current goal. Such theorems can be made
introduction rules with [THEN iffDx].

The current patch is for evaluation only. It assumes an
(op = : 'a -> 'a -> bool) operator, which is specific to HOL.
It is not clear how this should be generalised.

(*  Title:      HOL/MicroJava/J/Value.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Java Values} *}

theory Value imports Type begin

typedecl loc' -- "locations, i.e. abstract references on objects" 

datatype loc 
  = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
  | Loc loc'     -- "usual locations (references on objects)"

datatype val
  = Unit        -- "dummy result value of void methods"
  | Null        -- "null reference"
  | Bool bool   -- "Boolean value"
  | Intg int    -- "integer value, name Intg instead of Int because
                   of clash with HOL/Set.thy" 
  | Addr loc    -- "addresses, i.e. locations of objects "

consts
  the_Bool :: "val => bool"
  the_Intg :: "val => int"
  the_Addr :: "val => loc"

primrec
  "the_Bool (Bool b) = b"

primrec
  "the_Intg (Intg i) = i"

primrec
  "the_Addr (Addr a) = a"

consts
  defpval :: "prim_ty => val"  -- "default value for primitive types"
  default_val :: "ty => val"   -- "default value for all types"

primrec
  "defpval Void    = Unit"
  "defpval Boolean = Bool False"
  "defpval Integer = Intg 0"

primrec
  "default_val (PrimT pt) = defpval pt"
  "default_val (RefT  r ) = Null"

end