--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BCV/JType.ML Fri Sep 01 18:29:52 2000 +0200
@@ -0,0 +1,166 @@
+(* Title: HOL/BCV/JType.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+*)
+
+Goalw [lesub_def,subtype_def] "T [=_S T";
+by(Simp_tac 1);
+qed "subtype_refl";
+AddIffs [subtype_refl];
+
+Goalw [lesub_def,subtype_def,is_Class_def]
+ "(T [=_S Integer) = (T = Integer)";
+by(Simp_tac 1);
+qed "subtype_Int_conv";
+
+Goalw [lesub_def,subtype_def] "(Integer [=_S T) = (T = Integer)";
+by(Blast_tac 1);
+qed "Int_subtype_conv";
+
+Goalw [lesub_def,subtype_def,is_Class_def]
+ "(T [=_S Void) = (T = Void)";
+by(Simp_tac 1);
+qed "subtype_Void_conv";
+
+Goalw [lesub_def,subtype_def] "(Void [=_S T) = (T = Void)";
+by(Blast_tac 1);
+qed "Void_subtype_conv";
+
+AddIffs [subtype_Int_conv,Int_subtype_conv,
+ subtype_Void_conv,Void_subtype_conv];
+
+Goalw [lesub_def,subtype_def,is_Class_def]
+ "T [=_S NullT = (T=NullT)";
+by(Simp_tac 1);
+qed "subtype_NullT_conv";
+
+Goalw [lesub_def,subtype_def,is_Class_def]
+ "NullT [=_S T = (T=NullT | (? C. T = Class C))";
+by(simp_tac (simpset() addsplits [ty.split]) 1);
+qed "NullT_subtype_conv";
+
+AddIffs [NullT_subtype_conv,subtype_NullT_conv];
+
+Goalw [lesub_def,subtype_def,is_Class_def]
+ "T [=_S Class C = (T=NullT | (? D. T = Class D & (D,C) : S^*))";
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed "subtype_Class_conv";
+
+Goalw [lesub_def,subtype_def,refl_def]
+ "Class D [=_S T = (? C. T = Class C & (D,C):S^*)";
+by(Blast_tac 1);
+qed "Class_subtype_conv";
+
+AddIffs [Class_subtype_conv,subtype_Class_conv];
+
+Goalw [lesub_def,subtype_def,is_Class_def]
+ "[| A [=_S B; B [=_S C |] ==> A [=_S C";
+by(asm_full_simp_tac (simpset() addsplits [ty.split,ty.split_asm]) 1);
+by(blast_tac (claset() addDs [transD] addIs [rtrancl_trans]) 1);
+qed "subtype_transD";
+
+Goalw [order_def,subtype_def,lesub_def,is_Class_def]
+ "acyclic S ==> order (subtype S)";
+bd acyclic_impl_antisym_rtrancl 1;
+by(auto_tac (claset() addIs [rtrancl_trans],simpset() addsimps [antisymD]) );
+qed "acyclic_impl_order_subtype";
+
+Goalw [acc_def,lesssub_def]
+ "wf(S^-1) ==> acc(subtype S)";
+by(dres_inst_tac [("p","S^-1 - Id")] wf_subset 1);
+ by(Blast_tac 1);
+bd wf_trancl 1;
+by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by(rename_tac "M T" 1);
+by(case_tac "EX C. Class C : M" 1);
+ by(case_tac "T" 2);
+ by(Blast_tac 2);
+ by(Blast_tac 2);
+ by(res_inst_tac [("x","T")] bexI 2);
+ by(Blast_tac 2);
+ ba 2;
+ by(Blast_tac 2);
+by(eres_inst_tac [("x","{C. Class C : M}")] allE 1);
+by(Auto_tac);
+by(rename_tac "D" 1);
+by(res_inst_tac [("x","Class D")] bexI 1);
+ by(atac 2);
+by (Clarify_tac 1);
+by(cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1);
+by(Asm_full_simp_tac 1);
+be rtranclE 1;
+ by(Blast_tac 1);
+bd (converseI RS rtrancl_converseI) 1;
+by(subgoal_tac "(S-Id)^-1 = (S^-1 - Id)" 1);
+ by(Blast_tac 2);
+by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addIs [rtrancl_into_trancl2]) 1);
+qed "wf_converse_subcls1_impl_acc_subtype";
+
+Addsimps [is_type_def];
+
+Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def]
+ "[| univalent S; acyclic S |] ==> \
+\ closed (err(types S)) (lift2 (JType.sup S))";
+by(simp_tac (simpset() addsplits [err.split,ty.split]) 1);
+by(blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
+ addSIs [is_ubI]) 1);
+qed "closed_err_types";
+
+AddIffs [OK_le_conv];
+
+Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def]
+ "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)";
+by(asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1);
+
+br conjI 1;
+ by(Clarify_tac 1);
+ by(case_tac "x" 1);
+ by(Clarify_tac 1);
+ by(Simp_tac 1);
+ by(case_tac "y" 1);
+ by(Clarify_tac 1);
+ by(Simp_tac 1);
+ by(fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss
+ (simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
+ addsplits [ty.split])) 1);
+
+br conjI 1;
+ by(Clarify_tac 1);
+ by(case_tac "x" 1);
+ by(Clarify_tac 1);
+ by(Simp_tac 1);
+ by(case_tac "y" 1);
+ by(Clarify_tac 1);
+ by(Simp_tac 1);
+ by(fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss
+ (simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
+ addsplits [ty.split])) 1);
+
+by(Clarify_tac 1);
+by(case_tac "x" 1);
+ by(Clarify_tac 1);
+by(case_tac "y" 1);
+ by(Clarify_tac 1);
+by(asm_simp_tac(simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
+ addsplits [ty.split]) 1);
+br conjI 1;
+ by(Blast_tac 1);
+br conjI 1;
+ by(Blast_tac 1);
+br conjI 1;
+ by(Blast_tac 1);
+by(Clarify_tac 1);
+br conjI 1;
+ by(Clarify_tac 1);
+br conjI 1;
+ by(Clarify_tac 1);
+by(Asm_full_simp_tac 1);
+by(blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
+ addSIs [is_ubI]) 1);
+qed "err_semilat_JType_esl";
+
+DelIffs [OK_le_conv];