--- a/src/HOL/Divides.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Divides.ML Fri Aug 14 12:03:01 1998 +0200
@@ -201,7 +201,7 @@
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
-br le_trans 1;
+by (rtac le_trans 1);
by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
qed "div_le_mono2";
--- a/src/HOL/Fun.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Fun.ML Fri Aug 14 12:03:01 1998 +0200
@@ -78,7 +78,7 @@
by (rtac iffI 1);
by (etac arg_cong 2);
by (etac injD 1);
-ba 1;
+by (assume_tac 1);
qed "inj_eq";
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
--- a/src/HOL/Lambda/InductTermi.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Lambda/InductTermi.ML Fri Aug 14 12:03:01 1998 +0200
@@ -8,37 +8,37 @@
Goal "s : termi beta ==> !t. t : termi beta --> \
\ (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)";
-be acc_induct 1;
-be thin_rl 1;
-br allI 1;
-br impI 1;
-be acc_induct 1;
-by(Clarify_tac 1);
-br accI 1;
-by(safe_tac (claset() addSEs [apps_betasE]));
- ba 1;
- by(blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1);
- by(blast_tac (claset()
+by (etac acc_induct 1);
+by (etac thin_rl 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (etac acc_induct 1);
+by (Clarify_tac 1);
+by (rtac accI 1);
+by (safe_tac (claset() addSEs [apps_betasE]));
+ by (assume_tac 1);
+ by (blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1);
+ by (blast_tac (claset()
addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI]
addDs [acc_downwards]) 1);
(* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
-by(blast_tac (claset() addDs [apps_preserves_betas]) 1);
+by (blast_tac (claset() addDs [apps_preserves_betas]) 1);
qed_spec_mp "double_induction_lemma";
Goal "t : IT ==> t : termi(beta)";
be IT.induct 1;
- bd rev_subsetD 1;
- br lists_mono 1;
- br Int_lower2 1;
- by(Asm_full_simp_tac 1);
- bd lists_accD 1;
- be acc_induct 1;
- br accI 1;
- by(blast_tac (claset() addSDs [head_Var_reduction]) 1);
- be acc_induct 1;
- br accI 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [double_induction_lemma]) 1);
+ by (dtac rev_subsetD 1);
+ by (rtac lists_mono 1);
+ by (rtac Int_lower2 1);
+ by (Asm_full_simp_tac 1);
+ by (dtac lists_accD 1);
+ by (etac acc_induct 1);
+ by (rtac accI 1);
+ by (blast_tac (claset() addSDs [head_Var_reduction]) 1);
+ by (etac acc_induct 1);
+ by (rtac accI 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [double_induction_lemma]) 1);
qed "IT_implies_termi";
(*** Every terminating term is in IT ***)
@@ -55,69 +55,69 @@
(* Turned out to be redundant:
Goal "t : termi beta ==> \
\ !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
-be acc_induct 1;
-by(force_tac (claset()
+by (etac acc_induct 1);
+by (force_tac (claset()
addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1);
val lemma = result();
Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)";
-bd lemma 1;
-by(Blast_tac 1);
+by (dtac lemma 1);
+by (Blast_tac 1);
qed "apps_in_termi_betaD";
Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta";
-be acc_induct 1;
-by(force_tac (claset() addIs [accI],simpset()) 1);
+by (etac acc_induct 1);
+by (force_tac (claset() addIs [accI],simpset()) 1);
val lemma = result();
Goal "Abs r : termi beta ==> r : termi beta";
-bd lemma 1;
-by(Blast_tac 1);
+by (dtac lemma 1);
+by (Blast_tac 1);
qed "Abs_in_termi_betaD";
Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta";
-be acc_induct 1;
-by(force_tac (claset() addIs [accI],simpset()) 1);
+by (etac acc_induct 1);
+by (force_tac (claset() addIs [accI],simpset()) 1);
val lemma = result();
Goal "r$s : termi beta ==> r : termi beta & s : termi beta";
-bd lemma 1;
-by(Blast_tac 1);
+by (dtac lemma 1);
+by (Blast_tac 1);
qed "App_in_termi_betaD";
*)
Goal "r : termi beta ==> r : IT";
-be acc_induct 1;
-by(rename_tac "r" 1);
-be thin_rl 1;
-be rev_mp 1;
-by(Simp_tac 1);
-by(res_inst_tac [("t","r")] Apps_dB_induct 1);
- by(rename_tac "n ts" 1);
- by(Clarify_tac 1);
+by (etac acc_induct 1);
+by (rename_tac "r" 1);
+by (etac thin_rl 1);
+by (etac rev_mp 1);
+by (Simp_tac 1);
+by (res_inst_tac [("t","r")] Apps_dB_induct 1);
+ by (rename_tac "n ts" 1);
+ by (Clarify_tac 1);
brs IT.intrs 1;
- by(Clarify_tac 1);
- by(EVERY1[dtac bspec, atac]);
- be mp 1;
- by(Clarify_tac 1);
- bd converseI 1;
- by(EVERY1[dtac ex_step1I, atac]);
- by(Clarify_tac 1);
- by(rename_tac "us" 1);
- by(eres_inst_tac [("x","Var n $$ us")] allE 1);
- by(Force_tac 1);
-by(rename_tac "u ts" 1);
-by(exhaust_tac "ts" 1);
- by(Asm_full_simp_tac 1);
- by(blast_tac (claset() addIs IT.intrs) 1);
-by(rename_tac "s ss" 1);
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
+ by (Clarify_tac 1);
+ by (EVERY1[dtac bspec, atac]);
+ by (etac mp 1);
+ by (Clarify_tac 1);
+ by (dtac converseI 1);
+ by (EVERY1[dtac ex_step1I, atac]);
+ by (Clarify_tac 1);
+ by (rename_tac "us" 1);
+ by (eres_inst_tac [("x","Var n $$ us")] allE 1);
+ by (Force_tac 1);
+by (rename_tac "u ts" 1);
+by (exhaust_tac "ts" 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addIs IT.intrs) 1);
+by (rename_tac "s ss" 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
brs IT.intrs 1;
- by(blast_tac (claset() addIs [apps_preserves_beta]) 1);
-be mp 1;
- by(Clarify_tac 1);
- by(rename_tac "t" 1);
- by(eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1);
- by(Force_tac 1);
+ by (blast_tac (claset() addIs [apps_preserves_beta]) 1);
+by (etac mp 1);
+ by (Clarify_tac 1);
+ by (rename_tac "t" 1);
+ by (eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1);
+ by (Force_tac 1);
qed "termi_implies_IT";
--- a/src/HOL/Lambda/Lambda.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML Fri Aug 14 12:03:01 1998 +0200
@@ -140,20 +140,20 @@
Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
be beta.induct 1;
-by(ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
qed_spec_mp "subst_preserves_beta";
Addsimps [subst_preserves_beta];
Goal "r -> s ==> !i. lift r i -> lift s i";
be beta.induct 1;
-by(Auto_tac);
+by (Auto_tac);
qed_spec_mp "lift_preserves_beta";
Addsimps [lift_preserves_beta];
Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]";
-by(induct_tac "t" 1);
-by(asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
-by(asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
-by(asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
+by (induct_tac "t" 1);
+by (asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
+by (asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
+by (asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
qed_spec_mp "subst_preserves_beta2";
Addsimps [subst_preserves_beta2];
--- a/src/HOL/Lambda/ListApplication.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Lambda/ListApplication.ML Fri Aug 14 12:03:01 1998 +0200
@@ -5,97 +5,97 @@
*)
Goal "(r$$ts = s$$ts) = (r = s)";
-by(rev_induct_tac "ts" 1);
-by(Auto_tac);
+by (rev_induct_tac "ts" 1);
+by (Auto_tac);
qed "apps_eq_tail_conv";
AddIffs [apps_eq_tail_conv];
Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
-by(induct_tac "ss" 1);
-by(Auto_tac);
+by (induct_tac "ss" 1);
+by (Auto_tac);
qed_spec_mp "Var_eq_apps_conv";
AddIffs [Var_eq_apps_conv];
Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
-by(rev_induct_tac "rs" 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
-br allI 1;
-by(rev_induct_tac "ss" 1);
-by(Auto_tac);
+by (rev_induct_tac "rs" 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (rev_induct_tac "ss" 1);
+by (Auto_tac);
qed_spec_mp "Var_apps_eq_Var_apps_conv";
AddIffs [Var_apps_eq_Var_apps_conv];
Goal "(r$s = t$$ts) = \
\ (if ts = [] then r$s = t \
\ else (? ss. ts = ss@[s] & r = t$$ss))";
-by(res_inst_tac [("xs","ts")] rev_exhaust 1);
-by(Auto_tac);
+by (res_inst_tac [("xs","ts")] rev_exhaust 1);
+by (Auto_tac);
qed "App_eq_foldl_conv";
Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
-by(rev_induct_tac "ss" 1);
-by(Auto_tac);
+by (rev_induct_tac "ss" 1);
+by (Auto_tac);
qed "Abs_eq_apps_conv";
AddIffs [Abs_eq_apps_conv];
Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
-by(rev_induct_tac "ss" 1);
-by(Auto_tac);
+by (rev_induct_tac "ss" 1);
+by (Auto_tac);
qed "apps_eq_Abs_conv";
AddIffs [apps_eq_Abs_conv];
Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
-by(rev_induct_tac "rs" 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
-br allI 1;
-by(rev_induct_tac "ss" 1);
-by(Auto_tac);
+by (rev_induct_tac "rs" 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (rev_induct_tac "ss" 1);
+by (Auto_tac);
qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
AddIffs [Abs_apps_eq_Abs_apps_conv];
Goal "!s t. Abs s $ t ~= (Var n)$$ss";
-by(rev_induct_tac "ss" 1);
-by(Auto_tac);
+by (rev_induct_tac "ss" 1);
+by (Auto_tac);
qed_spec_mp "Abs_App_neq_Var_apps";
AddIffs [Abs_App_neq_Var_apps];
Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
-by(rev_induct_tac "ss" 1);
- by(Simp_tac 1);
-br allI 1;
-by(rev_induct_tac "ts" 1);
-by(Auto_tac);
+by (rev_induct_tac "ss" 1);
+ by (Simp_tac 1);
+by (rtac allI 1);
+by (rev_induct_tac "ts" 1);
+by (Auto_tac);
qed_spec_mp "Var_apps_neq_Abs_apps";
AddIffs [Var_apps_neq_Abs_apps];
Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
-by(induct_tac "t" 1);
- by(res_inst_tac[("x","[]")] exI 1);
- by(Simp_tac 1);
- by(Clarify_tac 1);
- by(rename_tac "ts1 ts2 h1 h2" 1);
- by(res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
+by (induct_tac "t" 1);
+ by (res_inst_tac[("x","[]")] exI 1);
+ by (Simp_tac 1);
+ by (Clarify_tac 1);
+ by (rename_tac "ts1 ts2 h1 h2" 1);
+ by (res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
qed "ex_head_tail";
Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
-by(rev_induct_tac "rs" 1);
-by(Auto_tac);
+by (rev_induct_tac "rs" 1);
+by (Auto_tac);
qed "size_apps";
Addsimps [size_apps];
Goal "[| 0 < k; m <= n |] ==> m < n+k";
-by(exhaust_tac "k" 1);
- by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
-br le_imp_less_Suc 1;
-by(exhaust_tac "n" 1);
- by(Asm_full_simp_tac 1);
-by(hyp_subst_tac 1);
-be trans_le_add1 1;
+by (exhaust_tac "k" 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac le_imp_less_Suc 1);
+by (exhaust_tac "n" 1);
+ by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by (etac trans_le_add1 1);
val lemma = result();
(* a customized induction schema for $$ *)
@@ -104,39 +104,39 @@
"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
\|] ==> !t. size t = n --> P t";
-by(res_inst_tac [("n","n")] less_induct 1);
-br allI 1;
-by(cut_inst_tac [("t","t")] ex_head_tail 1);
-by(Clarify_tac 1);
-be disjE 1;
- by(Clarify_tac 1);
- brs prems 1;
- by(Clarify_tac 1);
- by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
- by(Simp_tac 1);
- br lemma 1;
- by(Force_tac 1);
- br elem_le_sum 1;
- by(Force_tac 1);
-by(Clarify_tac 1);
-brs prems 1;
-by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
-by(Simp_tac 1);
-by(Clarify_tac 1);
-by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
-by(Simp_tac 1);
-br le_imp_less_Suc 1;
-br trans_le_add1 1;
-br trans_le_add2 1;
-br elem_le_sum 1;
-by(Force_tac 1);
+by (res_inst_tac [("n","n")] less_induct 1);
+by (rtac allI 1);
+by (cut_inst_tac [("t","t")] ex_head_tail 1);
+by (Clarify_tac 1);
+by (etac disjE 1);
+ by (Clarify_tac 1);
+ by (resolve_tac prems 1);
+ by (Clarify_tac 1);
+ by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
+ by (Simp_tac 1);
+ by (rtac lemma 1);
+ by (Force_tac 1);
+ by (rtac elem_le_sum 1);
+ by (Force_tac 1);
+by (Clarify_tac 1);
+by (resolve_tac prems 1);
+by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
+by (Simp_tac 1);
+by (Clarify_tac 1);
+by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
+by (Simp_tac 1);
+by (rtac le_imp_less_Suc 1);
+by (rtac trans_le_add1 1);
+by (rtac trans_le_add2 1);
+by (rtac elem_le_sum 1);
+by (Force_tac 1);
val lemma = result() RS spec RS mp;
val prems = Goal
"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
\|] ==> P t";
-by(res_inst_tac [("x1","t")] lemma 1);
-br refl 3;
-by(REPEAT(ares_tac prems 1));
+by (res_inst_tac [("x1","t")] lemma 1);
+by (rtac refl 3);
+by (REPEAT(ares_tac prems 1));
qed "Apps_dB_induct";
--- a/src/HOL/Lambda/ListBeta.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Lambda/ListBeta.ML Fri Aug 14 12:03:01 1998 +0200
@@ -7,21 +7,21 @@
Goal
"v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
be beta.induct 1;
-by(Asm_full_simp_tac 1);
-br allI 1;
-by(res_inst_tac [("xs","rs")] rev_exhaust 1);
-by(Asm_full_simp_tac 1);
-by(force_tac (claset() addIs [append_step1I],simpset()) 1);
-br allI 1;
-by(res_inst_tac [("xs","rs")] rev_exhaust 1);
-by(Asm_full_simp_tac 1);
-by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
-by(Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("xs","rs")] rev_exhaust 1);
+by (Asm_full_simp_tac 1);
+by (force_tac (claset() addIs [append_step1I],simpset()) 1);
+by (rtac allI 1);
+by (res_inst_tac [("xs","rs")] rev_exhaust 1);
+by (Asm_full_simp_tac 1);
+by (force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
+by (Asm_full_simp_tac 1);
val lemma = result();
Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)";
-bd lemma 1;
-by(Blast_tac 1);
+by (dtac lemma 1);
+by (Blast_tac 1);
qed "head_Var_reduction";
Goal "u -> u' ==> !r rs. u = r$$rs --> \
@@ -29,31 +29,31 @@
\ (? rs'. rs => rs' & u' = r$$rs') | \
\ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
be beta.induct 1;
- by(clarify_tac (claset() delrules [disjCI]) 1);
- by(exhaust_tac "r" 1);
- by(Asm_full_simp_tac 1);
- by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
- by(split_asm_tac [split_if_asm] 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
- by(Asm_full_simp_tac 1);
- by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
- by(split_asm_tac [split_if_asm] 1);
- by(Asm_full_simp_tac 1);
- by(Asm_full_simp_tac 1);
- by(clarify_tac (claset() delrules [disjCI]) 1);
- bd (App_eq_foldl_conv RS iffD1) 1;
- by(split_asm_tac [split_if_asm] 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
- by(force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
- by(clarify_tac (claset() delrules [disjCI]) 1);
- bd (App_eq_foldl_conv RS iffD1) 1;
- by(split_asm_tac [split_if_asm] 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
- by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
-by(Asm_full_simp_tac 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (exhaust_tac "r" 1);
+ by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
+ by (split_asm_tac [split_if_asm] 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
+ by (split_asm_tac [split_if_asm] 1);
+ by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (dtac (App_eq_foldl_conv RS iffD1) 1);
+ by (split_asm_tac [split_if_asm] 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+ by (force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (dtac (App_eq_foldl_conv RS iffD1) 1);
+ by (split_asm_tac [split_if_asm] 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+ by (force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
+by (Asm_full_simp_tac 1);
val lemma = result();
Goal "[| r$$rs -> s; \
@@ -61,8 +61,8 @@
\ !rs'. rs => rs' --> s = r$$rs' --> R; \
\ !t u us. r = Abs t --> rs = u#us --> s = t[u/0]$$us --> R \
\ |] ==> R";
-bd lemma 1;
-by(blast_tac HOL_cs 1);
+by (dtac lemma 1);
+by (blast_tac HOL_cs 1);
val lemma = result();
bind_thm("apps_betasE",
impI RSN (4,impI RSN (4,impI RSN (4,allI RSN (4,allI RSN (4,allI RSN (4,
@@ -71,27 +71,27 @@
AddSEs [apps_betasE];
Goal "r -> s ==> r$$ss -> s$$ss";
-by(res_inst_tac [("xs","ss")] rev_induct 1);
-by(Auto_tac);
+by (res_inst_tac [("xs","ss")] rev_induct 1);
+by (Auto_tac);
qed "apps_preserves_beta";
Addsimps [apps_preserves_beta];
Goal "r ->> s ==> r$$ss ->> s$$ss";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
qed "apps_preserves_beta2";
Addsimps [apps_preserves_beta2];
Goal "!ss. rs => ss --> r$$rs -> r$$ss";
-by(res_inst_tac [("xs","rs")] rev_induct 1);
- by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(res_inst_tac [("xs","ss")] rev_exhaust 1);
- by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
-bd Snoc_step1_SnocD 1;
-by(Blast_tac 1);
+by (res_inst_tac [("xs","rs")] rev_induct 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("xs","ss")] rev_exhaust 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (dtac Snoc_step1_SnocD 1);
+by (Blast_tac 1);
qed_spec_mp "apps_preserves_betas";
Addsimps [apps_preserves_betas];
--- a/src/HOL/Lambda/ListOrder.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Lambda/ListOrder.ML Fri Aug 14 12:03:01 1998 +0200
@@ -5,55 +5,55 @@
*)
Goalw [step1_def] "step1(r^-1) = (step1 r)^-1";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "step1_converse";
Addsimps [step1_converse];
Goal "(p : step1(r^-1)) = (p : (step1 r)^-1)";
-by(Auto_tac);
+by (Auto_tac);
qed "in_step1_converse";
AddIffs [in_step1_converse];
Goalw [step1_def] "([],xs) ~: step1 r";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "not_Nil_step1";
AddIffs [not_Nil_step1];
Goalw [step1_def] "(xs,[]) ~: step1 r";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "not_step1_Nil";
AddIffs [not_step1_Nil];
Goalw [step1_def]
"((y#ys,x#xs) : step1 r) = ((y,x):r & xs=ys | x=y & (ys,xs) : step1 r)";
-by(Asm_full_simp_tac 1);
-br iffI 1;
- be exE 1;
- by(rename_tac "ts" 1);
- by(exhaust_tac "ts" 1);
- by(Force_tac 1);
- by(Force_tac 1);
-be disjE 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [Cons_eq_appendI]) 1);
+by (Asm_full_simp_tac 1);
+by (rtac iffI 1);
+ by (etac exE 1);
+ by (rename_tac "ts" 1);
+ by (exhaust_tac "ts" 1);
+ by (Force_tac 1);
+ by (Force_tac 1);
+by (etac disjE 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [Cons_eq_appendI]) 1);
qed "Cons_step1_Cons";
AddIffs [Cons_step1_Cons];
Goalw [step1_def]
"(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
\ ==> (ys@vs,xs@us) : step1 r";
-by(Auto_tac);
-by(Force_tac 1);
-by(blast_tac (claset() addIs [append_eq_appendI]) 1);
+by (Auto_tac);
+by (Force_tac 1);
+by (blast_tac (claset() addIs [append_eq_appendI]) 1);
qed "append_step1I";
Goal "[| (ys,x#xs) : step1 r; \
\ !y. ys = y#xs --> (y,x) : r --> R; \
\ !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
\ |] ==> R";
-by(exhaust_tac "ys" 1);
- by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
-by(Blast_tac 1);
+by (exhaust_tac "ys" 1);
+ by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
+by (Blast_tac 1);
val lemma = result();
bind_thm("Cons_step1E",
impI RSN (3,impI RSN (3,allI RSN (3,impI RSN (2,
@@ -62,44 +62,44 @@
Goalw [step1_def]
"(ys@[y],xs@[x]) : step1 r ==> ((ys,xs) : step1 r & y=x | ys=xs & (y,x) : r)";
-by(Asm_full_simp_tac 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
-by(rename_tac "vs" 1);
-by(res_inst_tac [("xs","vs")]rev_exhaust 1);
- by(Force_tac 1);
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (rename_tac "vs" 1);
+by (res_inst_tac [("xs","vs")]rev_exhaust 1);
+ by (Force_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
qed "Snoc_step1_SnocD";
Goal "x : acc r ==> !xs. xs : acc(step1 r) --> x#xs : acc(step1 r)";
-be acc_induct 1;
-be thin_rl 1;
-by(Clarify_tac 1);
-be acc_induct 1;
-br accI 1;
-by(Blast_tac 1);
+by (etac acc_induct 1);
+by (etac thin_rl 1);
+by (Clarify_tac 1);
+by (etac acc_induct 1);
+by (rtac accI 1);
+by (Blast_tac 1);
val lemma = result();
qed_spec_mp "Cons_acc_step1I";
AddSIs [Cons_acc_step1I];
Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
be lists.induct 1;
- br accI 1;
- by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
-br accI 1;
-by(fast_tac (claset() addDs [acc_downward]) 1);
+ by (rtac accI 1);
+ by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
+by (rtac accI 1);
+by (fast_tac (claset() addDs [acc_downward]) 1);
qed "lists_accD";
Goalw [step1_def]
"[| x : set xs; (y,x) : r |] ==> ? ys. (ys,xs) : step1 r & y : set ys";
-bd (in_set_conv_decomp RS iffD1) 1;
-by(Force_tac 1);
+by (dtac (in_set_conv_decomp RS iffD1) 1);
+by (Force_tac 1);
qed "ex_step1I";
Goal "xs : acc(step1 r) ==> xs : lists(acc r)";
-be acc_induct 1;
-by(Clarify_tac 1);
-br accI 1;
-by(EVERY1[dtac ex_step1I, atac]);
-by(Blast_tac 1);
+by (etac acc_induct 1);
+by (Clarify_tac 1);
+by (rtac accI 1);
+by (EVERY1[dtac ex_step1I, atac]);
+by (Blast_tac 1);
qed "lists_accI";
--- a/src/HOL/List.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/List.ML Fri Aug 14 12:03:01 1998 +0200
@@ -232,17 +232,17 @@
(* trivial rules for solving @-equations automatically *)
Goal "xs = ys ==> xs = [] @ ys";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "eq_Nil_appendI";
Goal "[| x#xs1 = ys; xs = xs1 @ zs |] ==> x#xs = ys@zs";
-bd sym 1;
-by(Asm_simp_tac 1);
+by (dtac sym 1);
+by (Asm_simp_tac 1);
qed "Cons_eq_appendI";
Goal "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us";
-bd sym 1;
-by(Asm_simp_tac 1);
+by (dtac sym 1);
+by (Asm_simp_tac 1);
qed "append_eq_appendI";
@@ -411,20 +411,20 @@
Addsimps [in_set_filter];
Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(Asm_simp_tac 1);
-br iffI 1;
-by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
-by(REPEAT(etac exE 1));
-by(exhaust_tac "ys" 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (Asm_simp_tac 1);
+by (rtac iffI 1);
+by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
+by (REPEAT(etac exE 1));
+by (exhaust_tac "ys" 1);
by Auto_tac;
qed "in_set_conv_decomp";
(* eliminate `lists' in favour of `set' *)
Goal "(xs : lists A) = (!x : set xs. x : A)";
-by(induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by Auto_tac;
qed "in_lists_conv_set";
@@ -799,7 +799,7 @@
section "foldl";
Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
-by(induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by Auto_tac;
qed_spec_mp "foldl_append";
Addsimps [foldl_append];
@@ -808,19 +808,19 @@
because it requires an additional transitivity step
*)
Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
-by(induct_tac "ns" 1);
- by(Simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [trans_le_add1]) 1);
+by (induct_tac "ns" 1);
+ by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [trans_le_add1]) 1);
qed_spec_mp "start_le_sum";
Goal "n : set ns ==> n <= foldl op+ 0 ns";
-by(auto_tac (claset() addIs [start_le_sum],
+by (auto_tac (claset() addIs [start_le_sum],
simpset() addsimps [in_set_conv_decomp]));
qed "elem_le_sum";
Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
-by(induct_tac "ns" 1);
+by (induct_tac "ns" 1);
by Auto_tac;
qed_spec_mp "sum_eq_0_conv";
AddIffs [sum_eq_0_conv];
@@ -864,29 +864,29 @@
section"Lexcicographic orderings on lists";
Goal "wf r ==> wf(lexn r n)";
-by(induct_tac "n" 1);
-by(Simp_tac 1);
-by(Simp_tac 1);
-br wf_subset 1;
-br Int_lower1 2;
-br wf_prod_fun_image 1;
-br injI 2;
-by(Auto_tac);
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (rtac wf_subset 1);
+by (rtac Int_lower1 2);
+by (rtac wf_prod_fun_image 1);
+by (rtac injI 2);
+by (Auto_tac);
qed "wf_lexn";
Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
-by(induct_tac "n" 1);
-by(Auto_tac);
+by (induct_tac "n" 1);
+by (Auto_tac);
qed_spec_mp "lexn_length";
Goalw [lex_def] "wf r ==> wf(lex r)";
-br wf_UN 1;
-by(blast_tac (claset() addIs [wf_lexn]) 1);
-by(Clarify_tac 1);
-by(rename_tac "m n" 1);
-by(subgoal_tac "m ~= n" 1);
- by(Blast_tac 2);
-by(blast_tac (claset() addDs [lexn_length,not_sym]) 1);
+by (rtac wf_UN 1);
+by (blast_tac (claset() addIs [wf_lexn]) 1);
+by (Clarify_tac 1);
+by (rename_tac "m n" 1);
+by (subgoal_tac "m ~= n" 1);
+ by (Blast_tac 2);
+by (blast_tac (claset() addDs [lexn_length,not_sym]) 1);
qed "wf_lex";
AddSIs [wf_lex];
@@ -894,30 +894,30 @@
"lexn r n = \
\ {(xs,ys). length xs = n & length ys = n & \
\ (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
-by(asm_full_simp_tac (simpset() delsimps [length_Suc_conv]
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [length_Suc_conv]
addsimps [lex_prod_def]) 1);
-by(auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
- by(Blast_tac 1);
- by(rename_tac "a xys x xs' y ys'" 1);
- by(res_inst_tac [("x","a#xys")] exI 1);
- by(Simp_tac 1);
-by(exhaust_tac "xys" 1);
- by(ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
-by(Blast_tac 1);
+by (auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
+ by (Blast_tac 1);
+ by (rename_tac "a xys x xs' y ys'" 1);
+ by (res_inst_tac [("x","a#xys")] exI 1);
+ by (Simp_tac 1);
+by (exhaust_tac "xys" 1);
+ by (ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
+by (Blast_tac 1);
qed "lexn_conv";
Goalw [lex_def]
"lex r = \
\ {(xs,ys). length xs = length ys & \
\ (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
-by(force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
+by (force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
qed "lex_conv";
Goalw [lexico_def] "wf r ==> wf(lexico r)";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "wf_lexico";
AddSIs [wf_lexico];
@@ -925,29 +925,29 @@
[lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
"lexico r = {(xs,ys). length xs < length ys | \
\ length xs = length ys & (xs,ys) : lex r}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "lexico_conv";
Goal "([],ys) ~: lex r";
-by(simp_tac (simpset() addsimps [lex_conv]) 1);
+by (simp_tac (simpset() addsimps [lex_conv]) 1);
qed "Nil_notin_lex";
Goal "(xs,[]) ~: lex r";
-by(simp_tac (simpset() addsimps [lex_conv]) 1);
+by (simp_tac (simpset() addsimps [lex_conv]) 1);
qed "Nil2_notin_lex";
AddIffs [Nil_notin_lex,Nil2_notin_lex];
Goal "((x#xs,y#ys) : lex r) = \
\ ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";
-by(simp_tac (simpset() addsimps [lex_conv]) 1);
-br iffI 1;
- by(blast_tac (claset() addIs [Cons_eq_appendI]) 2);
-by(REPEAT(eresolve_tac [conjE, exE] 1));
-by(exhaust_tac "xys" 1);
-by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsimps [lex_conv]) 1);
+by (rtac iffI 1);
+ by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
+by (REPEAT(eresolve_tac [conjE, exE] 1));
+by (exhaust_tac "xys" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
qed "Cons_in_lex";
AddIffs [Cons_in_lex];
--- a/src/HOL/Set.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Set.ML Fri Aug 14 12:03:01 1998 +0200
@@ -170,7 +170,7 @@
(*Anti-symmetry of the subset relation*)
Goal "[| A <= B; B <= A |] ==> A = (B::'a set)";
-br set_ext 1;
+by (rtac set_ext 1);
by (blast_tac (claset() addIs [subsetD]) 1);
qed "subset_antisym";
val equalityI = subset_antisym;
--- a/src/HOL/WF.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/WF.ML Fri Aug 14 12:03:01 1998 +0200
@@ -72,7 +72,7 @@
*---------------------------------------------------------------------------*)
Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
-bd spec 1;
+by (dtac spec 1);
by (etac (mp RS spec) 1);
by (Blast_tac 1);
val lemma1 = result();
@@ -140,32 +140,32 @@
\ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
\ Domain(r j) Int Range(r i) = {} \
\ |] ==> wf(UN i:I. r i)";
-by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
-by(Clarify_tac 1);
-by(rename_tac "A a" 1);
-by(case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
- by(Clarify_tac 1);
- by(EVERY1[dtac bspec, atac,
+by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (rename_tac "A a" 1);
+by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
+ by (Clarify_tac 1);
+ by (EVERY1[dtac bspec, atac,
eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]);
- by(EVERY1[etac allE,etac impE]);
- by(Blast_tac 1);
- by(Clarify_tac 1);
- by(rename_tac "z'" 1);
- by(res_inst_tac [("x","z'")] bexI 1);
- ba 2;
- by(Clarify_tac 1);
- by(rename_tac "j" 1);
- by(case_tac "r j = r i" 1);
- by(EVERY1[etac allE,etac impE,atac]);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
- by(blast_tac (claset() addEs [equalityE]) 1);
-by(Asm_full_simp_tac 1);
-by(case_tac "? i. i:I" 1);
- by(Clarify_tac 1);
- by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
- by(Blast_tac 1);
-by(Blast_tac 1);
+ by (EVERY1[etac allE,etac impE]);
+ by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (rename_tac "z'" 1);
+ by (res_inst_tac [("x","z'")] bexI 1);
+ by (assume_tac 2);
+ by (Clarify_tac 1);
+ by (rename_tac "j" 1);
+ by (case_tac "r j = r i" 1);
+ by (EVERY1[etac allE,etac impE,atac]);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+ by (blast_tac (claset() addEs [equalityE]) 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "? i. i:I" 1);
+ by (Clarify_tac 1);
+ by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
+ by (Blast_tac 1);
+by (Blast_tac 1);
qed "wf_UN";
Goalw [Union_def]
@@ -173,16 +173,16 @@
\ !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \
\ Domain s Int Range r = {} \
\ |] ==> wf(Union R)";
-br wf_UN 1;
-by(Blast_tac 1);
-by(Blast_tac 1);
+by (rtac wf_UN 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
qed "wf_Union";
Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
\ |] ==> wf(r Un s)";
-br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
-by(Blast_tac 1);
-by(Blast_tac 1);
+by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
qed "wf_Un";
(*---------------------------------------------------------------------------
@@ -190,12 +190,12 @@
*---------------------------------------------------------------------------*)
Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
-by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
-by(Clarify_tac 1);
-by(case_tac "? p. f p : Q" 1);
-by(eres_inst_tac [("x","{p. f p : Q}")]allE 1);
-by(fast_tac (claset() addDs [injD]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (case_tac "? p. f p : Q" 1);
+by (eres_inst_tac [("x","{p. f p : Q}")]allE 1);
+by (fast_tac (claset() addDs [injD]) 1);
+by (Blast_tac 1);
qed "wf_prod_fun_image";
(*** acyclic ***)
--- a/src/HOL/ex/LocaleGroup.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/ex/LocaleGroup.ML Fri Aug 14 12:03:01 1998 +0200
@@ -19,10 +19,10 @@
(* Mit dieser Def ist es halt schwierig *)
goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G";
by (res_inst_tac [("t","op #")] ssubst 1);
-br ext 1;
-br ext 1;
-br meta_eq_to_obj_eq 1;
-br (thm "binop_def") 1;
+by (rtac ext 1);
+by (rtac ext 1);
+by (rtac meta_eq_to_obj_eq 1);
+by (rtac (thm "binop_def") 1);
by (Asm_full_simp_tac 1);
val binop_funcset = result();
@@ -32,9 +32,9 @@
goal LocaleGroup.thy "inv : carrier G -> carrier G";
by (res_inst_tac [("t","inv")] ssubst 1);
-br ext 1;
-br meta_eq_to_obj_eq 1;
-br (thm "inv_def") 1;
+by (rtac ext 1);
+by (rtac meta_eq_to_obj_eq 1);
+by (rtac (thm "inv_def") 1);
by (Asm_full_simp_tac 1);
val inv_funcset = result();
@@ -71,27 +71,27 @@
(* remarkable: In the following step the use of e_ax1 instead of unit_ax1
is better! It doesn't produce G: Group as subgoal and the nice syntax stays *)
by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
-ba 1;
+by (assume_tac 1);
(* great: we can use the nice syntax even in res_inst_tac *)
by (res_inst_tac [("P","%r. r # y = z")] subst 1);
by (res_inst_tac [("x","x")] inv_ax2 1);
-ba 1;
-br (binop_assoc RS ssubst) 1;
-br inv_closed 1;
-ba 1;
-ba 1;
-ba 1;
-be ssubst 1;
-br (binop_assoc RS subst) 1;
-br inv_closed 1;
-ba 1;
-ba 1;
-ba 1;
-br (inv_ax2 RS ssubst) 1;
-ba 1;
-br (e_ax1 RS ssubst) 1;
-ba 1;
-br refl 1;
+by (assume_tac 1);
+by (stac binop_assoc 1);
+by (rtac inv_closed 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (etac ssubst 1);
+by (rtac (binop_assoc RS subst) 1);
+by (rtac inv_closed 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (stac inv_ax2 1);
+by (assume_tac 1);
+by (stac e_ax1 1);
+by (assume_tac 1);
+by (rtac refl 1);
val left_cancellation = result();
@@ -105,57 +105,57 @@
by (fold_goals_tac [thm "inv_def"]);
by (fast_tac (claset() addSEs [inv_closed]) 1);
by (afs [binop_closed, e_closed] 1);
-ba 1;
-br (binop_assoc RS subst) 1;
+by (assume_tac 1);
+by (rtac (binop_assoc RS subst) 1);
by (fast_tac (claset() addSEs [inv_closed]) 1);
-ba 1;
-br (e_closed) 1;
-br (inv_ax2 RS ssubst) 1;
-ba 1;
-br (e_ax1 RS ssubst) 1;
-br e_closed 1;
-br refl 1;
+by (assume_tac 1);
+by (rtac (e_closed) 1);
+by (stac inv_ax2 1);
+by (assume_tac 1);
+by (stac e_ax1 1);
+by (rtac e_closed 1);
+by (rtac refl 1);
val e_ax2 = result();
goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e";
by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1);
-ba 1;
+by (assume_tac 1);
by (res_inst_tac [("x","x")] left_cancellation 1);
-ba 1;
-ba 1;
-br e_closed 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac e_closed 1);
+by (assume_tac 1);
val idempotent_e = result();
goal LocaleGroup.thy "!! x. x: carrier G ==> x # (x -|) = e";
-br idempotent_e 1;
+by (rtac idempotent_e 1);
by (afs [binop_closed,inv_closed] 1);
-br (binop_assoc RS ssubst) 1;
-ba 1;
+by (stac binop_assoc 1);
+by (assume_tac 1);
by (afs [inv_closed] 1);
by (afs [binop_closed,inv_closed] 1);
by (res_inst_tac [("t","x -| # x # x -|")] subst 1);
-br binop_assoc 1;
+by (rtac binop_assoc 1);
by (afs [inv_closed] 1);
-ba 1;
+by (assume_tac 1);
by (afs [inv_closed] 1);
-br (inv_ax2 RS ssubst) 1;
-ba 1;
-br (e_ax1 RS ssubst) 1;
+by (stac inv_ax2 1);
+by (assume_tac 1);
+by (stac e_ax1 1);
by (afs [inv_closed] 1);
-br refl 1;
+by (rtac refl 1);
val inv_ax1 = result();
goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \
\ x # y = e |] ==> y = x -|";
by (res_inst_tac [("x","x")] left_cancellation 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
by (afs [inv_closed] 1);
-br (inv_ax1 RS ssubst) 1;
-ba 1;
-ba 1;
+by (stac inv_ax1 1);
+by (assume_tac 1);
+by (assume_tac 1);
val inv_unique = result();
goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x";
@@ -163,19 +163,19 @@
by (fold_goals_tac [thm "inv_def"]);
by (afs [inv_closed] 1);
by (afs [inv_closed] 1);
-ba 1;
+by (assume_tac 1);
by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
val inv_inv = result();
goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\
\ ==> (x # y) -| = y -| # x -|";
-br sym 1;
-br inv_unique 1;
+by (rtac sym 1);
+by (rtac inv_unique 1);
by (afs [binop_closed] 1);
by (afs [inv_closed,binop_closed] 1);
by (afs [binop_assoc,inv_closed,binop_closed] 1);
by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1);
-ba 1;
+by (assume_tac 1);
by (afs [inv_closed] 1);
by (afs [inv_closed] 1);
by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
@@ -185,15 +185,15 @@
goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\
\ z : carrier G; y # x = z # x|] ==> y = z";
by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
-ba 1;
+by (assume_tac 1);
by (res_inst_tac [("P","%r. y # r = z")] subst 1);
-br inv_ax1 1;
-ba 1;
-br (binop_assoc RS subst) 1;
-ba 1;
-ba 1;
+by (rtac inv_ax1 1);
+by (assume_tac 1);
+by (rtac (binop_assoc RS subst) 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (afs [inv_closed] 1);
-be ssubst 1;
+by (etac ssubst 1);
by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1);
val right_cancellation = result();
--- a/src/HOL/ex/PiSets.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/ex/PiSets.ML Fri Aug 14 12:03:01 1998 +0200
@@ -26,57 +26,57 @@
(* individual theorems for convenient use *)
val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q";
by (fold_goals_tac [p1]);
-br p2 1;
+by (rtac p2 1);
val apply_def = result();
goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)";
-be ssubst 1;
-br refl 1;
+by (etac ssubst 1);
+by (rtac refl 1);
val extend = result();
val [p1] = goal HOL.thy "P ==> ~~P";
-br notI 1;
-br (p1 RSN(2, notE)) 1;
-ba 1;
+by (rtac notI 1);
+by (rtac (p1 RSN(2, notE)) 1);
+by (assume_tac 1);
val notnotI = result();
val [p1] = goal Set.thy "? x. x: S ==> S ~= {}";
-br contrapos 1;
-br (p1 RS notnotI) 1;
-be ssubst 1;
-br notI 1;
-be exE 1;
-be emptyE 1;
+by (rtac contrapos 1);
+by (rtac (p1 RS notnotI) 1);
+by (etac ssubst 1);
+by (rtac notI 1);
+by (etac exE 1);
+by (etac emptyE 1);
val ExEl_NotEmpty = result();
val [p1] = goal HOL.thy "~x ==> x = False";
val l1 = (p1 RS (not_def RS apply_def)) RS mp;
val l2 = read_instantiate [("P","x")] FalseE;
-br iffI 1;
-br l1 1;
-br l2 2;
-ba 1;
-ba 1;
+by (rtac iffI 1);
+by (rtac l1 1);
+by (rtac l2 2);
+by (assume_tac 1);
+by (assume_tac 1);
val NoteqFalseEq = result();
val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)";
-br exCI 1;
+by (rtac exCI 1);
(* 1. ! x. ~ P x ==> P ?a *)
val l1 = p1 RS NoteqFalseEq;
(* l1 = (! x. ~ P x) = False *)
val l2 = l1 RS iffD1;
val l3 = l1 RS iffD2;
val l4 = read_instantiate [("P", "P ?a")] FalseE;
-br (l2 RS l4) 1;
-ba 1;
+by (rtac (l2 RS l4) 1);
+by (assume_tac 1);
val NotAllNot_Ex = result();
val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)";
-br notnotD 1;
-br (p1 RS contrapos) 1;
-br NotAllNot_Ex 1;
-ba 1;
+by (rtac notnotD 1);
+by (rtac (p1 RS contrapos) 1);
+by (rtac NotAllNot_Ex 1);
+by (assume_tac 1);
val NotEx_AllNot = result();
goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}";
@@ -93,20 +93,20 @@
val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)";
-br (q1 RS ssubst) 1;
-br q2 1;
+by (stac q1 1);
+by (rtac q2 1);
val forw_subst = result();
val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)";
-br (q1 RS subst) 1;
-br q2 1;
+by (rtac (q1 RS subst) 1);
+by (rtac q2 1);
val forw_ssubst = result();
goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A";
-br (surjective_pairing RS subst) 1;
-br (surjective_pairing RS subst) 1;
-br (surjective_pairing RS subst) 1;
-br refl 1;
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac refl 1);
val blow4 = result();
goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)";
@@ -116,27 +116,27 @@
goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \
\ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))";
-bd (blow4 RS forw_subst) 1;
+by (dtac (blow4 RS forw_subst) 1);
by (afs [split_def] 1);
val apply_quadr = result();
goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)";
-br (surjective_pairing RS subst) 1;
-br refl 1;
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac refl 1);
val surj_pair_forw = result();
goal Prod.thy "!! A B x. x: A Times B ==> fst x: A";
by (forward_tac [surj_pair_forw] 1);
-bd forw_ssubst 1;
-ba 1;
-be SigmaD1 1;
+by (dtac forw_ssubst 1);
+by (assume_tac 1);
+by (etac SigmaD1 1);
val TimesE1 = result();
goal Prod.thy "!! A B x. x: A Times B ==> snd x: B";
by (forward_tac [surj_pair_forw] 1);
-bd forw_ssubst 1;
-ba 1;
-be SigmaD2 1;
+by (dtac forw_ssubst 1);
+by (assume_tac 1);
+by (etac SigmaD2 1);
val TimesE2 = result();
(* -> and Pi *)
@@ -148,16 +148,16 @@
val [q1,q2] = goal PiSets.thy
"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: Pi A B";
-by (rewrite_goals_tac [Pi_def]);
-br CollectI 1;
-br allI 1;
+by (rewtac Pi_def);
+by (rtac CollectI 1);
+by (rtac allI 1);
by (case_tac "x : A" 1);
-br (if_P RS ssubst) 1;
-ba 1;
-be q1 1;
-br (if_not_P RS ssubst) 1;
-ba 1;
-be q2 1;
+by (stac if_P 1);
+by (assume_tac 1);
+by (etac q1 1);
+by (stac if_not_P 1);
+by (assume_tac 1);
+by (etac q2 1);
val Pi_I = result();
goal PiSets.thy
@@ -199,7 +199,7 @@
goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\
\ ==> f = g";
-br ext 1;
+by (rtac ext 1);
by (case_tac "x : A" 1);
by (Fast_tac 1);
by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1);
@@ -207,7 +207,7 @@
goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\
\ ==> f = g";
-br ext 1;
+by (rtac ext 1);
by (case_tac "x : A" 1);
by (Fast_tac 1);
by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1);
@@ -215,28 +215,28 @@
(* compose *)
goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C";
-br funcsetI 1;
+by (rtac funcsetI 1);
by (rewrite_goals_tac [compose_def,restrict_def]);
by (afs [funcsetE1] 1);
-br (if_not_P RS ssubst) 1;
-ba 1;
-br refl 1;
+by (stac if_not_P 1);
+by (assume_tac 1);
+by (rtac refl 1);
val funcset_compose = result();
goal PiSets.thy "!! A B C f g h. [| f: A -> B; g: B -> C; h: C -> D |]\
\ ==> compose A h (compose A g f) = compose A (compose B h g) f";
by (res_inst_tac [("A","A")] function_extensionality 1);
-br funcset_compose 1;
-br funcset_compose 1;
-ba 1;
-ba 1;
-ba 1;
-br funcset_compose 1;
-ba 1;
-br funcset_compose 1;
-ba 1;
-ba 1;
-br ballI 1;
+by (rtac funcset_compose 1);
+by (rtac funcset_compose 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac funcset_compose 1);
+by (assume_tac 1);
+by (rtac funcset_compose 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac ballI 1);
by (rewrite_goals_tac [compose_def,restrict_def]);
by (afs [funcsetE1,if_P RS ssubst] 1);
val compose_assoc = result();
@@ -247,88 +247,88 @@
goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\
\ ==> compose A g f `` A = C";
-br equalityI 1;
-br subsetI 1;
-be imageE 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
by (rotate_tac 4 1);
-be ssubst 1;
-br (funcset_compose RS funcsetE1) 1;
-ba 1;
-ba 1;
-ba 1;
-br subsetI 1;
+by (etac ssubst 1);
+by (rtac (funcset_compose RS funcsetE1) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac subsetI 1);
by (hyp_subst_tac 1);
-be imageE 1;
+by (etac imageE 1);
by (rotate_tac 3 1);
-be ssubst 1;
-be imageE 1;
+by (etac ssubst 1);
+by (etac imageE 1);
by (rotate_tac 3 1);
-be ssubst 1;
-be (composeE1 RS subst) 1;
-ba 1;
-ba 1;
-br imageI 1;
-ba 1;
+by (etac ssubst 1);
+by (etac (composeE1 RS subst) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac imageI 1);
+by (assume_tac 1);
val surj_compose = result();
goal PiSets.thy "!! A B C g f.[| f : A -> B; g: B -> C; f `` A = B; inj_on f A; inj_on g B |]\
\ ==> inj_on (compose A g f) A";
-br inj_onI 1;
+by (rtac inj_onI 1);
by (forward_tac [composeE1] 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
by (forward_tac [composeE1] 1);
-ba 1;
+by (assume_tac 1);
by (rotate_tac 7 1);
-ba 1;
+by (assume_tac 1);
by (step_tac (claset() addSEs [inj_onD]) 1);
by (rotate_tac 5 1);
-be subst 1;
-be subst 1;
-ba 1;
-be imageI 1;
-be imageI 1;
+by (etac subst 1);
+by (etac subst 1);
+by (assume_tac 1);
+by (etac imageI 1);
+by (etac imageI 1);
val inj_on_compose = result();
(* restrict / lam *)
goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B";
-by (rewrite_goals_tac [restrict_def]);
-br funcsetI 1;
+by (rewtac restrict_def);
+by (rtac funcsetI 1);
by (afs [if_P RS ssubst] 1);
-be subsetD 1;
-be imageI 1;
+by (etac subsetD 1);
+by (etac imageI 1);
by (afs [if_not_P RS ssubst] 1);
val restrict_in_funcset = result();
goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B";
-br restrict_in_funcset 1;
+by (rtac restrict_in_funcset 1);
by (afs [image_def] 1);
by (Step_tac 1);
by (Fast_tac 1);
val restrictI = result();
goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B";
-by (rewrite_goals_tac [restrict_def]);
-br Pi_I 1;
+by (rewtac restrict_def);
+by (rtac Pi_I 1);
by (afs [if_P RS ssubst] 1);
by (Asm_full_simp_tac 1);
val restrictI_Pi = result();
(* The following proof has to be redone *)
goal PiSets.thy "!! f A B C.[| f `` A <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
-br restrict_in_funcset 1;
+by (rtac restrict_in_funcset 1);
by (afs [image_def] 1);
by (afs [Pi_def,subset_def] 1);
by (afs [restrict_def] 1);
by (Step_tac 1);
by (Asm_full_simp_tac 1);
by (dres_inst_tac [("x","f xa")] spec 1);
-bd mp 1;
-br bexI 1;
-br refl 1;
-ba 1;
+by (dtac mp 1);
+by (rtac bexI 1);
+by (rtac refl 1);
+by (assume_tac 1);
by (dres_inst_tac [("x","xb")] spec 1);
by (Asm_full_simp_tac 1);
(* fini 1 *)
@@ -336,7 +336,7 @@
val restrict_in_funcset2 = result();
goal PiSets.thy "!! f A B C.[| !x: A. ! y: B. f x y: C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
-br restrict_in_funcset 1;
+by (rtac restrict_in_funcset 1);
by (afs [image_def] 1);
by (afs [Pi_def,subset_def] 1);
by (afs [restrict_def] 1);
@@ -387,7 +387,7 @@
goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\
\ ==> (lam x: A. f x) = (lam x: A. g x)";
-br ext 1;
+by (rtac ext 1);
by (case_tac "x: A" 1);
by (afs [restrictE1] 1);
by (afs [restrictE2] 1);
@@ -396,89 +396,89 @@
(* Invers *)
goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x";
-by (rewrite_goals_tac [image_def]);
-bd equalityD2 1;
-bd subsetD 1;
-ba 1;
-bd CollectD 1;
-be bexE 1;
-bd sym 1;
-be bexI 1;
-ba 1;
+by (rewtac image_def);
+by (dtac equalityD2 1);
+by (dtac subsetD 1);
+by (assume_tac 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (dtac sym 1);
+by (etac bexI 1);
+by (assume_tac 1);
val surj_image = result();
val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \
\ ==> (lam x: B. (Inv A f) x) : B -> A";
-br restrict_in_funcset 1;
-by (rewrite_goals_tac [image_def]);
-br subsetI 1;
-bd CollectD 1;
-be bexE 1;
-be ssubst 1;
-bd (q1 RS surj_image) 1;
-be bexE 1;
-be subst 1;
-by (rewrite_goals_tac [Inv_def]);
+by (rtac restrict_in_funcset 1);
+by (rewtac image_def);
+by (rtac subsetI 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac ssubst 1);
+by (dtac (q1 RS surj_image) 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rewtac Inv_def);
by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1);
-br (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-be (q2 RS funcsetE1) 1;
+by (rtac (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (etac (q2 RS funcsetE1) 1);
val Inv_funcset = result();
val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
\ ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x";
-br ballI 1;
-br (restrictE1 RS ssubst) 1;
-be (q1 RS funcsetE1) 1;
-by (rewrite_goals_tac [Inv_def]);
-br (q2 RS inj_onD) 1;
-ba 3;
+by (rtac ballI 1);
+by (stac restrictE1 1);
+by (etac (q1 RS funcsetE1) 1);
+by (rewtac Inv_def);
+by (rtac (q2 RS inj_onD) 1);
+by (assume_tac 3);
by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1);
-br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-be (q1 RS funcsetE1) 1;
+by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (etac (q1 RS funcsetE1) 1);
by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1);
-br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-be (q1 RS funcsetE1) 1;
+by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (etac (q1 RS funcsetE1) 1);
val Inv_f_f = result();
val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\
\ ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x";
-br ballI 1;
-br (restrictE1 RS ssubst) 1;
-ba 1;
-by (rewrite_goals_tac [Inv_def]);
+by (rtac ballI 1);
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (rewtac Inv_def);
by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1);
-br (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-ba 1;
+by (rtac (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (assume_tac 1);
val f_Inv_f = result();
val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
-br function_extensionality 1;
-br funcset_compose 1;
-br q1 1;
-br (q1 RS (q3 RS Inv_funcset)) 1;
-br restrict_in_funcset 1;
+by (rtac function_extensionality 1);
+by (rtac funcset_compose 1);
+by (rtac q1 1);
+by (rtac (q1 RS (q3 RS Inv_funcset)) 1);
+by (rtac restrict_in_funcset 1);
by (Fast_tac 1);
-br ballI 1;
+by (rtac ballI 1);
by (afs [compose_def] 1);
-br (restrictE1 RS ssubst) 1;
-ba 1;
-br (restrictE1 RS ssubst) 1;
-ba 1;
-be (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1;
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (etac (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1);
val comp_Inv_id = result();
(* Pi and its application @@ *)
goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}";
-bd NotEmpty_ExEl 1;
-be exE 1;
-by (rewrite_goals_tac [Pi_def]);
-bd CollectD 1;
-br ballI 1;
-br ExEl_NotEmpty 1;
+by (dtac NotEmpty_ExEl 1);
+by (etac exE 1);
+by (rewtac Pi_def);
+by (dtac CollectD 1);
+by (rtac ballI 1);
+by (rtac ExEl_NotEmpty 1);
by (res_inst_tac [("x","x xa")] exI 1);
by (afs [if_P RS subst] 1);
val Pi_total1 = result();
@@ -488,38 +488,38 @@
val SetEx_NotNotAll = result();
goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}";
-br notnotD 1;
-br (Pi_total1 RSN(2,contrapos)) 1;
-ba 2;
-be SetEx_NotNotAll 1;
+by (rtac notnotD 1);
+by (rtac (Pi_total1 RSN(2,contrapos)) 1);
+by (assume_tac 2);
+by (etac SetEx_NotNotAll 1);
val Pi_total2 = result();
val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)";
-by (rewrite_goals_tac [Fset_apply_def]);
-br equalityI 1;
-br subsetI 1;
-be imageE 1;
-be ssubst 1;
-by (rewrite_goals_tac [Pi_def]);
-bd CollectD 1;
-bd spec 1;
-br (q1 RS if_P RS subst) 1;
-ba 1;
-br subsetI 1;
-by (rewrite_goals_tac [image_def]);
-br CollectI 1;
-br exE 1;
-br (q2 RS NotEmpty_ExEl) 1;
+by (rewtac Fset_apply_def);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
+by (etac ssubst 1);
+by (rewtac Pi_def);
+by (dtac CollectD 1);
+by (dtac spec 1);
+by (rtac (q1 RS if_P RS subst) 1);
+by (assume_tac 1);
+by (rtac subsetI 1);
+by (rewtac image_def);
+by (rtac CollectI 1);
+by (rtac exE 1);
+by (rtac (q2 RS NotEmpty_ExEl) 1);
by (res_inst_tac [("x","%y. if (y = a) then x else xa y")] bexI 1);
by (Simp_tac 1);
by (Simp_tac 1);
-br allI 1;
+by (rtac allI 1);
by (case_tac "xb: A" 1);
by (afs [if_P RS ssubst] 1);
by (case_tac "xb = a" 1);
by (afs [if_P RS ssubst] 1);
by (afs [if_not_P RS ssubst] 1);
-by (rewrite_goals_tac [Pi_def]);
+by (rewtac Pi_def);
by (afs [if_P RS ssubst] 1);
by (afs [if_not_P RS ssubst] 1);
by (case_tac "xb = a" 1);
@@ -530,32 +530,32 @@
val Pi_app_def = result();
goal PiSets.thy "!! a A B C. [| a: A; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI y: B a. C a y) ~= {}";
-bd NotEmpty_ExEl 1;
-be exE 1;
-by (rewrite_goals_tac [Pi_def]);
-bd CollectD 1;
-bd spec 1;
-br ExEl_NotEmpty 1;
-br exI 1;
-be (if_P RS eq_reflection RS apply_def) 1;
-ba 1;
+by (dtac NotEmpty_ExEl 1);
+by (etac exE 1);
+by (rewtac Pi_def);
+by (dtac CollectD 1);
+by (dtac spec 1);
+by (rtac ExEl_NotEmpty 1);
+by (rtac exI 1);
+by (etac (if_P RS eq_reflection RS apply_def) 1);
+by (assume_tac 1);
val NotEmptyPiStep = result();
val [q1,q2,q3] = goal PiSets.thy
"[|a : A; b: B a; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI x: A. PI y: B x. C x y) @@ a @@ b = C a b";
by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]);
by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]);
-br refl 1;
+by (rtac refl 1);
val Pi_app2_def = result();
(* Sigma does a better job ( the following is from PiSig.ML) *)
goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\
\ ==> Sigma A B ^^ {a} = Pi A B @@ a";
-br (Pi_app_def RS ssubst) 1;
-ba 1;
-ba 1;
+by (stac Pi_app_def 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1);
-by (rewrite_goals_tac [Bex_def]);
+by (rewtac Bex_def);
by (Fast_tac 1);
val PiSig_image_eq = result();
@@ -567,25 +567,25 @@
(* Bijection between Pi in terms of => and Pi in terms of Sigma *)
goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B";
by (afs [PiBij_def,Pi_def,restrictE1] 1);
-br subsetI 1;
+by (rtac subsetI 1);
by (split_all_tac 1);
-bd CollectD 1;
+by (dtac CollectD 1);
by (Asm_full_simp_tac 1);
val PiBij_subset_Sigma = result();
goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
by (afs [PiBij_def,restrictE1] 1);
-br ballI 1;
-br ex1I 1;
-ba 2;
-br refl 1;
+by (rtac ballI 1);
+by (rtac ex1I 1);
+by (assume_tac 2);
+by (rtac refl 1);
val PiBij_unique = result();
goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))";
by (afs [PiBij_def,restrictE1] 1);
-br ballI 1;
-br ex1I 1;
-be conjunct2 2;
+by (rtac ballI 1);
+by (rtac ex1I 1);
+by (etac conjunct2 2);
by (afs [PiE1] 1);
val PiBij_unique2 = result();
@@ -595,15 +595,15 @@
goal PiSets.thy "!! A B. PiBij A B: Pi A B -> Graph A B";
by (afs [PiBij_def] 1);
-br restrictI 1;
+by (rtac restrictI 1);
by (strip 1);
by (afs [Graph_def] 1);
-br conjI 1;
-br subsetI 1;
+by (rtac conjI 1);
+by (rtac subsetI 1);
by (strip 2);
-br ex1I 2;
-br refl 2;
-ba 2;
+by (rtac ex1I 2);
+by (rtac refl 2);
+by (assume_tac 2);
by (split_all_tac 1);
by (afs [Pi_def] 1);
val PiBij_func = result();
@@ -611,25 +611,25 @@
goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B; \
\ {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\
\ ==> f x = g x";
-be equalityE 1;
-by (rewrite_goals_tac [subset_def]);
+by (etac equalityE 1);
+by (rewtac subset_def);
by (dres_inst_tac [("x","(x, f x)")] bspec 1);
by (Fast_tac 1);
by (Fast_tac 1);
val set_eq_lemma = result();
goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
-br inj_onI 1;
-br Pi_extensionality 1;
-ba 1;
-ba 1;
+by (rtac inj_onI 1);
+by (rtac Pi_extensionality 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (strip 1);
by (afs [PiBij_def,restrictE1] 1);
by (re_tac set_eq_lemma 2 1);
-ba 1;
-ba 2;
+by (assume_tac 1);
+by (assume_tac 2);
by (afs [restrictE1] 1);
-be subst 1;
+by (etac subst 1);
by (afs [restrictE1] 1);
val inj_PiBij = result();
@@ -638,85 +638,85 @@
val Ex1_Ex = result();
goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
-br equalityI 1;
+by (rtac equalityI 1);
by (afs [image_def] 1);
-br subsetI 1;
+by (rtac subsetI 1);
by (Asm_full_simp_tac 1);
-be bexE 1;
-be ssubst 1;
+by (etac bexE 1);
+by (etac ssubst 1);
by (afs [PiBij_in_Graph] 1);
-br subsetI 1;
+by (rtac subsetI 1);
by (afs [image_def] 1);
by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
-br restrictI_Pi 2;
+by (rtac restrictI_Pi 2);
by (strip 2);
-br ex1E 2;
+by (rtac ex1E 2);
by (afs [Graph_def] 2);
-be conjE 2;
-bd bspec 2;
-ba 2;
-ba 2;
-br (select_equality RS ssubst) 2;
-ba 2;
+by (etac conjE 2);
+by (dtac bspec 2);
+by (assume_tac 2);
+by (assume_tac 2);
+by (stac select_equality 2);
+by (assume_tac 2);
by (Blast_tac 2);
(* gets hung up on by (afs [Graph_def] 2); *)
-by (SELECT_GOAL (rewrite_goals_tac [Graph_def]) 2);
+by (SELECT_GOAL (rewtac Graph_def) 2);
by (Blast_tac 2);
(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
by (afs [PiBij_def,Graph_def] 1);
-br (restrictE1 RS ssubst) 1;
-br restrictI_Pi 1;
+by (stac restrictE1 1);
+by (rtac restrictI_Pi 1);
(* again like the old 2. subgoal *)
by (strip 1);
-br ex1E 1;
-be conjE 1;
-bd bspec 1;
-ba 1;
-ba 1;
-br (select_equality RS ssubst) 1;
-ba 1;
+by (rtac ex1E 1);
+by (etac conjE 1);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (stac select_equality 1);
+by (assume_tac 1);
by (Blast_tac 1);
by (Blast_tac 1);
(* *)
-br equalityI 1;
-br subsetI 1;
-br CollectI 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (rtac CollectI 1);
by (split_all_tac 1);
by (Simp_tac 1);
-br conjI 1;
+by (rtac conjI 1);
by (Blast_tac 1);
-be conjE 1;
-bd subsetD 1;
-ba 1;
-bd SigmaD1 1;
-bd bspec 1;
-ba 1;
-br (restrictE1 RS ssubst) 1;
-ba 1;
-br sym 1;
-br select_equality 1;
-ba 1;
+by (etac conjE 1);
+by (dtac subsetD 1);
+by (assume_tac 1);
+by (dtac SigmaD1 1);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (rtac sym 1);
+by (rtac select_equality 1);
+by (assume_tac 1);
by (Blast_tac 1);
(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *)
-br subsetI 1;
+by (rtac subsetI 1);
by (Asm_full_simp_tac 1);
by (split_all_tac 1);
by (Asm_full_simp_tac 1);
-be conjE 1;
-be conjE 1;
+by (etac conjE 1);
+by (etac conjE 1);
by (afs [restrictE1] 1);
-bd bspec 1;
-ba 1;
-bd Ex1_Ex 1;
-by (rewrite_goals_tac [Ex_def]);
-ba 1;
+by (dtac bspec 1);
+by (assume_tac 1);
+by (dtac Ex1_Ex 1);
+by (rewtac Ex_def);
+by (assume_tac 1);
val surj_PiBij = result();
goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \
\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
-br (Inv_f_f RS bspec) 1;
-ba 4;
+by (rtac (Inv_f_f RS bspec) 1);
+by (assume_tac 4);
by (afs [PiBij_func] 1);
by (afs [inj_PiBij] 1);
by (afs [surj_PiBij] 1);
@@ -724,29 +724,29 @@
goal PiSets.thy "!! A B. [| f: Graph A B |] ==> \
\ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
-br (PiBij_func RS (f_Inv_f RS bspec)) 1;
+by (rtac (PiBij_func RS (f_Inv_f RS bspec)) 1);
by (afs [surj_PiBij] 1);
-ba 1;
+by (assume_tac 1);
val PiBij_bij2 = result();
goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f";
-br injI 1;
+by (rtac injI 1);
by (dres_inst_tac [("f","g")] arg_cong 1);
by (forw_inst_tac [("x","x")] spec 1);
by (rotate_tac 2 1);
-be subst 1;
+by (etac subst 1);
by (forw_inst_tac [("x","y")] spec 1);
by (rotate_tac 2 1);
-be subst 1;
-ba 1;
+by (etac subst 1);
+by (assume_tac 1);
val inj_lemma = result();
goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g";
by (afs [surj_def] 1);
-br allI 1;
+by (rtac allI 1);
by (res_inst_tac [("x","f y")] exI 1);
-bd spec 1;
-be sym 1;
+by (dtac spec 1);
+by (etac sym 1);
val surj_lemma = result();
goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}";
@@ -763,11 +763,11 @@
goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C";
-br subsetI 1;
-br Pi_I 1;
+by (rtac subsetI 1);
+by (rtac Pi_I 1);
by (afs [Pi_def] 2);
-bd bspec 1;
-ba 1;
-be subsetD 1;
+by (dtac bspec 1);
+by (assume_tac 1);
+by (etac subsetD 1);
by (afs [PiE1] 1);
val Pi_subset1 = result();