tidied
authorpaulson
Thu Sep 30 15:43:50 2004 +0200 (2004-09-30)
changeset 15219fb4b5c2cca8b
parent 15218 39747a9e3c37
child 15220 cc88c8ee4d2f
tidied
src/HOL/Hyperreal/Integration.thy
     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Thu Sep 30 07:14:34 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Thu Sep 30 15:43:50 2004 +0200
     1.3 @@ -114,10 +114,8 @@
     1.4  
     1.5  lemma partition_le: "partition(a,b) D ==> a \<le> b"
     1.6  apply (frule partition [THEN iffD1], safe)
     1.7 -apply (rotate_tac 2)
     1.8 -apply (drule_tac x = "psize D" in spec, safe)
     1.9 -apply (rule ccontr)
    1.10 -apply (case_tac "psize D = 0", safe)
    1.11 +apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
    1.12 +apply (case_tac "psize D = 0")
    1.13  apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
    1.14  done
    1.15  
    1.16 @@ -130,7 +128,7 @@
    1.17  apply (drule_tac x = "psize D" in spec)
    1.18  apply (rule ccontr)
    1.19  apply (drule_tac n = "psize D - 1" in partition_lt)
    1.20 -prefer 3 apply (blast, auto)
    1.21 +apply auto
    1.22  done
    1.23  
    1.24  lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
    1.25 @@ -194,7 +192,6 @@
    1.26               (if n < psize D1 then D1 n else D2 (n - psize D1)) =
    1.27               (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
    1.28                else D2 (psize D1 + psize D2 - psize D1)))"
    1.29 -apply safe
    1.30  apply (auto intro: partition_lt_gen)
    1.31  apply (subgoal_tac "psize D1 = Suc n")
    1.32  apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt)
    1.33 @@ -206,37 +203,37 @@
    1.34       "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
    1.35        ==> D1(N) < D2 (psize D2)"
    1.36  apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans)
    1.37 -apply (erule partition_gt, assumption)
    1.38 +apply (erule partition_gt)
    1.39  apply (auto simp add: partition_rhs partition_le)
    1.40  done
    1.41  
    1.42  lemma lemma_partition_append2:
    1.43       "[| partition (a, b) D1; partition (b, c) D2 |]
    1.44        ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
    1.45 -          psize D1 + psize D2"
    1.46 -apply (rule_tac D2 = "%n. if n < psize D1 then D1 n else D2 (n - psize D1) "
    1.47 -       in psize_def [THEN meta_eq_to_obj_eq, THEN ssubst])
    1.48 +          psize D1 + psize D2" 
    1.49 +apply (unfold psize_def 
    1.50 +         [of "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"])
    1.51  apply (rule some1_equality)
    1.52 -prefer 2 apply (blast intro!: lemma_partition_append1)
    1.53 -apply (rule ex1I, rule lemma_partition_append1, auto)
    1.54 -apply (rule ccontr)
    1.55 -apply (simp add: linorder_neq_iff, safe)
    1.56 -apply (rotate_tac 3)
    1.57 -apply (drule_tac x = "psize D1 + psize D2" in spec, auto)
    1.58 -apply (case_tac "N < psize D1")
    1.59 -apply (auto dest: lemma_psize1)
    1.60 -apply (subgoal_tac "N - psize D1 < psize D2")
    1.61 + prefer 2 apply (blast intro!: lemma_partition_append1)
    1.62 +apply (rule ex1I, rule lemma_partition_append1) 
    1.63 +apply (simp_all split: split_if_asm)
    1.64 + txt{*The case @{term "N < psize D1"}*} 
    1.65 + apply (drule_tac x = "psize D1 + psize D2" and P="%n. ?P n & ?Q n" in spec) 
    1.66 + apply (force dest: lemma_psize1)
    1.67 +apply (rule order_antisym);
    1.68 + txt{*The case @{term "psize D1 \<le> N"}: 
    1.69 +       proving @{term "N \<le> psize D1 + psize D2"}*}
    1.70 + apply (drule_tac x = "psize D1 + psize D2" in spec)
    1.71 + apply (simp add: partition_rhs2)
    1.72 +apply (case_tac "N - psize D1 < psize D2") 
    1.73   prefer 2 apply arith
    1.74 -apply (drule_tac a = b and b = c in partition_gt, auto)
    1.75 -apply (drule_tac x = "psize D1 + psize D2" in spec)
    1.76 -apply (auto simp add: partition_rhs2)
    1.77 + txt{*Proving @{term "psize D1 + psize D2 \<le> N"}*}
    1.78 +apply (drule_tac x = "psize D1 + psize D2" and P="%n. N\<le>n --> ?P n" in spec, simp)
    1.79 +apply (drule_tac a = b and b = c in partition_gt, assumption, simp)
    1.80  done
    1.81  
    1.82 -lemma tpart_eq_lhs_rhs:
    1.83 -"[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
    1.84 -apply (simp add: tpart_def)
    1.85 -apply (auto simp add: partition_eq)
    1.86 -done
    1.87 +lemma tpart_eq_lhs_rhs: "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
    1.88 +by (auto simp add: tpart_def partition_eq)
    1.89  
    1.90  lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D"
    1.91  by (simp add: tpart_def)
    1.92 @@ -275,7 +272,7 @@
    1.93  apply (auto simp add: partition_lhs partition_rhs)
    1.94  done
    1.95  
    1.96 -text{*We can always find a division which is fine wrt any gauge*}
    1.97 +text{*We can always find a division that is fine wrt any gauge*}
    1.98  
    1.99  lemma partition_exists:
   1.100       "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |]
   1.101 @@ -284,7 +281,7 @@
   1.102                     (\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))" 
   1.103         in lemma_BOLZANO2)
   1.104  apply safe
   1.105 -apply (blast intro: real_le_trans)+
   1.106 +apply (blast intro: order_trans)+
   1.107  apply (auto intro: partition_append)
   1.108  apply (case_tac "a \<le> x & x \<le> b")
   1.109  apply (rule_tac [2] x = 1 in exI, auto)
   1.110 @@ -339,15 +336,13 @@
   1.111  by (induct_tac "m", auto)
   1.112  
   1.113  lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
   1.114 -apply (drule real_le_imp_less_or_eq, auto)
   1.115 -apply (auto simp add: rsum_def Integral_def)
   1.116 +apply (auto simp add: order_le_less rsum_def Integral_def)
   1.117  apply (rule_tac x = "%x. b - a" in exI)
   1.118  apply (auto simp add: gauge_def abs_interval_iff tpart_def partition)
   1.119  done
   1.120  
   1.121  lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
   1.122 -apply (drule real_le_imp_less_or_eq, auto)
   1.123 -apply (auto simp add: rsum_def Integral_def)
   1.124 +apply (auto simp add: order_le_less rsum_def Integral_def)
   1.125  apply (rule_tac x = "%x. b - a" in exI)
   1.126  apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff 
   1.127                 right_diff_distrib [symmetric] partition tpart_def)
   1.128 @@ -355,9 +350,8 @@
   1.129  
   1.130  lemma Integral_mult:
   1.131       "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
   1.132 -apply (drule real_le_imp_less_or_eq)
   1.133 -apply (auto dest: Integral_unique [OF real_le_refl Integral_zero])
   1.134 -apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] real_mult_assoc)
   1.135 +apply (auto simp add: order_le_less dest: Integral_unique [OF real_le_refl Integral_zero])
   1.136 +apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] mult_assoc)
   1.137  apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
   1.138   prefer 2 apply force
   1.139  apply (drule_tac x = "e/abs c" in spec, auto)
   1.140 @@ -428,19 +422,17 @@
   1.141  apply (frule strad1, assumption+)
   1.142  apply (rule_tac x = s in exI, auto)
   1.143  apply (rule_tac x = u and y = v in linorder_cases, auto)
   1.144 -apply (rule_tac j = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> + 
   1.145 +apply (rule_tac y = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> + 
   1.146                       \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
   1.147 -       in real_le_trans)
   1.148 -apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
   1.149 +       in order_trans)
   1.150 +apply (rule abs_triangle_ineq [THEN [2] order_trans])
   1.151  apply (simp add: right_diff_distrib, arith)
   1.152  apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
   1.153  apply (rule add_mono)
   1.154 -apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar>" in real_le_trans)
   1.155 - prefer 2 apply simp apply arith
   1.156 -apply (erule_tac [!]
   1.157 -       V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
   1.158 -        in thin_rl)
   1.159 -apply (drule_tac x = v in spec, auto, arith)
   1.160 +apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
   1.161 + prefer 2 apply (simp, arith)
   1.162 +apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
   1.163 +apply (drule_tac x = v in spec, simp, arith)
   1.164  apply (drule_tac x = u in spec, auto, arith)
   1.165  apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
   1.166  apply (rule order_trans)
   1.167 @@ -449,8 +441,8 @@
   1.168  done
   1.169  
   1.170  lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
   1.171 -      ==> Integral(a,b) f' (f(b) - f(a))"
   1.172 -apply (drule real_le_imp_less_or_eq, auto)
   1.173 +             ==> Integral(a,b) f' (f(b) - f(a))"
   1.174 +apply (drule order_le_imp_less_or_eq, auto) 
   1.175  apply (auto simp add: Integral_def)
   1.176  apply (rule ccontr)
   1.177  apply (subgoal_tac "\<forall>e. 0 < e --> (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e))")
   1.178 @@ -469,7 +461,7 @@
   1.179   apply (simp add: partition_lhs partition_rhs)
   1.180  apply (drule sym, simp)
   1.181  apply (simp (no_asm) add: sumr_diff)
   1.182 -apply (rule sumr_rabs [THEN real_le_trans])
   1.183 +apply (rule sumr_rabs [THEN order_trans])
   1.184  apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
   1.185  apply (simp add: abs_minus_commute)
   1.186  apply (rule_tac t = ea in ssubst, assumption)
   1.187 @@ -498,9 +490,7 @@
   1.188  lemma partition_psize_Least:
   1.189       "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)"
   1.190  apply (auto intro!: Least_equality [symmetric] partition_rhs)
   1.191 -apply (rule ccontr)
   1.192 -apply (drule partition_ub_lt)
   1.193 -apply (auto simp add: linorder_not_less [symmetric])
   1.194 +apply (auto dest: partition_ub_lt simp add: linorder_not_less [symmetric])
   1.195  done
   1.196  
   1.197  lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))"
   1.198 @@ -563,7 +553,7 @@
   1.199  
   1.200  lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
   1.201  apply (cut_tac m = n and n = "psize D" in less_linear, auto)
   1.202 -apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   1.203 +apply (cut_tac m = m and n = n in less_linear)
   1.204  apply (cut_tac m = m and n = "psize D" in less_linear)
   1.205  apply (auto dest: partition_gt)
   1.206  apply (drule_tac n = m in partition_lt_gen, auto)
   1.207 @@ -584,12 +574,12 @@
   1.208  apply (assumption, assumption)
   1.209  apply (rule some_equality)
   1.210  apply (auto intro: partition_lt_Suc)
   1.211 -apply (drule_tac n = n in partition_lt_gen)
   1.212 -apply (assumption, arith, arith)
   1.213 +apply (drule_tac n = n in partition_lt_gen, assumption)
   1.214 +apply (arith, arith)
   1.215  apply (cut_tac m = na and n = "psize D" in less_linear)
   1.216  apply (auto dest: partition_lt_cancel)
   1.217  apply (rule_tac x=N and y=n in linorder_cases)
   1.218 -apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, auto)
   1.219 +apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
   1.220  apply (drule_tac n = n in partition_lt_gen, auto, arith)
   1.221  apply (drule_tac x = n in spec)
   1.222  apply (simp split: split_if_asm)
   1.223 @@ -599,11 +589,11 @@
   1.224       "partition (a, b) D
   1.225        ==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D"
   1.226  apply (frule_tac r = n in partition_ub)
   1.227 -apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
   1.228 +apply (drule_tac x = "D n" in order_le_imp_less_or_eq)
   1.229  apply (auto simp add: lemma_partition_eq [symmetric])
   1.230  apply (frule_tac r = n in partition_lb)
   1.231 -apply (drule lemma_additivity4_psize_eq)
   1.232 -apply (rule_tac [3] ccontr, auto)
   1.233 +apply (drule (2) lemma_additivity4_psize_eq)  
   1.234 +apply (rule ccontr, auto)
   1.235  apply (frule_tac not_leE [THEN [2] partition_eq_bound])
   1.236  apply (auto simp add: partition_rhs)
   1.237  done
   1.238 @@ -611,8 +601,7 @@
   1.239  lemma lemma_psize_left_less_psize2:
   1.240       "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |]
   1.241        ==> na < psize D"
   1.242 -apply (erule_tac lemma_psize_left_less_psize [THEN [2] less_le_trans], assumption)
   1.243 -done
   1.244 +by (erule lemma_psize_left_less_psize [THEN [2] less_le_trans])
   1.245  
   1.246  
   1.247  lemma lemma_additivity3:
   1.248 @@ -627,7 +616,7 @@
   1.249  done
   1.250  
   1.251  lemma psize_const [simp]: "psize (%x. k) = 0"
   1.252 -by (simp add: psize_def, auto)
   1.253 +by (auto simp add: psize_def)
   1.254  
   1.255  lemma lemma_additivity3a:
   1.256       "[| partition(a,b) D; D na < D n; D n < D (Suc na);
   1.257 @@ -642,11 +631,7 @@
   1.258  apply (simp add: psize_def [of "(%x. D (x + n))"]);
   1.259  apply (rule_tac a = "psize D - n" in someI2, auto)
   1.260    apply (simp add: partition less_diff_conv)
   1.261 - apply (simp add: le_diff_conv)
   1.262 - apply (case_tac "psize D \<le> n")
   1.263 -  apply (simp add: partition_rhs2)
   1.264 - apply (simp add: partition linorder_not_le)
   1.265 -apply (rule ccontr, drule not_leE)
   1.266 + apply (simp add: le_diff_conv partition_rhs2 split: nat_diff_split)
   1.267  apply (drule_tac x = "psize D - n" in spec, auto)
   1.268  apply (frule partition_rhs, safe)
   1.269  apply (frule partition_lt_cancel, assumption)
   1.270 @@ -655,10 +640,10 @@
   1.271   apply blast
   1.272  apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)"
   1.273         in spec)
   1.274 -apply (simp (no_asm_simp))
   1.275 +apply simp
   1.276  done
   1.277  
   1.278 -lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n"
   1.279 +lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n" 
   1.280  apply (rule ccontr, drule not_leE)
   1.281  apply (frule partition_lt_Suc, assumption)
   1.282  apply (frule_tac r = "Suc n" in partition_ub, auto)
   1.283 @@ -677,25 +662,24 @@
   1.284  apply (frule psize_le_n)
   1.285  apply (drule_tac x = "psize D - n" in spec, simp)
   1.286  apply (drule partition [THEN iffD1], safe)
   1.287 -apply (drule_tac x = "Suc n" and P="%na. psize D \<le> na \<longrightarrow> D na = D n" in spec, auto)
   1.288 +apply (drule_tac x = "Suc n" and P="%na. ?s \<le> na \<longrightarrow> D na = D n" in spec, auto)
   1.289  done
   1.290  
   1.291  lemma better_lemma_psize_right_eq:
   1.292       "partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n"
   1.293 -apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
   1.294 +apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq])
   1.295  apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1)
   1.296  done
   1.297  
   1.298  lemma lemma_psize_right_eq1:
   1.299       "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D"
   1.300 -apply (simp add: psize_def [of "(%x. D (x + n))"]);
   1.301 +apply (simp add: psize_def [of "(%x. D (x + n))"])
   1.302  apply (rule_tac a = "psize D - n" in someI2, auto)
   1.303    apply (simp add: partition less_diff_conv)
   1.304   apply (subgoal_tac "n \<le> psize D")
   1.305    apply (simp add: partition le_diff_conv)
   1.306   apply (rule ccontr, drule not_leE)
   1.307 - apply (drule_tac less_imp_le [THEN [2] partition_rhs2], auto)
   1.308 -apply (rule ccontr, drule not_leE)
   1.309 + apply (drule_tac less_imp_le [THEN [2] partition_rhs2], assumption, simp)
   1.310  apply (drule_tac x = "psize D" in spec)
   1.311  apply (simp add: partition)
   1.312  done
   1.313 @@ -716,7 +700,7 @@
   1.314  
   1.315  lemma lemma_psize_right_eq:
   1.316       "[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D"
   1.317 -apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
   1.318 +apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq])
   1.319  apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1)
   1.320  done
   1.321  
   1.322 @@ -725,21 +709,18 @@
   1.323        ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n,
   1.324            %x. if D x < D n then p(x) else D n)"
   1.325  apply (frule_tac r = n in tpart_partition [THEN partition_ub])
   1.326 -apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
   1.327 +apply (drule_tac x = "D n" in order_le_imp_less_or_eq)
   1.328  apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric])
   1.329  apply (frule_tac tpart_partition [THEN [3] lemma_additivity1])
   1.330  apply (auto simp add: tpart_def)
   1.331 -apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq], auto)
   1.332 -  prefer 3
   1.333 -  apply (drule linorder_not_less [THEN iffD1])
   1.334 -  apply (drule_tac x=na in spec, arith)
   1.335 +apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN order_le_imp_less_or_eq], auto)
   1.336 +  prefer 3 apply (drule_tac x=na in spec, arith)
   1.337   prefer 2 apply (blast dest: lemma_additivity3)
   1.338 -apply (frule lemma_additivity4_psize_eq)
   1.339 -apply (assumption+)
   1.340 +apply (frule (2) lemma_additivity4_psize_eq)
   1.341  apply (rule partition [THEN iffD2])
   1.342  apply (frule partition [THEN iffD1])
   1.343 -apply (auto intro: partition_lt_gen)
   1.344 - apply (drule (1) partition_lt_cancel, arith)
   1.345 +apply safe 
   1.346 +apply (auto simp add: partition_lt_gen)  
   1.347  apply (drule (1) partition_lt_cancel, arith)
   1.348  done
   1.349  
   1.350 @@ -780,7 +761,7 @@
   1.351  apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
   1.352  apply (simp add: tpart_def, safe)
   1.353  apply (subgoal_tac "D n \<le> p (na + n)")
   1.354 -apply (drule_tac y = "p (na + n)" in real_le_imp_less_or_eq)
   1.355 +apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
   1.356  apply safe
   1.357  apply (simp split: split_if_asm, simp)
   1.358  apply (drule less_le_trans, assumption)
   1.359 @@ -898,17 +879,14 @@
   1.360  lemma partition_exists2:
   1.361       "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |]
   1.362        ==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"
   1.363 -apply safe
   1.364 -apply (rule partition_exists, auto)
   1.365 -done
   1.366 +by (blast dest: partition_exists) 
   1.367  
   1.368  lemma monotonic_anti_derivative:
   1.369       "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
   1.370           \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
   1.371        ==> f b - f a \<le> g b - g a"
   1.372  apply (rule Integral_le, assumption)
   1.373 -apply (rule_tac [2] FTC1)
   1.374 -apply (rule_tac [4] FTC1, auto)
   1.375 +apply (auto intro: FTC1) 
   1.376  done
   1.377  
   1.378  end