# HG changeset patch # User paulson # Date 843734867 -7200 # Node ID 03a843f0f4472cbf50faf608bf698c972a2e2c92 # Parent 474b3f208789031d17a058244b198a7c5570949c Ran expandshort diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Arith.ML Thu Sep 26 12:47:47 1996 +0200 @@ -164,7 +164,7 @@ (*Associative law for multiplication*) qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" (fn _ => [nat_ind_tac "m" 1, - ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]); + ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]); qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, @@ -539,7 +539,7 @@ (*strict, in 1st argument; proof is by induction on k>0*) goal Arith.thy "!!i::nat. [| i k*i < k*j"; -be zero_less_natE 1; +by (etac zero_less_natE 1); by (Asm_simp_tac 1); by (nat_ind_tac "x" 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono]))); @@ -564,26 +564,26 @@ by (res_inst_tac [("n","m")] less_induct 1); by (case_tac "na (k*m) mod (k*n) = k * (m mod n)"; by (res_inst_tac [("n","m")] less_induct 1); by (case_tac "na P(y-{x}) \ \ |] ==> c<=b --> P(b-c)"; by (rtac (major RS Fin_induct) 1); -by (rtac (Diff_insert RS ssubst) 2); +by (stac Diff_insert 2); by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems@[Diff_subset RS Fin_subset])))); val lemma = result(); @@ -259,7 +259,7 @@ [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1); by (simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq] - addcongs [rev_conj_cong]) 1); + addcongs [rev_conj_cong]) 1); be subst 1; br refl 1; by (rtac notI 1); @@ -290,7 +290,7 @@ qed "card_Suc_Diff"; goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A"; -by (resolve_tac [Suc_less_SucD] 1); +by (rtac Suc_less_SucD 1); by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1); qed "card_Diff"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Fun.ML --- a/src/HOL/Fun.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Fun.ML Thu Sep 26 12:47:47 1996 +0200 @@ -173,7 +173,7 @@ ComplI, IntI, DiffI, UnCI, insertCI]; AddIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE, - make_elim singleton_inject, + make_elim singleton_inject, CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; AddEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D, subsetD, subsetCE]; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/HOL.ML Thu Sep 26 12:47:47 1996 +0200 @@ -214,22 +214,22 @@ [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ - rtac classical 1, - dtac p2 1, - etac notE 1, - rtac p1 1]); + rtac classical 1, + dtac p2 1, + etac notE 1, + rtac p1 1]); qed_goal "swap2" HOL.thy "[| P; Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [ - rtac notI 1, - dtac p2 1, - etac notE 1, - rtac p1 1]); + rtac notI 1, + dtac p2 1, + etac notE 1, + rtac p1 1]); (** Unique existence **) section "?!"; qed_goalw "ex1I" HOL.thy [Ex1_def] - "[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)" + "[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)" (fn prems => [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Hoare/Arith2.ML --- a/src/HOL/Hoare/Arith2.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Hoare/Arith2.ML Thu Sep 26 12:47:47 1996 +0200 @@ -30,16 +30,16 @@ \ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \ \ |] ==> P m n k"; by (res_inst_tac [("x","m")] spec 1); -br diff_induct 1; -br allI 1; -br allI 2; +by (rtac diff_induct 1); +by (rtac allI 1); +by (rtac allI 2); by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1); by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4); -br allI 7; +by (rtac allI 7); by (nat_ind_tac "xa" 7); by (ALLGOALS (resolve_tac prems)); -ba 1; -ba 1; +by (assume_tac 1); +by (assume_tac 1); by (Fast_tac 1); by (Fast_tac 1); qed "diff_induct3"; @@ -48,33 +48,33 @@ val prems=goal Arith.thy "~m (m - n) - k = m - ((n + k)::nat)"; by (cut_facts_tac prems 1); -br mp 1; -ba 2; +by (rtac mp 1); +by (assume_tac 2); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); by (ALLGOALS Asm_simp_tac); qed "diff_not_assoc"; val prems=goal Arith.thy "[|~m (m - n) + k = m - ((n - k)::nat)"; by (cut_facts_tac prems 1); -bd conjI 1; -ba 1; +by (dtac conjI 1); +by (assume_tac 1); by (res_inst_tac [("P","~m (m + n) - k = m + ((n - k)::nat)"; by (cut_facts_tac prems 1); -br mp 1; -ba 2; +by (rtac mp 1); +by (assume_tac 2); by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); by (ALLGOALS Asm_simp_tac); qed "add_diff_assoc"; @@ -82,12 +82,12 @@ (*** more ***) val prems = goal Arith.thy "m~=(n::nat) = (m n-m~=0"; @@ -117,7 +117,7 @@ by (res_inst_tac [("n","k")] natE 1); by (ALLGOALS Asm_full_simp_tac); by (nat_ind_tac "x" 1); -be add_less_mono 2; +by (etac add_less_mono 2); by (ALLGOALS Asm_full_simp_tac); qed "mult_less_mono_r"; @@ -126,8 +126,8 @@ by (nat_ind_tac "k" 1); by (ALLGOALS Simp_tac); by (fold_goals_tac [le_def]); -be add_le_mono 1; -ba 1; +by (etac add_le_mono 1); +by (assume_tac 1); qed "mult_not_less_mono_r"; val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k"; @@ -139,10 +139,10 @@ val prems = goal Arith.thy "[|0 m*k~=n*k"; by (cut_facts_tac prems 1); by (res_inst_tac [("P","m n mod n = 0"; by (cut_facts_tac prems 1); -br (mod_def RS wf_less_trans) 1; +by (rtac (mod_def RS wf_less_trans) 1); by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1); -be mod_less 1; +by (etac mod_less 1); qed "mod_nn_is_0"; val prems=goal thy "0 m mod n = (m+n) mod n"; by (cut_facts_tac prems 1); by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1); -br add_commute 1; +by (rtac add_commute 1); by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1); -br diff_add_inverse 1; -br sym 1; -be mod_geq 1; +by (rtac diff_add_inverse 1); +by (rtac sym 1); +by (etac mod_geq 1); by (res_inst_tac [("s","n<=n+m"),("t","~n+m m*n mod n = 0"; by (cut_facts_tac prems 1); by (nat_ind_tac "m" 1); by (Simp_tac 1); -be mod_less 1; +by (etac mod_less 1); by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1); by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1); qed "mod_prod_nn_is_0"; @@ -196,25 +196,25 @@ val prems=goal thy "[|0 (m+n) mod x = 0"; by (cut_facts_tac prems 1); by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (Asm_simp_tac 1); by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1); -br add_mult_distrib 1; -be mod_prod_nn_is_0 1; +by (rtac add_mult_distrib 1); +by (etac mod_prod_nn_is_0 1); qed "mod0_sum"; val prems=goal thy "[|0 (m-n) mod x = 0"; by (cut_facts_tac prems 1); by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (Asm_simp_tac 1); by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1); -br diff_mult_distrib 1; -be mod_prod_nn_is_0 1; +by (rtac diff_mult_distrib 1); +by (etac mod_prod_nn_is_0 1); qed "mod0_diff"; @@ -223,11 +223,11 @@ val prems = goal thy "0 m*n div n = m"; by (cut_facts_tac prems 1); -br (mult_not_eq_mono_r RS not_imp_swap) 1; -ba 1; -ba 1; +by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1); +by (assume_tac 1); +by (assume_tac 1); by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1); -ba 1; +by (assume_tac 1); by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1); by (Asm_simp_tac 1); qed "div_prod_nn_is_m"; @@ -243,32 +243,32 @@ val prems=goalw thy [divides_def] "x divides n ==> x<=n"; by (cut_facts_tac prems 1); -br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1; +by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1); by (Asm_simp_tac 1); -br (less_not_refl2 RS not_sym) 1; +by (rtac (less_not_refl2 RS not_sym) 1); by (Asm_simp_tac 1); qed "divides_le"; val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)"; by (cut_facts_tac prems 1); by (REPEAT ((dtac conjE 1) THEN (atac 2))); -br conjI 1; +by (rtac conjI 1); by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1); -ba 1; -be conjI 1; -br mod0_sum 1; +by (assume_tac 1); +by (etac conjI 1); +by (rtac mod0_sum 1); by (ALLGOALS atac); qed "divides_sum"; val prems=goalw thy [divides_def] "[|x divides m; x divides n; n x divides (m-n)"; by (cut_facts_tac prems 1); by (REPEAT ((dtac conjE 1) THEN (atac 2))); -br conjI 1; -be less_imp_diff_positive 1; -be conjI 1; -br mod0_diff 1; +by (rtac conjI 1); +by (etac less_imp_diff_positive 1); +by (etac conjI 1); +by (rtac mod0_diff 1); by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def]))); -be less_not_sym 1; +by (etac less_not_sym 1); qed "divides_diff"; @@ -277,16 +277,16 @@ val prems=goalw thy [cd_def] "0 cd n n n"; by (cut_facts_tac prems 1); -bd divides_nn 1; +by (dtac divides_nn 1); by (Asm_simp_tac 1); qed "cd_nnn"; val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n"; by (cut_facts_tac prems 1); -bd conjE 1; -ba 2; -bd divides_le 1; -bd divides_le 1; +by (dtac conjE 1); +by (assume_tac 2); +by (dtac divides_le 1); +by (dtac divides_le 1); by (Asm_simp_tac 1); qed "cd_le"; @@ -296,32 +296,32 @@ val prems=goalw thy [cd_def] "n cd x m n = cd x (m-n) n"; by (cut_facts_tac prems 1); -br iffI 1; -bd conjE 1; -ba 2; -br conjI 1; -br divides_diff 1; -bd conjE 5; -ba 6; -br conjI 5; -bd less_not_sym 5; -bd add_diff_inverse 5; +by (rtac iffI 1); +by (dtac conjE 1); +by (assume_tac 2); +by (rtac conjI 1); +by (rtac divides_diff 1); +by (dtac conjE 5); +by (assume_tac 6); +by (rtac conjI 5); +by (dtac less_not_sym 5); +by (dtac add_diff_inverse 5); by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5); by (ALLGOALS Asm_full_simp_tac); qed "cd_diff_l"; val prems=goalw thy [cd_def] "m cd x m n = cd x m (n-m)"; by (cut_facts_tac prems 1); -br iffI 1; -bd conjE 1; -ba 2; -br conjI 1; -br divides_diff 2; -bd conjE 5; -ba 6; -br conjI 5; -bd less_not_sym 6; -bd add_diff_inverse 6; +by (rtac iffI 1); +by (dtac conjE 1); +by (assume_tac 2); +by (rtac conjI 1); +by (rtac divides_diff 2); +by (dtac conjE 5); +by (assume_tac 6); +by (rtac conjI 5); +by (dtac less_not_sym 6); +by (dtac add_diff_inverse 6); by (dres_inst_tac [("n","n-m")] divides_sum 6); by (ALLGOALS Asm_full_simp_tac); qed "cd_diff_r"; @@ -331,15 +331,15 @@ val prems = goalw thy [gcd_def] "0 n = gcd n n"; by (cut_facts_tac prems 1); -bd cd_nnn 1; -br (select_equality RS sym) 1; -be conjI 1; -br allI 1; -br impI 1; -bd cd_le 1; -bd conjE 2; -ba 3; -br le_anti_sym 2; +by (dtac cd_nnn 1); +by (rtac (select_equality RS sym) 1); +by (etac conjI 1); +by (rtac allI 1); +by (rtac impI 1); +by (dtac cd_le 1); +by (dtac conjE 2); +by (assume_tac 3); +by (rtac le_anti_sym 2); by (dres_inst_tac [("x","x")] cd_le 2); by (dres_inst_tac [("x","n")] spec 3); by (ALLGOALS Asm_full_simp_tac); @@ -353,16 +353,16 @@ by (cut_facts_tac prems 1); by (subgoal_tac "n !x.cd x m n = cd x (m-n) n" 1); by (Asm_simp_tac 1); -br allI 1; -be cd_diff_l 1; +by (rtac allI 1); +by (etac cd_diff_l 1); qed "gcd_diff_l"; val prems=goalw thy [gcd_def] "m gcd m n = gcd m (n-m)"; by (cut_facts_tac prems 1); by (subgoal_tac "m !x.cd x m n = cd x m (n-m)" 1); by (Asm_simp_tac 1); -br allI 1; -be cd_diff_r 1; +by (rtac allI 1); +by (etac cd_diff_r 1); qed "gcd_diff_r"; @@ -381,7 +381,7 @@ by (nat_ind_tac "k" 1); by (ALLGOALS Asm_simp_tac); by (fold_goals_tac [pow_def]); -br (pow_add_reduce RS sym) 1; +by (rtac (pow_add_reduce RS sym) 1); qed "pow_pow_reduce"; (*** fac ***) diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Hoare/Examples.ML --- a/src/HOL/Hoare/Examples.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Hoare/Examples.ML Thu Sep 26 12:47:47 1996 +0200 @@ -14,8 +14,8 @@ "{m=0 & s=0} \ \ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\ \ {s = a*b}"; -by(hoare_tac 1); -by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac))); +by (hoare_tac 1); +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac))); qed "multiply_by_add"; @@ -78,7 +78,7 @@ by (subgoal_tac "a*a=a pow 2" 1); by (Asm_simp_tac 1); -by (rtac (pow_pow_reduce RS ssubst) 1); +by (stac pow_pow_reduce 1); by (subgoal_tac "(b div 2)*2=b" 1); by (subgoal_tac "0<2" 2); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Hoare/List_Examples.ML --- a/src/HOL/Hoare/List_Examples.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Hoare/List_Examples.ML Thu Sep 26 12:47:47 1996 +0200 @@ -6,11 +6,11 @@ \ y := hd x # y; x := tl x \ \ END \ \{y=rev(X)}"; -by(hoare_tac 1); -by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1); -by(safe_tac (!claset)); -by(Asm_full_simp_tac 1); -by(Asm_full_simp_tac 1); +by (hoare_tac 1); +by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1); +by (safe_tac (!claset)); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); qed "imperative_reverse"; goal thy @@ -21,9 +21,9 @@ \ y := hd x # y; x := tl x \ \ END \ \{y = X@Y}"; -by(hoare_tac 1); -by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1); -by(safe_tac (!claset)); -by(Asm_full_simp_tac 1); -by(Asm_full_simp_tac 1); +by (hoare_tac 1); +by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1); +by (safe_tac (!claset)); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); qed "imperative_append"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/IMP/Denotation.ML --- a/src/HOL/IMP/Denotation.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/IMP/Denotation.ML Thu Sep 26 12:47:47 1996 +0200 @@ -15,11 +15,11 @@ goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"; -by(Simp_tac 1); -by(EVERY[stac (Gamma_mono RS lfp_Tarski) 1, +by (Simp_tac 1); +by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1, stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1, - Simp_tac 1, - IF_UNSOLVED no_tac]); + Simp_tac 1, + IF_UNSOLVED no_tac]); qed "C_While_If"; @@ -31,7 +31,7 @@ by (etac evalc.induct 1); auto(); (* while *) -by(rewtac Gamma_def); +by (rewtac Gamma_def); by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); by (Fast_tac 1); by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); @@ -44,8 +44,8 @@ goal Denotation.thy "!s t. (s,t):C(c) --> -c-> t"; by (com.induct_tac "c" 1); -by(ALLGOALS Full_simp_tac); -by(ALLGOALS (TRY o Fast_tac)); +by (ALLGOALS Full_simp_tac); +by (ALLGOALS (TRY o Fast_tac)); (* while *) by (strip_tac 1); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/IMP/Hoare.ML --- a/src/HOL/IMP/Hoare.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/IMP/Hoare.ML Thu Sep 26 12:47:47 1996 +0200 @@ -24,38 +24,38 @@ qed "hoare_sound"; goalw Hoare.thy [swp_def] "swp SKIP Q = Q"; -by(Simp_tac 1); -br ext 1; +by (Simp_tac 1); +by (rtac ext 1); by (Fast_tac 1); qed "swp_SKIP"; goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))"; -by(Simp_tac 1); +by (Simp_tac 1); qed "swp_Ass"; goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)"; -by(Simp_tac 1); -br ext 1; +by (Simp_tac 1); +by (rtac ext 1); by (Fast_tac 1); qed "swp_Semi"; goalw Hoare.thy [swp_def] "swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \ \ (~b s --> swp d Q s))"; -by(Simp_tac 1); -br ext 1; +by (Simp_tac 1); +by (rtac ext 1); by (Fast_tac 1); qed "swp_If"; goalw Hoare.thy [swp_def] "!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s"; -by(stac C_While_If 1); -by(Asm_simp_tac 1); +by (stac C_While_If 1); +by (Asm_simp_tac 1); qed "swp_While_True"; goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s"; -by(stac C_While_If 1); -by(Asm_simp_tac 1); +by (stac C_While_If 1); +by (Asm_simp_tac 1); by (Fast_tac 1); qed "swp_While_False"; @@ -73,12 +73,12 @@ AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If]; goal Hoare.thy "!Q. |- {swp c Q} c {Q}"; -by(com.induct_tac "c" 1); -by(ALLGOALS Simp_tac); +by (com.induct_tac "c" 1); +by (ALLGOALS Simp_tac); by (REPEAT_FIRST Fast_tac); by (deepen_tac (!claset addIs [hoare.conseq]) 0 1); by (Step_tac 1); -br hoare.conseq 1; +by (rtac hoare.conseq 1); be thin_rl 1; by (Fast_tac 1); br hoare.While 1; @@ -91,13 +91,13 @@ by(safe_tac HOL_cs); by(rotate_tac ~1 1); by(Asm_full_simp_tac 1); -by(rotate_tac ~1 1); -by(Asm_full_simp_tac 1); +by (rotate_tac ~1 1); +by (Asm_full_simp_tac 1); qed_spec_mp "swp_is_pre"; goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}"; -br (swp_is_pre RSN (2,hoare.conseq)) 1; +by (rtac (swp_is_pre RSN (2,hoare.conseq)) 1); by (Fast_tac 2); -by(rewrite_goals_tac [hoare_valid_def,swp_def]); +by (rewrite_goals_tac [hoare_valid_def,swp_def]); by (Fast_tac 1); qed "hoare_relative_complete"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/IMP/Transition.ML --- a/src/HOL/IMP/Transition.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/IMP/Transition.ML Thu Sep 26 12:47:47 1996 +0200 @@ -23,30 +23,30 @@ AddIs evalc1.intrs; goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0"; -be rel_pow_E2 1; +by (etac rel_pow_E2 1); by (Asm_full_simp_tac 1); -by(Fast_tac 1); +by (Fast_tac 1); val hlemma = result(); goal Transition.thy "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ \ (c;d, s) -*-> (SKIP, u)"; -by(nat_ind_tac "n" 1); +by (nat_ind_tac "n" 1); (* case n = 0 *) by(fast_tac (!claset addIs [rtrancl_into_rtrancl2])1); (* induction step *) by (safe_tac (!claset addSDs [rel_pow_Suc_D2])); -by(split_all_tac 1); -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); +by (split_all_tac 1); +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); qed_spec_mp "lemma1"; goal Transition.thy "!!c s s1. -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; -be evalc.induct 1; +by (etac evalc.induct 1); (* SKIP *) -br rtrancl_refl 1; +by (rtac rtrancl_refl 1); (* ASSIGN *) by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); @@ -69,7 +69,7 @@ goal Transition.thy "!c d s u. (c;d,s) -n-> (SKIP,u) --> \ \ (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)"; -by(nat_ind_tac "n" 1); +by (nat_ind_tac "n" 1); (* case n = 0 *) by (fast_tac (!claset addss !simpset) 1); (* induction step *) @@ -93,17 +93,17 @@ by (fast_tac (!claset addSDs [lemma2,rel_pow_imp_rtrancl]) 1); (* IF *) -be rel_pow_E2 1; +by (etac rel_pow_E2 1); by (Asm_full_simp_tac 1); by (fast_tac (!claset addSDs [rel_pow_imp_rtrancl]) 1); (* WHILE, induction on the length of the computation *) -by(rotate_tac 1 1); +by (rotate_tac 1 1); by (etac rev_mp 1); by (res_inst_tac [("x","s")] spec 1); -by(res_inst_tac [("n","n")] less_induct 1); +by (res_inst_tac [("n","n")] less_induct 1); by (strip_tac 1); -be rel_pow_E2 1; +by (etac rel_pow_E2 1); by (Asm_full_simp_tac 1); by (eresolve_tac evalc1_Es 1); @@ -111,7 +111,7 @@ by (fast_tac (!claset addSDs [hlemma]) 1); (* WhileTrue *) -by(fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); +by (fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); qed_spec_mp "evalc1_impl_evalc"; @@ -128,17 +128,17 @@ goal Transition.thy "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \ \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; -be converse_rtrancl_induct2 1; -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); +by (etac converse_rtrancl_induct2 1); +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); qed_spec_mp "my_lemma1"; goal Transition.thy "!!c s s1. -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; -be evalc.induct 1; +by (etac evalc.induct 1); (* SKIP *) -br rtrancl_refl 1; +by (rtac rtrancl_refl 1); (* ASSIGN *) by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); @@ -193,15 +193,15 @@ goal Transition.thy "!!c s. ((c,s) -1-> (c',s')) ==> (!t. -c-> t --> -c-> t)"; -be evalc1.induct 1; +by (etac evalc1.induct 1); auto(); qed_spec_mp "FB_lemma3"; val [major] = goal Transition.thy "(c,s) -*-> (c',s') ==> -c-> t --> -c-> t"; -br (major RS rtrancl_induct2) 1; -by(Fast_tac 1); -by(fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1); +by (rtac (major RS rtrancl_induct2) 1); +by (Fast_tac 1); +by (fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1); qed_spec_mp "FB_lemma2"; goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> -c-> t"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/IMP/VC.ML --- a/src/HOL/IMP/VC.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/IMP/VC.ML Thu Sep 26 12:47:47 1996 +0200 @@ -13,7 +13,7 @@ val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]); goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}"; -by(acom.induct_tac "c" 1); +by (acom.induct_tac "c" 1); by(ALLGOALS Simp_tac); by(Fast_tac 1); by(Fast_tac 1); @@ -21,7 +21,7 @@ (* if *) by(Deepen_tac 4 1); (* while *) -by(safe_tac HOL_cs); +by (safe_tac HOL_cs); by (resolve_tac hoare.intrs 1); br lemma 1; brs hoare.intrs 1; @@ -30,19 +30,19 @@ qed "vc_sound"; goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)"; -by(acom.induct_tac "c" 1); +by (acom.induct_tac "c" 1); by(ALLGOALS Asm_simp_tac); -by(EVERY1[rtac allI, rtac allI, rtac impI]); -by(EVERY1[etac allE, etac allE, etac mp]); -by(EVERY1[etac allE, etac allE, etac mp, atac]); +by (EVERY1[rtac allI, rtac allI, rtac impI]); +by (EVERY1[etac allE, etac allE, etac mp]); +by (EVERY1[etac allE, etac allE, etac mp, atac]); qed_spec_mp "wp_mono"; goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"; -by(acom.induct_tac "c" 1); +by (acom.induct_tac "c" 1); by(ALLGOALS Asm_simp_tac); -by(safe_tac HOL_cs); -by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); -by(fast_tac (HOL_cs addEs [wp_mono]) 1); +by (safe_tac HOL_cs); +by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); +by (fast_tac (HOL_cs addEs [wp_mono]) 1); qed_spec_mp "vc_mono"; goal VC.thy @@ -64,12 +64,12 @@ by(res_inst_tac [("x","Awhile b Pa ac")] exI 1); by(Asm_simp_tac 1); by (safe_tac HOL_cs); -by(res_inst_tac [("x","ac")] exI 1); -by(Asm_simp_tac 1); -by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); +by (res_inst_tac [("x","ac")] exI 1); +by (Asm_simp_tac 1); +by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); qed "vc_complete"; goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)"; -by(acom.induct_tac "c" 1); -by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def]))); +by (acom.induct_tac "c" 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def]))); qed "vcwp_vc_wp"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Lambda/Commutation.ML --- a/src/HOL/Lambda/Commutation.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Lambda/Commutation.ML Thu Sep 26 12:47:47 1996 +0200 @@ -11,30 +11,30 @@ (*** square ***) goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T"; -by(Fast_tac 1); +by (Fast_tac 1); qed "square_sym"; goalw Commutation.thy [square_def] "!!R. [| square R S T U; T <= T' |] ==> square R S T' U"; -by(Fast_tac 1); +by (Fast_tac 1); qed "square_subset"; goalw Commutation.thy [square_def] "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)"; -by(Fast_tac 1); +by (Fast_tac 1); qed "square_reflcl"; goalw Commutation.thy [square_def] "!!R. square R S S T ==> square (R^*) S S (T^*)"; -by(strip_tac 1); +by (strip_tac 1); by (etac rtrancl_induct 1); -by(Fast_tac 1); -by(best_tac (!claset addSEs [rtrancl_into_rtrancl]) 1); +by (Fast_tac 1); +by (best_tac (!claset addSEs [rtrancl_into_rtrancl]) 1); qed "square_rtrancl"; goalw Commutation.thy [commute_def] "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)"; -by(fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl] +by (fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl] addEs [r_into_rtrancl] addss !simpset) 1); qed "square_rtrancl_reflcl_commute"; @@ -42,23 +42,23 @@ (*** commute ***) goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R"; -by(fast_tac (!claset addIs [square_sym]) 1); +by (fast_tac (!claset addIs [square_sym]) 1); qed "commute_sym"; goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)"; -by(fast_tac (!claset addIs [square_rtrancl,square_sym]) 1); +by (fast_tac (!claset addIs [square_rtrancl,square_sym]) 1); qed "commute_rtrancl"; goalw Commutation.thy [commute_def,square_def] "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T"; -by(Fast_tac 1); +by (Fast_tac 1); qed "commute_Un"; (*** diamond, confluence and union ***) goalw Commutation.thy [diamond_def] "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)"; -by(REPEAT(ares_tac [commute_Un,commute_sym] 1)); +by (REPEAT(ares_tac [commute_Un,commute_sym] 1)); qed "diamond_Un"; goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)"; @@ -67,20 +67,20 @@ goalw Commutation.thy [diamond_def] "!!R. square R R (R^=) (R^=) ==> confluent R"; -by(fast_tac (!claset addIs [square_rtrancl_reflcl_commute,r_into_rtrancl] +by (fast_tac (!claset addIs [square_rtrancl_reflcl_commute,r_into_rtrancl] addEs [square_subset]) 1); qed "square_reflcl_confluent"; goal Commutation.thy "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \ \ ==> confluent(R Un S)"; -br (rtrancl_Un_rtrancl RS subst) 1; +by (rtac (rtrancl_Un_rtrancl RS subst) 1); by (fast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1); qed "confluent_Un"; goal Commutation.thy "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)"; -by(fast_tac (!claset addIs [diamond_confluent] +by (fast_tac (!claset addIs [diamond_confluent] addDs [rtrancl_subset RS sym] addss !simpset) 1); qed "diamond_to_confluence"; @@ -92,9 +92,9 @@ by(fast_tac (HOL_cs addIs [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1); -by(safe_tac HOL_cs); +by (safe_tac HOL_cs); by (etac rtrancl_induct 1); by(Fast_tac 1); -by(slow_best_tac (!claset addIs [r_into_rtrancl] +by (slow_best_tac (!claset addIs [r_into_rtrancl] addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1); qed "Church_Rosser_confluent"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Lambda/Eta.ML --- a/src/HOL/Lambda/Eta.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Lambda/Eta.ML Thu Sep 26 12:47:47 1996 +0200 @@ -26,29 +26,29 @@ section "Arithmetic lemmas"; goal HOL.thy "!!P. P ==> P=True"; -by(fast_tac HOL_cs 1); +by (fast_tac HOL_cs 1); qed "True_eq"; Addsimps [less_not_sym RS True_eq]; goal Arith.thy "i < j --> pred i < j"; -by(nat_ind_tac "j" 1); -by(ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq]))); -by(nat_ind_tac "j1" 1); -by(ALLGOALS Asm_simp_tac); +by (nat_ind_tac "j" 1); +by (ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq]))); +by (nat_ind_tac "j1" 1); +by (ALLGOALS Asm_simp_tac); qed_spec_mp "less_imp_pred_less"; goal Arith.thy "i ~ pred j < i"; -by(nat_ind_tac "j" 1); -by(ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq]))); +by (nat_ind_tac "j" 1); +by (ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq]))); qed_spec_mp "less_imp_not_pred_less"; Addsimps [less_imp_not_pred_less]; goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i"; -by(nat_ind_tac "j" 1); -by(ALLGOALS Simp_tac); -by(simp_tac(!simpset addsimps [less_Suc_eq])1); -by(fast_tac (HOL_cs addDs [less_not_sym]) 1); +by (nat_ind_tac "j" 1); +by (ALLGOALS Simp_tac); +by (simp_tac(!simpset addsimps [less_Suc_eq])1); +by (fast_tac (HOL_cs addDs [less_not_sym]) 1); qed_spec_mp "less_interval1"; @@ -56,50 +56,50 @@ goal Eta.thy "!i k. free (lift t k) i = \ \ (i < k & free t i | k < i & free t (pred i))"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong]))); -by(fast_tac HOL_cs 2); -by(safe_tac (HOL_cs addSIs [iffI])); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong]))); +by (fast_tac HOL_cs 2); +by (safe_tac (HOL_cs addSIs [iffI])); by (dtac Suc_mono 1); -by(ALLGOALS(Asm_full_simp_tac)); -by(dtac less_trans_Suc 1 THEN atac 1); -by(dtac less_trans_Suc 2 THEN atac 2); -by(ALLGOALS(Asm_full_simp_tac)); +by (ALLGOALS(Asm_full_simp_tac)); +by (dtac less_trans_Suc 1 THEN atac 1); +by (dtac less_trans_Suc 2 THEN atac 2); +by (ALLGOALS(Asm_full_simp_tac)); qed "free_lift"; Addsimps [free_lift]; goal Eta.thy "!i k t. free (s[t/k]) i = \ \ (free s k & free t i | free s (if i t ==> !i. free t i = free s i"; by (etac eta.induct 1); -by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong]))); +by (ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong]))); qed_spec_mp "free_eta"; goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i"; -by(asm_simp_tac (!simpset addsimps [free_eta]) 1); +by (asm_simp_tac (!simpset addsimps [free_eta]) 1); qed "not_free_eta"; goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]"; -by(db.induct_tac "s" 1); -by(ALLGOALS(simp_tac (addsplit (!simpset)))); -by(fast_tac HOL_cs 1); -by(fast_tac HOL_cs 1); +by (db.induct_tac "s" 1); +by (ALLGOALS(simp_tac (addsplit (!simpset)))); +by (fast_tac HOL_cs 1); +by (fast_tac HOL_cs 1); qed_spec_mp "subst_not_free"; goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i"; @@ -108,8 +108,8 @@ goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]"; by (etac eta.induct 1); -by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def]))); -by(asm_simp_tac (!simpset addsimps [subst_decr]) 1); +by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def]))); +by (asm_simp_tac (!simpset addsimps [subst_decr]) 1); qed_spec_mp "eta_subst"; Addsimps [eta_subst]; @@ -122,11 +122,11 @@ goalw Eta.thy [square_def,id_def] "square eta eta (eta^=) (eta^=)"; by (rtac (impI RS allI RS allI) 1); by (etac eta.induct 1); -by(ALLGOALS(fast_tac (!claset addSEs [eta_decr,not_free_eta] addss !simpset))); +by (ALLGOALS(fast_tac (!claset addSEs [eta_decr,not_free_eta] addss !simpset))); val lemma = result(); goal Eta.thy "confluent(eta)"; -by(rtac (lemma RS square_reflcl_confluent) 1); +by (rtac (lemma RS square_reflcl_confluent) 1); qed "eta_confluent"; section "Congruence rules for -e>>"; @@ -155,69 +155,69 @@ goal Eta.thy "!!s t. s -> t ==> (!i. free t i --> free s i)"; by (etac beta.induct 1); -by(ALLGOALS(Asm_full_simp_tac)); +by (ALLGOALS(Asm_full_simp_tac)); qed_spec_mp "free_beta"; goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)"; by (etac beta.induct 1); -by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym]))); +by (ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym]))); qed_spec_mp "beta_decr"; goalw Eta.thy [decr_def] "decr (Var i) k = (if i<=k then Var i else Var(pred i))"; -by(simp_tac (addsplit (!simpset) addsimps [le_def]) 1); +by (simp_tac (addsplit (!simpset) addsimps [le_def]) 1); qed "decr_Var"; Addsimps [decr_Var]; goalw Eta.thy [decr_def] "decr (s@t) i = (decr s i)@(decr t i)"; -by(Simp_tac 1); +by (Simp_tac 1); qed "decr_App"; Addsimps [decr_App]; goalw Eta.thy [decr_def] "decr (Fun s) i = Fun (decr s (Suc i))"; -by(Simp_tac 1); +by (Simp_tac 1); qed "decr_Fun"; Addsimps [decr_Fun]; goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq]))); -by(fast_tac HOL_cs 1); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq]))); +by (fast_tac HOL_cs 1); qed "decr_not_free"; Addsimps [decr_not_free]; goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)"; by (etac eta.induct 1); -by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def]))); -by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1); +by (ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def]))); +by (asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1); qed_spec_mp "eta_lift"; Addsimps [eta_lift]; goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]"; -by(db.induct_tac "u" 1); -by(ALLGOALS(asm_simp_tac (addsplit (!simpset)))); -by(fast_tac (!claset addIs [r_into_rtrancl]) 1); -by(fast_tac (!claset addSIs [rtrancl_eta_App]) 1); -by(fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1); +by (db.induct_tac "u" 1); +by (ALLGOALS(asm_simp_tac (addsplit (!simpset)))); +by (fast_tac (!claset addIs [r_into_rtrancl]) 1); +by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1); +by (fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1); qed_spec_mp "rtrancl_eta_subst"; goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)"; by (rtac (impI RS allI RS allI) 1); by (etac beta.induct 1); -by(strip_tac 1); +by (strip_tac 1); by (eresolve_tac eta_cases 1); by (eresolve_tac eta_cases 1); -by(fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1); -by(slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1); -by(slow_tac (!claset addIs [rtrancl_eta_subst]) 1); -by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1); -by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1); -by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr] +by (fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1); +by (slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1); +by (slow_tac (!claset addIs [rtrancl_eta_subst]) 1); +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1); +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1); +by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr] addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1); qed "square_beta_eta"; goal Eta.thy "confluent(beta Un eta)"; -by(REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un, +by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un, beta_confluent,eta_confluent,square_beta_eta] 1)); qed "confluent_beta_eta"; @@ -225,7 +225,7 @@ section "Implicit definition of -e>: Fun(lift s 0 @ Var 0) -e> s"; goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)"; -by(db.induct_tac "s" 1); +by (db.induct_tac "s" 1); by(simp_tac (!simpset setloop (split_tac [expand_if])) 1); by(SELECT_GOAL(safe_tac HOL_cs)1); by(res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1); @@ -258,24 +258,24 @@ by(Simp_tac 1); by(fast_tac HOL_cs 1); by(Simp_tac 1); -by(Asm_simp_tac 1); -be thin_rl 1; -br allI 1; -br iffI 1; +by (Asm_simp_tac 1); +by (etac thin_rl 1); +by (rtac allI 1); +by (rtac iffI 1); be exE 1; by(res_inst_tac [("x","Fun t")] exI 1); by(Asm_simp_tac 1); -be exE 1; -be rev_mp 1; -by(res_inst_tac [("db","t")] db_case_distinction 1); +by (etac exE 1); +by (etac rev_mp 1); +by (res_inst_tac [("db","t")] db_case_distinction 1); by(simp_tac (!simpset setloop (split_tac [expand_if])) 1); by(Simp_tac 1); -by(Simp_tac 1); -by(fast_tac HOL_cs 1); +by (Simp_tac 1); +by (fast_tac HOL_cs 1); qed_spec_mp "not_free_iff_lifted"; goalw Eta.thy [decr_def] "(!s. (~free s 0) --> R(Fun(s @ Var 0))(decr s 0)) = \ \ (!s. R(Fun(lift s 0 @ Var 0))(s))"; -by(fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1); +by (fast_tac (HOL_cs addss (!simpset addsimps [lemma,not_free_iff_lifted])) 1); qed "explicit_is_implicit"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Lambda/Lambda.ML --- a/src/HOL/Lambda/Lambda.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Lambda/Lambda.ML Thu Sep 26 12:47:47 1996 +0200 @@ -14,22 +14,22 @@ goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k"; by (rtac le_less_trans 1); by (assume_tac 2); -by(asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1); -by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1); +by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1); +by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1); qed "lt_trans1"; goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k"; by (etac less_le_trans 1); -by(asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1); -by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1); +by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1); +by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1); qed "lt_trans2"; val major::prems = goal Nat.thy "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P"; by (rtac (major RS lessE) 1); -by(ALLGOALS Asm_full_simp_tac); -by(resolve_tac prems 1 THEN etac sym 1); -by(fast_tac (HOL_cs addIs prems) 1); +by (ALLGOALS Asm_full_simp_tac); +by (resolve_tac prems 1 THEN etac sym 1); +by (fast_tac (HOL_cs addIs prems) 1); qed "leqE"; goal Arith.thy "!!i. Suc i < j ==> i < pred j "; @@ -101,9 +101,9 @@ goal Lambda.thy "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; -by(db.induct_tac "t" 1); -by(ALLGOALS Asm_simp_tac); -by(strip_tac 1); +by (db.induct_tac "t" 1); +by (ALLGOALS Asm_simp_tac); +by (strip_tac 1); by (excluded_middle_tac "nat < i" 1); by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI]))); @@ -111,9 +111,9 @@ goal Lambda.thy "!i j s. j < Suc i --> \ \ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))); -by(strip_tac 1); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))); +by (strip_tac 1); by (excluded_middle_tac "nat < j" 1); by (Asm_full_simp_tac 1); by (eres_inst_tac [("j","nat")] leqE 1); @@ -130,9 +130,9 @@ goal Lambda.thy "!i j s. i < Suc j -->\ \ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))); -by(strip_tac 1); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))); +by (strip_tac 1); by (excluded_middle_tac "nat < j" 1); by (Asm_full_simp_tac 1); by (eres_inst_tac [("i","j")] leqE 1); @@ -141,26 +141,26 @@ (!simpset addsimps [less_SucI,gt_pred]))); by (hyp_subst_tac 1); by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1); -by(split_tac [expand_if] 1); +by (split_tac [expand_if] 1); by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1); qed "lift_subst_lt"; goal Lambda.thy "!k s. (lift t k)[s/k] = t"; -by(db.induct_tac "t" 1); -by(ALLGOALS Asm_simp_tac); -by(split_tac [expand_if] 1); -by(ALLGOALS Asm_full_simp_tac); +by (db.induct_tac "t" 1); +by (ALLGOALS Asm_simp_tac); +by (split_tac [expand_if] 1); +by (ALLGOALS Asm_full_simp_tac); qed "subst_lift"; Addsimps [subst_lift]; goal Lambda.thy "!i j u v. i < Suc j --> \ \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt]))); -by(strip_tac 1); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt]))); +by (strip_tac 1); by (excluded_middle_tac "nat < Suc(Suc j)" 1); -by(Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); by (forward_tac [lessI RS less_trans] 1); by (etac leqE 1); by (asm_simp_tac (!simpset addsimps [lt_pred]) 2); @@ -182,24 +182,24 @@ (*** Equivalence proof for optimized substitution ***) goal Lambda.thy "!k. liftn 0 t k = t"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac(addsplit(!simpset)))); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); qed "liftn_0"; Addsimps [liftn_0]; goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac(addsplit(!simpset)))); -by(fast_tac (HOL_cs addDs [add_lessD1]) 1); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); +by (fast_tac (HOL_cs addDs [add_lessD1]) 1); qed "liftn_lift"; Addsimps [liftn_lift]; goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]"; -by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac(addsplit(!simpset)))); +by (db.induct_tac "t" 1); +by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); qed "substn_subst_n"; Addsimps [substn_subst_n]; goal Lambda.thy "substn t s 0 = t[s/0]"; -by(Simp_tac 1); +by (Simp_tac 1); qed "substn_subst_0"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Lambda/ParRed.ML --- a/src/HOL/Lambda/ParRed.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Lambda/ParRed.ML Thu Sep 26 12:47:47 1996 +0200 @@ -21,13 +21,13 @@ (*** beta <= par_beta <= beta^* ***) goal ParRed.thy "(Var n => t) = (t = Var n)"; -by(Fast_tac 1); +by (Fast_tac 1); qed "par_beta_varL"; Addsimps [par_beta_varL]; goal ParRed.thy "t => t"; -by(db.induct_tac "t" 1); -by(ALLGOALS Asm_simp_tac); +by (db.induct_tac "t" 1); +by (ALLGOALS Asm_simp_tac); qed"par_beta_refl"; Addsimps [par_beta_refl]; (* AddSIs [par_beta_refl]; causes search to blow up *) @@ -50,21 +50,21 @@ (*** => ***) goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n"; -by(db.induct_tac "t" 1); -by(ALLGOALS(fast_tac (!claset addss (!simpset)))); +by (db.induct_tac "t" 1); +by (ALLGOALS(fast_tac (!claset addss (!simpset)))); qed_spec_mp "par_beta_lift"; Addsimps [par_beta_lift]; goal ParRed.thy "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"; -by(db.induct_tac "t" 1); +by (db.induct_tac "t" 1); by(asm_simp_tac (addsplit(!simpset)) 1); by(strip_tac 1); bes par_beta_cases 1; by(Asm_simp_tac 1); by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1); by(fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1); -by(fast_tac (!claset addss (!simpset)) 1); +by (fast_tac (!claset addss (!simpset)) 1); qed_spec_mp "par_beta_subst"; (*** Confluence (directly) ***) @@ -72,14 +72,14 @@ goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; by (rtac (impI RS allI RS allI) 1); by (etac par_beta.induct 1); -by(ALLGOALS(fast_tac (!claset addSIs [par_beta_subst]))); +by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst]))); qed "diamond_par_beta"; (*** cd ***) goal ParRed.thy "!t. s => t --> t => cd s"; -by(db.induct_tac "s" 1); +by (db.induct_tac "s" 1); by(Simp_tac 1); be rev_mp 1; by(db.induct_tac "db1" 1); @@ -89,10 +89,10 @@ (*** Confluence (via cd) ***) goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; -by(fast_tac (HOL_cs addIs [par_beta_cd]) 1); +by (fast_tac (HOL_cs addIs [par_beta_cd]) 1); qed "diamond_par_beta2"; goal ParRed.thy "confluent(beta)"; -by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, +by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, par_beta_subset_beta,beta_subset_par_beta]) 1); qed"beta_confluent"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/MiniML/I.ML --- a/src/HOL/MiniML/I.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/MiniML/I.ML Thu Sep 26 12:47:47 1996 +0200 @@ -116,11 +116,11 @@ goal I.thy "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)"; -by(cut_facts_tac [(read_instantiate[("x","id_subst")] +by (cut_facts_tac [(read_instantiate[("x","id_subst")] (read_instantiate[("x","[]")](thm RS spec) RS spec RS spec))] 1); -by(Full_simp_tac 1); -by(fast_tac HOL_cs 1); +by (Full_simp_tac 1); +by (fast_tac HOL_cs 1); qed; assuming that thm is the undischarged version of I_correct_wrt_W. @@ -149,23 +149,23 @@ be exE 1; by(split_all_tac 1); by(Full_simp_tac 1); -by(Asm_simp_tac 1); -by(strip_tac 1); -be exE 1; -by(REPEAT(etac conjE 1)); -by(split_all_tac 1); -by(Full_simp_tac 1); -bd lemma 1; +by (Asm_simp_tac 1); +by (strip_tac 1); +by (etac exE 1); +by (REPEAT(etac conjE 1)); +by (split_all_tac 1); +by (Full_simp_tac 1); +by (dtac lemma 1); by(fast_tac HOL_cs 1); -be exE 1; -be conjE 1; -by(hyp_subst_tac 1); -by(Asm_simp_tac 1); -br exI 1; -br conjI 1; +by (etac exE 1); +by (etac conjE 1); +by (hyp_subst_tac 1); +by (Asm_simp_tac 1); +by (rtac exI 1); +by (rtac conjI 1); br refl 1; -by(Simp_tac 1); -be disjE 1; +by (Simp_tac 1); +by (etac disjE 1); br disjI1 1; by(full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1); by(EVERY[etac allE 1, etac allE 1, etac allE 1, @@ -175,23 +175,23 @@ br new_tv_subst_comp_2 1; by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1); by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1); -br disjI2 1; -be exE 1; -by(split_all_tac 1); -be conjE 1; -by(Full_simp_tac 1); -bd lemma 1; +by (rtac disjI2 1); +by (etac exE 1); +by (split_all_tac 1); +by (etac conjE 1); +by (Full_simp_tac 1); +by (dtac lemma 1); br conjI 1; by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1); br new_tv_subst_comp_1 1; by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1); by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1); -be exE 1; -be conjE 1; -by(hyp_subst_tac 1); -by(asm_full_simp_tac (!simpset addsimps +by (etac exE 1); +by (etac conjE 1); +by (hyp_subst_tac 1); +by (asm_full_simp_tac (!simpset addsimps [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1); -by(asm_simp_tac (!simpset addcongs [conj_cong] addsimps +by (asm_simp_tac (!simpset addcongs [conj_cong] addsimps [eq_sym_conv,subst_comp_te RS sym,subst_comp_tel RS sym]) 1); qed_spec_mp "I_complete_wrt_W"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/MiniML/Maybe.ML --- a/src/HOL/MiniML/Maybe.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/MiniML/Maybe.ML Thu Sep 26 12:47:47 1996 +0200 @@ -21,8 +21,8 @@ goal Maybe.thy "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; -by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1); -by(fast_tac HOL_cs 1); +by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); +by (fast_tac HOL_cs 1); qed "bind_eq_Fail"; Addsimps [bind_eq_Fail]; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/MiniML/MiniML.ML --- a/src/HOL/MiniML/MiniML.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/MiniML/MiniML.ML Thu Sep 26 12:47:47 1996 +0200 @@ -16,7 +16,7 @@ (* case VarI *) by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1); -by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1); +by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1); (* case AbsI *) by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); (* case AppI *) diff -r 474b3f208789 -r 03a843f0f447 src/HOL/MiniML/ROOT.ML --- a/src/HOL/MiniML/ROOT.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/MiniML/ROOT.ML Thu Sep 26 12:47:47 1996 +0200 @@ -1,12 +1,12 @@ -(* Title: HOL/MiniML/ROOT.ML +(* Title: HOL/MiniML/ROOT.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM Type inference for let-free MiniML *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/MiniML"; Unify.trace_bound := 20; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/MiniML/Type.ML --- a/src/HOL/MiniML/Type.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/MiniML/Type.ML Thu Sep 26 12:47:47 1996 +0200 @@ -6,7 +6,7 @@ goalw thy [new_tv_def] "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \ \ new_tv n u"; -by( fast_tac (set_cs addDs [mgu_free]) 1); +by ( fast_tac (set_cs addDs [mgu_free]) 1); qed "mgu_new"; (* application of id_subst does not change type expression *) @@ -28,8 +28,8 @@ Addsimps [app_subst_id_tel]; goalw Type.thy [id_subst_def,o_def] "$s o id_subst = s"; -br ext 1; -by(Simp_tac 1); +by (rtac ext 1); +by (Simp_tac 1); qed "o_id_subst"; Addsimps[o_id_subst]; @@ -117,36 +117,36 @@ goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] "new_tv n id_subst"; -by(Simp_tac 1); +by (Simp_tac 1); qed "new_tv_id_subst"; Addsimps[new_tv_id_subst]; goalw thy [new_tv_def] "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ \ (! l. l < n --> new_tv n (s l) ))"; -by( safe_tac HOL_cs ); +by ( safe_tac HOL_cs ); (* ==> *) -by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); -by( subgoal_tac "m:cod s | s l = TVar l" 1); -by( safe_tac HOL_cs ); -by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); -by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); -by(Asm_full_simp_tac 1); -by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); +by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); +by ( subgoal_tac "m:cod s | s l = TVar l" 1); +by ( safe_tac HOL_cs ); +by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); +by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); +by (Asm_full_simp_tac 1); +by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); (* <== *) -by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); -by( safe_tac set_cs ); -by( cut_inst_tac [("m","m"),("n","n")] less_linear 1); -by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); -by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1); -by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); +by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); +by ( safe_tac set_cs ); +by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1); +by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); +by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1); +by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); qed "new_tv_subst"; goal thy "new_tv n = list_all (new_tv n)"; by (rtac ext 1); -by(list.induct_tac "x" 1); -by(ALLGOALS Asm_simp_tac); +by (list.induct_tac "x" 1); +by (ALLGOALS Asm_simp_tac); qed "new_tv_list"; (* substitution affects only variables occurring freely *) @@ -169,7 +169,7 @@ "n<=m --> new_tv n (t::typ) --> new_tv m t"; by (typ.induct_tac "t" 1); (* case TVar n *) -by( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1); +by ( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1); (* case Fun t1 t2 *) by (Asm_simp_tac 1); qed_spec_mp "new_tv_le"; @@ -177,9 +177,9 @@ goal thy "n<=m --> new_tv n (ts::typ list) --> new_tv m ts"; -by( list.induct_tac "ts" 1); +by ( list.induct_tac "ts" 1); (* case [] *) -by(Simp_tac 1); +by (Simp_tac 1); (* case a#al *) by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1); qed_spec_mp "new_tv_list_le"; @@ -212,7 +212,7 @@ goal thy "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; -by( simp_tac (!simpset addsimps [new_tv_list]) 1); +by ( simp_tac (!simpset addsimps [new_tv_list]) 1); by (list.induct_tac "ts" 1); by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); qed_spec_mp "new_tv_subst_tel"; @@ -221,7 +221,7 @@ (* auxilliary lemma *) goal thy "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)"; -by( simp_tac (!simpset addsimps [new_tv_list]) 1); +by ( simp_tac (!simpset addsimps [new_tv_list]) 1); by (list.induct_tac "ts" 1); by (ALLGOALS Asm_full_simp_tac); qed "new_tv_Suc_list"; @@ -302,50 +302,50 @@ (* some useful theorems *) goalw thy [free_tv_subst] "!!v. v : cod s ==> v : free_tv s"; -by( fast_tac set_cs 1); +by ( fast_tac set_cs 1); qed "codD"; goalw thy [free_tv_subst,dom_def] "!! x. x ~: free_tv s ==> s x = TVar x"; -by( fast_tac set_cs 1); +by ( fast_tac set_cs 1); qed "not_free_impl_id"; goalw thy [new_tv_def] "!! n. [| new_tv n t; m:free_tv t |] ==> m (? s t. (? m. W e [] n = Ok(s,t,m)) & \ \ (? r. t' = $r t))"; -by(cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")] +by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")] W_complete_lemma 1); -by(ALLGOALS Asm_full_simp_tac); +by (ALLGOALS Asm_full_simp_tac); qed "W_complete"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Nat.ML Thu Sep 26 12:47:47 1996 +0200 @@ -16,12 +16,12 @@ (* Zero is a natural number -- this also justifies the type definition*) goal Nat.thy "Zero_Rep: Nat"; -by (rtac (Nat_unfold RS ssubst) 1); +by (stac Nat_unfold 1); by (rtac (singletonI RS UnI1) 1); qed "Zero_RepI"; val prems = goal Nat.thy "i: Nat ==> Suc_Rep(i) : Nat"; -by (rtac (Nat_unfold RS ssubst) 1); +by (stac Nat_unfold 1); by (rtac (imageI RS UnI2) 1); by (resolve_tac prems 1); qed "Suc_RepI"; @@ -293,12 +293,12 @@ Addsimps [gr_implies_not0]; qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [ - rtac iffI 1, - etac gr_implies_not0 1, - rtac natE 1, - contr_tac 1, - etac ssubst 1, - rtac zero_less_Suc 1]); + rtac iffI 1, + etac gr_implies_not0 1, + rtac natE 1, + contr_tac 1, + etac ssubst 1, + rtac zero_less_Suc 1]); (** Inductive (?) properties **) @@ -408,8 +408,8 @@ (* goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)"; -by(stac (less_Suc_eq RS sym) 1); -by(rtac Suc_less_eq 1); +by (stac (less_Suc_eq RS sym) 1); +by (rtac Suc_less_eq 1); qed "Suc_le_eq"; this could make the simpset (with less_Suc_eq added again) more confluent, @@ -562,23 +562,23 @@ qed_goalw "Least_Suc" Nat.thy [Least_def] "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" (fn _ => [ - rtac select_equality 1, - fold_goals_tac [Least_def], - safe_tac (!claset addSEs [LeastI]), - res_inst_tac [("n","j")] natE 1, - Fast_tac 1, - fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1, - res_inst_tac [("n","k")] natE 1, - Fast_tac 1, - hyp_subst_tac 1, - rewtac Least_def, - rtac (select_equality RS arg_cong RS sym) 1, - safe_tac (!claset), - dtac Suc_mono 1, - Fast_tac 1, - cut_facts_tac [less_linear] 1, - safe_tac (!claset), - atac 2, - Fast_tac 2, - dtac Suc_mono 1, - Fast_tac 1]); + rtac select_equality 1, + fold_goals_tac [Least_def], + safe_tac (!claset addSEs [LeastI]), + res_inst_tac [("n","j")] natE 1, + Fast_tac 1, + fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1, + res_inst_tac [("n","k")] natE 1, + Fast_tac 1, + hyp_subst_tac 1, + rewtac Least_def, + rtac (select_equality RS arg_cong RS sym) 1, + safe_tac (!claset), + dtac Suc_mono 1, + Fast_tac 1, + cut_facts_tac [less_linear] 1, + safe_tac (!claset), + atac 2, + Fast_tac 2, + dtac Suc_mono 1, + Fast_tac 1]); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Option.ML --- a/src/HOL/Option.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Option.ML Thu Sep 26 12:47:47 1996 +0200 @@ -27,5 +27,5 @@ by (option.induct_tac "opt" 1); by (Simp_tac 1); by (Asm_full_simp_tac 1); -by(Fast_tac 1); +by (Fast_tac 1); qed"expand_option_case"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Prod.ML Thu Sep 26 12:47:47 1996 +0200 @@ -331,28 +331,28 @@ fun ap_split (Type("*", [T1,T2])) T3 u = split_const(T1,T2,T3) $ Abs("v", T1, - ap_split T2 T3 - ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ - Bound 0)) + ap_split T2 T3 + ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ + Bound 0)) | ap_split T T3 u = u; (*Makes a nested tuple from a list, following the product type structure*) fun mk_tuple (Type("*", [T1,T2])) tms = mk_Pair (mk_tuple T1 tms, - mk_tuple T2 (drop (length (factors T1), tms))) + mk_tuple T2 (drop (length (factors T1), tms))) | mk_tuple T (t::_) = t; (*Attempts to remove occurrences of split, and pair-valued parameters*) val remove_split = rewrite_rule [split RS eq_reflection] o - rule_by_tactic (ALLGOALS split_all_tac); + rule_by_tactic (ALLGOALS split_all_tac); (*Uncurries any Var of function type in the rule*) fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) = let val T' = factors T1 ---> T2 - val newt = ap_split T1 T2 (Var(v,T')) - val cterm = Thm.cterm_of (#sign(rep_thm rl)) + val newt = ap_split T1 T2 (Var(v,T')) + val cterm = Thm.cterm_of (#sign(rep_thm rl)) in - remove_split (instantiate ([], [(cterm t, cterm newt)]) rl) + remove_split (instantiate ([], [(cterm t, cterm newt)]) rl) end | split_rule_var (t,rl) = rl; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/RelPow.ML --- a/src/HOL/RelPow.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/RelPow.ML Thu Sep 26 12:47:47 1996 +0200 @@ -10,7 +10,7 @@ Addsimps [rel_pow_0]; goal RelPow.thy "R^1 = R"; -by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1); +by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1); qed "rel_pow_1"; Addsimps [rel_pow_1]; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Relation.ML Thu Sep 26 12:47:47 1996 +0200 @@ -104,7 +104,7 @@ AddSEs [converseE]; goalw Relation.thy [converse_def] "converse(converse R) = R"; -by(Fast_tac 1); +by (Fast_tac 1); qed "converse_converse"; (** Domain **) diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Set.ML --- a/src/HOL/Set.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Set.ML Thu Sep 26 12:47:47 1996 +0200 @@ -11,7 +11,7 @@ section "Relating predicates and sets"; val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}"; -by (rtac (mem_Collect_eq RS ssubst) 1); +by (stac mem_Collect_eq 1); by (rtac prem 1); qed "CollectI"; @@ -350,10 +350,10 @@ bind_thm ("singletonE", make_elim singletonD); qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [ - rtac iffI 1, - etac singletonD 1, - hyp_subst_tac 1, - rtac singletonI 1]); + rtac iffI 1, + etac singletonD 1, + hyp_subst_tac 1, + rtac singletonI 1]); val [major] = goal Set.thy "{a}={b} ==> a=b"; by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1); @@ -502,7 +502,7 @@ val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, - mem_Collect_eq]; + mem_Collect_eq]; (*Not for Addsimps -- it can cause goals to blow up!*) goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Sexp.ML --- a/src/HOL/Sexp.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Sexp.ML Thu Sep 26 12:47:47 1996 +0200 @@ -11,17 +11,17 @@ (** sexp_case **) goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)"; -by (resolve_tac [select_equality] 1); +by (rtac select_equality 1); by (ALLGOALS (Fast_tac)); qed "sexp_case_Leaf"; goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)"; -by (resolve_tac [select_equality] 1); +by (rtac select_equality 1); by (ALLGOALS (Fast_tac)); qed "sexp_case_Numb"; goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N"; -by (resolve_tac [select_equality] 1); +by (rtac select_equality 1); by (ALLGOALS (Fast_tac)); qed "sexp_case_Scons"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/Trancl.ML Thu Sep 26 12:47:47 1996 +0200 @@ -116,7 +116,7 @@ Addsimps [rtrancl_idemp]; goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*"; -bd rtrancl_mono 1; +by (dtac rtrancl_mono 1); by (Asm_full_simp_tac 1); qed "rtrancl_subset_rtrancl"; @@ -163,23 +163,23 @@ "[| (a,b) : r^*; P(b); \ \ !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] \ \ ==> P(a)"; -br ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1; -brs prems 1; -by(fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1); +by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1); +by (resolve_tac prems 1); +by (fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1); qed "converse_rtrancl_induct"; val prems = goal Trancl.thy "[| ((a,b),(c,d)) : r^*; P c d; \ \ !!x y z u.[| ((x,y),(z,u)) : r; ((z,u),(c,d)) : r^*; P z u |] ==> P x y\ \ |] ==> P a b"; -by(res_inst_tac[("R","P")]splitD 1); -by(res_inst_tac[("P","split P")]converse_rtrancl_induct 1); -brs prems 1; -by(Simp_tac 1); -brs prems 1; -by(split_all_tac 1); -by(Asm_full_simp_tac 1); -by(REPEAT(ares_tac prems 1)); +by (res_inst_tac[("R","P")]splitD 1); +by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1); +by (resolve_tac prems 1); +by (Simp_tac 1); +by (resolve_tac prems 1); +by (split_all_tac 1); +by (Asm_full_simp_tac 1); +by (REPEAT(ares_tac prems 1)); qed "converse_rtrancl_induct2"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/WF.ML --- a/src/HOL/WF.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/WF.ML Thu Sep 26 12:47:47 1996 +0200 @@ -129,7 +129,7 @@ by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] is_the_recfun 1); by (rewtac is_recfun_def); - by (rtac (cuts_eq RS ssubst) 1); + by (stac cuts_eq 1); by (rtac allI 1); by (rtac impI 1); by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1); @@ -159,7 +159,7 @@ by (wf_ind_tac "a" prems 1); by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); by (rewrite_goals_tac [is_recfun_def, wftrec_def]); -by (rtac (cuts_eq RS ssubst) 1); +by (stac cuts_eq 1); (*Applying the substitution: must keep the quantified assumption!!*) by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac, etac (mp RS ssubst), atac]); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/datatype.ML --- a/src/HOL/datatype.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/datatype.ML Thu Sep 26 12:47:47 1996 +0200 @@ -225,7 +225,7 @@ val xrules = let val (first_part, scnd_part) = calc_xrules 1 1 cons_list in [Syntax.<-> (("logic", "case x of " ^ first_part), - ("logic", tname ^ "_case " ^ scnd_part ^ " x"))] + ("logic", tname ^ "_case " ^ scnd_part ^ " x"))] end; (*type declarations for constructors*) diff -r 474b3f208789 -r 03a843f0f447 src/HOL/equalities.ML --- a/src/HOL/equalities.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/equalities.ML Thu Sep 26 12:47:47 1996 +0200 @@ -93,8 +93,8 @@ goalw Set.thy [image_def] "(%x. if P x then f x else g x) `` S \ \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))"; -by(split_tac [expand_if] 1); -by(Fast_tac 1); +by (split_tac [expand_if] 1); +by (Fast_tac 1); qed "if_image_distrib"; Addsimps[if_image_distrib]; @@ -535,22 +535,22 @@ fun prover s = prove_goal Set.thy s (fn _ => [Fast_tac 1]) in val UN1_simps = map prover - ["(UN x. insert a (B x)) = insert a (UN x. B x)", - "(UN x. A x Int B) = ((UN x.A x) Int B)", - "(UN x. A Int B x) = (A Int (UN x.B x))", - "(UN x. A x Un B) = ((UN x.A x) Un B)", - "(UN x. A Un B x) = (A Un (UN x.B x))", - "(UN x. A x - B) = ((UN x.A x) - B)", - "(UN x. A - B x) = (A - (INT x.B x))"]; + ["(UN x. insert a (B x)) = insert a (UN x. B x)", + "(UN x. A x Int B) = ((UN x.A x) Int B)", + "(UN x. A Int B x) = (A Int (UN x.B x))", + "(UN x. A x Un B) = ((UN x.A x) Un B)", + "(UN x. A Un B x) = (A Un (UN x.B x))", + "(UN x. A x - B) = ((UN x.A x) - B)", + "(UN x. A - B x) = (A - (INT x.B x))"]; val INT1_simps = map prover - ["(INT x. insert a (B x)) = insert a (INT x. B x)", - "(INT x. A x Int B) = ((INT x.A x) Int B)", - "(INT x. A Int B x) = (A Int (INT x.B x))", - "(INT x. A x Un B) = ((INT x.A x) Un B)", - "(INT x. A Un B x) = (A Un (INT x.B x))", - "(INT x. A x - B) = ((INT x.A x) - B)", - "(INT x. A - B x) = (A - (UN x.B x))"]; + ["(INT x. insert a (B x)) = insert a (INT x. B x)", + "(INT x. A x Int B) = ((INT x.A x) Int B)", + "(INT x. A Int B x) = (A Int (INT x.B x))", + "(INT x. A x Un B) = ((INT x.A x) Un B)", + "(INT x. A Un B x) = (A Un (INT x.B x))", + "(INT x. A x - B) = ((INT x.A x) - B)", + "(INT x. A - B x) = (A - (UN x.B x))"]; (*Analogous laws for bounded Unions and Intersections are conditional on the index set's being non-empty. Thus they are probably NOT worth diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/Comb.ML --- a/src/HOL/ex/Comb.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/Comb.ML Thu Sep 26 12:47:47 1996 +0200 @@ -167,13 +167,13 @@ goal Comb.thy "contract^* = parcontract^*"; by (REPEAT (resolve_tac [equalityI, - contract_subset_parcontract RS rtrancl_mono, - parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1)); + contract_subset_parcontract RS rtrancl_mono, + parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1)); qed "reduce_eq_parreduce"; goal Comb.thy "diamond(contract^*)"; by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, - diamond_parcontract]) 1); + diamond_parcontract]) 1); qed "diamond_reduce"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/InSort.ML --- a/src/HOL/ex/InSort.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/InSort.ML Thu Sep 26 12:47:47 1996 +0200 @@ -8,37 +8,37 @@ goalw InSort.thy [Sorting.total_def] "!!f. [| total(f); ~f x y |] ==> f y x"; -by(Fast_tac 1); +by (Fast_tac 1); qed "totalD"; goalw InSort.thy [Sorting.transf_def] "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x"; -by(Fast_tac 1); +by (Fast_tac 1); qed "transfD"; goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))"; -by(list.induct_tac "xs" 1); -by(Asm_simp_tac 1); -by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); -by(Fast_tac 1); +by (list.induct_tac "xs" 1); +by (Asm_simp_tac 1); +by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); +by (Fast_tac 1); Addsimps [result()]; goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs"; -by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "list_all_imp"; val prems = goal InSort.thy "[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs"; -by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); -by(cut_facts_tac prems 1); -by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1); -by(fast_tac (!claset addDs [totalD,transfD]) 1); +by (list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (cut_facts_tac prems 1); +by (cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1); +by (fast_tac (!claset addDs [totalD,transfD]) 1); Addsimps [result()]; goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; -by(list.induct_tac "xs" 1); -by(ALLGOALS Asm_simp_tac); +by (list.induct_tac "xs" 1); +by (ALLGOALS Asm_simp_tac); qed "sorted_insort"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/LList.ML --- a/src/HOL/ex/LList.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/LList.ML Thu Sep 26 12:47:47 1996 +0200 @@ -393,7 +393,7 @@ AddIs ([Rep_llist]@llist.intrs); AddSDs [inj_onto_Abs_llist RS inj_ontoD, - inj_Rep_llist RS injD, Leaf_inject]; + inj_Rep_llist RS injD, Leaf_inject]; goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)"; by (Fast_tac 1); @@ -648,7 +648,7 @@ by (rtac (prem2 RS image_mono RS subset_trans) 1); by (rtac (image_compose RS subst) 1); by (rtac (prod_fun_compose RS subst) 1); -by (rtac (image_Un RS ssubst) 1); +by (stac image_Un 1); by (stac prod_fun_range_eq_diag 1); by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1); by (rtac (subset_Sigma_llist RS Un_least) 1); @@ -671,7 +671,7 @@ "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))"; by (rtac (Rep_llist_inverse RS subst) 1); by (rtac prod_fun_imageI 1); -by (rtac (image_Un RS ssubst) 1); +by (stac image_Un 1); by (stac prod_fun_range_eq_diag 1); by (rtac (Rep_llist RS LListD_Fun_diag_I) 1); qed "llistD_Fun_range_I"; @@ -744,7 +744,7 @@ qed "lmap_iterates"; goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))"; -by (rtac (lmap_iterates RS ssubst) 1); +by (stac lmap_iterates 1); by (rtac iterates 1); qed "iterates_lmap"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/LexProd.ML --- a/src/HOL/ex/LexProd.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/LexProd.ML Thu Sep 26 12:47:47 1996 +0200 @@ -10,7 +10,7 @@ val prems = goal Prod.thy "!a b. P((a,b)) ==> !p.P(p)"; by (cut_facts_tac prems 1); by (rtac allI 1); -by (rtac (surjective_pairing RS ssubst) 1); +by (stac surjective_pairing 1); by (Fast_tac 1); qed "split_all_pair"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/Mutil.ML --- a/src/HOL/ex/Mutil.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/Mutil.ML Thu Sep 26 12:47:47 1996 +0200 @@ -17,8 +17,8 @@ by (etac tiling.induct 1); by (Simp_tac 1); by (fast_tac (!claset addIs tiling.intrs - addss (HOL_ss addsimps [Un_assoc, - subset_empty_iff RS sym])) 1); + addss (HOL_ss addsimps [Un_assoc, + subset_empty_iff RS sym])) 1); qed_spec_mp "tiling_UnI"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/PropLog.ML --- a/src/HOL/ex/PropLog.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/PropLog.ML Thu Sep 26 12:47:47 1996 +0200 @@ -18,7 +18,7 @@ (*Rule is called I for Identity Combinator, not for Introduction*) goal PropLog.thy "H |- p->p"; -by(best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1); +by (best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1); qed "thms_I"; (** Weakening, left and right **) @@ -35,7 +35,7 @@ val weaken_left_Un2 = Un_upper2 RS weaken_left; goal PropLog.thy "!!H. H |- q ==> H |- p->q"; -by(fast_tac (!claset addIs [thms.K,thms.MP]) 1); +by (fast_tac (!claset addIs [thms.K,thms.MP]) 1); qed "weaken_right"; (*The deduction theorem*) @@ -43,7 +43,7 @@ by (etac thms.induct 1); by (ALLGOALS (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, - thms.S RS thms.MP RS thms.MP, weaken_right]))); + thms.S RS thms.MP RS thms.MP, weaken_right]))); qed "deduction"; @@ -102,7 +102,7 @@ (*This formulation is required for strong induction hypotheses*) goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)"; by (rtac (expand_if RS iffD2) 1); -by(PropLog.pl.induct_tac "p" 1); +by (PropLog.pl.induct_tac "p" 1); by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H]))); by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, weaken_right, imp_false] diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/Puzzle.ML --- a/src/HOL/ex/Puzzle.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/Puzzle.ML Thu Sep 26 12:47:47 1996 +0200 @@ -22,7 +22,7 @@ by (dtac not_leE 1); by (subgoal_tac "f(na) <= f(f(na))" 1); by (fast_tac (!claset addIs [Puzzle.f_ax]) 2); -br lessD 1; +by (rtac lessD 1); by (best_tac (!claset delrules [le_refl] addIs [Puzzle.f_ax, le_less_trans]) 1); val lemma = result() RS spec RS mp; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/Qsort.ML --- a/src/HOL/ex/Qsort.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/Qsort.ML Thu Sep 26 12:47:47 1996 +0200 @@ -9,40 +9,40 @@ Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x"; -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); result(); goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))"; -by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); Addsimps [result()]; goal Qsort.thy "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))"; -by(list.induct_tac "xs" 1); -by(ALLGOALS Asm_simp_tac); +by (list.induct_tac "xs" 1); +by (ALLGOALS Asm_simp_tac); val alls_lemma=result(); Addsimps [alls_lemma]; goal HOL.thy "((P --> Q) & (~P --> Q)) = Q"; -by(Fast_tac 1); +by (Fast_tac 1); val lemma = result(); goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))"; -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(Asm_simp_tac 1); -by(asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1); -by(asm_simp_tac (!simpset addsimps [lemma]) 1); +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by (Asm_simp_tac 1); +by (asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1); +by (asm_simp_tac (!simpset addsimps [lemma]) 1); Addsimps [result()]; goal Qsort.thy "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ \ (Alls x:xs. Alls y:ys. le x y))"; -by(list.induct_tac "xs" 1); -by(Asm_simp_tac 1); -by(asm_simp_tac (!simpset delsimps [alls_lemma]) 1); +by (list.induct_tac "xs" 1); +by (Asm_simp_tac 1); +by (asm_simp_tac (!simpset delsimps [alls_lemma]) 1); Addsimps [result()]; @@ -50,12 +50,12 @@ goal Qsort.thy "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(Asm_simp_tac 1); -by(asm_full_simp_tac (!simpset addsimps []) 1); -by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1); -by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); -by(Fast_tac 1); +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by (Asm_simp_tac 1); +by (asm_full_simp_tac (!simpset addsimps []) 1); +by (asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1); +by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); +by (Fast_tac 1); result(); (* A verification based on predicate calculus rather than combinators *) @@ -67,31 +67,31 @@ goal Qsort.thy "x mem qsort le xs = x mem xs"; -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); -by(Fast_tac 1); +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (Fast_tac 1); Addsimps [result()]; goal Qsort.thy "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ \ (!x. x mem xs --> (!y. y mem ys --> le x y)))"; -by(list.induct_tac "xs" 1); -by(Asm_simp_tac 1); -by(asm_simp_tac (!simpset setloop (split_tac [expand_if]) - delsimps [list_all_conj] - addsimps [list_all_mem_conv]) 1); -by(Fast_tac 1); +by (list.induct_tac "xs" 1); +by (Asm_simp_tac 1); +by (asm_simp_tac (!simpset setloop (split_tac [expand_if]) + delsimps [list_all_conj] + addsimps [list_all_mem_conv]) 1); +by (Fast_tac 1); Addsimps [result()]; goal Qsort.thy "!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; -by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(Simp_tac 1); -by(asm_simp_tac (!simpset setloop (split_tac [expand_if]) - delsimps [list_all_conj] - addsimps [list_all_mem_conv]) 1); -by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); -by(Fast_tac 1); +by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by (Simp_tac 1); +by (asm_simp_tac (!simpset setloop (split_tac [expand_if]) + delsimps [list_all_conj] + addsimps [list_all_mem_conv]) 1); +by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); +by (Fast_tac 1); result(); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/SList.ML --- a/src/HOL/ex/SList.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/SList.ML Thu Sep 26 12:47:47 1996 +0200 @@ -125,10 +125,10 @@ goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)"; -by(list_ind_tac "xs" 1); -by(Simp_tac 1); -by(Asm_simp_tac 1); -by(REPEAT(resolve_tac [exI,refl,conjI] 1)); +by (list_ind_tac "xs" 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +by (REPEAT(resolve_tac [exI,refl,conjI] 1)); qed "neq_Nil_conv2"; (** Conversion rules for List_case: case analysis operator **) @@ -243,7 +243,7 @@ goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)"; by (rtac list_induct2 1); -by(ALLGOALS Asm_simp_tac); +by (ALLGOALS Asm_simp_tac); qed "Rep_map_type"; goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil"; @@ -275,16 +275,16 @@ (*** Unfolding the basic combinators ***) -val [null_Nil, null_Cons] = list_recs null_def; -val [_, hd_Cons] = list_recs hd_def; -val [_, tl_Cons] = list_recs tl_def; -val [ttl_Nil, ttl_Cons] = list_recs ttl_def; -val [append_Nil3, append_Cons] = list_recs append_def; -val [mem_Nil, mem_Cons] = list_recs mem_def; -val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def; -val [map_Nil, map_Cons] = list_recs map_def; -val [list_case_Nil, list_case_Cons] = list_recs list_case_def; -val [filter_Nil, filter_Cons] = list_recs filter_def; +val [null_Nil, null_Cons] = list_recs null_def; +val [_, hd_Cons] = list_recs hd_def; +val [_, tl_Cons] = list_recs tl_def; +val [ttl_Nil, ttl_Cons] = list_recs ttl_def; +val [append_Nil3, append_Cons] = list_recs append_def; +val [mem_Nil, mem_Cons] = list_recs mem_def; +val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def; +val [map_Nil, map_Cons] = list_recs map_def; +val [list_case_Nil, list_case_Cons] = list_recs list_case_def; +val [filter_Nil, filter_Cons] = list_recs filter_def; Addsimps [null_Nil, ttl_Nil, @@ -299,25 +299,25 @@ (** @ - append **) goal SList.thy "(xs@ys)@zs = xs@(ys@zs)"; -by(list_ind_tac "xs" 1); -by(ALLGOALS Asm_simp_tac); +by (list_ind_tac "xs" 1); +by (ALLGOALS Asm_simp_tac); qed "append_assoc2"; goal SList.thy "xs @ [] = xs"; -by(list_ind_tac "xs" 1); -by(ALLGOALS Asm_simp_tac); +by (list_ind_tac "xs" 1); +by (ALLGOALS Asm_simp_tac); qed "append_Nil4"; (** mem **) goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; -by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (list_ind_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mem_append2"; goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; -by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (list_ind_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mem_filter2"; @@ -339,9 +339,9 @@ goal SList.thy "P(list_case a f xs) = ((xs=[] --> P(a)) & \ \ (!y ys. xs=y#ys --> P(f y ys)))"; -by(list_ind_tac "xs" 1); -by(ALLGOALS Asm_simp_tac); -by(Fast_tac 1); +by (list_ind_tac "xs" 1); +by (ALLGOALS Asm_simp_tac); +by (Fast_tac 1); qed "expand_list_case2"; @@ -365,7 +365,7 @@ goal SList.thy "!!f. (!!x. f(x): sexp) ==> \ \ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"; by (list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac(!simpset addsimps +by (ALLGOALS(asm_simp_tac(!simpset addsimps [Rep_map_type,list_sexp RS subsetD]))); qed "Abs_Rep_map"; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/Sorting.ML --- a/src/HOL/ex/Sorting.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/Sorting.ML Thu Sep 26 12:47:47 1996 +0200 @@ -11,14 +11,14 @@ Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons]; goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x"; -by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mset_app_distr"; goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \ \ mset xs x"; -by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +by (list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mset_compl_add"; Addsimps [mset_app_distr, mset_compl_add]; diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/String.ML --- a/src/HOL/ex/String.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/String.ML Thu Sep 26 12:47:47 1996 +0200 @@ -1,20 +1,20 @@ goal String.thy "hd(''ABCD'') = CHR ''A''"; -by(Simp_tac 1); +by (Simp_tac 1); result(); goal String.thy "hd(''ABCD'') ~= CHR ''B''"; -by(Simp_tac 1); +by (Simp_tac 1); result(); goal String.thy "''ABCD'' ~= ''ABCX''"; -by(Simp_tac 1); +by (Simp_tac 1); result(); goal String.thy "''ABCD'' = ''ABCD''"; -by(Simp_tac 1); +by (Simp_tac 1); result(); goal String.thy "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; -by(Simp_tac 1); +by (Simp_tac 1); result(); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/meson.ML --- a/src/HOL/ex/meson.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/meson.ML Thu Sep 26 12:47:47 1996 +0200 @@ -189,10 +189,10 @@ fun skolemize th = if not (has_consts ["Ex"] (prop_of th)) then th else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, - disj_exD, disj_exD1, disj_exD2])) + disj_exD, disj_exD1, disj_exD2])) handle THM _ => skolemize (forward_res skolemize - (tryres (th, [conj_forward, disj_forward, all_forward]))) + (tryres (th, [conj_forward, disj_forward, all_forward]))) handle THM _ => forward_res skolemize (th RS ex_forward); @@ -211,7 +211,7 @@ | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; val term_False = term_of (read_cterm (sign_of HOL.thy) - ("False", Type("bool",[]))); + ("False", Type("bool",[]))); (*Include False as a literal: an occurrence of ~False is a tautology*) fun is_taut th = taut_lits ((true,term_False) :: literals (prop_of th)); @@ -272,8 +272,8 @@ fun forward_res2 nf hyps st = case Sequence.pull (REPEAT - (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) - st) + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) + st) of Some(th,_) => th | None => raise THM("forward_res2", 0, [st]); @@ -426,7 +426,7 @@ MESON (fn cls => THEN_BEST_FIRST (resolve_tac (gocls cls) 1) (has_fewer_prems 1, sizef) - (prolog_step_tac (make_horns cls) 1)); + (prolog_step_tac (make_horns cls) 1)); (*First, breaks the goal into independent units*) val safe_best_meson_tac = @@ -451,7 +451,7 @@ val nrtac = net_resolve_tac horns in fn i => eq_assume_tac i ORELSE match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) - ((assume_tac i APPEND nrtac i) THEN check_tac) + ((assume_tac i APPEND nrtac i) THEN check_tac) end; fun iter_deepen_prolog_tac horns = @@ -460,8 +460,8 @@ val iter_deepen_meson_tac = MESON (fn cls => (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1) - (has_fewer_prems 1) - (prolog_step_tac' (make_horns cls)))); + (has_fewer_prems 1) + (prolog_step_tac' (make_horns cls)))); val safe_meson_tac = SELECT_GOAL (TRY (safe_tac (!claset)) THEN diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/mesontest.ML --- a/src/HOL/ex/mesontest.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/mesontest.ML Thu Sep 26 12:47:47 1996 +0200 @@ -326,7 +326,7 @@ by (safe_meson_tac 1); result(); -writeln"Problem 27"; (*13 Horn clauses*) +writeln"Problem 27"; (*13 Horn clauses*) goal HOL.thy "(? x. P x & ~Q x) & \ \ (! x. P x --> R x) & \ \ (! x. M x & L x --> P x) & \ @@ -335,7 +335,7 @@ by (safe_meson_tac 1); result(); -writeln"Problem 28. AMENDED"; (*14 Horn clauses*) +writeln"Problem 28. AMENDED"; (*14 Horn clauses*) goal HOL.thy "(! x. P x --> (! x. Q x)) & \ \ ((! x. Q x | R x) --> (? x. Q x & S x)) & \ \ ((? x.S x) --> (! x. L x --> M x)) \ @@ -344,7 +344,7 @@ result(); writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; - (*62 Horn clauses*) + (*62 Horn clauses*) goal HOL.thy "(? x. F x) & (? y. G y) \ \ --> ( ((! x. F x --> H x) & (! y. G y --> J y)) = \ \ (! x y. F x & G y --> H x & J y))"; @@ -447,7 +447,7 @@ writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ \ --> (! x. (! y. q x y = (q y x::bool)))"; -by (safe_best_meson_tac 1); +by (safe_best_meson_tac 1); (*1.6 secs; iter. deepening is slightly slower*) result(); @@ -466,7 +466,7 @@ \ (? x. f x & (! y. h x y --> l y) \ \ & (! y. g y & h x y --> j x y)) \ \ --> (? x. f x & ~ (? y. g y & h x y))"; -by (safe_best_meson_tac 1); +by (safe_best_meson_tac 1); (*1.6 secs; iter. deepening is slightly slower*) result(); @@ -477,12 +477,12 @@ \ (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) & \ \ (! x y. f x & f y & h x y --> ~j y x) \ \ --> (! x. f x --> g x)"; -by (safe_best_meson_tac 1); +by (safe_best_meson_tac 1); (*1.7 secs; iter. deepening is slightly slower*) result(); writeln"Problem 47. Schubert's Steamroller"; - (*26 clauses; 63 Horn clauses*) + (*26 clauses; 63 Horn clauses*) goal HOL.thy "(! x. P1 x --> P0 x) & (? x.P1 x) & \ \ (! x. P2 x --> P0 x) & (? x.P2 x) & \ @@ -501,7 +501,7 @@ \ (! x y. P3 x & P5 y --> ~R x y) & \ \ (! x. (P4 x|P5 x) --> (? y.Q0 y & R x y)) \ \ --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))"; -by (safe_meson_tac 1); (*119 secs*) +by (safe_meson_tac 1); (*119 secs*) result(); (*The Los problem? Circulated by John Harrison*) @@ -510,7 +510,7 @@ \ (! x y. P x y --> P y x) & \ \ (! (x::'a) y. P x y | Q x y) \ \ --> (! x y. P x y) | (! x y. Q x y)"; -by (safe_best_meson_tac 1); (*3 secs; iter. deepening is VERY slow*) +by (safe_best_meson_tac 1); (*3 secs; iter. deepening is VERY slow*) result(); (*A similar example, suggested by Johannes Schumann and credited to Pelletier*) diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/set.ML --- a/src/HOL/ex/set.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/set.ML Thu Sep 26 12:47:47 1996 +0200 @@ -12,7 +12,7 @@ (*** A unique fixpoint theorem --- fast/best/meson all fail ***) val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"; -by(EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong, +by (EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong, rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); result(); @@ -92,7 +92,7 @@ \ bij = (%z. if z:X then f(z) else g(z)) |] ==> \ \ inj(bij) & surj(bij)"; val f_eq_gE = make_elim (compl RS disj_lemma); -by (rtac (bij RS ssubst) 1); +by (stac bij 1); by (rtac conjI 1); by (rtac (compl RS surj_if_then_else) 2); by (rewtac inj_def); diff -r 474b3f208789 -r 03a843f0f447 src/HOL/ex/unsolved.ML --- a/src/HOL/ex/unsolved.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/ex/unsolved.ML Thu Sep 26 12:47:47 1996 +0200 @@ -7,7 +7,7 @@ *) (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 1989. 1--23*) - (*27 clauses; 81 Horn clauses*) + (*27 clauses; 81 Horn clauses*) goal HOL.thy "? x x'. ! y. ? z z'. (~P y y | P x x | ~S z x) & \ \ (S x y | ~S y z | Q z' z') & \ \ (Q x' y | ~Q y z' | S x' x')"; @@ -32,7 +32,7 @@ \ killed agatha agatha"; (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) - author U. Egly; 46 clauses; 264 Horn clauses*) + author U. Egly; 46 clauses; 264 Horn clauses*) goal HOL.thy "((EX X. (a X) & (ALL Y. (c Y) --> (ALL Z. (d X Y Z)))) --> \ \ (EX W. (c W) & (ALL Y. (c Y) --> (ALL Z. (d W Y Z))))) \ diff -r 474b3f208789 -r 03a843f0f447 src/HOL/indrule.ML --- a/src/HOL/indrule.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/indrule.ML Thu Sep 26 12:47:47 1996 +0200 @@ -120,7 +120,7 @@ fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm val pfree = Free(pred_name ^ "_" ^ rec_name, - elem_factors ---> Ind_Syntax.boolT) + elem_factors ---> Ind_Syntax.boolT) val qconcl = foldr Ind_Syntax.mk_all (elem_frees, @@ -148,8 +148,8 @@ Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls); val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], - resolve_tac [allI, impI, conjI, Part_eqI, refl], - dresolve_tac [spec, mp, splitD]]; + resolve_tac [allI, impI, conjI, Part_eqI, refl], + dresolve_tac [spec, mp, splitD]]; val lemma = (*makes the link between the two induction rules*) prove_goalw_cterm part_rec_defs @@ -158,7 +158,7 @@ (fn prems => [cut_facts_tac prems 1, REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN - lemma_tac 1)]) + lemma_tac 1)]) handle e => print_sign_exn sign e; (*Mutual induction follows by freeness of Inl/Inr.*) @@ -223,8 +223,8 @@ struct val induct = standard (Prod_Syntax.split_rule_var - (Var((pred_name,2), elem_type --> Ind_Syntax.boolT), - induct0)); + (Var((pred_name,2), elem_type --> Ind_Syntax.boolT), + induct0)); (*Just "True" unless there's true mutual recursion. This saves storage.*) val mutual_induct = diff -r 474b3f208789 -r 03a843f0f447 src/HOL/intr_elim.ML --- a/src/HOL/intr_elim.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/intr_elim.ML Thu Sep 26 12:47:47 1996 +0200 @@ -82,7 +82,7 @@ fun intro_tacsf disjIn prems = [(*insert prems and underlying sets*) cut_facts_tac prems 1, - rtac (unfold RS ssubst) 1, + stac unfold 1, REPEAT (resolve_tac [Part_eqI,CollectI] 1), (*Now 1-2 subgoals: the disjunction, perhaps equality.*) rtac disjIn 1, diff -r 474b3f208789 -r 03a843f0f447 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/simpdata.ML Thu Sep 26 12:47:47 1996 +0200 @@ -33,8 +33,8 @@ (*** Addition of rules to simpsets and clasets simultaneously ***) (*Takes UNCONDITIONAL theorems of the form A<->B to - the Safe Intr rule B==>A and - the Safe Destruct rule A==>B. + the Safe Intr rule B==>A and + the Safe Destruct rule A==>B. Also ~A goes to the Safe Elim rule A ==> ?R Failing other cases, A is added as a Safe Intr rule*) local @@ -42,31 +42,31 @@ fun addIff th = (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of - (Const("not",_) $ A) => - AddSEs [zero_var_indexes (th RS notE)] - | (con $ _ $ _) => - if con=iff_const - then (AddSIs [zero_var_indexes (th RS iffD2)]; - AddSDs [zero_var_indexes (th RS iffD1)]) - else AddSIs [th] - | _ => AddSIs [th]; + (Const("not",_) $ A) => + AddSEs [zero_var_indexes (th RS notE)] + | (con $ _ $ _) => + if con=iff_const + then (AddSIs [zero_var_indexes (th RS iffD2)]; + AddSDs [zero_var_indexes (th RS iffD1)]) + else AddSIs [th] + | _ => AddSIs [th]; Addsimps [th]) handle _ => error ("AddIffs: theorem must be unconditional\n" ^ - string_of_thm th) + string_of_thm th) fun delIff th = (case HOLogic.dest_Trueprop (#prop(rep_thm th)) of - (Const("not",_) $ A) => - Delrules [zero_var_indexes (th RS notE)] - | (con $ _ $ _) => - if con=iff_const - then Delrules [zero_var_indexes (th RS iffD2), - zero_var_indexes (th RS iffD1)] - else Delrules [th] - | _ => Delrules [th]; + (Const("not",_) $ A) => + Delrules [zero_var_indexes (th RS notE)] + | (con $ _ $ _) => + if con=iff_const + then Delrules [zero_var_indexes (th RS iffD2), + zero_var_indexes (th RS iffD1)] + else Delrules [th] + | _ => Delrules [th]; Delsimps [th]) handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ - string_of_thm th) + string_of_thm th) in val AddIffs = seq addIff val DelIffs = seq delIff @@ -85,19 +85,19 @@ fun atomize pairs = let fun atoms th = - (case concl_of th of - Const("Trueprop",_) $ p => - (case head_of p of - Const(a,_) => - (case assoc(pairs,a) of - Some(rls) => flat (map atoms ([th] RL rls)) - | None => [th]) - | _ => [th]) - | _ => [th]) + (case concl_of th of + Const("Trueprop",_) $ p => + (case head_of p of + Const(a,_) => + (case assoc(pairs,a) of + Some(rls) => flat (map atoms ([th] RL rls)) + | None => [th]) + | _ => [th]) + | _ => [th]) in atoms end; fun mk_meta_eq r = case concl_of r of - Const("==",_)$_$_ => r + Const("==",_)$_$_ => r | _$(Const("op =",_)$_$_) => r RS eq_reflection | _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False | _ => r RS P_imp_P_eq_True; @@ -153,8 +153,8 @@ val expand_if = prove_goal HOL.thy "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), - rtac (if_P RS ssubst) 2, - rtac (if_not_P RS ssubst) 1, + stac if_P 2, + stac if_not_P 1, REPEAT(fast_tac HOL_cs 1) ]); val if_bool_eq = prove_goal HOL.thy @@ -183,21 +183,21 @@ (*Miniscoping: pushing in existential quantifiers*) val ex_simps = map prover - ["(EX x. P x & Q) = ((EX x.P x) & Q)", - "(EX x. P & Q x) = (P & (EX x.Q x))", - "(EX x. P x | Q) = ((EX x.P x) | Q)", - "(EX x. P | Q x) = (P | (EX x.Q x))", - "(EX x. P x --> Q) = ((ALL x.P x) --> Q)", - "(EX x. P --> Q x) = (P --> (EX x.Q x))"]; + ["(EX x. P x & Q) = ((EX x.P x) & Q)", + "(EX x. P & Q x) = (P & (EX x.Q x))", + "(EX x. P x | Q) = ((EX x.P x) | Q)", + "(EX x. P | Q x) = (P | (EX x.Q x))", + "(EX x. P x --> Q) = ((ALL x.P x) --> Q)", + "(EX x. P --> Q x) = (P --> (EX x.Q x))"]; (*Miniscoping: pushing in universal quantifiers*) val all_simps = map prover - ["(ALL x. P x & Q) = ((ALL x.P x) & Q)", - "(ALL x. P & Q x) = (P & (ALL x.Q x))", - "(ALL x. P x | Q) = ((ALL x.P x) | Q)", - "(ALL x. P | Q x) = (P | (ALL x.Q x))", - "(ALL x. P x --> Q) = ((EX x.P x) --> Q)", - "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; + ["(ALL x. P x & Q) = ((ALL x.P x) & Q)", + "(ALL x. P & Q x) = (P & (ALL x.Q x))", + "(ALL x. P x | Q) = ((ALL x.P x) | Q)", + "(ALL x. P | Q x) = (P | (ALL x.Q x))", + "(ALL x. P x --> Q) = ((EX x.P x) --> Q)", + "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; val HOL_ss = empty_ss setmksimps (mksimps mksimps_pairs) @@ -205,7 +205,7 @@ ORELSE' etac FalseE) setsubgoaler asm_simp_tac addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc, - cases_simp] + cases_simp] @ ex_simps @ all_simps @ simp_thms) addcongs [imp_cong]; @@ -245,13 +245,13 @@ val conj_cong = let val th = prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" - (fn _=> [fast_tac HOL_cs 1]) + (fn _=> [fast_tac HOL_cs 1]) in standard (impI RSN (2, th RS mp RS mp)) end; val rev_conj_cong = let val th = prove_goal HOL.thy "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" - (fn _=> [fast_tac HOL_cs 1]) + (fn _=> [fast_tac HOL_cs 1]) in standard (impI RSN (2, th RS mp RS mp)) end; (* '|' congruence rule: not included by default! *) @@ -259,7 +259,7 @@ val disj_cong = let val th = prove_goal HOL.thy "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" - (fn _=> [fast_tac HOL_cs 1]) + (fn _=> [fast_tac HOL_cs 1]) in standard (impI RSN (2, th RS mp RS mp)) end; (** 'if' congruence rules: neither included by default! *)