src/HOL/BCV/JType.ML

     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
 
 Goalw [lesub_def,subtype_def] "T [=_S T";
-by(Simp_tac 1);
+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);
+by (Simp_tac 1);
 qed "subtype_Int_conv";
 
 Goalw [lesub_def,subtype_def] "(Integer [=_S T) = (T = Integer)";
-by(Blast_tac 1);
+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);
+by (Simp_tac 1);
 qed "subtype_Void_conv";
 
 Goalw [lesub_def,subtype_def] "(Void [=_S T) = (T = Void)";
-by(Blast_tac 1);
+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);
+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);
+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);
+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);
+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);
+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]) );
+by (dtac 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 (dres_inst_tac [("p","S^-1 - Id")] wf_subset 1);
+ by (Blast_tac 1);
+by (dtac 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 (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);
+  by (assume_tac 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);
+by (cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1);
+by (Asm_full_simp_tac 1);
+by (etac rtranclE 1);
+ by (Blast_tac 1);
+by (dtac 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]
+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);
+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
+by (rtac 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
+by (rtac 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]
+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]
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+by (rtac 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];