src/HOL/BCV/Listn.ML

--- a/src/HOL/BCV/Listn.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Listn.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -21,7 +21,7 @@
 AddIffs [Nil_le_conv,Cons_notle_Nil];
 
 Goalw [lesub_def,Listn.le_def] "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "Cons_le_Cons";
 AddIffs [Cons_le_Cons];
 
@@ -34,7 +34,7 @@
 
 Goalw [unfold_lesub_list]
  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
-by(rewtac Listn.le_def);
+by (rewtac Listn.le_def);
 by (asm_full_simp_tac (simpset() addsimps [list_all2_conv_all_nth,nth_list_update]) 1);
 qed "list_update_le_cong";
 
@@ -59,7 +59,7 @@
 Goalw [unfold_lesub_list]
  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys";
 by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
-br nth_equalityI 1;
+by (rtac nth_equalityI 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
@@ -67,8 +67,8 @@
 qed "le_list_antisym";
 
 Goal "order r ==> order(Listn.le r)";
-by(stac order_def 1);
-by(blast_tac (claset() addIs [le_list_refl,le_list_trans,le_list_antisym]
+by (stac order_def 1);
+by (blast_tac (claset() addIs [le_list_refl,le_list_trans,le_list_antisym]
                        addDs [order_refl]) 1);
 qed "order_listI";
 Addsimps [order_listI];
@@ -81,11 +81,11 @@
 Addsimps [lesub_list_impl_same_size];
 
 Goalw [lesssub_def] "xs <_(Listn.le r) ys ==> size ys = size xs";
-by(Auto_tac);
+by (Auto_tac);
 qed "lesssub_list_impl_same_size";
 
 Goalw [list_def] "[| length xs = n; set xs <= A |] ==> xs : list n A";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "listI";
 
 Goalw [list_def] "xs : list n A ==> length xs = n";
@@ -94,7 +94,7 @@
 Addsimps [listE_length];
 
 Goal "[| xs : list n A; p < n |] ==> p < length xs";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "less_lengthI";
 
 Goalw [list_def] "xs : list n A ==> set xs <= A";
@@ -159,7 +159,7 @@
 Goal "!ys. length(xs +[f] ys) = min(length xs) (length ys)";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsplits [list.split]) 1);
 qed_spec_mp "length_plus_list";
 Addsimps [length_plus_list];
@@ -208,23 +208,23 @@
 qed_spec_mp "list_update_incr";
 
 Goalw [acc_def] "[| order r; acc r |] ==> acc(Listn.le r)";
-by(subgoal_tac
+by (subgoal_tac
  "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})" 1);
- be wf_subset 1;
- by(blast_tac (claset() addIs [lesssub_list_impl_same_size]) 1);
-br wf_UN 1;
+ by (etac wf_subset 1);
+ by (blast_tac (claset() addIs [lesssub_list_impl_same_size]) 1);
+by (rtac wf_UN 1);
  by (Clarify_tac 2);
- by(rename_tac "m n" 2);
- by(case_tac "m=n" 2);
-  by(Asm_full_simp_tac 2);
- br conjI 2;
-  by(fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
- by(fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
+ by (rename_tac "m n" 2);
+ by (case_tac "m=n" 2);
+  by (Asm_full_simp_tac 2);
+ by (rtac conjI 2);
+  by (fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
+ by (fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
 by (Clarify_tac 1);
-by(rename_tac "n" 1);
+by (rename_tac "n" 1);
 by (induct_tac "n" 1);
  by (simp_tac (simpset() addsimps [lesssub_def] addcongs [conj_cong]) 1);
-by(rename_tac "k" 1);
+by (rename_tac "k" 1);
 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
 by (simp_tac (simpset() addsimps [length_Suc_conv] addcongs [conj_cong]) 1);
 by (Clarify_tac 1);
@@ -240,53 +240,53 @@
 by (Clarify_tac 1);
 by (rename_tac "maxA xs" 1);
 by (eres_inst_tac [("x","{ys. size ys = size xs & maxA#ys : M}")] allE 1);
-be impE 1;
- by(Blast_tac 1);
+by (etac impE 1);
+ by (Blast_tac 1);
 by (Clarify_tac 1);
 by (thin_tac "m : M" 1);
 by (thin_tac "maxA#xs : M" 1);
 by (rtac bexI 1);
- ba 2;
+ by (assume_tac 2);
 by (Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
 qed "acc_le_listI";
 AddSIs [acc_le_listI];
 
 
 Goalw [closed_def]
  "closed S f ==> closed (list n S) (map2 f)";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
-by(Simp_tac 1);
+by (Clarify_tac 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "closed_listI";
 
 
 Goalw [Listn.sl_def]
  "!!L. semilat L ==> semilat (Listn.sl n L)";
-by(split_all_tac 1);
-by(simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1);
-br conjI 1;
- by(Asm_simp_tac 1);
-br conjI 1;
- by(asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1);
-by(simp_tac (HOL_basic_ss addsimps [list_def]) 1);
+by (split_all_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1);
+by (rtac conjI 1);
+ by (Asm_simp_tac 1);
+by (rtac conjI 1);
+ by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1);
+by (simp_tac (HOL_basic_ss addsimps [list_def]) 1);
 by (asm_simp_tac (simpset() addsimps [plus_list_ub1,plus_list_ub2,plus_list_lub]) 1);
 qed "semilat_Listn_sl";
 
 
 Goal "!xes. xes : list n (err A) --> coalesce xes : err(list n A)";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (simp_tac (simpset() addsimps [plussub_def,Err.sup_def,lift2_def] addsplits [err.split]) 1);
-by(Force_tac 1);
+by (Force_tac 1);
 qed_spec_mp "coalesce_in_err_list";
 
 
@@ -298,37 +298,37 @@
  "semilat(err A, Err.le r, lift2 f) ==> \
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \      (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
-by(force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1);
+by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1);
 qed_spec_mp "coalesce_eq_OK1_D";
 
 Goal
  "semilat(err A, Err.le r, lift2 f) ==> \
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \      (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
-by(force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1);
+by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1);
 qed_spec_mp "coalesce_eq_OK2_D";
 
 Goalw [semilat_Def,plussub_def,err_def]
  "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; \
 \    u:A; x <=_r u; y <=_r u |] ==> z <=_r u";
-by(asm_full_simp_tac (simpset() addsimps [lift2_def]) 1);
-by(Clarify_tac 1);
-by(rotate_tac ~3 1);
-by(etac thin_rl 1);
-by(etac thin_rl 1);
-by(Force_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [lift2_def]) 1);
+by (Clarify_tac 1);
+by (rotate_tac ~3 1);
+by (etac thin_rl 1);
+by (etac thin_rl 1);
+by (Force_tac 1);
 qed "lift2_le_ub";
 
 Goal
@@ -336,22 +336,22 @@
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \      (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us \
 \               & us : list n A --> zs <=[r] us))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Blast_tac 2);
-by(blast_tac (claset() addIs [lift2_le_ub]) 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 2);
+by (blast_tac (claset() addIs [lift2_le_ub]) 1);
 qed_spec_mp "coalesce_eq_OK_ub_D";
 
 Goal
  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] \
 \ ==> ~(? u:A. x <=_r u & y <=_r u)";
-by(asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1);
+by (asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1);
 qed "lift2_eq_ErrD";
 
 Goal
@@ -359,39 +359,39 @@
 \ |] ==> !xs. xs:list n A --> (!ys. ys:list n A --> \
 \  coalesce (xs +[f] ys) = Err --> \
 \ ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
- by(blast_tac (claset() addDs [lift2_eq_ErrD]) 1);
-by(Blast_tac 1);
+ by (blast_tac (claset() addDs [lift2_eq_ErrD]) 1);
+by (Blast_tac 1);
 qed_spec_mp "coalesce_eq_Err_D";
 
 
 Goalw [closed_def]
  "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)";
-by(simp_tac (simpset() addsimps [err_def]) 1);
+by (simp_tac (simpset() addsimps [err_def]) 1);
 qed "closed_err_lift2_conv";
 
 Goalw [map2_def]
  "closed (err A) (lift2 f) ==> \
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \     map2 f xs ys : list n (err A))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsimps [plussub_def,closed_err_lift2_conv]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "closed_map2_list";
 
 Goal
  "closed (err A) (lift2 f) ==> \
 \ closed (err (list n A)) (lift2 (sup f))";
-by(fast_tac (claset() addss (simpset() addsimps
+by (fast_tac (claset() addss (simpset() addsimps
  [closed_def,plussub_def,sup_def,lift2_def,
   coalesce_in_err_list,closed_map2_list]
  addsplits [err.split])) 1);
@@ -400,24 +400,24 @@
 Goalw [Err.sl_def]
  "err_semilat (A,r,f) ==> \
 \ err_semilat (list n A, Listn.le r, sup f)";
-by(asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1);
-by(simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1);
-by(asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1);
-br conjI 1;
- bd semilatDorderI 1;
- by(Asm_full_simp_tac 1);
-by(simp_tac (HOL_basic_ss addsimps
+by (asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1);
+by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1);
+by (rtac conjI 1);
+ by (dtac semilatDorderI 1);
+ by (Asm_full_simp_tac 1);
+by (simp_tac (HOL_basic_ss addsimps
      [unfold_lesub_err,Err.le_def,err_def,sup_def,lift2_def]) 1);
 by (asm_simp_tac (simpset() addsimps
      [coalesce_eq_OK1_D,coalesce_eq_OK2_D] addsplits [err.split]) 1);
-by(blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1);
+by (blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1);
 qed "err_semilat_sup";
 
 Goalw [Listn.upto_esl_def]
  "!!L. err_semilat L ==> err_semilat(upto_esl m L)";
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
-by(fast_tac (claset()
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (claset()
   addSIs [err_semilat_UnionI,err_semilat_sup]
   addDs [lesub_list_impl_same_size] addss (simpset()
   addsimps [plussub_def,Listn.sup_def])) 1);