--- a/src/HOL/AxClasses/Lattice/Lattice.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML Fri Jan 29 16:26:12 1999 +0100
@@ -2,7 +2,7 @@
context HOL.thy;
Goalw [Ex_def] "EX x. P x ==> P (@x. P x)";
- ba 1;
+ by (assume_tac 1);
qed "selectI1";
context thy;
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML Fri Jan 29 16:26:12 1999 +0100
@@ -66,8 +66,8 @@
qed "le_dual_refl";
Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
- br impI 1;
- br (le_trans RS mp) 1;
+ by (rtac impI 1);
+ by (rtac (le_trans RS mp) 1);
by (Blast_tac 1);
qed "le_dual_trans";
--- a/src/HOL/Finite.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Finite.ML Fri Jan 29 16:26:12 1999 +0100
@@ -112,7 +112,7 @@
Addsimps [finite_Diff];
Goal "finite(A - insert a B) = finite(A-B)";
-by(stac Diff_insert 1);
+by (stac Diff_insert 1);
by (case_tac "a : A-B" 1);
by (rtac (finite_insert RS sym RS trans) 1);
by (stac insert_Diff 1);
@@ -331,38 +331,38 @@
AddSIs cardR.intrs;
Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)";
-be cardR.induct 1;
- by(Blast_tac 1);
-by(Blast_tac 1);
+by (etac cardR.induct 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
qed "cardR_SucD";
Goal "(A,m): cardR ==> (!n a. m = Suc n --> a:A --> (A-{a},n) : cardR)";
-be cardR.induct 1;
- by(Auto_tac);
-by(asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
-by(Auto_tac);
-by(forward_tac [cardR_SucD] 1);
-by(Blast_tac 1);
+by (etac cardR.induct 1);
+ by (Auto_tac);
+by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
+by (Auto_tac);
+by (forward_tac [cardR_SucD] 1);
+by (Blast_tac 1);
val lemma = result();
Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR";
-bd lemma 1;
-by(Asm_full_simp_tac 1);
+by (dtac lemma 1);
+by (Asm_full_simp_tac 1);
val lemma = result();
Goal "(A,m): cardR ==> (!n. (A,n) : cardR --> n=m)";
-be cardR.induct 1;
- by(safe_tac (claset() addSEs [cardR_insertE]));
-by(rename_tac "B b m" 1);
-by(case_tac "a = b" 1);
- by(subgoal_tac "A = B" 1);
- by(blast_tac (claset() addEs [equalityE]) 2);
- by(Blast_tac 1);
-by(subgoal_tac "? C. A = insert b C & B = insert a C" 1);
- by(res_inst_tac [("x","A Int B")] exI 2);
- by(blast_tac (claset() addEs [equalityE]) 2);
-by(forw_inst_tac [("A","B")] cardR_SucD 1);
-by(blast_tac (claset() addDs [lemma]) 1);
+by (etac cardR.induct 1);
+ by (safe_tac (claset() addSEs [cardR_insertE]));
+by (rename_tac "B b m" 1);
+by (case_tac "a = b" 1);
+ by (subgoal_tac "A = B" 1);
+ by (blast_tac (claset() addEs [equalityE]) 2);
+ by (Blast_tac 1);
+by (subgoal_tac "? C. A = insert b C & B = insert a C" 1);
+ by (res_inst_tac [("x","A Int B")] exI 2);
+ by (blast_tac (claset() addEs [equalityE]) 2);
+by (forw_inst_tac [("A","B")] cardR_SucD 1);
+by (blast_tac (claset() addDs [lemma]) 1);
qed_spec_mp "cardR_determ";
Goal "(A,n) : cardR ==> finite(A)";
@@ -730,26 +730,26 @@
(*** setsum ***)
Goalw [setsum_def] "setsum f {} = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "setsum_empty";
Addsimps [setsum_empty];
Goalw [setsum_def]
"[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
-by(asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
+by (asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
qed "setsum_insert";
Addsimps [setsum_insert];
Goalw [setsum_def]
"[| finite A; finite B; A Int B = {} |] ==> \
\ setsum f (A Un B) = setsum f A + setsum f B";
-by(asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
+by (asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
qed_spec_mp "setsum_disj_Un";
Goal "[| finite F |] ==> \
\ setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
-be finite_induct 1;
-by(auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
-by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
-by(Auto_tac);
+by (etac finite_induct 1);
+by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
+by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
+by (Auto_tac);
qed_spec_mp "setsum_diff1";
--- a/src/HOL/Hoare/Examples.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Hoare/Examples.ML Fri Jan 29 16:26:12 1999 +0100
@@ -14,7 +14,7 @@
\ INV {s=m*b} \
\ DO s := s+b; m := m+1 OD \
\ {s = a*b}";
-by(hoare_tac (Asm_full_simp_tac) 1);
+by (hoare_tac (Asm_full_simp_tac) 1);
qed "multiply_by_add";
(*** Euclid's algorithm for GCD ***)
@@ -49,7 +49,7 @@
\ c := c*a; b := b-1 \
\ OD \
\ {c = A^B}";
-by(hoare_tac (Asm_full_simp_tac) 1);
+by (hoare_tac (Asm_full_simp_tac) 1);
by (exhaust_tac "b" 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
@@ -116,7 +116,7 @@
\ {(i < length A --> A!i = 0) & \
\ (i = length A --> (!j. j < length A --> A!j ~= 0))}";
by (hoare_tac Asm_full_simp_tac 1);
-by(blast_tac (claset() addSEs [less_SucE]) 1);
+by (blast_tac (claset() addSEs [less_SucE]) 1);
qed "zero_search";
(*
@@ -146,30 +146,30 @@
\ OD \
\ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}";
(* expand and delete abbreviations first *)
-by(asm_simp_tac HOL_basic_ss 1);
-by(REPEAT(etac thin_rl 1));
+by (asm_simp_tac HOL_basic_ss 1);
+by (REPEAT(etac thin_rl 1));
by (hoare_tac Asm_full_simp_tac 1);
- by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
- by(Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
- br conjI 1;
- by(Clarify_tac 1);
- bd (pred_less_imp_le RS le_imp_less_Suc) 1;
- by(blast_tac (claset() addSEs [less_SucE]) 1);
- br less_imp_diff_less 1;
- by(Blast_tac 1);
- by(Clarify_tac 1);
- by(asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by(Clarify_tac 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
-by(Asm_simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- br order_antisym 1;
- by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
-by(Clarify_tac 1);
-by(Asm_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
+ by (Clarify_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
+ by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
+ by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (dtac (pred_less_imp_le RS le_imp_less_Suc) 1);
+ by (blast_tac (claset() addSEs [less_SucE]) 1);
+ by (rtac less_imp_diff_less 1);
+ by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
+ by (Clarify_tac 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_simp_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rtac order_antisym 1);
+ by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_simp_tac 1);
qed "Partition";
--- a/src/HOL/Hoare/Hoare.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Hoare/Hoare.ML Fri Jan 29 16:26:12 1999 +0100
@@ -9,43 +9,43 @@
(*** The proof rules ***)
Goalw [Valid_def] "p <= q ==> Valid p SKIP q";
-by(Auto_tac);
+by (Auto_tac);
qed "SkipRule";
Goalw [Valid_def] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
-by(Auto_tac);
+by (Auto_tac);
qed "BasicRule";
Goalw [Valid_def] "[| Valid P c1 Q; Valid Q c2 R |] ==> Valid P (c1;c2) R";
-by(Asm_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Blast_tac 1);
qed "SeqRule";
Goalw [Valid_def]
"[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \
\ Valid w c1 q; Valid w' c2 q |] \
\ ==> Valid p (IF b THEN c1 ELSE c2 FI) q";
-by(Asm_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Blast_tac 1);
qed "CondRule";
Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \
\ ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b";
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
val lemma = result() RS spec RS spec RS mp RS mp;
Goalw [Valid_def]
"[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \
\ ==> Valid p (WHILE b INV {i} DO c OD) q";
-by(Asm_simp_tac 1);
-by(Clarify_tac 1);
-bd lemma 1;
-ba 2;
-by(Blast_tac 1);
-by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (dtac lemma 1);
+by (assume_tac 2);
+by (Blast_tac 1);
+by (Blast_tac 1);
qed "WhileRule";
(*** The tactics ***)
--- a/src/HOL/IMP/Natural.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/IMP/Natural.ML Fri Jan 29 16:26:12 1999 +0100
@@ -31,20 +31,20 @@
Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
\ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
-be evalc.induct 1;
-by(Auto_tac);
+by (etac evalc.induct 1);
+by (Auto_tac);
val lemma1 = result() RS spec RS mp RS mp;
Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
\ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
-be evalc.induct 1;
-by(ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
-by(case_tac "P s" 1);
-by(Auto_tac);
+by (etac evalc.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+by (case_tac "P s" 1);
+by (Auto_tac);
val lemma2 = result() RS spec RS mp;
Goal "!x. P x --> Q x ==> \
\ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
-by(blast_tac (claset() addIs [lemma1,lemma2]) 1);
+by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
qed "Hoare_example";
--- a/src/HOL/Induct/Multiset.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Induct/Multiset.ML Fri Jan 29 16:26:12 1999 +0100
@@ -9,39 +9,39 @@
(** Preservation of representing set `multiset' **)
Goalw [multiset_def] "(%a. 0) : multiset";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "const0_in_multiset";
Addsimps [const0_in_multiset];
Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "only1_in_multiset";
Addsimps [only1_in_multiset];
Goalw [multiset_def]
"[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
-by(Asm_full_simp_tac 1);
-bd finite_UnI 1;
-ba 1;
-by(asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
+by (Asm_full_simp_tac 1);
+by (dtac finite_UnI 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
qed "union_preserves_multiset";
Addsimps [union_preserves_multiset];
Goalw [multiset_def]
"[| M : multiset |] ==> (%a. M a - N a) : multiset";
-by(Asm_full_simp_tac 1);
-be (rotate_prems 1 finite_subset) 1;
-by(Auto_tac);
+by (Asm_full_simp_tac 1);
+by (etac (rotate_prems 1 finite_subset) 1);
+by (Auto_tac);
qed "diff_preserves_multiset";
Addsimps [diff_preserves_multiset];
(** Injectivity of Rep_multiset **)
Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
-br iffI 1;
- by(Asm_simp_tac 1);
-by(dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
-by(Asm_full_simp_tac 1);
+by (rtac iffI 1);
+ by (Asm_simp_tac 1);
+by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
+by (Asm_full_simp_tac 1);
qed "multiset_eq_conv_Rep_eq";
Addsimps [multiset_eq_conv_Rep_eq];
Addsimps [expand_fun_eq];
@@ -49,13 +49,13 @@
Goal
"[| f : multiset; g : multiset |] ==> \
\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
-br iffI 1;
- by(dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
- by(Asm_full_simp_tac 1);
-by(subgoal_tac "f = g" 1);
- by(Asm_simp_tac 1);
-br ext 1;
-by(Blast_tac 1);
+by (rtac iffI 1);
+ by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
+ by (Asm_full_simp_tac 1);
+by (subgoal_tac "f = g" 1);
+ by (Asm_simp_tac 1);
+by (rtac ext 1);
+by (Blast_tac 1);
qed "Abs_multiset_eq";
Addsimps [Abs_multiset_eq];
*)
@@ -66,18 +66,18 @@
Goalw [union_def,empty_def]
"M + {#} = M & {#} + M = M";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "union_empty";
Addsimps [union_empty];
Goalw [union_def]
"(M::'a multiset) + N = N + M";
-by(simp_tac (simpset() addsimps add_ac) 1);
+by (simp_tac (simpset() addsimps add_ac) 1);
qed "union_comm";
Goalw [union_def]
"((M::'a multiset)+N)+K = M+(N+K)";
-by(simp_tac (simpset() addsimps add_ac) 1);
+by (simp_tac (simpset() addsimps add_ac) 1);
qed "union_assoc";
qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
@@ -90,13 +90,13 @@
Goalw [empty_def,diff_def]
"M-{#} = M & {#}-M = {#}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "diff_empty";
Addsimps [diff_empty];
Goalw [union_def,diff_def]
"M+{#a#}-{#a#} = M";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "diff_union_inverse2";
Addsimps [diff_union_inverse2];
@@ -104,57 +104,57 @@
Goalw [count_def,empty_def]
"count {#} a = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "count_empty";
Addsimps [count_empty];
Goalw [count_def,single_def]
"count {#b#} a = (if b=a then 1 else 0)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "count_single";
Addsimps [count_single];
Goalw [count_def,union_def]
"count (M+N) a = count M a + count N a";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "count_union";
Addsimps [count_union];
Goalw [count_def,diff_def]
"count (M-N) a = count M a - count N a";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "count_diff";
Addsimps [count_diff];
(* set_of *)
Goalw [set_of_def] "set_of {#} = {}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "set_of_empty";
Addsimps [set_of_empty];
Goalw [set_of_def]
"set_of {#b#} = {b}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "set_of_single";
Addsimps [set_of_single];
Goalw [set_of_def]
"set_of(M+N) = set_of M Un set_of N";
-by(Auto_tac);
+by (Auto_tac);
qed "set_of_union";
Addsimps [set_of_union];
(* size *)
Goalw [size_def] "size {#} = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "size_empty";
Addsimps [size_empty];
Goalw [size_def]
"size {#b#} = 1";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "size_single";
Addsimps [size_single];
@@ -166,99 +166,99 @@
(* equalities *)
Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "multiset_eq_conv_count_eq";
Goalw [single_def,empty_def] "{#a#} ~= {#} & {#} ~= {#a#}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "single_not_empty";
Addsimps [single_not_empty];
Goalw [single_def] "({#a#}={#b#}) = (a=b)";
-by(Auto_tac);
+by (Auto_tac);
qed "single_eq_single";
Addsimps [single_eq_single];
Goalw [union_def,empty_def]
"(M+N = {#}) = (M = {#} & N = {#})";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "union_eq_empty";
AddIffs [union_eq_empty];
Goalw [union_def,empty_def]
"({#} = M+N) = (M = {#} & N = {#})";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "empty_eq_union";
AddIffs [empty_eq_union];
Goalw [union_def]
"(M+K = N+K) = (M=(N::'a multiset))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "union_right_cancel";
Addsimps [union_right_cancel];
Goalw [union_def]
"(K+M = K+N) = (M=(N::'a multiset))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "union_left_cancel";
Addsimps [union_left_cancel];
Goalw [empty_def,single_def,union_def]
"(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
-by(simp_tac (simpset() addsimps [add_is_1]) 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsimps [add_is_1]) 1);
+by (Blast_tac 1);
qed "union_is_single";
Goalw [empty_def,single_def,union_def]
"({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
-by(simp_tac (simpset() addsimps [one_is_add]) 1);
-by(blast_tac (claset() addDs [sym]) 1);
+by (simp_tac (simpset() addsimps [one_is_add]) 1);
+by (blast_tac (claset() addDs [sym]) 1);
qed "single_is_union";
Goalw [single_def,union_def,diff_def]
"(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
-by(Simp_tac 1);
-br conjI 1;
- by(Force_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-br iffI 1;
- br conjI 1;
- by(Clarify_tac 1);
- br conjI 1;
- by(asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+by (Simp_tac 1);
+by (rtac conjI 1);
+ by (Force_tac 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rtac iffI 1);
+ by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rtac conjI 1);
+ by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
(* PROOF FAILED:
-by(Blast_tac 1);
+by (Blast_tac 1);
*)
- by(Fast_tac 1);
- by(Asm_simp_tac 1);
-by(Force_tac 1);
+ by (Fast_tac 1);
+ by (Asm_simp_tac 1);
+by (Force_tac 1);
qed "add_eq_conv_diff";
(* FIXME
val prems = Goal
"[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
-by(res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
+by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
measure_induct 1);
-by(Clarify_tac 1);
-brs prems 1;
- ba 1;
-by(Clarify_tac 1);
-by(subgoal_tac "finite G" 1);
- by(fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
-be allE 1;
-be impE 1;
- by(Blast_tac 2);
-by(asm_simp_tac (simpset() addsimps [psubset_card]) 1);
+by (Clarify_tac 1);
+by (resolve_tac prems 1);
+ by (assume_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "finite G" 1);
+ by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
+by (etac allE 1);
+by (etac impE 1);
+ by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
val lemma = result();
val prems = Goal
"[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
-br (lemma RS mp) 1;
+by (rtac (lemma RS mp) 1);
by (REPEAT(ares_tac prems 1));
qed "finite_psubset_induct";
@@ -268,65 +268,65 @@
(** Towards the induction rule **)
Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
-be finite_induct 1;
-by(Auto_tac);
+by (etac finite_induct 1);
+by (Auto_tac);
qed "setsum_0";
Addsimps [setsum_0];
Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
-be finite_induct 1;
-by(Auto_tac);
+by (etac finite_induct 1);
+by (Auto_tac);
val lemma = result();
Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
-bd lemma 1;
-by(Fast_tac 1);
+by (dtac lemma 1);
+by (Fast_tac 1);
qed "setsum_SucD";
Goal "[| finite F; 0 < f a |] ==> \
\ setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
-be finite_induct 1;
-by(Auto_tac);
- by(asm_simp_tac (simpset() addsimps add_ac) 1);
-by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
-by(Auto_tac);
+by (etac finite_induct 1);
+by (Auto_tac);
+ by (asm_simp_tac (simpset() addsimps add_ac) 1);
+by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
+by (Auto_tac);
qed "setsum_decr";
val prems = Goalw [multiset_def]
"[| P(%a.0); \
\ !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
\ ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
- by(Clarify_tac 1);
- by(subgoal_tac "f = (%a.0)" 1);
- by(Asm_simp_tac 1);
- brs prems 1;
- br ext 1;
- by(Force_tac 1);
-by(Clarify_tac 1);
-by(forward_tac [setsum_SucD] 1);
- ba 1;
-by(Clarify_tac 1);
-by(rename_tac "a" 1);
-by(subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
- be (rotate_prems 1 finite_subset) 2;
- by(Simp_tac 2);
- by(Blast_tac 2);
-by(subgoal_tac
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+ by (Clarify_tac 1);
+ by (subgoal_tac "f = (%a.0)" 1);
+ by (Asm_simp_tac 1);
+ by (resolve_tac prems 1);
+ by (rtac ext 1);
+ by (Force_tac 1);
+by (Clarify_tac 1);
+by (forward_tac [setsum_SucD] 1);
+ by (assume_tac 1);
+by (Clarify_tac 1);
+by (rename_tac "a" 1);
+by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
+ by (etac (rotate_prems 1 finite_subset) 2);
+ by (Simp_tac 2);
+ by (Blast_tac 2);
+by (subgoal_tac
"f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
- br ext 2;
- by(Asm_simp_tac 2);
-by(EVERY1[etac ssubst, resolve_tac prems]);
- by(Blast_tac 1);
-by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
- by(Blast_tac 1);
-by(asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
-by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
- by(Blast_tac 2);
-by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
- by(Blast_tac 2);
-by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
+ by (rtac ext 2);
+ by (Asm_simp_tac 2);
+by (EVERY1[etac ssubst, resolve_tac prems]);
+ by (Blast_tac 1);
+by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
+ by (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
+by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
+ by (Blast_tac 2);
+by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
+ by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
addcongs [conj_cong]) 1);
val lemma = result();
@@ -334,22 +334,22 @@
"[| f : multiset; \
\ P(%a.0); \
\ !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
-by(rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
-by(REPEAT(ares_tac (refl::prems) 1));
+by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
+by (REPEAT(ares_tac (refl::prems) 1));
qed "Rep_multiset_induct";
val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
"[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
by (rtac (Rep_multiset_inverse RS subst) 1);
by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
- by(rtac prem1 1);
-by(Clarify_tac 1);
-by(subgoal_tac
+ by (rtac prem1 1);
+by (Clarify_tac 1);
+by (subgoal_tac
"f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
- by(Simp_tac 2);
-be ssubst 1;
-by(etac (Abs_multiset_inverse RS subst) 1);
-by(etac(simplify (simpset()) prem2)1);
+ by (Simp_tac 2);
+by (etac ssubst 1);
+by (etac (Abs_multiset_inverse RS subst) 1);
+by (etac(simplify (simpset()) prem2)1);
qed "multiset_induct";
Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
@@ -357,14 +357,14 @@
Goal
"(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
-by(simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
-by(Auto_tac);
+by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
+by (Auto_tac);
qed "add_eq_conv_ex";
(** order **)
Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "not_less_empty";
AddIffs [not_less_empty];
@@ -372,22 +372,22 @@
"(N,M0 + {#a#}) : mult1(r) = \
\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
\ (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
-br iffI 1;
- by(asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
- by(Clarify_tac 1);
- be disjE 1;
- by(Blast_tac 1);
- by(Clarify_tac 1);
- by(res_inst_tac [("x","Ka+K")] exI 1);
- by(simp_tac (simpset() addsimps union_ac) 1);
- by(Blast_tac 1);
-be disjE 1;
- by(Clarify_tac 1);
- by(res_inst_tac [("x","aa")] exI 1);
- by(res_inst_tac [("x","M0+{#a#}")] exI 1);
- by(res_inst_tac [("x","K")] exI 1);
- by(simp_tac (simpset() addsimps union_ac) 1);
-by(Blast_tac 1);
+by (rtac iffI 1);
+ by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
+ by (Clarify_tac 1);
+ by (etac disjE 1);
+ by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (res_inst_tac [("x","Ka+K")] exI 1);
+ by (simp_tac (simpset() addsimps union_ac) 1);
+ by (Blast_tac 1);
+by (etac disjE 1);
+ by (Clarify_tac 1);
+ by (res_inst_tac [("x","aa")] exI 1);
+ by (res_inst_tac [("x","M0+{#a#}")] exI 1);
+ by (res_inst_tac [("x","K")] exI 1);
+ by (simp_tac (simpset() addsimps union_ac) 1);
+by (Blast_tac 1);
qed "less_add_conv";
Open_locale "MSOrd";
@@ -398,47 +398,47 @@
"[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
\ !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
\ ==> M0+{#a#} : W";
-br accI 1;
-by(rename_tac "N" 1);
-by(full_simp_tac (simpset() addsimps [less_add_conv]) 1);
-be disjE 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(rotate_tac ~1 1);
-be rev_mp 1;
-by(res_inst_tac [("M","K")] multiset_induct 1);
- by(Asm_simp_tac 1);
-by(simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
-by(Blast_tac 1);
+by (rtac accI 1);
+by (rename_tac "N" 1);
+by (full_simp_tac (simpset() addsimps [less_add_conv]) 1);
+by (etac disjE 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rotate_tac ~1 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("M","K")] multiset_induct 1);
+ by (Asm_simp_tac 1);
+by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
+by (Blast_tac 1);
qed "lemma1";
Goalw [W_def]
"[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
-be acc_induct 1;
-by(blast_tac (claset() addIs [export lemma1]) 1);
+by (etac acc_induct 1);
+by (blast_tac (claset() addIs [export lemma1]) 1);
qed "lemma2";
Goalw [W_def]
"wf(r) ==> !M:W. M+{#a#} : W";
-by(eres_inst_tac [("a","a")] wf_induct 1);
-by(blast_tac (claset() addIs [export lemma2]) 1);
+by (eres_inst_tac [("a","a")] wf_induct 1);
+by (blast_tac (claset() addIs [export lemma2]) 1);
qed "lemma3";
Goalw [W_def] "wf(r) ==> M : W";
-by(res_inst_tac [("M","M")] multiset_induct 1);
- br accI 1;
- by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addDs [export lemma3]) 1);
+by (res_inst_tac [("M","M")] multiset_induct 1);
+ by (rtac accI 1);
+ by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addDs [export lemma3]) 1);
qed "all_accessible";
Close_locale "MSOrd";
Goal "wf(r) ==> wf(mult1 r)";
-by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
+by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
qed "wf_mult1";
Goalw [mult_def] "wf(r) ==> wf(mult r)";
-by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
+by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
qed "wf_mult";
(** Equivalence of mult with the usual (closure-free) def **)
@@ -446,7 +446,7 @@
(* Badly needed: a linear arithmetic tactic for multisets *)
Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})";
-by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
qed "diff_union_single_conv";
(* One direction *)
@@ -454,35 +454,35 @@
"trans r ==> \
\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
\ (!k : set_of K. ? j : set_of J. (k,j) : r))";
-be converse_trancl_induct 1;
- by(Clarify_tac 1);
- by(res_inst_tac [("x","M0")] exI 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
-by(case_tac "elem K a" 1);
- by(res_inst_tac [("x","I")] exI 1);
- by(Simp_tac 1);
- by(res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
- by(asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
- by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
- by(asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
- by(full_simp_tac (simpset() addsimps [trans_def]) 1);
- by(Blast_tac 1);
-by(subgoal_tac "elem I a" 1);
- by(res_inst_tac [("x","I-{#a#}")] exI 1);
- by(res_inst_tac [("x","J+{#a#}")] exI 1);
- by(res_inst_tac [("x","K + Ka")] exI 1);
- br conjI 1;
- by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
+by (etac converse_trancl_induct 1);
+ by (Clarify_tac 1);
+ by (res_inst_tac [("x","M0")] exI 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
+by (case_tac "elem K a" 1);
+ by (res_inst_tac [("x","I")] exI 1);
+ by (Simp_tac 1);
+ by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
+ by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
+ by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
+ by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
+ by (full_simp_tac (simpset() addsimps [trans_def]) 1);
+ by (Blast_tac 1);
+by (subgoal_tac "elem I a" 1);
+ by (res_inst_tac [("x","I-{#a#}")] exI 1);
+ by (res_inst_tac [("x","J+{#a#}")] exI 1);
+ by (res_inst_tac [("x","K + Ka")] exI 1);
+ by (rtac conjI 1);
+ by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
addsplits [nat_diff_split]) 1);
- br conjI 1;
- by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
- by(Asm_full_simp_tac 1);
- by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
+ by (rtac conjI 1);
+ by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
+ by (Asm_full_simp_tac 1);
+ by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
addsplits [nat_diff_split]) 1);
- by(full_simp_tac (simpset() addsimps [trans_def]) 1);
- by(Blast_tac 1);
-by(subgoal_tac "elem (M0 +{#a#}) a" 1);
- by(Asm_full_simp_tac 1);
-by(Simp_tac 1);
+ by (full_simp_tac (simpset() addsimps [trans_def]) 1);
+ by (Blast_tac 1);
+by (subgoal_tac "elem (M0 +{#a#}) a" 1);
+ by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
qed "mult_implies_one_step";
--- a/src/HOL/Lex/RegExp2NA.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML Fri Jan 29 16:26:12 1999 +0100
@@ -9,37 +9,37 @@
(******************************************************)
Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "fin_atom";
Goalw [atom_def] "start (atom a) = [True]";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "start_atom";
Goalw [atom_def,step_def]
"(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "in_step_atom_Some";
Addsimps [in_step_atom_Some];
Goal
"([False],[False]) : steps (atom a) w = (w = [])";
by (induct_tac "w" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
qed "False_False_in_steps_atom";
Goal
"(start (atom a), [False]) : steps (atom a) w = (w = [a])";
by (induct_tac "w" 1);
- by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
-by(asm_full_simp_tac (simpset()
+ by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
+by (asm_full_simp_tac (simpset()
addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
qed "start_fin_in_steps_atom";
Goal
"accepts (atom a) w = (w = [a])";
-by(simp_tac(simpset() addsimps
+by (simp_tac(simpset() addsimps
[accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
qed "accepts_atom";
@@ -67,13 +67,13 @@
Goalw [union_def,step_def]
"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_in_step_union";
Goalw [union_def,step_def]
"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "False_in_step_union";
AddIffs [True_in_step_union,False_in_step_union];
@@ -102,8 +102,8 @@
"!L R. (start(union L R),q) : step(union L R) a = \
\ (? p. (q = True#p & (start L,p) : step L a) | \
\ (q = False#p & (start R,p) : step R a))";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed_spec_mp "start_step_union";
AddIffs [start_step_union];
@@ -112,17 +112,17 @@
\ ( (w = [] & q = start(union L R)) | \
\ (w ~= [] & (? p. q = True # p & (start L,p) : steps L w | \
\ q = False # p & (start R,p) : steps R w)))";
-by(exhaust_tac "w" 1);
+by (exhaust_tac "w" 1);
by (Asm_simp_tac 1);
- by(Blast_tac 1);
+ by (Blast_tac 1);
by (Asm_simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "steps_union";
Goalw [union_def]
"!L R. fin (union L R) (start(union L R)) = \
\ (fin L (start L) | fin R (start R))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "fin_start_union";
AddIffs [fin_start_union];
@@ -130,8 +130,8 @@
"accepts (union L R) w = (accepts L w | accepts R w)";
by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
(* get rid of case_tac: *)
-by(case_tac "w = []" 1);
-by(Auto_tac);
+by (case_tac "w = []" 1);
+by (Auto_tac);
qed "accepts_union";
AddIffs [accepts_union];
@@ -160,14 +160,14 @@
\ ((? r. q=True#r & (p,r): step L a) | \
\ (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_step_conc";
Goalw [conc_def,step_def]
"!L R. (False#p,q) : step (conc L R) a = \
\ (? r. q = False#r & (p,r) : step R a)";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "False_step_conc";
AddIffs [True_step_conc, False_step_conc];
@@ -185,16 +185,16 @@
Goal
"!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
by (Simp_tac 1);
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_True_steps_concI";
Goal
"!L R. (True#p,False#q) : step (conc L R) a = \
\ (fin L p & (start R,q) : step R a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "True_False_step_conc";
AddIffs [True_False_step_conc];
@@ -205,26 +205,26 @@
\ (? r. (p,r) : steps L u & fin L r & \
\ (? s. (start R,s) : step R a & \
\ (? t. (s,t) : steps R v & q = False#t)))))";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
-be disjE 1;
- by(clarify_tac (claset() delrules [disjCI]) 1);
- by(etac allE 1 THEN mp_tac 1);
- be disjE 1;
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (etac disjE 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac allE 1 THEN mp_tac 1);
+ by (etac disjE 1);
by (Blast_tac 1);
- br disjI2 1;
+ by (rtac disjI2 1);
by (Clarify_tac 1);
- by(Simp_tac 1);
- by(res_inst_tac[("x","a#u")] exI 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
+ by (res_inst_tac[("x","a#u")] exI 1);
+ by (Simp_tac 1);
by (Blast_tac 1);
-br disjI2 1;
+by (rtac disjI2 1);
by (Clarify_tac 1);
-by(Simp_tac 1);
-by(res_inst_tac[("x","[]")] exI 1);
-by(Simp_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac[("x","[]")] exI 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed_spec_mp "True_steps_concD";
@@ -235,7 +235,7 @@
\ (? r. (p,r) : steps L u & fin L r & \
\ (? s. (start R,s) : step R a & \
\ (? t. (s,t) : steps R v & q = False#t)))))";
-by(force_tac (claset() addDs [True_steps_concD]
+by (force_tac (claset() addDs [True_steps_concD]
addIs [True_True_steps_concI],simpset()) 1);
qed "True_steps_conc";
@@ -243,7 +243,7 @@
Goalw [conc_def]
"!L R. start(conc L R) = True#start L";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "start_conc";
Goalw [conc_def]
@@ -257,27 +257,27 @@
"accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
by (simp_tac (simpset() addsimps
[accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
-br iffI 1;
+by (rtac iffI 1);
by (Clarify_tac 1);
- be disjE 1;
+ by (etac disjE 1);
by (Clarify_tac 1);
- be disjE 1;
- by(res_inst_tac [("x","w")] exI 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
- by(Blast_tac 1);
- be disjE 1;
- by(Blast_tac 1);
+ by (etac disjE 1);
+ by (res_inst_tac [("x","w")] exI 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+ by (Blast_tac 1);
+ by (etac disjE 1);
+ by (Blast_tac 1);
by (Clarify_tac 1);
- by(res_inst_tac [("x","u")] exI 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
+ by (res_inst_tac [("x","u")] exI 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
by (Clarify_tac 1);
-by(exhaust_tac "v" 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
+by (exhaust_tac "v" 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
qed "accepts_conc";
(******************************************************)
@@ -285,19 +285,19 @@
(******************************************************)
Goalw [epsilon_def,step_def] "step epsilon a = {}";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "step_epsilon";
Addsimps [step_epsilon];
Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
-by(induct_tac "w" 1);
-by(Auto_tac);
+by (induct_tac "w" 1);
+by (Auto_tac);
qed "steps_epsilon";
Goal "accepts epsilon w = (w = [])";
-by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
-by(simp_tac (simpset() addsimps [epsilon_def]) 1);
+by (simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
+by (simp_tac (simpset() addsimps [epsilon_def]) 1);
qed "accepts_epsilon";
AddIffs [accepts_epsilon];
@@ -306,41 +306,41 @@
(******************************************************)
Goalw [plus_def] "!A. start (plus A) = start A";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "start_plus";
Addsimps [start_plus];
Goalw [plus_def] "!A. fin (plus A) = fin A";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "fin_plus";
AddIffs [fin_plus];
Goalw [plus_def,step_def]
"!A. (p,q) : step A a --> (p,q) : step (plus A) a";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "step_plusI";
Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(blast_tac (claset() addIs [step_plusI]) 1);
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [step_plusI]) 1);
qed_spec_mp "steps_plusI";
Goalw [plus_def,step_def]
"!A. (p,r): step (plus A) a = \
\ ( (p,r): step A a | fin A p & (start A,r) : step A a )";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "step_plus_conv";
AddIffs [step_plus_conv];
Goal
"[| (start A,q) : steps A u; u ~= []; fin A p |] \
\ ==> (p,q) : steps (plus A) u";
-by(exhaust_tac "u" 1);
- by(Blast_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [steps_plusI]) 1);
+by (exhaust_tac "u" 1);
+ by (Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [steps_plusI]) 1);
qed "fin_steps_plusI";
(* reverse list induction! Complicates matters for conc? *)
@@ -349,24 +349,24 @@
\ (? us v. w = concat us @ v & \
\ (!u:set us. u ~= [] & accepts A u) & \
\ (start A,r) : steps A v)";
-by(rev_induct_tac "w" 1);
+by (rev_induct_tac "w" 1);
by (Simp_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
+ by (res_inst_tac [("x","[]")] exI 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by(etac allE 1 THEN mp_tac 1);
+by (etac allE 1 THEN mp_tac 1);
by (Clarify_tac 1);
-be disjE 1;
- by(res_inst_tac [("x","us")] exI 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
-by(exhaust_tac "v" 1);
- by(res_inst_tac [("x","us")] exI 1);
- by(Asm_full_simp_tac 1);
-by(res_inst_tac [("x","us@[v]")] exI 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by(Blast_tac 1);
+by (etac disjE 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
+by (exhaust_tac "v" 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","us@[v]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (Blast_tac 1);
qed_spec_mp "start_steps_plusD";
Goal
@@ -374,54 +374,54 @@
\ (? us v. w = concat us @ v & \
\ (!u:set us. accepts A u) & \
\ (start A,r) : steps A v)";
-by(rev_induct_tac "w" 1);
+by (rev_induct_tac "w" 1);
by (Simp_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
+ by (res_inst_tac [("x","[]")] exI 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by(etac allE 1 THEN mp_tac 1);
+by (etac allE 1 THEN mp_tac 1);
by (Clarify_tac 1);
-be disjE 1;
- by(res_inst_tac [("x","us")] exI 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
-by(res_inst_tac [("x","us@[v]")] exI 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by(Blast_tac 1);
+by (etac disjE 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
+by (res_inst_tac [("x","us@[v]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (Blast_tac 1);
qed_spec_mp "start_steps_plusD";
Goal
"us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
-by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by(rev_induct_tac "us" 1);
- by(Simp_tac 1);
-by(rename_tac "u us" 1);
-by(Simp_tac 1);
+by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (rev_induct_tac "us" 1);
+ by (Simp_tac 1);
+by (rename_tac "u us" 1);
+by (Simp_tac 1);
by (Clarify_tac 1);
-by(case_tac "us = []" 1);
- by(Asm_full_simp_tac 1);
- by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (case_tac "us = []" 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
by (Clarify_tac 1);
-by(case_tac "u = []" 1);
- by(Asm_full_simp_tac 1);
- by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (case_tac "u = []" 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
qed_spec_mp "steps_star_cycle";
Goal
"accepts (plus A) w = \
\ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
-br iffI 1;
- by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (rtac iffI 1);
+ by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
by (Clarify_tac 1);
- bd start_steps_plusD 1;
+ by (dtac start_steps_plusD 1);
by (Clarify_tac 1);
- by(res_inst_tac [("x","us@[v]")] exI 1);
- by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [steps_star_cycle]) 1);
+ by (res_inst_tac [("x","us@[v]")] exI 1);
+ by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [steps_star_cycle]) 1);
qed "accepts_plus";
AddIffs [accepts_plus];
@@ -432,24 +432,24 @@
Goalw [star_def]
"accepts (star A) w = \
\ (? us. (!u : set us. accepts A u) & w = concat us)";
-br iffI 1;
+by (rtac iffI 1);
by (Clarify_tac 1);
- be disjE 1;
- by(res_inst_tac [("x","[]")] exI 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
- by(Blast_tac 1);
-by(Force_tac 1);
+ by (etac disjE 1);
+ by (res_inst_tac [("x","[]")] exI 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+ by (Blast_tac 1);
+by (Force_tac 1);
qed "accepts_star";
(***** Correctness of r2n *****)
Goal
"!w. accepts (rexp2na r) w = (w : lang r)";
-by(induct_tac "r" 1);
- by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
- by(simp_tac(simpset() addsimps [accepts_atom]) 1);
- by(Asm_simp_tac 1);
- by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
-by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
+by (induct_tac "r" 1);
+ by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by (simp_tac(simpset() addsimps [accepts_atom]) 1);
+ by (Asm_simp_tac 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
+by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
qed_spec_mp "accepts_rexp2na";
--- a/src/HOL/Lex/RegSet.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Lex/RegSet.ML Fri Jan 29 16:26:12 1999 +0100
@@ -16,7 +16,7 @@
Goal
"w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
by (rtac iffI 1);
- be star.induct 1;
+ by (etac star.induct 1);
by (res_inst_tac [("x","[]")] exI 1);
by (Simp_tac 1);
by (Clarify_tac 1);
--- a/src/HOL/List.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/List.ML Fri Jan 29 16:26:12 1999 +0100
@@ -384,7 +384,7 @@
val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
by (stac (rev_rev_ident RS sym) 1);
-br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
+by (res_inst_tac [("list", "rev xs")] list.induct 1);
by (ALLGOALS Simp_tac);
by (resolve_tac prems 1);
by (eresolve_tac prems 1);
@@ -571,7 +571,7 @@
section "nth";
Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
-by(simp_tac (simpset() addsplits [nat.split]) 1);
+by (simp_tac (simpset() addsplits [nat.split]) 1);
qed "nth_Cons";
Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
@@ -630,9 +630,9 @@
Addsimps [length_list_update];
Goal "!i j. i < length xs --> (xs[i:=x])!j = (if i=j then x else xs!j)";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
qed_spec_mp "nth_list_update";
@@ -874,13 +874,13 @@
(* Does not terminate! *)
Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
-by(induct_tac "j" 1);
+by (induct_tac "j" 1);
by Auto_tac;
qed "upt_rec";
Goal "j<=i ==> [i..j(] = []";
-by(stac upt_rec 1);
-by(Asm_simp_tac 1);
+by (stac upt_rec 1);
+by (Asm_simp_tac 1);
qed "upt_conv_Nil";
Addsimps [upt_conv_Nil];
@@ -889,27 +889,27 @@
qed "upt_Suc";
Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
-br trans 1;
-by(stac upt_rec 1);
-br refl 2;
+by (rtac trans 1);
+by (stac upt_rec 1);
+by (rtac refl 2);
by (Asm_simp_tac 1);
qed "upt_conv_Cons";
Goal "length [i..j(] = j-i";
-by(induct_tac "j" 1);
+by (induct_tac "j" 1);
by (Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
qed "length_upt";
Addsimps [length_upt];
Goal "i+k < j --> [i..j(] ! k = i+k";
-by(induct_tac "j" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
-by(Clarify_tac 1);
-by(subgoal_tac "n=i+k" 1);
- by(Asm_simp_tac 2);
-by(Asm_simp_tac 1);
+by (induct_tac "j" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
+by (Clarify_tac 1);
+by (subgoal_tac "n=i+k" 1);
+ by (Asm_simp_tac 2);
+by (Asm_simp_tac 1);
qed_spec_mp "nth_upt";
Addsimps [nth_upt];
--- a/src/HOL/Quot/FRACT.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Quot/FRACT.ML Fri Jan 29 16:26:12 1999 +0100
@@ -7,11 +7,11 @@
Goalw [per_def,per_NP_def]
"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
-br refl 1;
+by (rtac refl 1);
qed "inst_NP_per";
Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
-br per_class_eqI 1;
+by (rtac per_class_eqI 1);
by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
qed "test";
--- a/src/HOL/Quot/HQUOT.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Quot/HQUOT.ML Fri Jan 29 16:26:12 1999 +0100
@@ -124,33 +124,33 @@
(* theorems for any_in *)
Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
-br selectI2 1;
-br refl 1;
+by (rtac selectI2 1);
+by (rtac refl 1);
by (fold_goals_tac [peclass_def]);
-be er_class_eqE 1;
+by (etac er_class_eqE 1);
qed "er_any_in_class";
Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
-br selectI2 1;
-br refl 1;
+by (rtac selectI2 1);
+by (rtac refl 1);
by (fold_goals_tac [peclass_def]);
-br per_sym 1;
-be per_class_eqE 1;
-be sym 1;
+by (rtac per_sym 1);
+by (etac per_class_eqE 1);
+by (etac sym 1);
qed "per_any_in_class";
Goal "<[any_in (s::'a::er quot)]> = s";
-br per_class_all 1;
-br allI 1;
-br (er_any_in_class RS per_class_eqI) 1;
+by (rtac per_class_all 1);
+by (rtac allI 1);
+by (rtac (er_any_in_class RS per_class_eqI) 1);
qed "er_class_any_in";
(* equivalent theorem for per would need !x.x:D *)
Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
-br per_class_all 1;
-br allI 1;
-br (per_any_in_class RS per_class_eqI) 1;
-be spec 1;
+by (rtac per_class_all 1);
+by (rtac allI 1);
+by (rtac (per_any_in_class RS per_class_eqI) 1);
+by (etac spec 1);
qed "per_class_any_in";
(* is like theorem for class er *)
--- a/src/HOL/Quot/PER.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Quot/PER.ML Fri Jan 29 16:26:12 1999 +0100
@@ -12,7 +12,7 @@
(* Witness that quot is not empty *)
Goal "?z:{s.? r.!y. y:s=y===r}";
-br CollectI 1;
+by (rtac CollectI 1);
by (res_inst_tac [("x","x")] exI 1);
by (rtac allI 1);
by (rtac mem_Collect_eq 1);
--- a/src/HOL/Real/Real.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Real/Real.ML Fri Jan 29 16:26:12 1999 +0100
@@ -243,8 +243,8 @@
qed "real_less_add_left_cancel";
Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
-be real_less_trans 1;
-bd real_add_less_mono2 1;
+by (etac real_less_trans 1);
+by (dtac real_add_less_mono2 1);
by (Full_simp_tac 1);
qed "real_add_order";
@@ -255,9 +255,9 @@
qed "real_le_add_order";
Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
-bd real_add_less_mono1 1;
-be real_less_trans 1;
-be real_add_less_mono2 1;
+by (dtac real_add_less_mono1 1);
+by (etac real_less_trans 1);
+by (etac real_add_less_mono2 1);
qed "real_add_less_mono";
Goal "!!(q1::real). q1 <= q2 ==> x + q1 <= x + q2";
@@ -265,8 +265,8 @@
qed "real_add_left_le_mono1";
Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::real)";
-bd real_add_le_mono1 1;
-be real_le_trans 1;
+by (dtac real_add_le_mono1 1);
+by (etac real_le_trans 1);
by (Simp_tac 1);
qed "real_add_le_mono";
--- a/src/HOL/Trancl.ML Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Trancl.ML Fri Jan 29 16:26:12 1999 +0100
@@ -312,7 +312,7 @@
\ ==> P(a)";
by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
by (resolve_tac prems 1);
- be converseD 1;
+ by (etac converseD 1);
by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
qed "converse_trancl_induct";