--- 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<j; 0<k |] ==> 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<n" 1);
by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff,
- mult_less_mono2]) 1);
+ mult_less_mono2]) 1);
by (subgoal_tac "~ k*na < k*n" 1);
by (asm_simp_tac
(!simpset addsimps [zero_less_mult_iff, div_geq,
- diff_mult_distrib2 RS sym, diff_less]) 1);
+ diff_mult_distrib2 RS sym, diff_less]) 1);
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le,
- le_refl RS mult_le_mono]) 1);
+ le_refl RS mult_le_mono]) 1);
qed "div_cancel";
goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
by (res_inst_tac [("n","m")] less_induct 1);
by (case_tac "na<n" 1);
by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff,
- mult_less_mono2]) 1);
+ mult_less_mono2]) 1);
by (subgoal_tac "~ k*na < k*n" 1);
by (asm_simp_tac
(!simpset addsimps [zero_less_mult_iff, mod_geq,
- diff_mult_distrib2 RS sym, diff_less]) 1);
+ diff_mult_distrib2 RS sym, diff_less]) 1);
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le,
- le_refl RS mult_le_mono]) 1);
+ le_refl RS mult_le_mono]) 1);
qed "mult_mod_distrib";
--- a/src/HOL/Finite.ML Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/Finite.ML Thu Sep 26 12:47:47 1996 +0200
@@ -74,7 +74,7 @@
by (Simp_tac 1);
by (asm_simp_tac
(!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
- delsimps [insert_Fin]) 1);
+ delsimps [insert_Fin]) 1);
qed "Fin_imageI";
val major::prems = goal Finite.thy
@@ -83,7 +83,7 @@
\ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> 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";
--- 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];
--- 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)]);
--- 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<n+k ==> (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<n; ~n<k|] ==> (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<n & ~n<k")] mp 1);
-ba 2;
+by (assume_tac 2);
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
by (ALLGOALS Asm_simp_tac);
-br impI 1;
+by (rtac impI 1);
by (dres_inst_tac [("P","~x<y")] conjE 1);
-ba 2;
-br (Suc_diff_n RS sym) 1;
-br le_less_trans 1;
-be (not_less_eq RS subst) 2;
-br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
+by (assume_tac 2);
+by (rtac (Suc_diff_n RS sym) 1);
+by (rtac le_less_trans 1);
+by (etac (not_less_eq RS subst) 2);
+by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
qed "diff_add_not_assoc";
val prems=goal Arith.thy "~n<k ==> (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 | n<m)";
-br iffI 1;
+by (rtac iffI 1);
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
by (Asm_full_simp_tac 1);
-be disjE 1;
-be (less_not_refl2 RS not_sym) 1;
-be less_not_refl2 1;
+by (etac disjE 1);
+by (etac (less_not_refl2 RS not_sym) 1);
+by (etac less_not_refl2 1);
qed "not_eq_eq_less_or_gr";
val [prem] = goal Arith.thy "m<n ==> 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<k; m~=(n::nat)|] ==> m*k~=n*k";
by (cut_facts_tac prems 1);
by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
-br (less_not_refl2 RS not_sym) 2;
-be mult_less_mono_r 2;
-br less_not_refl2 3;
-be mult_less_mono_r 3;
+by (rtac (less_not_refl2 RS not_sym) 2);
+by (etac mult_less_mono_r 2);
+by (rtac less_not_refl2 3);
+by (etac mult_less_mono_r 3);
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
qed "mult_not_eq_mono_r";
@@ -166,29 +166,29 @@
val prems=goal thy "0<n ==> 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<n ==> 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<n")] subst 1);
by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
-br le_add1 1;
+by (rtac le_add1 1);
qed "mod_eq_add";
val prems=goal thy "0<n ==> 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<x; m mod x = 0; n mod x = 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<x; m mod x = 0; n mod x = 0; n<=m|] ==> (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<n ==> 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<m|] ==> 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<n ==> 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<m ==> 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<n ==> 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 ==> 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<m ==> !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<n ==> gcd m n = gcd m (n-m)";
by (cut_facts_tac prems 1);
by (subgoal_tac "m<n ==> !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 ***)
--- 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);
--- 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";
--- 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,s> -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);
--- 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";
--- 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,s> -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,s> -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',s'> -c-> t --> <c,s> -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',s'> -c-> t --> <c,s> -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,s> -c-> t";
--- 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";
--- 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";
--- 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<j --> ~ 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<k then i else Suc i))";
-by(db.induct_tac "s" 1);
-by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
+by (db.induct_tac "s" 1);
+by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
[less_not_refl2,less_not_refl2 RS not_sym])));
-by(fast_tac HOL_cs 2);
-by(safe_tac (HOL_cs addSIs [iffI]));
-by(ALLGOALS(Asm_simp_tac));
-by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
-by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
+by (fast_tac HOL_cs 2);
+by (safe_tac (HOL_cs addSIs [iffI]));
+by (ALLGOALS(Asm_simp_tac));
+by (fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
+by (fast_tac (HOL_cs addDs [less_not_sym]) 1);
by (dtac Suc_mono 1);
-by(dtac less_interval1 1 THEN atac 1);
-by(asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-by(dtac less_trans_Suc 1 THEN atac 1);
-by(Asm_full_simp_tac 1);
+by (dtac less_interval1 1 THEN atac 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (dtac less_trans_Suc 1 THEN atac 1);
+by (Asm_full_simp_tac 1);
qed "free_subst";
Addsimps [free_subst];
goal Eta.thy "!!s. s -e> 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";
--- 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";
--- 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";
--- 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";
--- 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];
--- 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 *)
--- 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;
--- 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<n";
-by( fast_tac HOL_cs 1 );
+by ( fast_tac HOL_cs 1 );
qed "free_tv_le_new_tv";
goal thy
"free_tv (s (v::nat)) <= cod s Un {v}";
-by( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
-by( safe_tac (HOL_cs addSIs [subsetI]) );
+by ( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
+by ( safe_tac (HOL_cs addSIs [subsetI]) );
by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
qed "free_tv_subst_var";
goal thy
"free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by( typ.induct_tac "t" 1);
+by ( typ.induct_tac "t" 1);
(* case TVar n *)
-by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
(* case Fun t1 t2 *)
-by( fast_tac (set_cs addss !simpset) 1);
+by ( fast_tac (set_cs addss !simpset) 1);
qed "free_tv_app_subst_te";
goal thy
"free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by( list.induct_tac "ts" 1);
+by ( list.induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case a#al *)
-by( cut_facts_tac [free_tv_app_subst_te] 1);
-by( fast_tac (set_cs addss !simpset) 1);
+by ( cut_facts_tac [free_tv_app_subst_te] 1);
+by ( fast_tac (set_cs addss !simpset) 1);
qed "free_tv_app_subst_tel";
goalw thy [free_tv_subst,dom_def]
"free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \
\ free_tv s1 Un free_tv s2";
-by( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
+by ( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
subsetD,free_tv_subst_var RS subsetD] addss (
!simpset addsimps [cod_def,dom_def])) 1);
qed "free_tv_comp_subst";
--- a/src/HOL/MiniML/W.ML Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/MiniML/W.ML Thu Sep 26 12:47:47 1996 +0200
@@ -22,11 +22,11 @@
setloop (split_tac [expand_bind])) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
-by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
+by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
(* case App e1 e2 *)
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
by (strip_tac 1);
-by( rename_tac "sa ta na sb tb nb sc" 1);
+by ( rename_tac "sa ta na sb tb nb sc" 1);
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
by (rtac (app_subst_Fun RS subst) 1);
@@ -83,7 +83,7 @@
(* auxiliary lemma *)
goal Maybe.thy "(y = Ok x) = (Ok x = y)";
-by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
qed "rotate_Ok";
@@ -121,7 +121,7 @@
by (eres_inst_tac [("x","sa")] allE 1);
by (eres_inst_tac [("x","ta")] allE 1);
by (eres_inst_tac [("x","nb")] allE 1);
-by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
by (rtac conjI 1);
by (rtac new_tv_subst_comp_2 1);
by (rtac new_tv_subst_comp_2 1);
@@ -134,25 +134,25 @@
1);
by (etac (sym RS mgu_new) 1);
by (best_tac (HOL_cs addDs [W_var_geD]
- addIs [new_tv_subst_te,new_tv_list_le,
- new_tv_subst_tel,
- lessI RS less_imp_le RS new_tv_le,
- lessI RS less_imp_le RS new_tv_subst_le,
- new_tv_le]) 1);
+ addIs [new_tv_subst_te,new_tv_list_le,
+ new_tv_subst_tel,
+ lessI RS less_imp_le RS new_tv_le,
+ lessI RS less_imp_le RS new_tv_subst_le,
+ new_tv_le]) 1);
by (fast_tac (HOL_cs addDs [W_var_geD]
- addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
- addss (!simpset)) 1);
+ addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
+ addss (!simpset)) 1);
by (rtac (lessI RS new_tv_subst_var) 1);
by (etac (sym RS mgu_new) 1);
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
addDs [W_var_geD]
- addIs [new_tv_list_le,
- new_tv_subst_tel,
- lessI RS less_imp_le RS new_tv_subst_le,
- new_tv_le]
- addss !simpset) 1);
+ addIs [new_tv_list_le,
+ new_tv_subst_tel,
+ lessI RS less_imp_le RS new_tv_subst_le,
+ new_tv_le]
+ addss !simpset) 1);
by (fast_tac (HOL_cs addDs [W_var_geD]
- addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
+ addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
addss (!simpset)) 1);
qed_spec_mp "new_tv_W";
@@ -226,7 +226,7 @@
(* case Var n *)
by (strip_tac 1);
by (simp_tac (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_if])) 1);
+ setloop (split_tac [expand_if])) 1);
by (eresolve_tac has_type_casesE 1);
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
by (res_inst_tac [("x","id_subst")] exI 1);
@@ -243,7 +243,7 @@
by (eres_inst_tac [("x","t2")] allE 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_bind]))) 1);
+ setloop (split_tac [expand_bind]))) 1);
(* case App e1 e2 *)
by (strip_tac 1);
@@ -264,7 +264,7 @@
by (safe_tac HOL_cs);
by (fast_tac HOL_cs 1);
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
- conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
+ conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
by (subgoal_tac
"$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
@@ -279,11 +279,11 @@
by (strip_tac 2);
by (subgoal_tac "na ~=ma" 2);
by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
- new_tv_not_free_tv,new_tv_le]) 3);
+ new_tv_not_free_tv,new_tv_le]) 3);
by (case_tac "na:free_tv sa" 2);
(* na ~: free_tv sa *)
by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
- setloop (split_tac [expand_if])) 3);
+ setloop (split_tac [expand_if])) 3);
(* na : free_tv sa *)
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
by (dtac eq_subst_tel_eq_free 2);
@@ -292,7 +292,7 @@
by (case_tac "na:dom sa" 2);
(* na ~: dom sa *)
by (asm_full_simp_tac (!simpset addsimps [dom_def]
- setloop (split_tac [expand_if])) 3);
+ setloop (split_tac [expand_if])) 3);
(* na : dom sa *)
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2);
@@ -302,9 +302,9 @@
by (dtac new_tv_subst_tel 3);
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
- (!simpset addsimps [cod_def,free_tv_subst])) 3);
+ (!simpset addsimps [cod_def,free_tv_subst])) 3);
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
- setloop (split_tac [expand_if]))) 2);
+ setloop (split_tac [expand_if]))) 2);
by (Simp_tac 2);
by (rtac eq_free_eq_subst_te 2);
@@ -316,9 +316,9 @@
by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
by (case_tac "na: free_tv t - free_tv sa" 2);
(* case na ~: free_tv t - free_tv sa *)
-by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
(* case na : free_tv t - free_tv sa *)
-by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
by (dtac eq_subst_tel_eq_free 2);
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -327,7 +327,7 @@
by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
by (safe_tac HOL_cs );
by (dtac mgu_Ok 1);
-by( fast_tac (HOL_cs addss !simpset) 1);
+by ( fast_tac (HOL_cs addss !simpset) 1);
by (REPEAT (resolve_tac [exI,conjI] 1));
by (fast_tac HOL_cs 1);
by (fast_tac HOL_cs 1);
@@ -336,13 +336,13 @@
by (res_inst_tac [("x","rb")] exI 1);
by (rtac conjI 1);
by (dres_inst_tac [("x","ma")] fun_cong 2);
-by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
+by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN
(2,trans)) 1);
-by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
by (rtac eq_free_eq_subst_tel 1);
-by( safe_tac HOL_cs );
+by ( safe_tac HOL_cs );
by (subgoal_tac "ma ~= na" 1);
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
by (etac conjE 2);
@@ -367,7 +367,7 @@
goal W.thy
"!!e. [] |- e :: t' ==> (? 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";
--- 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]);
--- 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";
--- 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;
--- 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];
--- 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 **)
--- 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))";
--- 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";
--- 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";
--- 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]);
--- 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*)
--- 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
--- 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";
--- 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";
--- 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";
--- 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";
--- 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";
--- 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]
--- 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;
--- 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();
--- 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";
--- 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];
--- 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();
--- 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
--- 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*)
--- 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);
--- 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))))) \
--- 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 =
--- 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,
--- 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! *)