Runtime.ML

goal thy
"get_Addr (Addr a) = a";
by (asm_simp_tac (simpset() addsimps [select_equality,get_Addr_def]) 1);
qed "get_Addr_Addr";

goal thy
"get_Intg (Intg a) = a";
by (asm_simp_tac (simpset() addsimps [select_equality,get_Intg_def]) 1);
qed "get_Intg_Intg";

goal thy
"get_Obj (Obj cn od) = (cn,od)";
by (asm_simp_tac (simpset() addsimps [select_equality,get_Obj_def]) 1);
qed "get_Obj_Obj";

goal thy
"get_Arr (Arr fd ad) = (fd,ad)";
by (asm_simp_tac (simpset() addsimps [select_equality,get_Arr_def]) 1);
qed "get_Arr_Arr";


goal thy
"default_val fd = Intg i --> fd = I";
by (induct_tac "fd" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed_spec_mp "default_val_Intg";

goal thy
"default_val fd = Addr a --> False ";
by (induct_tac "fd" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed_spec_mp "default_val_Addr";

goal thy
"default_val fd = Null --> (? cn. fd = L cn) |  (? fd'. fd = A fd')";
by (induct_tac "fd" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed_spec_mp "default_val_Null";

goal thy
"compatible CFS fd I --> fd=I";
by (induct_tac "fd" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed_spec_mp "compatible_I";