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/Decl.thy
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{Class Declarations and Programs} *}
theory Decl imports Type begin
types
fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)"
sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2"
'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class"
'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list"
-- "class = superclass, fields, methods"
'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1"
'c prog = "'c cdecl list" -- "program"
translations
"fdecl" <= (type) "vname \<times> ty"
"sig" <= (type) "mname \<times> ty list"
"mdecl c" <= (type) "sig \<times> ty \<times> c"
"class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
"cdecl c" <= (type) "cname \<times> (c class)"
"prog c" <= (type) "(c cdecl) list"
constdefs
"class" :: "'c prog => (cname \<rightharpoonup> 'c class)"
"class \<equiv> map_of"
is_class :: "'c prog => cname => bool"
"is_class G C \<equiv> class G C \<noteq> None"
lemma finite_is_class: "finite {C. is_class G C}"
apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done
consts
is_type :: "'c prog => ty => bool"
primrec
"is_type G (PrimT pt) = True"
"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
end