File Type.ML

open Type;

qed_goal "ty_exhaust" thy "(\<exists>pt. T = PrimT pt) \<or> (\<exists>rt. T = RefT rt)" (K[
	res_inst_tac [("P1.1","\<lambda>x. True")] (ref_ty_ty.induct RS conjunct2) 1, 
	ALLGOALS Fast_tac]);
qed_goal "tyE" thy 
	"\<lbrakk>\<And>pt. T = PrimT pt \<Longrightarrow> P;  \<And>rt. T = RefT rt \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" (fn prems =>[
	cut_facts_tac [ty_exhaust] 1,
	Safe_tac,
	REPEAT(eresolve_tac prems 1)]);
fun tyE_tac s = res_inst_tac [("T",s)] tyE THEN_ALL_NEW hyp_subst_tac;

qed_goal "non_PrimT" thy "(\<forall>pt. T \<noteq> PrimT pt) = (\<exists>t. T = RefT t)" (K [
	tyE_tac "T" 1, Auto_tac]);


qed_goalw "the_Class_eq" thy [the_Class_def] 
"the_Class (Class C)= C" (K [Auto_tac]);
Addsimps [the_Class_eq];