--- a/src/HOL/BCV/DFA_Framework.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/DFA_Framework.ML Mon Oct 09 12:23:45 2000 +0200
@@ -23,23 +23,23 @@
"[| order r; top r T; \
\ wti_is_stable_topless r T step wti succs n A; \
\ is_dfa r dfa step succs n A |] ==> is_bcv r T wti n A dfa";
-by(Clarify_tac 1);
+by (Clarify_tac 1);
by (dtac is_dfaD 1);
by (assume_tac 1);
-by(Clarify_tac 1);
-br iffI 1;
- br bexI 1;
- br conjI 1;
- ba 1;
+by (Clarify_tac 1);
+by (rtac iffI 1);
+ by (rtac bexI 1);
+ by (rtac conjI 1);
+ by (assume_tac 1);
by (asm_full_simp_tac
(simpset() addsimps[wti_is_stable_toplessD,stables_def]) 1);
- ba 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac
+ by (assume_tac 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac
(simpset() addsimps [imp_conjR,all_conj_distrib,wti_is_stable_toplessD,
stables_def] addcongs [conj_cong]) 1);
-by(dres_inst_tac [("x","ts")] bspec 1);
- ba 1;
+by (dres_inst_tac [("x","ts")] bspec 1);
+ by (assume_tac 1);
by (force_tac (claset()addDs [le_listD],simpset()) 1);
qed "is_bcv_dfa";
--- a/src/HOL/BCV/Err.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Err.ML Mon Oct 09 12:23:45 2000 +0200
@@ -32,12 +32,12 @@
Goal "order(le r) = order r";
-br iffI 1;
- by(stac order_def 1);
- by(blast_tac (claset() addDs [order_antisym,OK_le_err_OK RS iffD2]
+by (rtac iffI 1);
+ by (stac order_def 1);
+ by (blast_tac (claset() addDs [order_antisym,OK_le_err_OK RS iffD2]
addIs [order_trans,OK_le_err_OK RS iffD1]) 1);
-by(stac order_def 1);
-by(blast_tac (claset() addIs [le_err_refl,le_err_trans,le_err_antisym]
+by (stac order_def 1);
+by (blast_tac (claset() addIs [le_err_refl,le_err_trans,le_err_antisym]
addDs [order_refl]) 1);
qed "order_le_err";
AddIffs [order_le_err];
@@ -92,8 +92,8 @@
Goalw [sl_def,esl_def]
"!!L. semilat L ==> err_semilat(esl L)";
-by(split_all_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [semilat_errI]) 1);
+by (split_all_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [semilat_errI]) 1);
qed "err_semilat_eslI";
Goalw [acc_def,lesub_def,le_def,lesssub_def]
@@ -126,21 +126,21 @@
Goalw [lift_def]
"[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S";
by (asm_simp_tac (simpset() addsplits [err.split]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "lift_in_errI";
(** lift2 **)
Goalw [lift2_def,plussub_def] "Err +_(lift2 f) x = Err";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "Err_lift2";
Goalw [lift2_def,plussub_def] "x +_(lift2 f) Err = Err";
-by(simp_tac (simpset() addsplits [err.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
qed "lift2_Err";
Goalw [lift2_def,plussub_def] "OK x +_(lift2 f) OK y = x +_f y";
-by(simp_tac (simpset() addsplits [err.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
qed "OK_lift2_OK";
Addsimps [Err_lift2,lift2_Err,OK_lift2_OK];
@@ -164,16 +164,16 @@
Goalw [Err.sup_def,lift2_def,plussub_def]
"(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)";
-br iffI 1;
- by(Clarify_tac 2);
+by (rtac iffI 1);
+ by (Clarify_tac 2);
by (Asm_simp_tac 2);
-by(asm_full_simp_tac (simpset() addsplits [err.split_asm]) 1);
+by (asm_full_simp_tac (simpset() addsplits [err.split_asm]) 1);
qed "Err_sup_eq_OK_conv";
AddIffs [Err_sup_eq_OK_conv];
Goalw [Err.sup_def,lift2_def,plussub_def]
"(Err.sup f ex ey = Err) = (ex=Err | ey=Err)";
-by(simp_tac (simpset() addsplits [err.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
qed "Err_sup_eq_Err";
AddIffs [Err_sup_eq_Err];
@@ -181,56 +181,56 @@
(*** semilat (err A) (le r) f ***)
Goal "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err";
-by(blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
+by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
qed "semilat_le_err_Err_plus";
Goal "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err";
-by(blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
+by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
qed "semilat_le_err_plus_Err";
Addsimps [semilat_le_err_Err_plus,semilat_le_err_plus_Err];
Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \
\ ==> x <=_r z";
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1);
+by (Asm_simp_tac 1);
qed "semilat_le_err_OK1";
Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \
\ ==> y <=_r z";
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1);
+by (Asm_simp_tac 1);
qed "semilat_le_err_OK2";
Goalw [order_def] "[| x=y; order r |] ==> x <=_r y";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "eq_order_le";
Goal
"[| x:A; y:A; semilat(err A, le r, fe) |] ==> \
\ ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))";
-br iffI 1;
+by (rtac iffI 1);
by (Clarify_tac 1);
- bd (OK_le_err_OK RS iffD2) 1;
- bd (OK_le_err_OK RS iffD2) 1;
- bd semilat_lub 1;
- ba 1;
- ba 1;
- by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
- by(Asm_full_simp_tac 1);
-by(case_tac "(OK x) +_fe (OK y)" 1);
- ba 1;
-by(rename_tac "z" 1);
-by(subgoal_tac "OK z: err A" 1);
-bd eq_order_le 1;
- by(Blast_tac 1);
- by(blast_tac (claset() addDs [rotate_prems 3 (plus_le_conv RS iffD1)]) 1);
-by(etac subst 1);
-by(blast_tac (claset() addIs [closedD]) 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac semilat_lub 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (case_tac "(OK x) +_fe (OK y)" 1);
+ by (assume_tac 1);
+by (rename_tac "z" 1);
+by (subgoal_tac "OK z: err A" 1);
+by (dtac eq_order_le 1);
+ by (Blast_tac 1);
+ by (blast_tac (claset() addDs [rotate_prems 3 (plus_le_conv RS iffD1)]) 1);
+by (etac subst 1);
+by (blast_tac (claset() addIs [closedD]) 1);
qed "OK_plus_OK_eq_Err_conv";
Addsimps [OK_plus_OK_eq_Err_conv];
@@ -238,7 +238,7 @@
(* FIXME? *)
Goal "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "all_bex_swap_lemma";
AddIffs [all_bex_swap_lemma];
@@ -246,10 +246,10 @@
"[| !A:AS. closed (err A) (lift2 f); AS ~= {}; \
\ !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] \
\ ==> closed (err(Union AS)) (lift2 f)";
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(Fast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
qed "closed_err_Union_lift2I";
(* If AS = {} the thm collapses to
@@ -259,32 +259,32 @@
"[| !A:AS. err_semilat(A, r, f); AS ~= {}; \
\ !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] \
\ ==> err_semilat(Union AS, r, f)";
-by(asm_full_simp_tac (simpset() addsimps [closed_err_Union_lift2I]) 1);
-br conjI 1;
- by(Blast_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [err_def]) 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(rename_tac "A a u B b" 1);
- by(case_tac "A = B" 1);
- by(Asm_full_simp_tac 1);
- by(Asm_full_simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(rename_tac "A a u B b" 1);
- by(case_tac "A = B" 1);
- by(Asm_full_simp_tac 1);
- by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(rename_tac "A ya yb B yd z C c a b" 1);
-by(case_tac "A = B" 1);
- by(case_tac "A = C" 1);
- by(Asm_full_simp_tac 1);
- by(rotate_tac ~1 1);
- by(Asm_full_simp_tac 1);
-by(rotate_tac ~1 1);
-by(case_tac "B = C" 1);
- by(Asm_full_simp_tac 1);
-by(rotate_tac ~1 1);
-by(Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [closed_err_Union_lift2I]) 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [err_def]) 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rename_tac "A a u B b" 1);
+ by (case_tac "A = B" 1);
+ by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rename_tac "A a u B b" 1);
+ by (case_tac "A = B" 1);
+ by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (rename_tac "A ya yb B yd z C c a b" 1);
+by (case_tac "A = B" 1);
+ by (case_tac "A = C" 1);
+ by (Asm_full_simp_tac 1);
+ by (rotate_tac ~1 1);
+ by (Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (case_tac "B = C" 1);
+ by (Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
qed "err_semilat_UnionI";
--- a/src/HOL/BCV/JType.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/JType.ML Mon Oct 09 12:23:45 2000 +0200
@@ -5,26 +5,26 @@
*)
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,
@@ -32,72 +32,72 @@
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];
@@ -105,8 +105,8 @@
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";
@@ -114,52 +114,52 @@
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";
--- a/src/HOL/BCV/JVM.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/JVM.ML Mon Oct 09 12:23:45 2000 +0200
@@ -13,7 +13,7 @@
Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def]
"states S maxs maxr == opt(err((Union {list n (types S) |n. n <= maxs}) <*>\
\ list maxr (err(types S))))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "JVM_states_unfold";
Goalw [JVM.le_def,JVM.sl_def,Opt.sl_def,Err.sl_def,
@@ -21,70 +21,70 @@
Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def]
"JVM.le S m n == \
\ Opt.le(Err.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "JVM_le_unfold";
Goalw [wfis_def,wfi_def]
"[| wfis S md maxr bs; bs!p = Load n; p < size bs |] ==> n < maxr";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
qed "wf_LoadD";
Goalw [wfis_def,wfi_def]
"[| wfis S md maxr bs; bs!p = Store n; p < size bs |] ==> n < maxr";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
qed "wf_StoreD";
Goalw [wfis_def,wfi_def]
"[| wfis S md m bs; bs!p = New C; p < size bs |] ==> (C,Object):S^*";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
qed "wf_NewD";
Goalw [wfis_def,wfi_def,wf_mdict_def]
"[| wfis S md maxr bs; wf_mdict S md; bs!p = Invoke C m pT (Class R); \
\ p < size bs |] ==> (R,Object):S^*";
-by(force_tac (claset(),simpset()addsimps [all_set_conv_all_nth]) 1);
+by (force_tac (claset(),simpset()addsimps [all_set_conv_all_nth]) 1);
qed "wf_InvokeD";
Goalw [wfis_def,wfi_def]
"[|wfis S md m bs; bs!p = Getfield (Class C) D; p < size bs|] ==> \
\ (C,Object):S^*";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
qed "wf_GetfieldD";
Goal "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "special_ex_swap_lemma";
AddIffs [special_ex_swap_lemma];
Goalw [pres_type_def,list_def,step_def,JVM_states_unfold]
"[| wfis S md maxr bs; wf_mdict S md |] ==> \
\ pres_type (step S maxs rT bs) (size bs) (states S maxs maxr)";
-by(clarify_tac (claset() addSEs [option_map_in_optionI,lift_in_errI]) 1);
-by(asm_simp_tac (simpset()addsimps [exec_def] addsplits [instr.split]) 1);
+by (clarify_tac (claset() addSEs [option_map_in_optionI,lift_in_errI]) 1);
+by (asm_simp_tac (simpset()addsimps [exec_def] addsplits [instr.split]) 1);
-br conjI 1;
-by(fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss
+by (rtac conjI 1);
+by (fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss
(simpset() delsimps [is_type_def]addsplits [err.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD]
addSEs [wf_StoreD] addss (simpset() addsplits [list.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addIs [wf_GetfieldD]
addss (simpset() addsplits [list.split,ty.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addIs [wf_NewD] addss simpset()) 1);
-br conjI 1;
-by(DEPTH_SOLVE_1(rtac conjI 1 ORELSE
+by (rtac conjI 1);
+by (DEPTH_SOLVE_1(rtac conjI 1 ORELSE
Clarify_tac 1 THEN asm_full_simp_tac (simpset() addsimps [wf_InvokeD]
addsplits [list.split,ty.split,option.split]) 1));
@@ -100,60 +100,60 @@
\ (step S maxs rT bs) \
\ (wti S maxs rT bs) \
\ (succs bs) (size bs) (states S maxs maxr)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
-by(simp_tac (simpset() addsplits [err.split]) 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(EVERY1[etac allE, mp_tac]);
-by(rewrite_goals_tac [exec_def,succs_def]);
-by(split_tac [instr.split] 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (EVERY1[etac allE, mp_tac]);
+by (rewrite_goals_tac [exec_def,succs_def]);
+by (split_tac [instr.split] 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-by(Blast_tac 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (Blast_tac 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1);
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-by(Blast_tac 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (Blast_tac 1);
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]
addsimps [le_list_refl,le_err_refl] ) 1);
qed "wti_is_stable_topless";
@@ -162,80 +162,80 @@
"[| wfis S md maxr bs; wf_mdict S md |] ==> \
\ mono (JVM.le S maxs maxr) (step S maxs rT bs) (size bs) (states S maxs maxr)";
by (Clarify_tac 1);
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
by (Clarify_tac 1);
-by(Asm_simp_tac 1);
-by(split_tac [err.split] 1);
-br conjI 1;
+by (Asm_simp_tac 1);
+by (split_tac [err.split] 1);
+by (rtac conjI 1);
by (Clarify_tac 1);
by (Clarify_tac 1);
-by(simp_tac (simpset() addsimps [exec_def] delsplits [split_if]) 1);
-by(split_tac [instr.split] 1);
+by (simp_tac (simpset() addsimps [exec_def] delsplits [split_if]) 1);
+by (split_tac [instr.split] 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addDs [le_listD] addSEs [wf_LoadD]
addss (simpset() addsplits [err.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addIs [list_update_le_cong,le_listD] addSEs [wf_StoreD]
addss (simpset() addsplits [list.split])) 1);
-br conjI 1;
-by(Asm_simp_tac 1);
+by (rtac conjI 1);
+by (Asm_simp_tac 1);
-br conjI 1;
-by(Asm_simp_tac 1);
+by (rtac conjI 1);
+by (Asm_simp_tac 1);
-br conjI 1;
-by(fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
+by (rtac conjI 1);
+by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (claset() addDs [rtrancl_trans]
addss (simpset() addsplits [list.split])) 1);
-br conjI 1;
+by (rtac conjI 1);
by (Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsplits [list.split]) 1);
- br conjI 1;
+ by (asm_full_simp_tac (simpset() addsplits [list.split]) 1);
+ by (rtac conjI 1);
by (Clarify_tac 1);
by (Clarify_tac 1);
- br conjI 1;
+ by (rtac conjI 1);
by (Clarify_tac 1);
by (Clarify_tac 1);
- br conjI 1;
+ by (rtac conjI 1);
by (Clarify_tac 1);
by (Clarify_tac 1);
- by(Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1);
-br conjI 1;
-by(asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1);
+by (rtac conjI 1);
+by (asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1);
-br conjI 1;
+by (rtac conjI 1);
(* 39 *)
by (Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsplits [list.split]) 1);
+ by (asm_full_simp_tac (simpset() addsplits [list.split]) 1);
by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1);
-br conjI 1;
-by(fast_tac (claset() addss (simpset() addsplits [list.split,ty.split_asm]
+by (rtac conjI 1);
+by (fast_tac (claset() addss (simpset() addsplits [list.split,ty.split_asm]
addsimps [is_Class_def,is_ref_def])) 1);
-by(asm_simp_tac (simpset() addsplits [list.split]) 1);
-by(blast_tac (claset() addIs [subtype_transD]) 1);
+by (asm_simp_tac (simpset() addsplits [list.split]) 1);
+by (blast_tac (claset() addIs [subtype_transD]) 1);
qed "exec_mono";
Goalw [JVM.sl_def,stk_esl_def,reg_sl_def]
"[| univalent S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)";
-by(REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl,
+by (REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl,
err_semilat_eslI,semilat_Listn_sl,err_semilat_JType_esl] 1));
qed "semilat_JVM_slI";
Goal "JVM.sl S maxs maxr == \
\ (states S maxs maxr, JVM.le S maxs maxr, JVM.sup S maxs maxr)";
-by(simp_tac (simpset() addsimps [states_def,JVM.le_def,JVM.sup_def,
+by (simp_tac (simpset() addsimps [states_def,JVM.le_def,JVM.sup_def,
surjective_pairing RS sym]) 1);
qed "sl_triple_conv";
@@ -244,18 +244,18 @@
\ bounded (succs bs) (size bs) |] ==> \
\ is_bcv (JVM.le S maxs maxr) (Some Err) (wti S maxs rT bs) \
\ (size bs) (states S maxs maxr) (kiljvm S maxs maxr rT bs)";
-br is_bcv_kildall 1;
- by(simp_tac (simpset() addsimps [symmetric sl_triple_conv]) 1);
- by(blast_tac (claset() addSIs [semilat_JVM_slI] addDs [wf_acyclic]) 1);
- by(simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
- by(blast_tac (claset()
+by (rtac is_bcv_kildall 1);
+ by (simp_tac (simpset() addsimps [symmetric sl_triple_conv]) 1);
+ by (blast_tac (claset() addSIs [semilat_JVM_slI] addDs [wf_acyclic]) 1);
+ by (simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
+ by (blast_tac (claset()
addSIs [acyclic_impl_order_subtype,wf_converse_subcls1_impl_acc_subtype]
addDs [wf_acyclic]) 1);
- by(simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
- be exec_pres_type 1;
- ba 1;
- ba 1;
- be exec_mono 1;
- ba 1;
-be wti_is_stable_topless 1;
+ by (simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
+ by (etac exec_pres_type 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (etac exec_mono 1);
+ by (assume_tac 1);
+by (etac wti_is_stable_topless 1);
qed "is_bcv_kiljvm";
--- a/src/HOL/BCV/Kildall.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Kildall.ML Mon Oct 09 12:23:45 2000 +0200
@@ -34,8 +34,8 @@
"[| semilat(A,r,f) |] ==> \
\ !xs. xs : list n A --> x : A --> (!p : set ps. p<n) \
\ --> merges f x ps xs : list n A";
-by(ftac semilatDclosedI 1);
-by(rewtac closed_def);
+by (ftac semilatDclosedI 1);
+by (rewtac closed_def);
by (induct_tac "ps" 1);
by (Auto_tac);
qed_spec_mp "merges_preserves_type";
@@ -49,9 +49,9 @@
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
by (rtac order_trans 1);
- by(Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
by (etac list_update_incr 1);
- ba 1;
+ by (assume_tac 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addSIs [listE_set]
@@ -70,13 +70,13 @@
by (rtac context_conjI 1);
by (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs" 1);
by (EVERY[etac subst 2, rtac merges_incr 2]);
- by(force_tac (claset() addSDs [le_listD],
+ by (force_tac (claset() addSDs [le_listD],
simpset() addsimps [nth_list_update]) 1);
by (assume_tac 1);
by (blast_tac (claset() addSIs [listE_set]
addIs [closedD,listE_length RS nth_in]) 1);
- ba 1;
- by(Asm_simp_tac 1);
+ by (assume_tac 1);
+ by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rotate_tac ~2 1);
by (asm_full_simp_tac (simpset() addsimps
@@ -108,7 +108,7 @@
by (Clarify_tac 1);
by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
-by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
+by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
by (asm_simp_tac (simpset() addsimps [closedD]) 1);
by (asm_full_simp_tac (simpset() addsimps [list_update_le_listI]) 1);
val lemma = result();
@@ -125,9 +125,9 @@
Goal "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> \
\ (!p:set ps. p<n) --> \
\ (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)";
-by(induct_tac "ps" 1);
+by (induct_tac "ps" 1);
by (Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
+by (asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
qed_spec_mp "nth_merges";
@@ -137,14 +137,14 @@
\ propa f qs t ss w = \
\ (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)";
by (induct_tac "qs" 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
by (Simp_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
+by (Clarify_tac 1);
+by (rtac conjI 1);
by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by(Blast_tac 1);
+ by (Blast_tac 1);
by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "decomp_propa";
(** iter **)
@@ -152,17 +152,17 @@
val [iter_wf,iter_tc] = iter.tcs;
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
-by(REPEAT(rtac wf_same_fstI 1));
-by(split_all_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
-by(REPEAT(rtac wf_same_fstI 1));
-br wf_lex_prod 1;
- br wf_finite_psubset 2; (* FIXME *)
-by(Clarify_tac 1);
-bd (semilatDorderI RS acc_le_listI) 1;
- ba 1;
-by(rewrite_goals_tac [acc_def,lesssub_def]);
-ba 1;
+by (REPEAT(rtac wf_same_fstI 1));
+by (split_all_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
+by (REPEAT(rtac wf_same_fstI 1));
+by (rtac wf_lex_prod 1);
+ by (rtac wf_finite_psubset 2); (* FIXME *)
+by (Clarify_tac 1);
+by (dtac (semilatDorderI RS acc_le_listI) 1);
+ by (assume_tac 1);
+by (rewrite_goals_tac [acc_def,lesssub_def]);
+by (assume_tac 1);
qed "iter_wf";
Goalw [lesssub_def]
@@ -170,28 +170,28 @@
\ ss <[r] merges f t qs ss | \
\ merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w";
by (asm_simp_tac (simpset() addsimps [merges_incr]) 1);
-br impI 1;
-bd (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1;
- ba 1;
- ba 1;
- ba 1;
- by(Asm_simp_tac 1);
+by (rtac impI 1);
+by (dtac (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]
addsimps [le_iff_plus_unchanged RS sym]) 1);
by (blast_tac (claset() addSIs [psubsetI] addEs [equalityE]) 1);
qed "inter_tc_lemma";
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc));
-by(asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+by (asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
by (fast_tac (claset() addIs [someI]) 2);
-by(subgoal_tac "ss : list (size ss) A" 1);
+by (subgoal_tac "ss : list (size ss) A" 1);
by (blast_tac (claset() addSIs [listI]) 2);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
by (blast_tac (claset() addDs [boundedD]) 2);
-by(rotate_tac 1 1);
-by(asm_full_simp_tac (simpset() delsimps [listE_length]
+by (rotate_tac 1 1);
+by (asm_full_simp_tac (simpset() delsimps [listE_length]
addsimps [decomp_propa,finite_psubset_def,inter_tc_lemma,
bounded_nat_set_is_finite]) 1);
qed "iter_tc";
@@ -204,15 +204,15 @@
\ --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss) \
\ ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))\
\ ==> P A r f step succs ss w) ==> P A r f step succs ss w";
-by(res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
-by(rename_tac "w" 1);
-brs prems 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset()) 1);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
- by(rotate_tac ~1 1);
- by(asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+by (res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
+by (rename_tac "w" 1);
+by (resolve_tac prems 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset()) 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+ by (rotate_tac ~1 1);
+ by (asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
by (fast_tac (claset() addIs [someI]) 2);
by (blast_tac (claset() addDs [boundedD]) 1);
qed "iter_induct";
@@ -227,9 +227,9 @@
\ {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))";
by (rtac ((iter_tc RS (iter_wf RS (hd iter.simps))) RS trans) 1);
by (Asm_simp_tac 1);
-br impI 1;
-by(stac decomp_propa 1);
- by(subgoal_tac "(@p. p:w) : w" 1);
+by (rtac impI 1);
+by (stac decomp_propa 1);
+ by (subgoal_tac "(@p. p:w) : w" 1);
by (fast_tac (claset() addIs [someI]) 2);
by (blast_tac (claset() addDs [boundedD]) 1);
by (Simp_tac 1);
@@ -242,26 +242,26 @@
\ q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; \
\ q ~: w | q = p |] ==> \
\ stable r step succs (merges f (step p (ss!p)) (succs p) ss) q";
-by(subgoal_tac "step p (ss!p) : A" 1);
+by (subgoal_tac "step p (ss!p) : A" 1);
by (blast_tac (claset() addIs [listE_nth_in,pres_typeD]) 2);
by (Simp_tac 1);
-by(Clarify_tac 1);
-by(stac nth_merges 1);
- ba 1;
- ba 1;
- ba 2;
+by (Clarify_tac 1);
+by (stac nth_merges 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (assume_tac 2);
by (blast_tac (claset() addDs [boundedD]) 1);
by (blast_tac (claset() addDs [boundedD]) 1);
-by(stac nth_merges 1);
- ba 1;
- ba 1;
- ba 2;
+by (stac nth_merges 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (assume_tac 2);
by (blast_tac (claset() addDs [boundedD]) 1);
by (blast_tac (claset() addDs [boundedD]) 1);
by (Simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
qed "stable_pres_lemma";
@@ -289,43 +289,43 @@
\ (! ts:list n A. \
\ ss <=[r] ts & stables r step succs ts --> \
\ iter(((A,r,f),step,succs),ss,w) <=[r] ts)";
-by(res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
-by(Clarify_tac 1);
-by(ftac listE_length 1);
-by(hyp_subst_tac 1);
-by(stac iter_unfold 1);
- ba 1;
- ba 1;
+by (res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
+by (Clarify_tac 1);
+by (ftac listE_length 1);
+by (hyp_subst_tac 1);
+by (stac iter_unfold 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
by (Asm_simp_tac 1);
- ba 1;
- ba 1;
- ba 1;
-by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-br impI 1;
-be allE 1;
-be impE 1;
- by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (rtac impI 1);
+by (etac allE 1);
+by (etac impE 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
by (fast_tac (claset() addIs [someI]) 2);
-by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
+by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2);
-be impE 1;
- by(asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
- br conjI 1;
+by (etac impE 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
+ by (rtac conjI 1);
by (blast_tac (claset() addDs [boundedD]) 1);
- br conjI 1;
- by(blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
+ by (rtac conjI 1);
+ by (blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
by (blast_tac (claset() addSIs [stable_pres_lemma]) 1);
-by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
by (blast_tac (claset() addDs [boundedD]) 2);
-by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
+by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
by (blast_tac (claset() addIs [pres_typeD]) 2);
-br conjI 1;
+by (rtac conjI 1);
by (blast_tac (claset() addSIs [merges_incr] addIs [le_list_trans]) 1);
-by(Clarify_tac 1);
-by(EVERY1[dtac bspec, atac, etac mp]);
-by(asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
+by (Clarify_tac 1);
+by (EVERY1[dtac bspec, atac, etac mp]);
+by (asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
by (blast_tac (claset() addIs [merges_bounded_lemma]) 1);
qed_spec_mp "iter_properties";
@@ -334,11 +334,11 @@
"[| semilat(A,r,f); acc r; pres_type step n A; \
\ mono r step n A; bounded succs n|] ==> \
\ is_dfa r (kildall (A,r,f) step succs) step succs n A";
-by(Clarify_tac 1);
-by(Simp_tac 1);
-br iter_properties 1;
-by(asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
-by(blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
+by (Clarify_tac 1);
+by (Simp_tac 1);
+by (rtac iter_properties 1);
+by (asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
+by (blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
addDs [boundedD,pres_typeD]) 1);
qed "is_dfa_kildall";
--- 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);
--- a/src/HOL/BCV/Opt.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Opt.ML Mon Oct 09 12:23:45 2000 +0200
@@ -8,7 +8,7 @@
"o1 <=_(le r) o2 = \
\ (case o2 of None => o1=None | \
\ Some y => (case o1 of None => True | Some x => x <=_r y))";
-br refl 1;
+by (rtac refl 1);
qed "unfold_le_opt";
Goal "order r ==> o1 <=_(le r) o1";
@@ -27,32 +27,32 @@
qed_spec_mp "le_opt_antisym";
Goal "order r ==> order(le r)";
-by(stac order_def 1);
-by(blast_tac (claset() addIs [le_opt_refl,le_opt_trans,le_opt_antisym]) 1);
+by (stac order_def 1);
+by (blast_tac (claset() addIs [le_opt_refl,le_opt_trans,le_opt_antisym]) 1);
qed "order_le_opt";
AddSIs [order_le_opt];
Addsimps [order_le_opt];
Goalw [lesub_def,le_def] "None <=_(le r) ox";
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
qed "None_bot";
AddIffs [None_bot];
Goalw [lesub_def,le_def]
"(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
qed "Some_le";
AddIffs [Some_le];
Goalw [lesub_def,le_def] "(ox <=_(le r) None) = (ox = None)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
qed "le_None";
AddIffs [le_None];
Goalw [Opt.sl_def,semilat_def,closed_def,split RS eq_reflection]
"!!L. semilat L ==> semilat (Opt.sl L)";
-by(split_all_tac 1);
+by (split_all_tac 1);
by (asm_full_simp_tac (simpset() addsplits [option.split]
addsimps [lesub_def,Opt.le_def,plussub_def,Opt.sup_def,opt_def,Bex_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [order_def,lesub_def]) 1);
@@ -60,16 +60,16 @@
Goalw [top_def] "top (le r) (Some T) = top r T";
-br iffI 1;
- by(Blast_tac 1);
-br allI 1;
-by(case_tac "x" 1);
-by(ALLGOALS Asm_simp_tac);
+by (rtac iffI 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (case_tac "x" 1);
+by (ALLGOALS Asm_simp_tac);
qed "top_le_opt_Some";
AddIffs [top_le_opt_Some];
Goalw [top_def] "[| order r; top r T |] ==> (T <=_r x) = (x = T)";
-by(blast_tac (claset() addIs [order_antisym]) 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
qed "Top_le_conv";
@@ -100,6 +100,6 @@
"[| ox : opt S; !x:S. ox = Some x --> f x : S |] \
\ ==> option_map f ox : opt S";
by (asm_simp_tac (simpset() addsplits [option.split]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "option_map_in_optionI";
--- a/src/HOL/BCV/Product.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Product.ML Mon Oct 09 12:23:45 2000 +0200
@@ -10,29 +10,29 @@
Goalw [lesub_def,le_def]
"((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "le_prod_Pair_conv";
AddIffs [le_prod_Pair_conv];
Goalw [lesssub_def]
"((a1,b1) <_(Product.le rA rB) (a2,b2)) = \
\ (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "less_prod_Pair_conv";
Goalw [order_def] "order(Product.le rA rB) = (order rA & order rB)";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "order_le_prod";
AddIffs [order_le_prod];
Goalw [acc_def] "[| acc rA; acc rB |] ==> acc(Product.le rA rB)";
-br wf_subset 1;
- be wf_lex_prod 1;
- ba 1;
-by(auto_tac (claset(), simpset()
+by (rtac wf_subset 1);
+ by (etac wf_lex_prod 1);
+ by (assume_tac 1);
+by (auto_tac (claset(), simpset()
addsimps [lesssub_def,less_prod_Pair_conv,lex_prod_def]));
qed "acc_le_prodI";
AddSIs [acc_le_prodI];
@@ -41,8 +41,8 @@
Goalw [closed_def,plussub_def,lift2_def,err_def,sup_def]
"[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> \
\ closed (err(A<*>B)) (lift2(sup f g))";
-by(asm_full_simp_tac (simpset() addsplits [err.split]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [err.split]) 1);
+by (Blast_tac 1);
qed "closed_lift2_sup";
Goalw [plussub_def] "e1 +_(lift2 f) e2 == lift2 f e1 e2";
@@ -52,63 +52,63 @@
Goal
"[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] ==> \
\ (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))";
-br iffI 1;
+by (rtac iffI 1);
by (Clarify_tac 1);
- bd (OK_le_err_OK RS iffD2) 1;
- bd (OK_le_err_OK RS iffD2) 1;
- bd semilat_lub 1;
- ba 1;
- ba 1;
- by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
- by(Asm_full_simp_tac 1);
-by(case_tac "x +_f y" 1);
- ba 1;
-by(rename_tac "z" 1);
-by(subgoal_tac "OK z: err A" 1);
- by(ftac (rotate_prems 2 (read_instantiate_sg(sign_of Err.thy)[("x","OK(x::'a)"),("y","OK(y::'a)")]plus_le_conv RS iffD1))1);
- ba 1;
- by(Asm_simp_tac 1);
- by(blast_tac (claset() addDs [semilatDorderI,order_refl]) 1);
- by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
-by(etac subst 1);
-by(rewrite_goals_tac [semilat_def,err_def,closed_def]);
-by(Asm_full_simp_tac 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac semilat_lub 1);
+ by (assume_tac 1);
+ by (assume_tac 1);
+ by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (case_tac "x +_f y" 1);
+ by (assume_tac 1);
+by (rename_tac "z" 1);
+by (subgoal_tac "OK z: err A" 1);
+ by (ftac (rotate_prems 2 (read_instantiate_sg(sign_of Err.thy)[("x","OK(x::'a)"),("y","OK(y::'a)")]plus_le_conv RS iffD1))1);
+ by (assume_tac 1);
+ by (Asm_simp_tac 1);
+ by (blast_tac (claset() addDs [semilatDorderI,order_refl]) 1);
+ by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
+by (etac subst 1);
+by (rewrite_goals_tac [semilat_def,err_def,closed_def]);
+by (Asm_full_simp_tac 1);
qed "plus_eq_Err_conv";
Addsimps [plus_eq_Err_conv];
Goalw [esl_def,Err.sl_def]
"!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)";
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
-by(simp_tac (HOL_basic_ss addsimps [semilat_Def]) 1);
-by(asm_simp_tac(HOL_basic_ss addsimps[semilatDclosedI,closed_lift2_sup])1);
-by(simp_tac (HOL_basic_ss addsimps
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def]) 1);
+by (asm_simp_tac(HOL_basic_ss addsimps[semilatDclosedI,closed_lift2_sup])1);
+by (simp_tac (HOL_basic_ss addsimps
[unfold_lesub_err,Err.le_def,unfold_plussub_lift2,sup_def]) 1);
by (auto_tac (claset() addEs [semilat_le_err_OK1,semilat_le_err_OK2],
simpset() addsimps [lift2_def] addsplits [err.split]));
-by(blast_tac (claset() addDs [semilatDorderI]) 1);
-by(blast_tac (claset() addDs [semilatDorderI]) 1);
+by (blast_tac (claset() addDs [semilatDorderI]) 1);
+by (blast_tac (claset() addDs [semilatDorderI]) 1);
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "err_semilat_Product_esl";
--- a/src/HOL/BCV/Semilat.ML Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Semilat.ML Mon Oct 09 12:23:45 2000 +0200
@@ -5,37 +5,37 @@
*)
Goalw [order_def] "order r ==> x <=_r x";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "order_refl";
Addsimps [order_refl];
AddIs [order_refl];
Goalw [order_def] "[| order r; x <=_r y; y <=_r x |] ==> x = y";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "order_antisym";
Goalw [order_def] "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "order_trans";
Goalw [order_def,lesssub_def] "order r ==> ~ x <_r x";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "order_less_irrefl";
AddIs [order_less_irrefl];
Addsimps [order_less_irrefl];
Goalw [order_def,lesssub_def] "[| order r; x <_r y; y <_r z |] ==> x <_r z";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "order_less_trans";
Goalw [top_def] "top r T ==> x <=_r T";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "topD";
Addsimps [topD];
AddIs [topD];
Goal "[| order r; top r T |] ==> (T <=_r x) = (x = T)";
-by(blast_tac (claset() addIs [order_antisym]) 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
qed "top_le_conv";
Addsimps [top_le_conv];
@@ -44,32 +44,32 @@
\ (!x:A. !y:A. x <=_r x +_f y) & \
\ (!x:A. !y:A. y <=_r x +_f y) & \
\ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)";
-br (refl RS eq_reflection) 1;
+by (rtac (refl RS eq_reflection) 1);
qed "semilat_Def";
Goalw [semilat_Def] "semilat(A,r,f) ==> order r";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "semilatDorderI";
Addsimps [semilatDorderI];
AddIs [semilatDorderI];
Goalw [semilat_Def] "semilat(A,r,f) ==> closed A f";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "semilatDclosedI";
Addsimps [semilatDclosedI];
AddIs [semilatDclosedI];
Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "semilat_ub1";
Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "semilat_ub2";
Goalw [semilat_Def]
"[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "semilat_lub";
Addsimps [semilat_ub1,semilat_ub2,semilat_lub];
@@ -98,11 +98,11 @@
(*** closed ***)
Goalw [closed_def] "[| closed A f; x:A; y:A |] ==> x +_f y : A";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "closedD";
Goalw [closed_def] "closed UNIV f";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "closed_UNIV";
AddIffs [closed_UNIV];
@@ -110,17 +110,17 @@
Goalw [is_lub_def]
"is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)";
-ba 1;
+by (assume_tac 1);
qed "is_lubD";
Goalw [is_ub_def]
"[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "is_ubI";
Goalw [is_ub_def]
"is_ub r x y u ==> (x,u) : r & (y,u) : r";
-ba 1;
+by (assume_tac 1);
qed "is_ubD";
@@ -138,40 +138,40 @@
Goalw [is_lub_def,is_ub_def]
"[| univalent r; is_lub (r^*) x y u; (x',x) : r |] ==> \
\ EX v. is_lub (r^*) x' y v";
-by(case_tac "(y,x) : r^*" 1);
- by(case_tac "(y,x') : r^*" 1);
+by (case_tac "(y,x) : r^*" 1);
+ by (case_tac "(y,x') : r^*" 1);
by (Blast_tac 1);
- by(blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE]
+ by (blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE]
addDs [univalentD]) 1);
-br exI 1;
-br conjI 1;
- by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2]
+by (rtac exI 1);
+by (rtac conjI 1);
+ by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2]
addEs [converse_rtranclE] addDs [univalentD]) 1);
qed "extend_lub";
Goal "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \
\ (EX z. is_lub (r^*) x y z))";
-by(etac converse_rtrancl_induct 1);
- by(Clarify_tac 1);
- by(etac converse_rtrancl_induct 1);
- by(Blast_tac 1);
- by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-by(blast_tac (claset() addIs [extend_lub]) 1);
+by (etac converse_rtrancl_induct 1);
+ by (Clarify_tac 1);
+ by (etac converse_rtrancl_induct 1);
+ by (Blast_tac 1);
+ by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (blast_tac (claset() addIs [extend_lub]) 1);
qed_spec_mp "univalent_has_lubs";
Goalw [some_lub_def,is_lub_def]
"[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u";
-br someI2 1;
- ba 1;
-by(blast_tac (claset() addIs [antisymD]
+by (rtac someI2 1);
+ by (assume_tac 1);
+by (blast_tac (claset() addIs [antisymD]
addSDs [acyclic_impl_antisym_rtrancl]) 1);
qed "some_lub_conv";
Goal
"[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \
\ is_lub (r^*) x y (some_lub (r^*) x y)";
-by(fast_tac
+by (fast_tac
(claset() addDs [univalent_has_lubs]
addss (simpset() addsimps [some_lub_conv])) 1);
qed "is_lub_some_lub";