1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MicroJava/J/State.ML	Thu Nov 11 12:23:45 1999 +0100
     1.3 @@ -0,0 +1,77 @@
     1.4 +(*  Title:      HOL/MicroJava/J/State.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1999 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +val the_Addr_Addr = prove_goalw thy [the_Addr_def] 
    1.11 +	"the_Addr (Addr a) = a" (K [Auto_tac]);
    1.12 +
    1.13 +Addsimps [the_Addr_Addr];
    1.14 +
    1.15 +val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C" 
    1.16 +	(K [Simp_tac 1]);
    1.17 +
    1.18 +Addsimps [obj_ty_def2];
    1.19 +
    1.20 +val new_AddrD = prove_goalw thy [new_Addr_def] 
    1.21 +"\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
    1.22 +	asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
    1.23 +	rtac selectI 1,
    1.24 +	rtac disjI2 1,
    1.25 +	res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
    1.26 +	 Auto_tac ]);
    1.27 +
    1.28 +val raise_if_True = prove_goalw thy [raise_if_def] 
    1.29 +	"raise_if True x y \\<noteq> None"
    1.30 +(K [split_tac [expand_if] 1,Auto_tac]);
    1.31 +
    1.32 +val raise_if_False = prove_goalw thy [raise_if_def] 
    1.33 +	"raise_if False x y = y"
    1.34 +(K [Auto_tac]);
    1.35 +
    1.36 +val raise_if_Some = prove_goalw thy [raise_if_def] 
    1.37 +	"raise_if c x (Some y) \\<noteq> None" (K [Auto_tac]);
    1.38 +
    1.39 +val raise_if_Some2 = prove_goalw thy [raise_if_def] 
    1.40 +"raise_if c z (if x = None then Some y else x) \\<noteq> None" (K[
    1.41 +	induct_tac "x" 1,
    1.42 +	Auto_tac]);
    1.43 +val if_None_eq = prove_goal thy 
    1.44 +"(if x = None then None else x) = x" (K[
    1.45 +	induct_tac "x" 1,
    1.46 +	Auto_tac]);
    1.47 +
    1.48 +Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
    1.49 +
    1.50 +val raise_if_SomeD = prove_goalw thy [raise_if_def] 
    1.51 +	"raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z" 
    1.52 +(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
    1.53 +
    1.54 +val raise_if_NoneD = prove_goalw thy [raise_if_def] 
    1.55 +	"raise_if c x y = None \\<longrightarrow> \\<not> c \\<and>  y = None"
    1.56 +(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
    1.57 +
    1.58 +
    1.59 +val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
    1.60 +	"np a' x' = None \\<longrightarrow> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
    1.61 +	split_tac [expand_if] 1,
    1.62 +	Auto_tac ])) RS mp;
    1.63 +val np_None = (prove_goalw thy [np_def, raise_if_def] 
    1.64 +	"a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
    1.65 +	split_tac [expand_if] 1,
    1.66 +	Auto_tac ])) RS mp;
    1.67 +val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
    1.68 +	(fn _ => [Auto_tac ]);
    1.69 +val np_Null = prove_goalw thy [np_def, raise_if_def] 
    1.70 +	"np Null None = Some NullPointer" (fn _ => [
    1.71 +	Auto_tac ]);
    1.72 +val np_Addr = prove_goalw thy [np_def, raise_if_def] "np (Addr a) None = None" 
    1.73 +	(fn _ => [Auto_tac ]);
    1.74 +Addsimps[np_None, np_Some,np_Null,np_Addr];
    1.75 +
    1.76 +
    1.77 +
    1.78 +
    1.79 +
    1.80 +