isabelle: src/HOL/MicroJava/J/State.ML@114999ff8d19 (annotated)

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/J/State.ML
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2	ID: $Id$
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Author: David von Oheimb
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4	Copyright 1999 Technische Universitaet Muenchen
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5	*)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	7	Goalw [obj_ty_def] "obj_ty (C,fs) = Class C";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	8	by (Simp_tac 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	9	qed "obj_ty_def2";
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	10	Addsimps [obj_ty_def2];
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	11
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	12	Goalw [new_Addr_def]
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	13	"(a,x) = new_Addr h ==> h a = None \\<and> x = None \| x = Some OutOfMemory";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	14	by(asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	15	by(rtac someI 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	16	by(rtac disjI2 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	17	by(res_inst_tac [("r","snd (?a,Some OutOfMemory)")] trans 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	18	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	19	qed "new_AddrD";
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	20
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	21
10613 78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	22	Goalw [raise_if_def] "raise_if True x y \\<noteq> None";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	23	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	24	qed "raise_if_True";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	25
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	26	Goalw [raise_if_def] "raise_if False x y = y";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	27	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	28	qed "raise_if_False";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	29
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	30	Goalw [raise_if_def] "raise_if c x (Some y) \\<noteq> None";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	31	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	32	qed "raise_if_Some";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	33
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	34	Goalw [raise_if_def] "raise_if c z (if x = None then Some y else x) \\<noteq> None";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	35	by(induct_tac "x" 1);
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	36	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	37	qed "raise_if_Some2";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	38
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	39	Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2];
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	40
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	41	Goalw [raise_if_def]
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	42	"raise_if c x y = Some z \\<longrightarrow> c \\<and> Some z = Some x \| y = Some z";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	43	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	44	qed_spec_mp "raise_if_SomeD";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	45
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	46	Goalw [raise_if_def] "raise_if c x y = None --> \\<not> c \\<and> y = None";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	47	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	48	qed_spec_mp "raise_if_NoneD";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	49
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	50	Goalw [np_def, raise_if_def] "np a' x' = None --> x' = None \\<and> a' \\<noteq> Null";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	51	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	52	qed_spec_mp "np_NoneD";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	53
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	54	Goalw [np_def, raise_if_def] "a' \\<noteq> Null --> np a' x' = x'";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	55	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	56	qed_spec_mp "np_None";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	57
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	58	Goalw [np_def, raise_if_def] "np a' (Some xc) = Some xc";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	59	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	60	qed "np_Some";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	61
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	62	Goalw [np_def, raise_if_def] "np Null None = Some NullPointer";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	63	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	64	qed "np_Null";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	65
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	66	Goalw [np_def, raise_if_def] "np (Addr a) None = None";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	67	by Auto_tac;
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	68	qed "np_Addr";
78b1d6c3ee9c improved superclass entry for classes and definition status of is_class, class oheimb parents: 10042 diff changeset	69
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	70	Addsimps[np_None, np_Some,np_Null,np_Addr];
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	71
9348 f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: 8875 diff changeset	72	Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: 8875 diff changeset	73	\ Some (if c then xc else NullPointer)";
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: 8875 diff changeset	74	by (Simp_tac 1);
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: 8875 diff changeset	75	qed "np_raise_if";
f495dba0cb07 corrections (cast relation, Prog.ML -> Decl.ML) oheimb parents: 8875 diff changeset	76	Addsimps[np_raise_if];
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	77
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	78
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	79
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	80
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	81

author	kleing
	Tue, 12 Dec 2000 14:08:26 +0100
changeset 10650	114999ff8d19
parent 10613	78b1d6c3ee9c
permissions	-rw-r--r--