1.1 --- a/src/HOL/Divides.ML Fri Aug 14 12:02:35 1998 +0200
1.2 +++ b/src/HOL/Divides.ML Fri Aug 14 12:03:01 1998 +0200
1.3 @@ -201,7 +201,7 @@
1.4 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
1.5 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
1.6 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
1.7 -br le_trans 1;
1.8 +by (rtac le_trans 1);
1.9 by (Asm_simp_tac 1);
1.10 by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
1.11 qed "div_le_mono2";
2.1 --- a/src/HOL/Fun.ML Fri Aug 14 12:02:35 1998 +0200
2.2 +++ b/src/HOL/Fun.ML Fri Aug 14 12:03:01 1998 +0200
2.3 @@ -78,7 +78,7 @@
2.4 by (rtac iffI 1);
2.5 by (etac arg_cong 2);
2.6 by (etac injD 1);
2.7 -ba 1;
2.8 +by (assume_tac 1);
2.9 qed "inj_eq";
2.10
2.11 Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
3.1 --- a/src/HOL/Lambda/InductTermi.ML Fri Aug 14 12:02:35 1998 +0200
3.2 +++ b/src/HOL/Lambda/InductTermi.ML Fri Aug 14 12:03:01 1998 +0200
3.3 @@ -8,37 +8,37 @@
3.4
3.5 Goal "s : termi beta ==> !t. t : termi beta --> \
3.6 \ (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)";
3.7 -be acc_induct 1;
3.8 -be thin_rl 1;
3.9 -br allI 1;
3.10 -br impI 1;
3.11 -be acc_induct 1;
3.12 -by(Clarify_tac 1);
3.13 -br accI 1;
3.14 -by(safe_tac (claset() addSEs [apps_betasE]));
3.15 - ba 1;
3.16 - by(blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1);
3.17 - by(blast_tac (claset()
3.18 +by (etac acc_induct 1);
3.19 +by (etac thin_rl 1);
3.20 +by (rtac allI 1);
3.21 +by (rtac impI 1);
3.22 +by (etac acc_induct 1);
3.23 +by (Clarify_tac 1);
3.24 +by (rtac accI 1);
3.25 +by (safe_tac (claset() addSEs [apps_betasE]));
3.26 + by (assume_tac 1);
3.27 + by (blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1);
3.28 + by (blast_tac (claset()
3.29 addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI]
3.30 addDs [acc_downwards]) 1);
3.31 (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
3.32 -by(blast_tac (claset() addDs [apps_preserves_betas]) 1);
3.33 +by (blast_tac (claset() addDs [apps_preserves_betas]) 1);
3.34 qed_spec_mp "double_induction_lemma";
3.35
3.36 Goal "t : IT ==> t : termi(beta)";
3.37 be IT.induct 1;
3.38 - bd rev_subsetD 1;
3.39 - br lists_mono 1;
3.40 - br Int_lower2 1;
3.41 - by(Asm_full_simp_tac 1);
3.42 - bd lists_accD 1;
3.43 - be acc_induct 1;
3.44 - br accI 1;
3.45 - by(blast_tac (claset() addSDs [head_Var_reduction]) 1);
3.46 - be acc_induct 1;
3.47 - br accI 1;
3.48 - by(Blast_tac 1);
3.49 -by(blast_tac (claset() addIs [double_induction_lemma]) 1);
3.50 + by (dtac rev_subsetD 1);
3.51 + by (rtac lists_mono 1);
3.52 + by (rtac Int_lower2 1);
3.53 + by (Asm_full_simp_tac 1);
3.54 + by (dtac lists_accD 1);
3.55 + by (etac acc_induct 1);
3.56 + by (rtac accI 1);
3.57 + by (blast_tac (claset() addSDs [head_Var_reduction]) 1);
3.58 + by (etac acc_induct 1);
3.59 + by (rtac accI 1);
3.60 + by (Blast_tac 1);
3.61 +by (blast_tac (claset() addIs [double_induction_lemma]) 1);
3.62 qed "IT_implies_termi";
3.63
3.64 (*** Every terminating term is in IT ***)
3.65 @@ -55,69 +55,69 @@
3.66 (* Turned out to be redundant:
3.67 Goal "t : termi beta ==> \
3.68 \ !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
3.69 -be acc_induct 1;
3.70 -by(force_tac (claset()
3.71 +by (etac acc_induct 1);
3.72 +by (force_tac (claset()
3.73 addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1);
3.74 val lemma = result();
3.75
3.76 Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)";
3.77 -bd lemma 1;
3.78 -by(Blast_tac 1);
3.79 +by (dtac lemma 1);
3.80 +by (Blast_tac 1);
3.81 qed "apps_in_termi_betaD";
3.82
3.83 Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta";
3.84 -be acc_induct 1;
3.85 -by(force_tac (claset() addIs [accI],simpset()) 1);
3.86 +by (etac acc_induct 1);
3.87 +by (force_tac (claset() addIs [accI],simpset()) 1);
3.88 val lemma = result();
3.89
3.90 Goal "Abs r : termi beta ==> r : termi beta";
3.91 -bd lemma 1;
3.92 -by(Blast_tac 1);
3.93 +by (dtac lemma 1);
3.94 +by (Blast_tac 1);
3.95 qed "Abs_in_termi_betaD";
3.96
3.97 Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta";
3.98 -be acc_induct 1;
3.99 -by(force_tac (claset() addIs [accI],simpset()) 1);
3.100 +by (etac acc_induct 1);
3.101 +by (force_tac (claset() addIs [accI],simpset()) 1);
3.102 val lemma = result();
3.103
3.104 Goal "r$s : termi beta ==> r : termi beta & s : termi beta";
3.105 -bd lemma 1;
3.106 -by(Blast_tac 1);
3.107 +by (dtac lemma 1);
3.108 +by (Blast_tac 1);
3.109 qed "App_in_termi_betaD";
3.110 *)
3.111
3.112 Goal "r : termi beta ==> r : IT";
3.113 -be acc_induct 1;
3.114 -by(rename_tac "r" 1);
3.115 -be thin_rl 1;
3.116 -be rev_mp 1;
3.117 -by(Simp_tac 1);
3.118 -by(res_inst_tac [("t","r")] Apps_dB_induct 1);
3.119 - by(rename_tac "n ts" 1);
3.120 - by(Clarify_tac 1);
3.121 +by (etac acc_induct 1);
3.122 +by (rename_tac "r" 1);
3.123 +by (etac thin_rl 1);
3.124 +by (etac rev_mp 1);
3.125 +by (Simp_tac 1);
3.126 +by (res_inst_tac [("t","r")] Apps_dB_induct 1);
3.127 + by (rename_tac "n ts" 1);
3.128 + by (Clarify_tac 1);
3.129 brs IT.intrs 1;
3.130 - by(Clarify_tac 1);
3.131 - by(EVERY1[dtac bspec, atac]);
3.132 - be mp 1;
3.133 - by(Clarify_tac 1);
3.134 - bd converseI 1;
3.135 - by(EVERY1[dtac ex_step1I, atac]);
3.136 - by(Clarify_tac 1);
3.137 - by(rename_tac "us" 1);
3.138 - by(eres_inst_tac [("x","Var n $$ us")] allE 1);
3.139 - by(Force_tac 1);
3.140 -by(rename_tac "u ts" 1);
3.141 -by(exhaust_tac "ts" 1);
3.142 - by(Asm_full_simp_tac 1);
3.143 - by(blast_tac (claset() addIs IT.intrs) 1);
3.144 -by(rename_tac "s ss" 1);
3.145 -by(Asm_full_simp_tac 1);
3.146 -by(Clarify_tac 1);
3.147 + by (Clarify_tac 1);
3.148 + by (EVERY1[dtac bspec, atac]);
3.149 + by (etac mp 1);
3.150 + by (Clarify_tac 1);
3.151 + by (dtac converseI 1);
3.152 + by (EVERY1[dtac ex_step1I, atac]);
3.153 + by (Clarify_tac 1);
3.154 + by (rename_tac "us" 1);
3.155 + by (eres_inst_tac [("x","Var n $$ us")] allE 1);
3.156 + by (Force_tac 1);
3.157 +by (rename_tac "u ts" 1);
3.158 +by (exhaust_tac "ts" 1);
3.159 + by (Asm_full_simp_tac 1);
3.160 + by (blast_tac (claset() addIs IT.intrs) 1);
3.161 +by (rename_tac "s ss" 1);
3.162 +by (Asm_full_simp_tac 1);
3.163 +by (Clarify_tac 1);
3.164 brs IT.intrs 1;
3.165 - by(blast_tac (claset() addIs [apps_preserves_beta]) 1);
3.166 -be mp 1;
3.167 - by(Clarify_tac 1);
3.168 - by(rename_tac "t" 1);
3.169 - by(eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1);
3.170 - by(Force_tac 1);
3.171 + by (blast_tac (claset() addIs [apps_preserves_beta]) 1);
3.172 +by (etac mp 1);
3.173 + by (Clarify_tac 1);
3.174 + by (rename_tac "t" 1);
3.175 + by (eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1);
3.176 + by (Force_tac 1);
3.177 qed "termi_implies_IT";
4.1 --- a/src/HOL/Lambda/Lambda.ML Fri Aug 14 12:02:35 1998 +0200
4.2 +++ b/src/HOL/Lambda/Lambda.ML Fri Aug 14 12:03:01 1998 +0200
4.3 @@ -140,20 +140,20 @@
4.4
4.5 Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
4.6 be beta.induct 1;
4.7 -by(ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
4.8 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
4.9 qed_spec_mp "subst_preserves_beta";
4.10 Addsimps [subst_preserves_beta];
4.11
4.12 Goal "r -> s ==> !i. lift r i -> lift s i";
4.13 be beta.induct 1;
4.14 -by(Auto_tac);
4.15 +by (Auto_tac);
4.16 qed_spec_mp "lift_preserves_beta";
4.17 Addsimps [lift_preserves_beta];
4.18
4.19 Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]";
4.20 -by(induct_tac "t" 1);
4.21 -by(asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
4.22 -by(asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
4.23 -by(asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
4.24 +by (induct_tac "t" 1);
4.25 +by (asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
4.26 +by (asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
4.27 +by (asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
4.28 qed_spec_mp "subst_preserves_beta2";
4.29 Addsimps [subst_preserves_beta2];
5.1 --- a/src/HOL/Lambda/ListApplication.ML Fri Aug 14 12:02:35 1998 +0200
5.2 +++ b/src/HOL/Lambda/ListApplication.ML Fri Aug 14 12:03:01 1998 +0200
5.3 @@ -5,97 +5,97 @@
5.4 *)
5.5
5.6 Goal "(r$$ts = s$$ts) = (r = s)";
5.7 -by(rev_induct_tac "ts" 1);
5.8 -by(Auto_tac);
5.9 +by (rev_induct_tac "ts" 1);
5.10 +by (Auto_tac);
5.11 qed "apps_eq_tail_conv";
5.12 AddIffs [apps_eq_tail_conv];
5.13
5.14 Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
5.15 -by(induct_tac "ss" 1);
5.16 -by(Auto_tac);
5.17 +by (induct_tac "ss" 1);
5.18 +by (Auto_tac);
5.19 qed_spec_mp "Var_eq_apps_conv";
5.20 AddIffs [Var_eq_apps_conv];
5.21
5.22 Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
5.23 -by(rev_induct_tac "rs" 1);
5.24 - by(Simp_tac 1);
5.25 - by(Blast_tac 1);
5.26 -br allI 1;
5.27 -by(rev_induct_tac "ss" 1);
5.28 -by(Auto_tac);
5.29 +by (rev_induct_tac "rs" 1);
5.30 + by (Simp_tac 1);
5.31 + by (Blast_tac 1);
5.32 +by (rtac allI 1);
5.33 +by (rev_induct_tac "ss" 1);
5.34 +by (Auto_tac);
5.35 qed_spec_mp "Var_apps_eq_Var_apps_conv";
5.36 AddIffs [Var_apps_eq_Var_apps_conv];
5.37
5.38 Goal "(r$s = t$$ts) = \
5.39 \ (if ts = [] then r$s = t \
5.40 \ else (? ss. ts = ss@[s] & r = t$$ss))";
5.41 -by(res_inst_tac [("xs","ts")] rev_exhaust 1);
5.42 -by(Auto_tac);
5.43 +by (res_inst_tac [("xs","ts")] rev_exhaust 1);
5.44 +by (Auto_tac);
5.45 qed "App_eq_foldl_conv";
5.46
5.47 Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
5.48 -by(rev_induct_tac "ss" 1);
5.49 -by(Auto_tac);
5.50 +by (rev_induct_tac "ss" 1);
5.51 +by (Auto_tac);
5.52 qed "Abs_eq_apps_conv";
5.53 AddIffs [Abs_eq_apps_conv];
5.54
5.55 Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
5.56 -by(rev_induct_tac "ss" 1);
5.57 -by(Auto_tac);
5.58 +by (rev_induct_tac "ss" 1);
5.59 +by (Auto_tac);
5.60 qed "apps_eq_Abs_conv";
5.61 AddIffs [apps_eq_Abs_conv];
5.62
5.63 Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
5.64 -by(rev_induct_tac "rs" 1);
5.65 - by(Simp_tac 1);
5.66 - by(Blast_tac 1);
5.67 -br allI 1;
5.68 -by(rev_induct_tac "ss" 1);
5.69 -by(Auto_tac);
5.70 +by (rev_induct_tac "rs" 1);
5.71 + by (Simp_tac 1);
5.72 + by (Blast_tac 1);
5.73 +by (rtac allI 1);
5.74 +by (rev_induct_tac "ss" 1);
5.75 +by (Auto_tac);
5.76 qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
5.77 AddIffs [Abs_apps_eq_Abs_apps_conv];
5.78
5.79 Goal "!s t. Abs s $ t ~= (Var n)$$ss";
5.80 -by(rev_induct_tac "ss" 1);
5.81 -by(Auto_tac);
5.82 +by (rev_induct_tac "ss" 1);
5.83 +by (Auto_tac);
5.84 qed_spec_mp "Abs_App_neq_Var_apps";
5.85 AddIffs [Abs_App_neq_Var_apps];
5.86
5.87 Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
5.88 -by(rev_induct_tac "ss" 1);
5.89 - by(Simp_tac 1);
5.90 -br allI 1;
5.91 -by(rev_induct_tac "ts" 1);
5.92 -by(Auto_tac);
5.93 +by (rev_induct_tac "ss" 1);
5.94 + by (Simp_tac 1);
5.95 +by (rtac allI 1);
5.96 +by (rev_induct_tac "ts" 1);
5.97 +by (Auto_tac);
5.98 qed_spec_mp "Var_apps_neq_Abs_apps";
5.99 AddIffs [Var_apps_neq_Abs_apps];
5.100
5.101 Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
5.102 -by(induct_tac "t" 1);
5.103 - by(res_inst_tac[("x","[]")] exI 1);
5.104 - by(Simp_tac 1);
5.105 - by(Clarify_tac 1);
5.106 - by(rename_tac "ts1 ts2 h1 h2" 1);
5.107 - by(res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
5.108 - by(Simp_tac 1);
5.109 -by(Simp_tac 1);
5.110 +by (induct_tac "t" 1);
5.111 + by (res_inst_tac[("x","[]")] exI 1);
5.112 + by (Simp_tac 1);
5.113 + by (Clarify_tac 1);
5.114 + by (rename_tac "ts1 ts2 h1 h2" 1);
5.115 + by (res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
5.116 + by (Simp_tac 1);
5.117 +by (Simp_tac 1);
5.118 qed "ex_head_tail";
5.119
5.120 Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
5.121 -by(rev_induct_tac "rs" 1);
5.122 -by(Auto_tac);
5.123 +by (rev_induct_tac "rs" 1);
5.124 +by (Auto_tac);
5.125 qed "size_apps";
5.126 Addsimps [size_apps];
5.127
5.128 Goal "[| 0 < k; m <= n |] ==> m < n+k";
5.129 -by(exhaust_tac "k" 1);
5.130 - by(Asm_full_simp_tac 1);
5.131 -by(Asm_full_simp_tac 1);
5.132 -br le_imp_less_Suc 1;
5.133 -by(exhaust_tac "n" 1);
5.134 - by(Asm_full_simp_tac 1);
5.135 -by(hyp_subst_tac 1);
5.136 -be trans_le_add1 1;
5.137 +by (exhaust_tac "k" 1);
5.138 + by (Asm_full_simp_tac 1);
5.139 +by (Asm_full_simp_tac 1);
5.140 +by (rtac le_imp_less_Suc 1);
5.141 +by (exhaust_tac "n" 1);
5.142 + by (Asm_full_simp_tac 1);
5.143 +by (hyp_subst_tac 1);
5.144 +by (etac trans_le_add1 1);
5.145 val lemma = result();
5.146
5.147 (* a customized induction schema for $$ *)
5.148 @@ -104,39 +104,39 @@
5.149 "[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
5.150 \ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
5.151 \|] ==> !t. size t = n --> P t";
5.152 -by(res_inst_tac [("n","n")] less_induct 1);
5.153 -br allI 1;
5.154 -by(cut_inst_tac [("t","t")] ex_head_tail 1);
5.155 -by(Clarify_tac 1);
5.156 -be disjE 1;
5.157 - by(Clarify_tac 1);
5.158 - brs prems 1;
5.159 - by(Clarify_tac 1);
5.160 - by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
5.161 - by(Simp_tac 1);
5.162 - br lemma 1;
5.163 - by(Force_tac 1);
5.164 - br elem_le_sum 1;
5.165 - by(Force_tac 1);
5.166 -by(Clarify_tac 1);
5.167 -brs prems 1;
5.168 -by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
5.169 -by(Simp_tac 1);
5.170 -by(Clarify_tac 1);
5.171 -by(EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
5.172 -by(Simp_tac 1);
5.173 -br le_imp_less_Suc 1;
5.174 -br trans_le_add1 1;
5.175 -br trans_le_add2 1;
5.176 -br elem_le_sum 1;
5.177 -by(Force_tac 1);
5.178 +by (res_inst_tac [("n","n")] less_induct 1);
5.179 +by (rtac allI 1);
5.180 +by (cut_inst_tac [("t","t")] ex_head_tail 1);
5.181 +by (Clarify_tac 1);
5.182 +by (etac disjE 1);
5.183 + by (Clarify_tac 1);
5.184 + by (resolve_tac prems 1);
5.185 + by (Clarify_tac 1);
5.186 + by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
5.187 + by (Simp_tac 1);
5.188 + by (rtac lemma 1);
5.189 + by (Force_tac 1);
5.190 + by (rtac elem_le_sum 1);
5.191 + by (Force_tac 1);
5.192 +by (Clarify_tac 1);
5.193 +by (resolve_tac prems 1);
5.194 +by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
5.195 +by (Simp_tac 1);
5.196 +by (Clarify_tac 1);
5.197 +by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
5.198 +by (Simp_tac 1);
5.199 +by (rtac le_imp_less_Suc 1);
5.200 +by (rtac trans_le_add1 1);
5.201 +by (rtac trans_le_add2 1);
5.202 +by (rtac elem_le_sum 1);
5.203 +by (Force_tac 1);
5.204 val lemma = result() RS spec RS mp;
5.205
5.206 val prems = Goal
5.207 "[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
5.208 \ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
5.209 \|] ==> P t";
5.210 -by(res_inst_tac [("x1","t")] lemma 1);
5.211 -br refl 3;
5.212 -by(REPEAT(ares_tac prems 1));
5.213 +by (res_inst_tac [("x1","t")] lemma 1);
5.214 +by (rtac refl 3);
5.215 +by (REPEAT(ares_tac prems 1));
5.216 qed "Apps_dB_induct";
6.1 --- a/src/HOL/Lambda/ListBeta.ML Fri Aug 14 12:02:35 1998 +0200
6.2 +++ b/src/HOL/Lambda/ListBeta.ML Fri Aug 14 12:03:01 1998 +0200
6.3 @@ -7,21 +7,21 @@
6.4 Goal
6.5 "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
6.6 be beta.induct 1;
6.7 -by(Asm_full_simp_tac 1);
6.8 -br allI 1;
6.9 -by(res_inst_tac [("xs","rs")] rev_exhaust 1);
6.10 -by(Asm_full_simp_tac 1);
6.11 -by(force_tac (claset() addIs [append_step1I],simpset()) 1);
6.12 -br allI 1;
6.13 -by(res_inst_tac [("xs","rs")] rev_exhaust 1);
6.14 -by(Asm_full_simp_tac 1);
6.15 -by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
6.16 -by(Asm_full_simp_tac 1);
6.17 +by (Asm_full_simp_tac 1);
6.18 +by (rtac allI 1);
6.19 +by (res_inst_tac [("xs","rs")] rev_exhaust 1);
6.20 +by (Asm_full_simp_tac 1);
6.21 +by (force_tac (claset() addIs [append_step1I],simpset()) 1);
6.22 +by (rtac allI 1);
6.23 +by (res_inst_tac [("xs","rs")] rev_exhaust 1);
6.24 +by (Asm_full_simp_tac 1);
6.25 +by (force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
6.26 +by (Asm_full_simp_tac 1);
6.27 val lemma = result();
6.28
6.29 Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)";
6.30 -bd lemma 1;
6.31 -by(Blast_tac 1);
6.32 +by (dtac lemma 1);
6.33 +by (Blast_tac 1);
6.34 qed "head_Var_reduction";
6.35
6.36 Goal "u -> u' ==> !r rs. u = r$$rs --> \
6.37 @@ -29,31 +29,31 @@
6.38 \ (? rs'. rs => rs' & u' = r$$rs') | \
6.39 \ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
6.40 be beta.induct 1;
6.41 - by(clarify_tac (claset() delrules [disjCI]) 1);
6.42 - by(exhaust_tac "r" 1);
6.43 - by(Asm_full_simp_tac 1);
6.44 - by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
6.45 - by(split_asm_tac [split_if_asm] 1);
6.46 - by(Asm_full_simp_tac 1);
6.47 - by(Blast_tac 1);
6.48 - by(Asm_full_simp_tac 1);
6.49 - by(asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
6.50 - by(split_asm_tac [split_if_asm] 1);
6.51 - by(Asm_full_simp_tac 1);
6.52 - by(Asm_full_simp_tac 1);
6.53 - by(clarify_tac (claset() delrules [disjCI]) 1);
6.54 - bd (App_eq_foldl_conv RS iffD1) 1;
6.55 - by(split_asm_tac [split_if_asm] 1);
6.56 - by(Asm_full_simp_tac 1);
6.57 - by(Blast_tac 1);
6.58 - by(force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
6.59 - by(clarify_tac (claset() delrules [disjCI]) 1);
6.60 - bd (App_eq_foldl_conv RS iffD1) 1;
6.61 - by(split_asm_tac [split_if_asm] 1);
6.62 - by(Asm_full_simp_tac 1);
6.63 - by(Blast_tac 1);
6.64 - by(force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
6.65 -by(Asm_full_simp_tac 1);
6.66 + by (clarify_tac (claset() delrules [disjCI]) 1);
6.67 + by (exhaust_tac "r" 1);
6.68 + by (Asm_full_simp_tac 1);
6.69 + by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
6.70 + by (split_asm_tac [split_if_asm] 1);
6.71 + by (Asm_full_simp_tac 1);
6.72 + by (Blast_tac 1);
6.73 + by (Asm_full_simp_tac 1);
6.74 + by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
6.75 + by (split_asm_tac [split_if_asm] 1);
6.76 + by (Asm_full_simp_tac 1);
6.77 + by (Asm_full_simp_tac 1);
6.78 + by (clarify_tac (claset() delrules [disjCI]) 1);
6.79 + by (dtac (App_eq_foldl_conv RS iffD1) 1);
6.80 + by (split_asm_tac [split_if_asm] 1);
6.81 + by (Asm_full_simp_tac 1);
6.82 + by (Blast_tac 1);
6.83 + by (force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
6.84 + by (clarify_tac (claset() delrules [disjCI]) 1);
6.85 + by (dtac (App_eq_foldl_conv RS iffD1) 1);
6.86 + by (split_asm_tac [split_if_asm] 1);
6.87 + by (Asm_full_simp_tac 1);
6.88 + by (Blast_tac 1);
6.89 + by (force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
6.90 +by (Asm_full_simp_tac 1);
6.91 val lemma = result();
6.92
6.93 Goal "[| r$$rs -> s; \
6.94 @@ -61,8 +61,8 @@
6.95 \ !rs'. rs => rs' --> s = r$$rs' --> R; \
6.96 \ !t u us. r = Abs t --> rs = u#us --> s = t[u/0]$$us --> R \
6.97 \ |] ==> R";
6.98 -bd lemma 1;
6.99 -by(blast_tac HOL_cs 1);
6.100 +by (dtac lemma 1);
6.101 +by (blast_tac HOL_cs 1);
6.102 val lemma = result();
6.103 bind_thm("apps_betasE",
6.104 impI RSN (4,impI RSN (4,impI RSN (4,allI RSN (4,allI RSN (4,allI RSN (4,
6.105 @@ -71,27 +71,27 @@
6.106 AddSEs [apps_betasE];
6.107
6.108 Goal "r -> s ==> r$$ss -> s$$ss";
6.109 -by(res_inst_tac [("xs","ss")] rev_induct 1);
6.110 -by(Auto_tac);
6.111 +by (res_inst_tac [("xs","ss")] rev_induct 1);
6.112 +by (Auto_tac);
6.113 qed "apps_preserves_beta";
6.114 Addsimps [apps_preserves_beta];
6.115
6.116 Goal "r ->> s ==> r$$ss ->> s$$ss";
6.117 -by(etac rtrancl_induct 1);
6.118 - by(Blast_tac 1);
6.119 -by(blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
6.120 +by (etac rtrancl_induct 1);
6.121 + by (Blast_tac 1);
6.122 +by (blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
6.123 qed "apps_preserves_beta2";
6.124 Addsimps [apps_preserves_beta2];
6.125
6.126 Goal "!ss. rs => ss --> r$$rs -> r$$ss";
6.127 -by(res_inst_tac [("xs","rs")] rev_induct 1);
6.128 - by(Asm_full_simp_tac 1);
6.129 -by(Asm_full_simp_tac 1);
6.130 -by(Clarify_tac 1);
6.131 -by(res_inst_tac [("xs","ss")] rev_exhaust 1);
6.132 - by(Asm_full_simp_tac 1);
6.133 -by(Asm_full_simp_tac 1);
6.134 -bd Snoc_step1_SnocD 1;
6.135 -by(Blast_tac 1);
6.136 +by (res_inst_tac [("xs","rs")] rev_induct 1);
6.137 + by (Asm_full_simp_tac 1);
6.138 +by (Asm_full_simp_tac 1);
6.139 +by (Clarify_tac 1);
6.140 +by (res_inst_tac [("xs","ss")] rev_exhaust 1);
6.141 + by (Asm_full_simp_tac 1);
6.142 +by (Asm_full_simp_tac 1);
6.143 +by (dtac Snoc_step1_SnocD 1);
6.144 +by (Blast_tac 1);
6.145 qed_spec_mp "apps_preserves_betas";
6.146 Addsimps [apps_preserves_betas];
7.1 --- a/src/HOL/Lambda/ListOrder.ML Fri Aug 14 12:02:35 1998 +0200
7.2 +++ b/src/HOL/Lambda/ListOrder.ML Fri Aug 14 12:03:01 1998 +0200
7.3 @@ -5,55 +5,55 @@
7.4 *)
7.5
7.6 Goalw [step1_def] "step1(r^-1) = (step1 r)^-1";
7.7 -by(Blast_tac 1);
7.8 +by (Blast_tac 1);
7.9 qed "step1_converse";
7.10 Addsimps [step1_converse];
7.11
7.12 Goal "(p : step1(r^-1)) = (p : (step1 r)^-1)";
7.13 -by(Auto_tac);
7.14 +by (Auto_tac);
7.15 qed "in_step1_converse";
7.16 AddIffs [in_step1_converse];
7.17
7.18 Goalw [step1_def] "([],xs) ~: step1 r";
7.19 -by(Blast_tac 1);
7.20 +by (Blast_tac 1);
7.21 qed "not_Nil_step1";
7.22 AddIffs [not_Nil_step1];
7.23
7.24 Goalw [step1_def] "(xs,[]) ~: step1 r";
7.25 -by(Blast_tac 1);
7.26 +by (Blast_tac 1);
7.27 qed "not_step1_Nil";
7.28 AddIffs [not_step1_Nil];
7.29
7.30 Goalw [step1_def]
7.31 "((y#ys,x#xs) : step1 r) = ((y,x):r & xs=ys | x=y & (ys,xs) : step1 r)";
7.32 -by(Asm_full_simp_tac 1);
7.33 -br iffI 1;
7.34 - be exE 1;
7.35 - by(rename_tac "ts" 1);
7.36 - by(exhaust_tac "ts" 1);
7.37 - by(Force_tac 1);
7.38 - by(Force_tac 1);
7.39 -be disjE 1;
7.40 - by(Blast_tac 1);
7.41 -by(blast_tac (claset() addIs [Cons_eq_appendI]) 1);
7.42 +by (Asm_full_simp_tac 1);
7.43 +by (rtac iffI 1);
7.44 + by (etac exE 1);
7.45 + by (rename_tac "ts" 1);
7.46 + by (exhaust_tac "ts" 1);
7.47 + by (Force_tac 1);
7.48 + by (Force_tac 1);
7.49 +by (etac disjE 1);
7.50 + by (Blast_tac 1);
7.51 +by (blast_tac (claset() addIs [Cons_eq_appendI]) 1);
7.52 qed "Cons_step1_Cons";
7.53 AddIffs [Cons_step1_Cons];
7.54
7.55 Goalw [step1_def]
7.56 "(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
7.57 \ ==> (ys@vs,xs@us) : step1 r";
7.58 -by(Auto_tac);
7.59 -by(Force_tac 1);
7.60 -by(blast_tac (claset() addIs [append_eq_appendI]) 1);
7.61 +by (Auto_tac);
7.62 +by (Force_tac 1);
7.63 +by (blast_tac (claset() addIs [append_eq_appendI]) 1);
7.64 qed "append_step1I";
7.65
7.66 Goal "[| (ys,x#xs) : step1 r; \
7.67 \ !y. ys = y#xs --> (y,x) : r --> R; \
7.68 \ !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
7.69 \ |] ==> R";
7.70 -by(exhaust_tac "ys" 1);
7.71 - by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
7.72 -by(Blast_tac 1);
7.73 +by (exhaust_tac "ys" 1);
7.74 + by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
7.75 +by (Blast_tac 1);
7.76 val lemma = result();
7.77 bind_thm("Cons_step1E",
7.78 impI RSN (3,impI RSN (3,allI RSN (3,impI RSN (2,
7.79 @@ -62,44 +62,44 @@
7.80
7.81 Goalw [step1_def]
7.82 "(ys@[y],xs@[x]) : step1 r ==> ((ys,xs) : step1 r & y=x | ys=xs & (y,x) : r)";
7.83 -by(Asm_full_simp_tac 1);
7.84 -by(clarify_tac (claset() delrules [disjCI]) 1);
7.85 -by(rename_tac "vs" 1);
7.86 -by(res_inst_tac [("xs","vs")]rev_exhaust 1);
7.87 - by(Force_tac 1);
7.88 -by(Asm_full_simp_tac 1);
7.89 -by(Blast_tac 1);
7.90 +by (Asm_full_simp_tac 1);
7.91 +by (clarify_tac (claset() delrules [disjCI]) 1);
7.92 +by (rename_tac "vs" 1);
7.93 +by (res_inst_tac [("xs","vs")]rev_exhaust 1);
7.94 + by (Force_tac 1);
7.95 +by (Asm_full_simp_tac 1);
7.96 +by (Blast_tac 1);
7.97 qed "Snoc_step1_SnocD";
7.98
7.99 Goal "x : acc r ==> !xs. xs : acc(step1 r) --> x#xs : acc(step1 r)";
7.100 -be acc_induct 1;
7.101 -be thin_rl 1;
7.102 -by(Clarify_tac 1);
7.103 -be acc_induct 1;
7.104 -br accI 1;
7.105 -by(Blast_tac 1);
7.106 +by (etac acc_induct 1);
7.107 +by (etac thin_rl 1);
7.108 +by (Clarify_tac 1);
7.109 +by (etac acc_induct 1);
7.110 +by (rtac accI 1);
7.111 +by (Blast_tac 1);
7.112 val lemma = result();
7.113 qed_spec_mp "Cons_acc_step1I";
7.114 AddSIs [Cons_acc_step1I];
7.115
7.116 Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
7.117 be lists.induct 1;
7.118 - br accI 1;
7.119 - by(asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
7.120 -br accI 1;
7.121 -by(fast_tac (claset() addDs [acc_downward]) 1);
7.122 + by (rtac accI 1);
7.123 + by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
7.124 +by (rtac accI 1);
7.125 +by (fast_tac (claset() addDs [acc_downward]) 1);
7.126 qed "lists_accD";
7.127
7.128 Goalw [step1_def]
7.129 "[| x : set xs; (y,x) : r |] ==> ? ys. (ys,xs) : step1 r & y : set ys";
7.130 -bd (in_set_conv_decomp RS iffD1) 1;
7.131 -by(Force_tac 1);
7.132 +by (dtac (in_set_conv_decomp RS iffD1) 1);
7.133 +by (Force_tac 1);
7.134 qed "ex_step1I";
7.135
7.136 Goal "xs : acc(step1 r) ==> xs : lists(acc r)";
7.137 -be acc_induct 1;
7.138 -by(Clarify_tac 1);
7.139 -br accI 1;
7.140 -by(EVERY1[dtac ex_step1I, atac]);
7.141 -by(Blast_tac 1);
7.142 +by (etac acc_induct 1);
7.143 +by (Clarify_tac 1);
7.144 +by (rtac accI 1);
7.145 +by (EVERY1[dtac ex_step1I, atac]);
7.146 +by (Blast_tac 1);
7.147 qed "lists_accI";
8.1 --- a/src/HOL/List.ML Fri Aug 14 12:02:35 1998 +0200
8.2 +++ b/src/HOL/List.ML Fri Aug 14 12:03:01 1998 +0200
8.3 @@ -232,17 +232,17 @@
8.4 (* trivial rules for solving @-equations automatically *)
8.5
8.6 Goal "xs = ys ==> xs = [] @ ys";
8.7 -by(Asm_simp_tac 1);
8.8 +by (Asm_simp_tac 1);
8.9 qed "eq_Nil_appendI";
8.10
8.11 Goal "[| x#xs1 = ys; xs = xs1 @ zs |] ==> x#xs = ys@zs";
8.12 -bd sym 1;
8.13 -by(Asm_simp_tac 1);
8.14 +by (dtac sym 1);
8.15 +by (Asm_simp_tac 1);
8.16 qed "Cons_eq_appendI";
8.17
8.18 Goal "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us";
8.19 -bd sym 1;
8.20 -by(Asm_simp_tac 1);
8.21 +by (dtac sym 1);
8.22 +by (Asm_simp_tac 1);
8.23 qed "append_eq_appendI";
8.24
8.25
8.26 @@ -411,20 +411,20 @@
8.27 Addsimps [in_set_filter];
8.28
8.29 Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
8.30 -by(induct_tac "xs" 1);
8.31 - by(Simp_tac 1);
8.32 -by(Asm_simp_tac 1);
8.33 -br iffI 1;
8.34 -by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
8.35 -by(REPEAT(etac exE 1));
8.36 -by(exhaust_tac "ys" 1);
8.37 +by (induct_tac "xs" 1);
8.38 + by (Simp_tac 1);
8.39 +by (Asm_simp_tac 1);
8.40 +by (rtac iffI 1);
8.41 +by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
8.42 +by (REPEAT(etac exE 1));
8.43 +by (exhaust_tac "ys" 1);
8.44 by Auto_tac;
8.45 qed "in_set_conv_decomp";
8.46
8.47 (* eliminate `lists' in favour of `set' *)
8.48
8.49 Goal "(xs : lists A) = (!x : set xs. x : A)";
8.50 -by(induct_tac "xs" 1);
8.51 +by (induct_tac "xs" 1);
8.52 by Auto_tac;
8.53 qed "in_lists_conv_set";
8.54
8.55 @@ -799,7 +799,7 @@
8.56 section "foldl";
8.57
8.58 Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
8.59 -by(induct_tac "xs" 1);
8.60 +by (induct_tac "xs" 1);
8.61 by Auto_tac;
8.62 qed_spec_mp "foldl_append";
8.63 Addsimps [foldl_append];
8.64 @@ -808,19 +808,19 @@
8.65 because it requires an additional transitivity step
8.66 *)
8.67 Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
8.68 -by(induct_tac "ns" 1);
8.69 - by(Simp_tac 1);
8.70 -by(Asm_full_simp_tac 1);
8.71 -by(blast_tac (claset() addIs [trans_le_add1]) 1);
8.72 +by (induct_tac "ns" 1);
8.73 + by (Simp_tac 1);
8.74 +by (Asm_full_simp_tac 1);
8.75 +by (blast_tac (claset() addIs [trans_le_add1]) 1);
8.76 qed_spec_mp "start_le_sum";
8.77
8.78 Goal "n : set ns ==> n <= foldl op+ 0 ns";
8.79 -by(auto_tac (claset() addIs [start_le_sum],
8.80 +by (auto_tac (claset() addIs [start_le_sum],
8.81 simpset() addsimps [in_set_conv_decomp]));
8.82 qed "elem_le_sum";
8.83
8.84 Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
8.85 -by(induct_tac "ns" 1);
8.86 +by (induct_tac "ns" 1);
8.87 by Auto_tac;
8.88 qed_spec_mp "sum_eq_0_conv";
8.89 AddIffs [sum_eq_0_conv];
8.90 @@ -864,29 +864,29 @@
8.91 section"Lexcicographic orderings on lists";
8.92
8.93 Goal "wf r ==> wf(lexn r n)";
8.94 -by(induct_tac "n" 1);
8.95 -by(Simp_tac 1);
8.96 -by(Simp_tac 1);
8.97 -br wf_subset 1;
8.98 -br Int_lower1 2;
8.99 -br wf_prod_fun_image 1;
8.100 -br injI 2;
8.101 -by(Auto_tac);
8.102 +by (induct_tac "n" 1);
8.103 +by (Simp_tac 1);
8.104 +by (Simp_tac 1);
8.105 +by (rtac wf_subset 1);
8.106 +by (rtac Int_lower1 2);
8.107 +by (rtac wf_prod_fun_image 1);
8.108 +by (rtac injI 2);
8.109 +by (Auto_tac);
8.110 qed "wf_lexn";
8.111
8.112 Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
8.113 -by(induct_tac "n" 1);
8.114 -by(Auto_tac);
8.115 +by (induct_tac "n" 1);
8.116 +by (Auto_tac);
8.117 qed_spec_mp "lexn_length";
8.118
8.119 Goalw [lex_def] "wf r ==> wf(lex r)";
8.120 -br wf_UN 1;
8.121 -by(blast_tac (claset() addIs [wf_lexn]) 1);
8.122 -by(Clarify_tac 1);
8.123 -by(rename_tac "m n" 1);
8.124 -by(subgoal_tac "m ~= n" 1);
8.125 - by(Blast_tac 2);
8.126 -by(blast_tac (claset() addDs [lexn_length,not_sym]) 1);
8.127 +by (rtac wf_UN 1);
8.128 +by (blast_tac (claset() addIs [wf_lexn]) 1);
8.129 +by (Clarify_tac 1);
8.130 +by (rename_tac "m n" 1);
8.131 +by (subgoal_tac "m ~= n" 1);
8.132 + by (Blast_tac 2);
8.133 +by (blast_tac (claset() addDs [lexn_length,not_sym]) 1);
8.134 qed "wf_lex";
8.135 AddSIs [wf_lex];
8.136
8.137 @@ -894,30 +894,30 @@
8.138 "lexn r n = \
8.139 \ {(xs,ys). length xs = n & length ys = n & \
8.140 \ (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
8.141 -by(induct_tac "n" 1);
8.142 - by(Simp_tac 1);
8.143 - by(Blast_tac 1);
8.144 -by(asm_full_simp_tac (simpset() delsimps [length_Suc_conv]
8.145 +by (induct_tac "n" 1);
8.146 + by (Simp_tac 1);
8.147 + by (Blast_tac 1);
8.148 +by (asm_full_simp_tac (simpset() delsimps [length_Suc_conv]
8.149 addsimps [lex_prod_def]) 1);
8.150 -by(auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
8.151 - by(Blast_tac 1);
8.152 - by(rename_tac "a xys x xs' y ys'" 1);
8.153 - by(res_inst_tac [("x","a#xys")] exI 1);
8.154 - by(Simp_tac 1);
8.155 -by(exhaust_tac "xys" 1);
8.156 - by(ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
8.157 -by(Blast_tac 1);
8.158 +by (auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
8.159 + by (Blast_tac 1);
8.160 + by (rename_tac "a xys x xs' y ys'" 1);
8.161 + by (res_inst_tac [("x","a#xys")] exI 1);
8.162 + by (Simp_tac 1);
8.163 +by (exhaust_tac "xys" 1);
8.164 + by (ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
8.165 +by (Blast_tac 1);
8.166 qed "lexn_conv";
8.167
8.168 Goalw [lex_def]
8.169 "lex r = \
8.170 \ {(xs,ys). length xs = length ys & \
8.171 \ (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
8.172 -by(force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
8.173 +by (force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
8.174 qed "lex_conv";
8.175
8.176 Goalw [lexico_def] "wf r ==> wf(lexico r)";
8.177 -by(Blast_tac 1);
8.178 +by (Blast_tac 1);
8.179 qed "wf_lexico";
8.180 AddSIs [wf_lexico];
8.181
8.182 @@ -925,29 +925,29 @@
8.183 [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
8.184 "lexico r = {(xs,ys). length xs < length ys | \
8.185 \ length xs = length ys & (xs,ys) : lex r}";
8.186 -by(Simp_tac 1);
8.187 +by (Simp_tac 1);
8.188 qed "lexico_conv";
8.189
8.190 Goal "([],ys) ~: lex r";
8.191 -by(simp_tac (simpset() addsimps [lex_conv]) 1);
8.192 +by (simp_tac (simpset() addsimps [lex_conv]) 1);
8.193 qed "Nil_notin_lex";
8.194
8.195 Goal "(xs,[]) ~: lex r";
8.196 -by(simp_tac (simpset() addsimps [lex_conv]) 1);
8.197 +by (simp_tac (simpset() addsimps [lex_conv]) 1);
8.198 qed "Nil2_notin_lex";
8.199
8.200 AddIffs [Nil_notin_lex,Nil2_notin_lex];
8.201
8.202 Goal "((x#xs,y#ys) : lex r) = \
8.203 \ ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";
8.204 -by(simp_tac (simpset() addsimps [lex_conv]) 1);
8.205 -br iffI 1;
8.206 - by(blast_tac (claset() addIs [Cons_eq_appendI]) 2);
8.207 -by(REPEAT(eresolve_tac [conjE, exE] 1));
8.208 -by(exhaust_tac "xys" 1);
8.209 -by(Asm_full_simp_tac 1);
8.210 -by(Asm_full_simp_tac 1);
8.211 -by(Blast_tac 1);
8.212 +by (simp_tac (simpset() addsimps [lex_conv]) 1);
8.213 +by (rtac iffI 1);
8.214 + by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
8.215 +by (REPEAT(eresolve_tac [conjE, exE] 1));
8.216 +by (exhaust_tac "xys" 1);
8.217 +by (Asm_full_simp_tac 1);
8.218 +by (Asm_full_simp_tac 1);
8.219 +by (Blast_tac 1);
8.220 qed "Cons_in_lex";
8.221 AddIffs [Cons_in_lex];
8.222
9.1 --- a/src/HOL/Set.ML Fri Aug 14 12:02:35 1998 +0200
9.2 +++ b/src/HOL/Set.ML Fri Aug 14 12:03:01 1998 +0200
9.3 @@ -170,7 +170,7 @@
9.4
9.5 (*Anti-symmetry of the subset relation*)
9.6 Goal "[| A <= B; B <= A |] ==> A = (B::'a set)";
9.7 -br set_ext 1;
9.8 +by (rtac set_ext 1);
9.9 by (blast_tac (claset() addIs [subsetD]) 1);
9.10 qed "subset_antisym";
9.11 val equalityI = subset_antisym;
10.1 --- a/src/HOL/WF.ML Fri Aug 14 12:02:35 1998 +0200
10.2 +++ b/src/HOL/WF.ML Fri Aug 14 12:03:01 1998 +0200
10.3 @@ -72,7 +72,7 @@
10.4 *---------------------------------------------------------------------------*)
10.5
10.6 Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
10.7 -bd spec 1;
10.8 +by (dtac spec 1);
10.9 by (etac (mp RS spec) 1);
10.10 by (Blast_tac 1);
10.11 val lemma1 = result();
10.12 @@ -140,32 +140,32 @@
10.13 \ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
10.14 \ Domain(r j) Int Range(r i) = {} \
10.15 \ |] ==> wf(UN i:I. r i)";
10.16 -by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
10.17 -by(Clarify_tac 1);
10.18 -by(rename_tac "A a" 1);
10.19 -by(case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
10.20 - by(Clarify_tac 1);
10.21 - by(EVERY1[dtac bspec, atac,
10.22 +by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
10.23 +by (Clarify_tac 1);
10.24 +by (rename_tac "A a" 1);
10.25 +by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
10.26 + by (Clarify_tac 1);
10.27 + by (EVERY1[dtac bspec, atac,
10.28 eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]);
10.29 - by(EVERY1[etac allE,etac impE]);
10.30 - by(Blast_tac 1);
10.31 - by(Clarify_tac 1);
10.32 - by(rename_tac "z'" 1);
10.33 - by(res_inst_tac [("x","z'")] bexI 1);
10.34 - ba 2;
10.35 - by(Clarify_tac 1);
10.36 - by(rename_tac "j" 1);
10.37 - by(case_tac "r j = r i" 1);
10.38 - by(EVERY1[etac allE,etac impE,atac]);
10.39 - by(Asm_full_simp_tac 1);
10.40 - by(Blast_tac 1);
10.41 - by(blast_tac (claset() addEs [equalityE]) 1);
10.42 -by(Asm_full_simp_tac 1);
10.43 -by(case_tac "? i. i:I" 1);
10.44 - by(Clarify_tac 1);
10.45 - by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
10.46 - by(Blast_tac 1);
10.47 -by(Blast_tac 1);
10.48 + by (EVERY1[etac allE,etac impE]);
10.49 + by (Blast_tac 1);
10.50 + by (Clarify_tac 1);
10.51 + by (rename_tac "z'" 1);
10.52 + by (res_inst_tac [("x","z'")] bexI 1);
10.53 + by (assume_tac 2);
10.54 + by (Clarify_tac 1);
10.55 + by (rename_tac "j" 1);
10.56 + by (case_tac "r j = r i" 1);
10.57 + by (EVERY1[etac allE,etac impE,atac]);
10.58 + by (Asm_full_simp_tac 1);
10.59 + by (Blast_tac 1);
10.60 + by (blast_tac (claset() addEs [equalityE]) 1);
10.61 +by (Asm_full_simp_tac 1);
10.62 +by (case_tac "? i. i:I" 1);
10.63 + by (Clarify_tac 1);
10.64 + by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
10.65 + by (Blast_tac 1);
10.66 +by (Blast_tac 1);
10.67 qed "wf_UN";
10.68
10.69 Goalw [Union_def]
10.70 @@ -173,16 +173,16 @@
10.71 \ !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \
10.72 \ Domain s Int Range r = {} \
10.73 \ |] ==> wf(Union R)";
10.74 -br wf_UN 1;
10.75 -by(Blast_tac 1);
10.76 -by(Blast_tac 1);
10.77 +by (rtac wf_UN 1);
10.78 +by (Blast_tac 1);
10.79 +by (Blast_tac 1);
10.80 qed "wf_Union";
10.81
10.82 Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
10.83 \ |] ==> wf(r Un s)";
10.84 -br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
10.85 -by(Blast_tac 1);
10.86 -by(Blast_tac 1);
10.87 +by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1);
10.88 +by (Blast_tac 1);
10.89 +by (Blast_tac 1);
10.90 qed "wf_Un";
10.91
10.92 (*---------------------------------------------------------------------------
10.93 @@ -190,12 +190,12 @@
10.94 *---------------------------------------------------------------------------*)
10.95
10.96 Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
10.97 -by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
10.98 -by(Clarify_tac 1);
10.99 -by(case_tac "? p. f p : Q" 1);
10.100 -by(eres_inst_tac [("x","{p. f p : Q}")]allE 1);
10.101 -by(fast_tac (claset() addDs [injD]) 1);
10.102 -by(Blast_tac 1);
10.103 +by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
10.104 +by (Clarify_tac 1);
10.105 +by (case_tac "? p. f p : Q" 1);
10.106 +by (eres_inst_tac [("x","{p. f p : Q}")]allE 1);
10.107 +by (fast_tac (claset() addDs [injD]) 1);
10.108 +by (Blast_tac 1);
10.109 qed "wf_prod_fun_image";
10.110
10.111 (*** acyclic ***)
11.1 --- a/src/HOL/ex/LocaleGroup.ML Fri Aug 14 12:02:35 1998 +0200
11.2 +++ b/src/HOL/ex/LocaleGroup.ML Fri Aug 14 12:03:01 1998 +0200
11.3 @@ -19,10 +19,10 @@
11.4 (* Mit dieser Def ist es halt schwierig *)
11.5 goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G";
11.6 by (res_inst_tac [("t","op #")] ssubst 1);
11.7 -br ext 1;
11.8 -br ext 1;
11.9 -br meta_eq_to_obj_eq 1;
11.10 -br (thm "binop_def") 1;
11.11 +by (rtac ext 1);
11.12 +by (rtac ext 1);
11.13 +by (rtac meta_eq_to_obj_eq 1);
11.14 +by (rtac (thm "binop_def") 1);
11.15 by (Asm_full_simp_tac 1);
11.16 val binop_funcset = result();
11.17
11.18 @@ -32,9 +32,9 @@
11.19
11.20 goal LocaleGroup.thy "inv : carrier G -> carrier G";
11.21 by (res_inst_tac [("t","inv")] ssubst 1);
11.22 -br ext 1;
11.23 -br meta_eq_to_obj_eq 1;
11.24 -br (thm "inv_def") 1;
11.25 +by (rtac ext 1);
11.26 +by (rtac meta_eq_to_obj_eq 1);
11.27 +by (rtac (thm "inv_def") 1);
11.28 by (Asm_full_simp_tac 1);
11.29 val inv_funcset = result();
11.30
11.31 @@ -71,27 +71,27 @@
11.32 (* remarkable: In the following step the use of e_ax1 instead of unit_ax1
11.33 is better! It doesn't produce G: Group as subgoal and the nice syntax stays *)
11.34 by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
11.35 -ba 1;
11.36 +by (assume_tac 1);
11.37 (* great: we can use the nice syntax even in res_inst_tac *)
11.38 by (res_inst_tac [("P","%r. r # y = z")] subst 1);
11.39 by (res_inst_tac [("x","x")] inv_ax2 1);
11.40 -ba 1;
11.41 -br (binop_assoc RS ssubst) 1;
11.42 -br inv_closed 1;
11.43 -ba 1;
11.44 -ba 1;
11.45 -ba 1;
11.46 -be ssubst 1;
11.47 -br (binop_assoc RS subst) 1;
11.48 -br inv_closed 1;
11.49 -ba 1;
11.50 -ba 1;
11.51 -ba 1;
11.52 -br (inv_ax2 RS ssubst) 1;
11.53 -ba 1;
11.54 -br (e_ax1 RS ssubst) 1;
11.55 -ba 1;
11.56 -br refl 1;
11.57 +by (assume_tac 1);
11.58 +by (stac binop_assoc 1);
11.59 +by (rtac inv_closed 1);
11.60 +by (assume_tac 1);
11.61 +by (assume_tac 1);
11.62 +by (assume_tac 1);
11.63 +by (etac ssubst 1);
11.64 +by (rtac (binop_assoc RS subst) 1);
11.65 +by (rtac inv_closed 1);
11.66 +by (assume_tac 1);
11.67 +by (assume_tac 1);
11.68 +by (assume_tac 1);
11.69 +by (stac inv_ax2 1);
11.70 +by (assume_tac 1);
11.71 +by (stac e_ax1 1);
11.72 +by (assume_tac 1);
11.73 +by (rtac refl 1);
11.74 val left_cancellation = result();
11.75
11.76
11.77 @@ -105,57 +105,57 @@
11.78 by (fold_goals_tac [thm "inv_def"]);
11.79 by (fast_tac (claset() addSEs [inv_closed]) 1);
11.80 by (afs [binop_closed, e_closed] 1);
11.81 -ba 1;
11.82 -br (binop_assoc RS subst) 1;
11.83 +by (assume_tac 1);
11.84 +by (rtac (binop_assoc RS subst) 1);
11.85 by (fast_tac (claset() addSEs [inv_closed]) 1);
11.86 -ba 1;
11.87 -br (e_closed) 1;
11.88 -br (inv_ax2 RS ssubst) 1;
11.89 -ba 1;
11.90 -br (e_ax1 RS ssubst) 1;
11.91 -br e_closed 1;
11.92 -br refl 1;
11.93 +by (assume_tac 1);
11.94 +by (rtac (e_closed) 1);
11.95 +by (stac inv_ax2 1);
11.96 +by (assume_tac 1);
11.97 +by (stac e_ax1 1);
11.98 +by (rtac e_closed 1);
11.99 +by (rtac refl 1);
11.100 val e_ax2 = result();
11.101
11.102 goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e";
11.103 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1);
11.104 -ba 1;
11.105 +by (assume_tac 1);
11.106 by (res_inst_tac [("x","x")] left_cancellation 1);
11.107 -ba 1;
11.108 -ba 1;
11.109 -br e_closed 1;
11.110 -ba 1;
11.111 +by (assume_tac 1);
11.112 +by (assume_tac 1);
11.113 +by (rtac e_closed 1);
11.114 +by (assume_tac 1);
11.115 val idempotent_e = result();
11.116
11.117 goal LocaleGroup.thy "!! x. x: carrier G ==> x # (x -|) = e";
11.118 -br idempotent_e 1;
11.119 +by (rtac idempotent_e 1);
11.120 by (afs [binop_closed,inv_closed] 1);
11.121 -br (binop_assoc RS ssubst) 1;
11.122 -ba 1;
11.123 +by (stac binop_assoc 1);
11.124 +by (assume_tac 1);
11.125 by (afs [inv_closed] 1);
11.126 by (afs [binop_closed,inv_closed] 1);
11.127 by (res_inst_tac [("t","x -| # x # x -|")] subst 1);
11.128 -br binop_assoc 1;
11.129 +by (rtac binop_assoc 1);
11.130 by (afs [inv_closed] 1);
11.131 -ba 1;
11.132 +by (assume_tac 1);
11.133 by (afs [inv_closed] 1);
11.134 -br (inv_ax2 RS ssubst) 1;
11.135 -ba 1;
11.136 -br (e_ax1 RS ssubst) 1;
11.137 +by (stac inv_ax2 1);
11.138 +by (assume_tac 1);
11.139 +by (stac e_ax1 1);
11.140 by (afs [inv_closed] 1);
11.141 -br refl 1;
11.142 +by (rtac refl 1);
11.143 val inv_ax1 = result();
11.144
11.145
11.146 goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \
11.147 \ x # y = e |] ==> y = x -|";
11.148 by (res_inst_tac [("x","x")] left_cancellation 1);
11.149 -ba 1;
11.150 -ba 1;
11.151 +by (assume_tac 1);
11.152 +by (assume_tac 1);
11.153 by (afs [inv_closed] 1);
11.154 -br (inv_ax1 RS ssubst) 1;
11.155 -ba 1;
11.156 -ba 1;
11.157 +by (stac inv_ax1 1);
11.158 +by (assume_tac 1);
11.159 +by (assume_tac 1);
11.160 val inv_unique = result();
11.161
11.162 goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x";
11.163 @@ -163,19 +163,19 @@
11.164 by (fold_goals_tac [thm "inv_def"]);
11.165 by (afs [inv_closed] 1);
11.166 by (afs [inv_closed] 1);
11.167 -ba 1;
11.168 +by (assume_tac 1);
11.169 by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
11.170 val inv_inv = result();
11.171
11.172 goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\
11.173 \ ==> (x # y) -| = y -| # x -|";
11.174 -br sym 1;
11.175 -br inv_unique 1;
11.176 +by (rtac sym 1);
11.177 +by (rtac inv_unique 1);
11.178 by (afs [binop_closed] 1);
11.179 by (afs [inv_closed,binop_closed] 1);
11.180 by (afs [binop_assoc,inv_closed,binop_closed] 1);
11.181 by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1);
11.182 -ba 1;
11.183 +by (assume_tac 1);
11.184 by (afs [inv_closed] 1);
11.185 by (afs [inv_closed] 1);
11.186 by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
11.187 @@ -185,15 +185,15 @@
11.188 goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\
11.189 \ z : carrier G; y # x = z # x|] ==> y = z";
11.190 by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
11.191 -ba 1;
11.192 +by (assume_tac 1);
11.193 by (res_inst_tac [("P","%r. y # r = z")] subst 1);
11.194 -br inv_ax1 1;
11.195 -ba 1;
11.196 -br (binop_assoc RS subst) 1;
11.197 -ba 1;
11.198 -ba 1;
11.199 +by (rtac inv_ax1 1);
11.200 +by (assume_tac 1);
11.201 +by (rtac (binop_assoc RS subst) 1);
11.202 +by (assume_tac 1);
11.203 +by (assume_tac 1);
11.204 by (afs [inv_closed] 1);
11.205 -be ssubst 1;
11.206 +by (etac ssubst 1);
11.207 by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1);
11.208 val right_cancellation = result();
11.209
12.1 --- a/src/HOL/ex/PiSets.ML Fri Aug 14 12:02:35 1998 +0200
12.2 +++ b/src/HOL/ex/PiSets.ML Fri Aug 14 12:03:01 1998 +0200
12.3 @@ -26,57 +26,57 @@
12.4 (* individual theorems for convenient use *)
12.5 val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q";
12.6 by (fold_goals_tac [p1]);
12.7 -br p2 1;
12.8 +by (rtac p2 1);
12.9 val apply_def = result();
12.10
12.11 goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)";
12.12 -be ssubst 1;
12.13 -br refl 1;
12.14 +by (etac ssubst 1);
12.15 +by (rtac refl 1);
12.16 val extend = result();
12.17
12.18 val [p1] = goal HOL.thy "P ==> ~~P";
12.19 -br notI 1;
12.20 -br (p1 RSN(2, notE)) 1;
12.21 -ba 1;
12.22 +by (rtac notI 1);
12.23 +by (rtac (p1 RSN(2, notE)) 1);
12.24 +by (assume_tac 1);
12.25 val notnotI = result();
12.26
12.27 val [p1] = goal Set.thy "? x. x: S ==> S ~= {}";
12.28 -br contrapos 1;
12.29 -br (p1 RS notnotI) 1;
12.30 -be ssubst 1;
12.31 -br notI 1;
12.32 -be exE 1;
12.33 -be emptyE 1;
12.34 +by (rtac contrapos 1);
12.35 +by (rtac (p1 RS notnotI) 1);
12.36 +by (etac ssubst 1);
12.37 +by (rtac notI 1);
12.38 +by (etac exE 1);
12.39 +by (etac emptyE 1);
12.40 val ExEl_NotEmpty = result();
12.41
12.42
12.43 val [p1] = goal HOL.thy "~x ==> x = False";
12.44 val l1 = (p1 RS (not_def RS apply_def)) RS mp;
12.45 val l2 = read_instantiate [("P","x")] FalseE;
12.46 -br iffI 1;
12.47 -br l1 1;
12.48 -br l2 2;
12.49 -ba 1;
12.50 -ba 1;
12.51 +by (rtac iffI 1);
12.52 +by (rtac l1 1);
12.53 +by (rtac l2 2);
12.54 +by (assume_tac 1);
12.55 +by (assume_tac 1);
12.56 val NoteqFalseEq = result();
12.57
12.58 val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)";
12.59 -br exCI 1;
12.60 +by (rtac exCI 1);
12.61 (* 1. ! x. ~ P x ==> P ?a *)
12.62 val l1 = p1 RS NoteqFalseEq;
12.63 (* l1 = (! x. ~ P x) = False *)
12.64 val l2 = l1 RS iffD1;
12.65 val l3 = l1 RS iffD2;
12.66 val l4 = read_instantiate [("P", "P ?a")] FalseE;
12.67 -br (l2 RS l4) 1;
12.68 -ba 1;
12.69 +by (rtac (l2 RS l4) 1);
12.70 +by (assume_tac 1);
12.71 val NotAllNot_Ex = result();
12.72
12.73 val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)";
12.74 -br notnotD 1;
12.75 -br (p1 RS contrapos) 1;
12.76 -br NotAllNot_Ex 1;
12.77 -ba 1;
12.78 +by (rtac notnotD 1);
12.79 +by (rtac (p1 RS contrapos) 1);
12.80 +by (rtac NotAllNot_Ex 1);
12.81 +by (assume_tac 1);
12.82 val NotEx_AllNot = result();
12.83
12.84 goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}";
12.85 @@ -93,20 +93,20 @@
12.86
12.87
12.88 val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)";
12.89 -br (q1 RS ssubst) 1;
12.90 -br q2 1;
12.91 +by (stac q1 1);
12.92 +by (rtac q2 1);
12.93 val forw_subst = result();
12.94
12.95 val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)";
12.96 -br (q1 RS subst) 1;
12.97 -br q2 1;
12.98 +by (rtac (q1 RS subst) 1);
12.99 +by (rtac q2 1);
12.100 val forw_ssubst = result();
12.101
12.102 goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A";
12.103 -br (surjective_pairing RS subst) 1;
12.104 -br (surjective_pairing RS subst) 1;
12.105 -br (surjective_pairing RS subst) 1;
12.106 -br refl 1;
12.107 +by (rtac (surjective_pairing RS subst) 1);
12.108 +by (rtac (surjective_pairing RS subst) 1);
12.109 +by (rtac (surjective_pairing RS subst) 1);
12.110 +by (rtac refl 1);
12.111 val blow4 = result();
12.112
12.113 goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)";
12.114 @@ -116,27 +116,27 @@
12.115
12.116 goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \
12.117 \ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))";
12.118 -bd (blow4 RS forw_subst) 1;
12.119 +by (dtac (blow4 RS forw_subst) 1);
12.120 by (afs [split_def] 1);
12.121 val apply_quadr = result();
12.122
12.123 goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)";
12.124 -br (surjective_pairing RS subst) 1;
12.125 -br refl 1;
12.126 +by (rtac (surjective_pairing RS subst) 1);
12.127 +by (rtac refl 1);
12.128 val surj_pair_forw = result();
12.129
12.130 goal Prod.thy "!! A B x. x: A Times B ==> fst x: A";
12.131 by (forward_tac [surj_pair_forw] 1);
12.132 -bd forw_ssubst 1;
12.133 -ba 1;
12.134 -be SigmaD1 1;
12.135 +by (dtac forw_ssubst 1);
12.136 +by (assume_tac 1);
12.137 +by (etac SigmaD1 1);
12.138 val TimesE1 = result();
12.139
12.140 goal Prod.thy "!! A B x. x: A Times B ==> snd x: B";
12.141 by (forward_tac [surj_pair_forw] 1);
12.142 -bd forw_ssubst 1;
12.143 -ba 1;
12.144 -be SigmaD2 1;
12.145 +by (dtac forw_ssubst 1);
12.146 +by (assume_tac 1);
12.147 +by (etac SigmaD2 1);
12.148 val TimesE2 = result();
12.149
12.150 (* -> and Pi *)
12.151 @@ -148,16 +148,16 @@
12.152
12.153 val [q1,q2] = goal PiSets.thy
12.154 "[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: Pi A B";
12.155 -by (rewrite_goals_tac [Pi_def]);
12.156 -br CollectI 1;
12.157 -br allI 1;
12.158 +by (rewtac Pi_def);
12.159 +by (rtac CollectI 1);
12.160 +by (rtac allI 1);
12.161 by (case_tac "x : A" 1);
12.162 -br (if_P RS ssubst) 1;
12.163 -ba 1;
12.164 -be q1 1;
12.165 -br (if_not_P RS ssubst) 1;
12.166 -ba 1;
12.167 -be q2 1;
12.168 +by (stac if_P 1);
12.169 +by (assume_tac 1);
12.170 +by (etac q1 1);
12.171 +by (stac if_not_P 1);
12.172 +by (assume_tac 1);
12.173 +by (etac q2 1);
12.174 val Pi_I = result();
12.175
12.176 goal PiSets.thy
12.177 @@ -199,7 +199,7 @@
12.178
12.179 goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\
12.180 \ ==> f = g";
12.181 -br ext 1;
12.182 +by (rtac ext 1);
12.183 by (case_tac "x : A" 1);
12.184 by (Fast_tac 1);
12.185 by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1);
12.186 @@ -207,7 +207,7 @@
12.187
12.188 goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\
12.189 \ ==> f = g";
12.190 -br ext 1;
12.191 +by (rtac ext 1);
12.192 by (case_tac "x : A" 1);
12.193 by (Fast_tac 1);
12.194 by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1);
12.195 @@ -215,28 +215,28 @@
12.196
12.197 (* compose *)
12.198 goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C";
12.199 -br funcsetI 1;
12.200 +by (rtac funcsetI 1);
12.201 by (rewrite_goals_tac [compose_def,restrict_def]);
12.202 by (afs [funcsetE1] 1);
12.203 -br (if_not_P RS ssubst) 1;
12.204 -ba 1;
12.205 -br refl 1;
12.206 +by (stac if_not_P 1);
12.207 +by (assume_tac 1);
12.208 +by (rtac refl 1);
12.209 val funcset_compose = result();
12.210
12.211 goal PiSets.thy "!! A B C f g h. [| f: A -> B; g: B -> C; h: C -> D |]\
12.212 \ ==> compose A h (compose A g f) = compose A (compose B h g) f";
12.213 by (res_inst_tac [("A","A")] function_extensionality 1);
12.214 -br funcset_compose 1;
12.215 -br funcset_compose 1;
12.216 -ba 1;
12.217 -ba 1;
12.218 -ba 1;
12.219 -br funcset_compose 1;
12.220 -ba 1;
12.221 -br funcset_compose 1;
12.222 -ba 1;
12.223 -ba 1;
12.224 -br ballI 1;
12.225 +by (rtac funcset_compose 1);
12.226 +by (rtac funcset_compose 1);
12.227 +by (assume_tac 1);
12.228 +by (assume_tac 1);
12.229 +by (assume_tac 1);
12.230 +by (rtac funcset_compose 1);
12.231 +by (assume_tac 1);
12.232 +by (rtac funcset_compose 1);
12.233 +by (assume_tac 1);
12.234 +by (assume_tac 1);
12.235 +by (rtac ballI 1);
12.236 by (rewrite_goals_tac [compose_def,restrict_def]);
12.237 by (afs [funcsetE1,if_P RS ssubst] 1);
12.238 val compose_assoc = result();
12.239 @@ -247,88 +247,88 @@
12.240
12.241 goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\
12.242 \ ==> compose A g f `` A = C";
12.243 -br equalityI 1;
12.244 -br subsetI 1;
12.245 -be imageE 1;
12.246 +by (rtac equalityI 1);
12.247 +by (rtac subsetI 1);
12.248 +by (etac imageE 1);
12.249 by (rotate_tac 4 1);
12.250 -be ssubst 1;
12.251 -br (funcset_compose RS funcsetE1) 1;
12.252 -ba 1;
12.253 -ba 1;
12.254 -ba 1;
12.255 -br subsetI 1;
12.256 +by (etac ssubst 1);
12.257 +by (rtac (funcset_compose RS funcsetE1) 1);
12.258 +by (assume_tac 1);
12.259 +by (assume_tac 1);
12.260 +by (assume_tac 1);
12.261 +by (rtac subsetI 1);
12.262 by (hyp_subst_tac 1);
12.263 -be imageE 1;
12.264 +by (etac imageE 1);
12.265 by (rotate_tac 3 1);
12.266 -be ssubst 1;
12.267 -be imageE 1;
12.268 +by (etac ssubst 1);
12.269 +by (etac imageE 1);
12.270 by (rotate_tac 3 1);
12.271 -be ssubst 1;
12.272 -be (composeE1 RS subst) 1;
12.273 -ba 1;
12.274 -ba 1;
12.275 -br imageI 1;
12.276 -ba 1;
12.277 +by (etac ssubst 1);
12.278 +by (etac (composeE1 RS subst) 1);
12.279 +by (assume_tac 1);
12.280 +by (assume_tac 1);
12.281 +by (rtac imageI 1);
12.282 +by (assume_tac 1);
12.283 val surj_compose = result();
12.284
12.285
12.286 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 |]\
12.287 \ ==> inj_on (compose A g f) A";
12.288 -br inj_onI 1;
12.289 +by (rtac inj_onI 1);
12.290 by (forward_tac [composeE1] 1);
12.291 -ba 1;
12.292 -ba 1;
12.293 +by (assume_tac 1);
12.294 +by (assume_tac 1);
12.295 by (forward_tac [composeE1] 1);
12.296 -ba 1;
12.297 +by (assume_tac 1);
12.298 by (rotate_tac 7 1);
12.299 -ba 1;
12.300 +by (assume_tac 1);
12.301 by (step_tac (claset() addSEs [inj_onD]) 1);
12.302 by (rotate_tac 5 1);
12.303 -be subst 1;
12.304 -be subst 1;
12.305 -ba 1;
12.306 -be imageI 1;
12.307 -be imageI 1;
12.308 +by (etac subst 1);
12.309 +by (etac subst 1);
12.310 +by (assume_tac 1);
12.311 +by (etac imageI 1);
12.312 +by (etac imageI 1);
12.313 val inj_on_compose = result();
12.314
12.315
12.316 (* restrict / lam *)
12.317 goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B";
12.318 -by (rewrite_goals_tac [restrict_def]);
12.319 -br funcsetI 1;
12.320 +by (rewtac restrict_def);
12.321 +by (rtac funcsetI 1);
12.322 by (afs [if_P RS ssubst] 1);
12.323 -be subsetD 1;
12.324 -be imageI 1;
12.325 +by (etac subsetD 1);
12.326 +by (etac imageI 1);
12.327 by (afs [if_not_P RS ssubst] 1);
12.328 val restrict_in_funcset = result();
12.329
12.330 goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B";
12.331 -br restrict_in_funcset 1;
12.332 +by (rtac restrict_in_funcset 1);
12.333 by (afs [image_def] 1);
12.334 by (Step_tac 1);
12.335 by (Fast_tac 1);
12.336 val restrictI = result();
12.337
12.338 goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B";
12.339 -by (rewrite_goals_tac [restrict_def]);
12.340 -br Pi_I 1;
12.341 +by (rewtac restrict_def);
12.342 +by (rtac Pi_I 1);
12.343 by (afs [if_P RS ssubst] 1);
12.344 by (Asm_full_simp_tac 1);
12.345 val restrictI_Pi = result();
12.346
12.347 (* The following proof has to be redone *)
12.348 goal PiSets.thy "!! f A B C.[| f `` A <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
12.349 -br restrict_in_funcset 1;
12.350 +by (rtac restrict_in_funcset 1);
12.351 by (afs [image_def] 1);
12.352 by (afs [Pi_def,subset_def] 1);
12.353 by (afs [restrict_def] 1);
12.354 by (Step_tac 1);
12.355 by (Asm_full_simp_tac 1);
12.356 by (dres_inst_tac [("x","f xa")] spec 1);
12.357 -bd mp 1;
12.358 -br bexI 1;
12.359 -br refl 1;
12.360 -ba 1;
12.361 +by (dtac mp 1);
12.362 +by (rtac bexI 1);
12.363 +by (rtac refl 1);
12.364 +by (assume_tac 1);
12.365 by (dres_inst_tac [("x","xb")] spec 1);
12.366 by (Asm_full_simp_tac 1);
12.367 (* fini 1 *)
12.368 @@ -336,7 +336,7 @@
12.369 val restrict_in_funcset2 = result();
12.370
12.371 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";
12.372 -br restrict_in_funcset 1;
12.373 +by (rtac restrict_in_funcset 1);
12.374 by (afs [image_def] 1);
12.375 by (afs [Pi_def,subset_def] 1);
12.376 by (afs [restrict_def] 1);
12.377 @@ -387,7 +387,7 @@
12.378
12.379 goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\
12.380 \ ==> (lam x: A. f x) = (lam x: A. g x)";
12.381 -br ext 1;
12.382 +by (rtac ext 1);
12.383 by (case_tac "x: A" 1);
12.384 by (afs [restrictE1] 1);
12.385 by (afs [restrictE2] 1);
12.386 @@ -396,89 +396,89 @@
12.387 (* Invers *)
12.388
12.389 goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x";
12.390 -by (rewrite_goals_tac [image_def]);
12.391 -bd equalityD2 1;
12.392 -bd subsetD 1;
12.393 -ba 1;
12.394 -bd CollectD 1;
12.395 -be bexE 1;
12.396 -bd sym 1;
12.397 -be bexI 1;
12.398 -ba 1;
12.399 +by (rewtac image_def);
12.400 +by (dtac equalityD2 1);
12.401 +by (dtac subsetD 1);
12.402 +by (assume_tac 1);
12.403 +by (dtac CollectD 1);
12.404 +by (etac bexE 1);
12.405 +by (dtac sym 1);
12.406 +by (etac bexI 1);
12.407 +by (assume_tac 1);
12.408 val surj_image = result();
12.409
12.410 val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \
12.411 \ ==> (lam x: B. (Inv A f) x) : B -> A";
12.412 -br restrict_in_funcset 1;
12.413 -by (rewrite_goals_tac [image_def]);
12.414 -br subsetI 1;
12.415 -bd CollectD 1;
12.416 -be bexE 1;
12.417 -be ssubst 1;
12.418 -bd (q1 RS surj_image) 1;
12.419 -be bexE 1;
12.420 -be subst 1;
12.421 -by (rewrite_goals_tac [Inv_def]);
12.422 +by (rtac restrict_in_funcset 1);
12.423 +by (rewtac image_def);
12.424 +by (rtac subsetI 1);
12.425 +by (dtac CollectD 1);
12.426 +by (etac bexE 1);
12.427 +by (etac ssubst 1);
12.428 +by (dtac (q1 RS surj_image) 1);
12.429 +by (etac bexE 1);
12.430 +by (etac subst 1);
12.431 +by (rewtac Inv_def);
12.432 by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1);
12.433 -br (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
12.434 -be (q2 RS funcsetE1) 1;
12.435 +by (rtac (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
12.436 +by (etac (q2 RS funcsetE1) 1);
12.437 val Inv_funcset = result();
12.438
12.439
12.440 val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
12.441 \ ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x";
12.442 -br ballI 1;
12.443 -br (restrictE1 RS ssubst) 1;
12.444 -be (q1 RS funcsetE1) 1;
12.445 -by (rewrite_goals_tac [Inv_def]);
12.446 -br (q2 RS inj_onD) 1;
12.447 -ba 3;
12.448 +by (rtac ballI 1);
12.449 +by (stac restrictE1 1);
12.450 +by (etac (q1 RS funcsetE1) 1);
12.451 +by (rewtac Inv_def);
12.452 +by (rtac (q2 RS inj_onD) 1);
12.453 +by (assume_tac 3);
12.454 by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1);
12.455 -br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
12.456 -be (q1 RS funcsetE1) 1;
12.457 +by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
12.458 +by (etac (q1 RS funcsetE1) 1);
12.459 by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1);
12.460 -br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
12.461 -be (q1 RS funcsetE1) 1;
12.462 +by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
12.463 +by (etac (q1 RS funcsetE1) 1);
12.464 val Inv_f_f = result();
12.465
12.466 val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\
12.467 \ ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x";
12.468 -br ballI 1;
12.469 -br (restrictE1 RS ssubst) 1;
12.470 -ba 1;
12.471 -by (rewrite_goals_tac [Inv_def]);
12.472 +by (rtac ballI 1);
12.473 +by (stac restrictE1 1);
12.474 +by (assume_tac 1);
12.475 +by (rewtac Inv_def);
12.476 by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1);
12.477 -br (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
12.478 -ba 1;
12.479 +by (rtac (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
12.480 +by (assume_tac 1);
12.481 val f_Inv_f = result();
12.482
12.483 val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
12.484 \ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
12.485 -br function_extensionality 1;
12.486 -br funcset_compose 1;
12.487 -br q1 1;
12.488 -br (q1 RS (q3 RS Inv_funcset)) 1;
12.489 -br restrict_in_funcset 1;
12.490 +by (rtac function_extensionality 1);
12.491 +by (rtac funcset_compose 1);
12.492 +by (rtac q1 1);
12.493 +by (rtac (q1 RS (q3 RS Inv_funcset)) 1);
12.494 +by (rtac restrict_in_funcset 1);
12.495 by (Fast_tac 1);
12.496 -br ballI 1;
12.497 +by (rtac ballI 1);
12.498 by (afs [compose_def] 1);
12.499 -br (restrictE1 RS ssubst) 1;
12.500 -ba 1;
12.501 -br (restrictE1 RS ssubst) 1;
12.502 -ba 1;
12.503 -be (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1;
12.504 +by (stac restrictE1 1);
12.505 +by (assume_tac 1);
12.506 +by (stac restrictE1 1);
12.507 +by (assume_tac 1);
12.508 +by (etac (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1);
12.509 val comp_Inv_id = result();
12.510
12.511
12.512 (* Pi and its application @@ *)
12.513
12.514 goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}";
12.515 -bd NotEmpty_ExEl 1;
12.516 -be exE 1;
12.517 -by (rewrite_goals_tac [Pi_def]);
12.518 -bd CollectD 1;
12.519 -br ballI 1;
12.520 -br ExEl_NotEmpty 1;
12.521 +by (dtac NotEmpty_ExEl 1);
12.522 +by (etac exE 1);
12.523 +by (rewtac Pi_def);
12.524 +by (dtac CollectD 1);
12.525 +by (rtac ballI 1);
12.526 +by (rtac ExEl_NotEmpty 1);
12.527 by (res_inst_tac [("x","x xa")] exI 1);
12.528 by (afs [if_P RS subst] 1);
12.529 val Pi_total1 = result();
12.530 @@ -488,38 +488,38 @@
12.531 val SetEx_NotNotAll = result();
12.532
12.533 goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}";
12.534 -br notnotD 1;
12.535 -br (Pi_total1 RSN(2,contrapos)) 1;
12.536 -ba 2;
12.537 -be SetEx_NotNotAll 1;
12.538 +by (rtac notnotD 1);
12.539 +by (rtac (Pi_total1 RSN(2,contrapos)) 1);
12.540 +by (assume_tac 2);
12.541 +by (etac SetEx_NotNotAll 1);
12.542 val Pi_total2 = result();
12.543
12.544 val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)";
12.545 -by (rewrite_goals_tac [Fset_apply_def]);
12.546 -br equalityI 1;
12.547 -br subsetI 1;
12.548 -be imageE 1;
12.549 -be ssubst 1;
12.550 -by (rewrite_goals_tac [Pi_def]);
12.551 -bd CollectD 1;
12.552 -bd spec 1;
12.553 -br (q1 RS if_P RS subst) 1;
12.554 -ba 1;
12.555 -br subsetI 1;
12.556 -by (rewrite_goals_tac [image_def]);
12.557 -br CollectI 1;
12.558 -br exE 1;
12.559 -br (q2 RS NotEmpty_ExEl) 1;
12.560 +by (rewtac Fset_apply_def);
12.561 +by (rtac equalityI 1);
12.562 +by (rtac subsetI 1);
12.563 +by (etac imageE 1);
12.564 +by (etac ssubst 1);
12.565 +by (rewtac Pi_def);
12.566 +by (dtac CollectD 1);
12.567 +by (dtac spec 1);
12.568 +by (rtac (q1 RS if_P RS subst) 1);
12.569 +by (assume_tac 1);
12.570 +by (rtac subsetI 1);
12.571 +by (rewtac image_def);
12.572 +by (rtac CollectI 1);
12.573 +by (rtac exE 1);
12.574 +by (rtac (q2 RS NotEmpty_ExEl) 1);
12.575 by (res_inst_tac [("x","%y. if (y = a) then x else xa y")] bexI 1);
12.576 by (Simp_tac 1);
12.577 by (Simp_tac 1);
12.578 -br allI 1;
12.579 +by (rtac allI 1);
12.580 by (case_tac "xb: A" 1);
12.581 by (afs [if_P RS ssubst] 1);
12.582 by (case_tac "xb = a" 1);
12.583 by (afs [if_P RS ssubst] 1);
12.584 by (afs [if_not_P RS ssubst] 1);
12.585 -by (rewrite_goals_tac [Pi_def]);
12.586 +by (rewtac Pi_def);
12.587 by (afs [if_P RS ssubst] 1);
12.588 by (afs [if_not_P RS ssubst] 1);
12.589 by (case_tac "xb = a" 1);
12.590 @@ -530,32 +530,32 @@
12.591 val Pi_app_def = result();
12.592
12.593 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) ~= {}";
12.594 -bd NotEmpty_ExEl 1;
12.595 -be exE 1;
12.596 -by (rewrite_goals_tac [Pi_def]);
12.597 -bd CollectD 1;
12.598 -bd spec 1;
12.599 -br ExEl_NotEmpty 1;
12.600 -br exI 1;
12.601 -be (if_P RS eq_reflection RS apply_def) 1;
12.602 -ba 1;
12.603 +by (dtac NotEmpty_ExEl 1);
12.604 +by (etac exE 1);
12.605 +by (rewtac Pi_def);
12.606 +by (dtac CollectD 1);
12.607 +by (dtac spec 1);
12.608 +by (rtac ExEl_NotEmpty 1);
12.609 +by (rtac exI 1);
12.610 +by (etac (if_P RS eq_reflection RS apply_def) 1);
12.611 +by (assume_tac 1);
12.612 val NotEmptyPiStep = result();
12.613
12.614 val [q1,q2,q3] = goal PiSets.thy
12.615 "[|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";
12.616 by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]);
12.617 by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]);
12.618 -br refl 1;
12.619 +by (rtac refl 1);
12.620 val Pi_app2_def = result();
12.621
12.622 (* Sigma does a better job ( the following is from PiSig.ML) *)
12.623 goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\
12.624 \ ==> Sigma A B ^^ {a} = Pi A B @@ a";
12.625 -br (Pi_app_def RS ssubst) 1;
12.626 -ba 1;
12.627 -ba 1;
12.628 +by (stac Pi_app_def 1);
12.629 +by (assume_tac 1);
12.630 +by (assume_tac 1);
12.631 by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1);
12.632 -by (rewrite_goals_tac [Bex_def]);
12.633 +by (rewtac Bex_def);
12.634 by (Fast_tac 1);
12.635 val PiSig_image_eq = result();
12.636
12.637 @@ -567,25 +567,25 @@
12.638 (* Bijection between Pi in terms of => and Pi in terms of Sigma *)
12.639 goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B";
12.640 by (afs [PiBij_def,Pi_def,restrictE1] 1);
12.641 -br subsetI 1;
12.642 +by (rtac subsetI 1);
12.643 by (split_all_tac 1);
12.644 -bd CollectD 1;
12.645 +by (dtac CollectD 1);
12.646 by (Asm_full_simp_tac 1);
12.647 val PiBij_subset_Sigma = result();
12.648
12.649 goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
12.650 by (afs [PiBij_def,restrictE1] 1);
12.651 -br ballI 1;
12.652 -br ex1I 1;
12.653 -ba 2;
12.654 -br refl 1;
12.655 +by (rtac ballI 1);
12.656 +by (rtac ex1I 1);
12.657 +by (assume_tac 2);
12.658 +by (rtac refl 1);
12.659 val PiBij_unique = result();
12.660
12.661 goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))";
12.662 by (afs [PiBij_def,restrictE1] 1);
12.663 -br ballI 1;
12.664 -br ex1I 1;
12.665 -be conjunct2 2;
12.666 +by (rtac ballI 1);
12.667 +by (rtac ex1I 1);
12.668 +by (etac conjunct2 2);
12.669 by (afs [PiE1] 1);
12.670 val PiBij_unique2 = result();
12.671
12.672 @@ -595,15 +595,15 @@
12.673
12.674 goal PiSets.thy "!! A B. PiBij A B: Pi A B -> Graph A B";
12.675 by (afs [PiBij_def] 1);
12.676 -br restrictI 1;
12.677 +by (rtac restrictI 1);
12.678 by (strip 1);
12.679 by (afs [Graph_def] 1);
12.680 -br conjI 1;
12.681 -br subsetI 1;
12.682 +by (rtac conjI 1);
12.683 +by (rtac subsetI 1);
12.684 by (strip 2);
12.685 -br ex1I 2;
12.686 -br refl 2;
12.687 -ba 2;
12.688 +by (rtac ex1I 2);
12.689 +by (rtac refl 2);
12.690 +by (assume_tac 2);
12.691 by (split_all_tac 1);
12.692 by (afs [Pi_def] 1);
12.693 val PiBij_func = result();
12.694 @@ -611,25 +611,25 @@
12.695 goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B; \
12.696 \ {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\
12.697 \ ==> f x = g x";
12.698 -be equalityE 1;
12.699 -by (rewrite_goals_tac [subset_def]);
12.700 +by (etac equalityE 1);
12.701 +by (rewtac subset_def);
12.702 by (dres_inst_tac [("x","(x, f x)")] bspec 1);
12.703 by (Fast_tac 1);
12.704 by (Fast_tac 1);
12.705 val set_eq_lemma = result();
12.706
12.707 goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
12.708 -br inj_onI 1;
12.709 -br Pi_extensionality 1;
12.710 -ba 1;
12.711 -ba 1;
12.712 +by (rtac inj_onI 1);
12.713 +by (rtac Pi_extensionality 1);
12.714 +by (assume_tac 1);
12.715 +by (assume_tac 1);
12.716 by (strip 1);
12.717 by (afs [PiBij_def,restrictE1] 1);
12.718 by (re_tac set_eq_lemma 2 1);
12.719 -ba 1;
12.720 -ba 2;
12.721 +by (assume_tac 1);
12.722 +by (assume_tac 2);
12.723 by (afs [restrictE1] 1);
12.724 -be subst 1;
12.725 +by (etac subst 1);
12.726 by (afs [restrictE1] 1);
12.727 val inj_PiBij = result();
12.728
12.729 @@ -638,85 +638,85 @@
12.730 val Ex1_Ex = result();
12.731
12.732 goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
12.733 -br equalityI 1;
12.734 +by (rtac equalityI 1);
12.735 by (afs [image_def] 1);
12.736 -br subsetI 1;
12.737 +by (rtac subsetI 1);
12.738 by (Asm_full_simp_tac 1);
12.739 -be bexE 1;
12.740 -be ssubst 1;
12.741 +by (etac bexE 1);
12.742 +by (etac ssubst 1);
12.743 by (afs [PiBij_in_Graph] 1);
12.744 -br subsetI 1;
12.745 +by (rtac subsetI 1);
12.746 by (afs [image_def] 1);
12.747 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
12.748 -br restrictI_Pi 2;
12.749 +by (rtac restrictI_Pi 2);
12.750 by (strip 2);
12.751 -br ex1E 2;
12.752 +by (rtac ex1E 2);
12.753 by (afs [Graph_def] 2);
12.754 -be conjE 2;
12.755 -bd bspec 2;
12.756 -ba 2;
12.757 -ba 2;
12.758 -br (select_equality RS ssubst) 2;
12.759 -ba 2;
12.760 +by (etac conjE 2);
12.761 +by (dtac bspec 2);
12.762 +by (assume_tac 2);
12.763 +by (assume_tac 2);
12.764 +by (stac select_equality 2);
12.765 +by (assume_tac 2);
12.766 by (Blast_tac 2);
12.767 (* gets hung up on by (afs [Graph_def] 2); *)
12.768 -by (SELECT_GOAL (rewrite_goals_tac [Graph_def]) 2);
12.769 +by (SELECT_GOAL (rewtac Graph_def) 2);
12.770 by (Blast_tac 2);
12.771 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
12.772 by (afs [PiBij_def,Graph_def] 1);
12.773 -br (restrictE1 RS ssubst) 1;
12.774 -br restrictI_Pi 1;
12.775 +by (stac restrictE1 1);
12.776 +by (rtac restrictI_Pi 1);
12.777 (* again like the old 2. subgoal *)
12.778 by (strip 1);
12.779 -br ex1E 1;
12.780 -be conjE 1;
12.781 -bd bspec 1;
12.782 -ba 1;
12.783 -ba 1;
12.784 -br (select_equality RS ssubst) 1;
12.785 -ba 1;
12.786 +by (rtac ex1E 1);
12.787 +by (etac conjE 1);
12.788 +by (dtac bspec 1);
12.789 +by (assume_tac 1);
12.790 +by (assume_tac 1);
12.791 +by (stac select_equality 1);
12.792 +by (assume_tac 1);
12.793 by (Blast_tac 1);
12.794 by (Blast_tac 1);
12.795 (* *)
12.796 -br equalityI 1;
12.797 -br subsetI 1;
12.798 -br CollectI 1;
12.799 +by (rtac equalityI 1);
12.800 +by (rtac subsetI 1);
12.801 +by (rtac CollectI 1);
12.802 by (split_all_tac 1);
12.803 by (Simp_tac 1);
12.804 -br conjI 1;
12.805 +by (rtac conjI 1);
12.806 by (Blast_tac 1);
12.807 -be conjE 1;
12.808 -bd subsetD 1;
12.809 -ba 1;
12.810 -bd SigmaD1 1;
12.811 -bd bspec 1;
12.812 -ba 1;
12.813 -br (restrictE1 RS ssubst) 1;
12.814 -ba 1;
12.815 -br sym 1;
12.816 -br select_equality 1;
12.817 -ba 1;
12.818 +by (etac conjE 1);
12.819 +by (dtac subsetD 1);
12.820 +by (assume_tac 1);
12.821 +by (dtac SigmaD1 1);
12.822 +by (dtac bspec 1);
12.823 +by (assume_tac 1);
12.824 +by (stac restrictE1 1);
12.825 +by (assume_tac 1);
12.826 +by (rtac sym 1);
12.827 +by (rtac select_equality 1);
12.828 +by (assume_tac 1);
12.829 by (Blast_tac 1);
12.830 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *)
12.831 -br subsetI 1;
12.832 +by (rtac subsetI 1);
12.833 by (Asm_full_simp_tac 1);
12.834 by (split_all_tac 1);
12.835 by (Asm_full_simp_tac 1);
12.836 -be conjE 1;
12.837 -be conjE 1;
12.838 +by (etac conjE 1);
12.839 +by (etac conjE 1);
12.840 by (afs [restrictE1] 1);
12.841 -bd bspec 1;
12.842 -ba 1;
12.843 -bd Ex1_Ex 1;
12.844 -by (rewrite_goals_tac [Ex_def]);
12.845 -ba 1;
12.846 +by (dtac bspec 1);
12.847 +by (assume_tac 1);
12.848 +by (dtac Ex1_Ex 1);
12.849 +by (rewtac Ex_def);
12.850 +by (assume_tac 1);
12.851 val surj_PiBij = result();
12.852
12.853
12.854 goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \
12.855 \ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
12.856 -br (Inv_f_f RS bspec) 1;
12.857 -ba 4;
12.858 +by (rtac (Inv_f_f RS bspec) 1);
12.859 +by (assume_tac 4);
12.860 by (afs [PiBij_func] 1);
12.861 by (afs [inj_PiBij] 1);
12.862 by (afs [surj_PiBij] 1);
12.863 @@ -724,29 +724,29 @@
12.864
12.865 goal PiSets.thy "!! A B. [| f: Graph A B |] ==> \
12.866 \ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
12.867 -br (PiBij_func RS (f_Inv_f RS bspec)) 1;
12.868 +by (rtac (PiBij_func RS (f_Inv_f RS bspec)) 1);
12.869 by (afs [surj_PiBij] 1);
12.870 -ba 1;
12.871 +by (assume_tac 1);
12.872 val PiBij_bij2 = result();
12.873
12.874 goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f";
12.875 -br injI 1;
12.876 +by (rtac injI 1);
12.877 by (dres_inst_tac [("f","g")] arg_cong 1);
12.878 by (forw_inst_tac [("x","x")] spec 1);
12.879 by (rotate_tac 2 1);
12.880 -be subst 1;
12.881 +by (etac subst 1);
12.882 by (forw_inst_tac [("x","y")] spec 1);
12.883 by (rotate_tac 2 1);
12.884 -be subst 1;
12.885 -ba 1;
12.886 +by (etac subst 1);
12.887 +by (assume_tac 1);
12.888 val inj_lemma = result();
12.889
12.890 goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g";
12.891 by (afs [surj_def] 1);
12.892 -br allI 1;
12.893 +by (rtac allI 1);
12.894 by (res_inst_tac [("x","f y")] exI 1);
12.895 -bd spec 1;
12.896 -be sym 1;
12.897 +by (dtac spec 1);
12.898 +by (etac sym 1);
12.899 val surj_lemma = result();
12.900
12.901 goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}";
12.902 @@ -763,11 +763,11 @@
12.903
12.904
12.905 goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C";
12.906 -br subsetI 1;
12.907 -br Pi_I 1;
12.908 +by (rtac subsetI 1);
12.909 +by (rtac Pi_I 1);
12.910 by (afs [Pi_def] 2);
12.911 -bd bspec 1;
12.912 -ba 1;
12.913 -be subsetD 1;
12.914 +by (dtac bspec 1);
12.915 +by (assume_tac 1);
12.916 +by (etac subsetD 1);
12.917 by (afs [PiE1] 1);
12.918 val Pi_subset1 = result();