--- a/src/HOL/MicroJava/J/Type.thy Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Fri Aug 05 16:55:14 2011 +0200
@@ -12,6 +12,20 @@
definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
instance proof qed(simp add: equal_cnam_def)
end
+text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
+instantiation cnam :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []"
+instance proof qed
+end
+instantiation cnam :: term_of begin
+definition "term_of_class.term_of (C :: cnam) \<equiv>
+ Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])"
+instance proof qed
+end
+instantiation cnam :: partial_term_of begin
+definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined"
+instance proof qed
+end
-- "exceptions"
datatype
@@ -31,12 +45,38 @@
definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
instance proof qed(simp add: equal_vnam_def)
end
+instantiation vnam :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []"
+instance proof qed
+end
+instantiation vnam :: term_of begin
+definition "term_of_class.term_of (V :: vnam) \<equiv>
+ Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])"
+instance proof qed
+end
+instantiation vnam :: partial_term_of begin
+definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined"
+instance proof qed
+end
typedecl mname -- "method name"
instantiation mname :: equal begin
definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
instance proof qed(simp add: equal_mname_def)
end
+instantiation mname :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []"
+instance proof qed
+end
+instantiation mname :: term_of begin
+definition "term_of_class.term_of (M :: mname) \<equiv>
+ Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])"
+instance proof qed
+end
+instantiation mname :: partial_term_of begin
+definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined"
+instance proof qed
+end
-- "names for @{text This} pointer and local/field variables"
datatype vname