tuned document (headers, sections, spacing);
authorwenzelm
Fri Apr 13 21:26:35 2007 +0200 (2007-04-13)
changeset 22665cf152ff55d16
parent 22664 e965391e2864
child 22666 2d4d02efd9d9
tuned document (headers, sections, spacing);
src/HOL/Library/BigO.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Eval.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/Kleene_Algebras.thy
src/HOL/Library/Library/document/root.tex
src/HOL/Library/MLString.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Pure_term.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/SCT_Definition.thy
src/HOL/Library/SCT_Examples.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/Library/SCT_Interpretation.thy
src/HOL/Library/SCT_Misc.thy
src/HOL/Library/SCT_Theorem.thy
src/HOL/Library/Size_Change_Termination.thy
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 13 21:26:34 2007 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Apr 13 21:26:35 2007 +0200
     1.3 @@ -59,11 +59,11 @@
     1.4    apply (rule mult_right_mono)
     1.5    apply (rule abs_ge_self)
     1.6    apply (rule abs_ge_zero)
     1.7 -done
     1.8 +  done
     1.9  
    1.10  lemma bigo_alt_def: "O(f) = 
    1.11      {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
    1.12 -by (auto simp add: bigo_def bigo_pos_const)
    1.13 +  by (auto simp add: bigo_def bigo_pos_const)
    1.14  
    1.15  lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
    1.16    apply (auto simp add: bigo_alt_def)
    1.17 @@ -78,25 +78,25 @@
    1.18    apply (simp add: mult_ac)
    1.19    apply (rule mult_left_mono, assumption)
    1.20    apply (rule order_less_imp_le, assumption)
    1.21 -done
    1.22 +  done
    1.23  
    1.24  lemma bigo_refl [intro]: "f : O(f)"
    1.25    apply(auto simp add: bigo_def)
    1.26    apply(rule_tac x = 1 in exI)
    1.27    apply simp
    1.28 -done
    1.29 +  done
    1.30  
    1.31  lemma bigo_zero: "0 : O(g)"
    1.32    apply (auto simp add: bigo_def func_zero)
    1.33    apply (rule_tac x = 0 in exI)
    1.34    apply auto
    1.35 -done
    1.36 +  done
    1.37  
    1.38  lemma bigo_zero2: "O(%x.0) = {%x.0}"
    1.39    apply (auto simp add: bigo_def) 
    1.40    apply (rule ext)
    1.41    apply auto
    1.42 -done
    1.43 +  done
    1.44  
    1.45  lemma bigo_plus_self_subset [intro]: 
    1.46    "O(f) + O(f) <= O(f)"
    1.47 @@ -116,7 +116,7 @@
    1.48    apply (rule bigo_plus_self_subset)
    1.49    apply (rule set_zero_plus2) 
    1.50    apply (rule bigo_zero)
    1.51 -done
    1.52 +  done
    1.53  
    1.54  lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
    1.55    apply (rule subsetI)
    1.56 @@ -168,17 +168,17 @@
    1.57    apply simp
    1.58    apply (rule ext)
    1.59    apply (auto simp add: if_splits linorder_not_le)
    1.60 -done
    1.61 +  done
    1.62  
    1.63  lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
    1.64    apply (subgoal_tac "A + B <= O(f) + O(f)")
    1.65    apply (erule order_trans)
    1.66    apply simp
    1.67    apply (auto del: subsetI simp del: bigo_plus_idemp)
    1.68 -done
    1.69 +  done
    1.70  
    1.71  lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
    1.72 -  O(f + g) = O(f) + O(g)"
    1.73 +    O(f + g) = O(f) + O(g)"
    1.74    apply (rule equalityI)
    1.75    apply (rule bigo_plus_subset)
    1.76    apply (simp add: bigo_alt_def set_plus func_plus)
    1.77 @@ -211,7 +211,7 @@
    1.78    apply (rule abs_triangle_ineq)
    1.79    apply (rule add_nonneg_nonneg)
    1.80    apply assumption+
    1.81 -done
    1.82 +  done
    1.83  
    1.84  lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
    1.85      f : O(g)" 
    1.86 @@ -220,13 +220,13 @@
    1.87    apply auto
    1.88    apply (drule_tac x = x in spec)+
    1.89    apply (simp add: abs_mult [symmetric])
    1.90 -done
    1.91 +  done
    1.92  
    1.93  lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
    1.94      f : O(g)" 
    1.95    apply (erule bigo_bounded_alt [of f 1 g])
    1.96    apply simp
    1.97 -done
    1.98 +  done
    1.99  
   1.100  lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
   1.101      f : lb +o O(g)"
   1.102 @@ -237,21 +237,21 @@
   1.103    apply force
   1.104    apply (drule_tac x = x in spec)+
   1.105    apply force
   1.106 -done
   1.107 +  done
   1.108  
   1.109  lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
   1.110    apply (unfold bigo_def)
   1.111    apply auto
   1.112    apply (rule_tac x = 1 in exI)
   1.113    apply auto
   1.114 -done
   1.115 +  done
   1.116  
   1.117  lemma bigo_abs2: "f =o O(%x. abs(f x))"
   1.118    apply (unfold bigo_def)
   1.119    apply auto
   1.120    apply (rule_tac x = 1 in exI)
   1.121    apply auto
   1.122 -done
   1.123 +  done
   1.124  
   1.125  lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
   1.126    apply (rule equalityI)
   1.127 @@ -259,7 +259,7 @@
   1.128    apply (rule bigo_abs2)
   1.129    apply (rule bigo_elt_subset)
   1.130    apply (rule bigo_abs)
   1.131 -done
   1.132 +  done
   1.133  
   1.134  lemma bigo_abs4: "f =o g +o O(h) ==> 
   1.135      (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
   1.136 @@ -288,7 +288,7 @@
   1.137  qed
   1.138  
   1.139  lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
   1.140 -by (unfold bigo_def, auto)
   1.141 +  by (unfold bigo_def, auto)
   1.142  
   1.143  lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
   1.144  proof -
   1.145 @@ -326,7 +326,7 @@
   1.146    apply (rule mult_nonneg_nonneg)
   1.147    apply auto
   1.148    apply (simp add: mult_ac abs_mult)
   1.149 -done
   1.150 +  done
   1.151  
   1.152  lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
   1.153    apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
   1.154 @@ -337,20 +337,20 @@
   1.155    apply (force simp add: mult_ac)
   1.156    apply (rule mult_left_mono, assumption)
   1.157    apply (rule abs_ge_zero)
   1.158 -done
   1.159 +  done
   1.160  
   1.161  lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
   1.162    apply (rule subsetD)
   1.163    apply (rule bigo_mult)
   1.164    apply (erule set_times_intro, assumption)
   1.165 -done
   1.166 +  done
   1.167  
   1.168  lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
   1.169    apply (drule set_plus_imp_minus)
   1.170    apply (rule set_minus_imp_plus)
   1.171    apply (drule bigo_mult3 [where g = g and j = g])
   1.172    apply (auto simp add: ring_eq_simps mult_ac)
   1.173 -done
   1.174 +  done
   1.175  
   1.176  lemma bigo_mult5: "ALL x. f x ~= 0 ==>
   1.177      O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
   1.178 @@ -386,7 +386,7 @@
   1.179    apply (rule equalityI)
   1.180    apply (erule bigo_mult5)
   1.181    apply (rule bigo_mult2)
   1.182 -done
   1.183 +  done
   1.184  
   1.185  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   1.186      O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
   1.187 @@ -394,14 +394,14 @@
   1.188    apply assumption
   1.189    apply (rule set_times_mono3)
   1.190    apply (rule bigo_refl)
   1.191 -done
   1.192 +  done
   1.193  
   1.194  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   1.195      O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
   1.196    apply (rule equalityI)
   1.197    apply (erule bigo_mult7)
   1.198    apply (rule bigo_mult)
   1.199 -done
   1.200 +  done
   1.201  
   1.202  lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   1.203    by (auto simp add: bigo_def func_minus)
   1.204 @@ -411,7 +411,7 @@
   1.205    apply (drule set_plus_imp_minus)
   1.206    apply (drule bigo_minus)
   1.207    apply (simp add: diff_minus)
   1.208 -done
   1.209 +  done
   1.210  
   1.211  lemma bigo_minus3: "O(-f) = O(f)"
   1.212    by (auto simp add: bigo_def func_minus abs_minus_cancel)
   1.213 @@ -452,12 +452,12 @@
   1.214    apply (rule equalityI)
   1.215    apply (erule bigo_plus_absorb_lemma1)
   1.216    apply (erule bigo_plus_absorb_lemma2)
   1.217 -done
   1.218 +  done
   1.219  
   1.220  lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
   1.221    apply (subgoal_tac "f +o A <= f +o O(g)")
   1.222    apply force+
   1.223 -done
   1.224 +  done
   1.225  
   1.226  lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
   1.227    apply (subst set_minus_plus [symmetric])
   1.228 @@ -467,56 +467,56 @@
   1.229    apply (subst set_minus_plus)
   1.230    apply assumption
   1.231    apply  (simp add: diff_minus add_ac)
   1.232 -done
   1.233 +  done
   1.234  
   1.235  lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
   1.236    apply (rule iffI)
   1.237    apply (erule bigo_add_commute_imp)+
   1.238 -done
   1.239 +  done
   1.240  
   1.241  lemma bigo_const1: "(%x. c) : O(%x. 1)"
   1.242 -by (auto simp add: bigo_def mult_ac)
   1.243 +  by (auto simp add: bigo_def mult_ac)
   1.244  
   1.245  lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"
   1.246    apply (rule bigo_elt_subset)
   1.247    apply (rule bigo_const1)
   1.248 -done
   1.249 +  done
   1.250  
   1.251  lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   1.252    apply (simp add: bigo_def)
   1.253    apply (rule_tac x = "abs(inverse c)" in exI)
   1.254    apply (simp add: abs_mult [symmetric])
   1.255 -done
   1.256 +  done
   1.257  
   1.258  lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
   1.259 -by (rule bigo_elt_subset, rule bigo_const3, assumption)
   1.260 +  by (rule bigo_elt_subset, rule bigo_const3, assumption)
   1.261  
   1.262  lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.263      O(%x. c) = O(%x. 1)"
   1.264 -by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   1.265 +  by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   1.266  
   1.267  lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   1.268    apply (simp add: bigo_def)
   1.269    apply (rule_tac x = "abs(c)" in exI)
   1.270    apply (auto simp add: abs_mult [symmetric])
   1.271 -done
   1.272 +  done
   1.273  
   1.274  lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
   1.275 -by (rule bigo_elt_subset, rule bigo_const_mult1)
   1.276 +  by (rule bigo_elt_subset, rule bigo_const_mult1)
   1.277  
   1.278  lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
   1.279    apply (simp add: bigo_def)
   1.280    apply (rule_tac x = "abs(inverse c)" in exI)
   1.281    apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
   1.282 -done
   1.283 +  done
   1.284  
   1.285  lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> 
   1.286      O(f) <= O(%x. c * f x)"
   1.287 -by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   1.288 +  by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   1.289  
   1.290  lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.291      O(%x. c * f x) = O(f)"
   1.292 -by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   1.293 +  by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   1.294  
   1.295  lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.296      (%x. c) *o O(f) = O(f)"
   1.297 @@ -533,7 +533,7 @@
   1.298    apply (rule mult_left_mono)
   1.299    apply (erule spec)
   1.300    apply force
   1.301 -done
   1.302 +  done
   1.303  
   1.304  lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
   1.305    apply (auto intro!: subsetI
   1.306 @@ -547,7 +547,7 @@
   1.307    apply (erule spec)
   1.308    apply simp
   1.309    apply(simp add: mult_ac)
   1.310 -done
   1.311 +  done
   1.312  
   1.313  lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
   1.314  proof -
   1.315 @@ -571,6 +571,7 @@
   1.316    apply (erule bigo_compose1)
   1.317  done
   1.318  
   1.319 +
   1.320  subsection {* Setsum *}
   1.321  
   1.322  lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> 
   1.323 @@ -595,7 +596,7 @@
   1.324    apply (rule mult_right_mono) 
   1.325    apply (rule abs_ge_self)
   1.326    apply force
   1.327 -done
   1.328 +  done
   1.329  
   1.330  lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
   1.331      EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
   1.332 @@ -605,12 +606,12 @@
   1.333    apply clarsimp
   1.334    apply (rule_tac x = c in exI)
   1.335    apply force
   1.336 -done
   1.337 +  done
   1.338  
   1.339  lemma bigo_setsum2: "ALL y. 0 <= h y ==> 
   1.340      EX c. ALL y. abs(f y) <= c * (h y) ==>
   1.341        (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
   1.342 -by (rule bigo_setsum1, auto)  
   1.343 +  by (rule bigo_setsum1, auto)  
   1.344  
   1.345  lemma bigo_setsum3: "f =o O(h) ==>
   1.346      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.347 @@ -627,7 +628,7 @@
   1.348    apply (rule mult_left_mono)
   1.349    apply (erule spec)
   1.350    apply (rule abs_ge_zero)
   1.351 -done
   1.352 +  done
   1.353  
   1.354  lemma bigo_setsum4: "f =o g +o O(h) ==>
   1.355      (%x. SUM y : A x. l x y * f(k x y)) =o
   1.356 @@ -640,7 +641,7 @@
   1.357    apply (rule bigo_setsum3)
   1.358    apply (subst func_diff [symmetric])
   1.359    apply (erule set_plus_imp_minus)
   1.360 -done
   1.361 +  done
   1.362  
   1.363  lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
   1.364      ALL x. 0 <= h x ==>
   1.365 @@ -655,7 +656,7 @@
   1.366    apply (subst abs_of_nonneg)
   1.367    apply (rule mult_nonneg_nonneg)
   1.368    apply auto
   1.369 -done
   1.370 +  done
   1.371  
   1.372  lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
   1.373      ALL x. 0 <= h x ==>
   1.374 @@ -670,7 +671,8 @@
   1.375    apply (subst func_diff [symmetric])
   1.376    apply (drule set_plus_imp_minus)
   1.377    apply auto
   1.378 -done
   1.379 +  done
   1.380 +
   1.381  
   1.382  subsection {* Misc useful stuff *}
   1.383  
   1.384 @@ -679,13 +681,13 @@
   1.385    apply (subst bigo_plus_idemp [symmetric])
   1.386    apply (rule set_plus_mono2)
   1.387    apply assumption+
   1.388 -done
   1.389 +  done
   1.390  
   1.391  lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
   1.392    apply (subst bigo_plus_idemp [symmetric])
   1.393    apply (rule set_plus_intro)
   1.394    apply assumption+
   1.395 -done
   1.396 +  done
   1.397    
   1.398  lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> 
   1.399      (%x. c) * f =o O(h) ==> f =o O(h)"
   1.400 @@ -701,7 +703,7 @@
   1.401    apply (subst times_divide_eq_left [symmetric])
   1.402    apply (subst divide_self)
   1.403    apply (assumption, simp)
   1.404 -done
   1.405 +  done
   1.406  
   1.407  lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
   1.408      f =o O(h)"
   1.409 @@ -718,7 +720,7 @@
   1.410    apply (erule ssubst) back
   1.411    apply (erule spec)
   1.412    apply simp
   1.413 -done
   1.414 +  done
   1.415  
   1.416  lemma bigo_fix2: 
   1.417      "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> 
   1.418 @@ -730,7 +732,8 @@
   1.419    apply (rule set_plus_imp_minus)
   1.420    apply simp
   1.421    apply (simp add: func_diff)
   1.422 -done
   1.423 +  done
   1.424 +
   1.425  
   1.426  subsection {* Less than or equal to *}
   1.427  
   1.428 @@ -747,7 +750,7 @@
   1.429    apply (rule allI)
   1.430    apply (rule order_trans)
   1.431    apply (erule spec)+
   1.432 -done
   1.433 +  done
   1.434  
   1.435  lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
   1.436        g =o O(h)"
   1.437 @@ -757,15 +760,15 @@
   1.438    apply (rule order_trans)
   1.439    apply assumption
   1.440    apply (rule abs_ge_self)
   1.441 -done
   1.442 +  done
   1.443  
   1.444  lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
   1.445 -      g =o O(h)"
   1.446 +    g =o O(h)"
   1.447    apply (erule bigo_lesseq2)
   1.448    apply (rule allI)
   1.449    apply (subst abs_of_nonneg)
   1.450    apply (erule spec)+
   1.451 -done
   1.452 +  done
   1.453  
   1.454  lemma bigo_lesseq4: "f =o O(h) ==>
   1.455      ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
   1.456 @@ -774,7 +777,7 @@
   1.457    apply (rule allI)
   1.458    apply (subst abs_of_nonneg)
   1.459    apply (erule spec)+
   1.460 -done
   1.461 +  done
   1.462  
   1.463  lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   1.464    apply (unfold lesso_def)
   1.465 @@ -784,7 +787,7 @@
   1.466    apply (unfold func_zero)
   1.467    apply (rule ext)
   1.468    apply (simp split: split_max)
   1.469 -done
   1.470 +  done
   1.471  
   1.472  lemma bigo_lesso2: "f =o g +o O(h) ==>
   1.473      ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
   1.474 @@ -808,7 +811,7 @@
   1.475    prefer 2
   1.476    apply (rule abs_ge_zero)
   1.477    apply (simp add: compare_rls)
   1.478 -done
   1.479 +  done
   1.480  
   1.481  lemma bigo_lesso3: "f =o g +o O(h) ==>
   1.482      ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
   1.483 @@ -833,7 +836,7 @@
   1.484    prefer 2
   1.485    apply (rule abs_ge_zero)
   1.486    apply (simp add: compare_rls)
   1.487 -done
   1.488 +  done
   1.489  
   1.490  lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
   1.491      g =o h +o O(k) ==> f <o h =o O(k)"
   1.492 @@ -847,7 +850,7 @@
   1.493    apply (rule allI)
   1.494    apply (auto simp add: func_plus func_diff compare_rls 
   1.495      split: split_max abs_split)
   1.496 -done
   1.497 +  done
   1.498  
   1.499  lemma bigo_lesso5: "f <o g =o O(h) ==>
   1.500      EX C. ALL x. f x <= g x + C * abs(h x)"
   1.501 @@ -860,7 +863,7 @@
   1.502    apply (clarsimp simp add: compare_rls add_ac) 
   1.503    apply (rule abs_of_nonneg)
   1.504    apply (rule le_maxI2)
   1.505 -done
   1.506 +  done
   1.507  
   1.508  lemma lesso_add: "f <o g =o O(h) ==>
   1.509        k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"
   1.510 @@ -870,6 +873,6 @@
   1.511    apply assumption
   1.512    apply (force split: split_max)
   1.513    apply (auto split: split_max simp add: func_plus)
   1.514 -done
   1.515 +  done
   1.516  
   1.517  end
     2.1 --- a/src/HOL/Library/Commutative_Ring.thy	Fri Apr 13 21:26:34 2007 +0200
     2.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Fri Apr 13 21:26:35 2007 +0200
     2.3 @@ -325,6 +325,4 @@
     2.4  use "comm_ring.ML"
     2.5  setup CommRing.setup
     2.6  
     2.7 -thm mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]
     2.8 -
     2.9  end
     3.1 --- a/src/HOL/Library/Eval.thy	Fri Apr 13 21:26:34 2007 +0200
     3.2 +++ b/src/HOL/Library/Eval.thy	Fri Apr 13 21:26:35 2007 +0200
     3.3 @@ -151,4 +151,4 @@
     3.4  end;
     3.5  *}
     3.6  
     3.7 -end
     3.8 \ No newline at end of file
     3.9 +end
     4.1 --- a/src/HOL/Library/ExecutableSet.thy	Fri Apr 13 21:26:34 2007 +0200
     4.2 +++ b/src/HOL/Library/ExecutableSet.thy	Fri Apr 13 21:26:35 2007 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -section {* Definitional rewrites *}
     4.8 +subsection {* Definitional rewrites *}
     4.9  
    4.10  instance set :: (eq) eq ..
    4.11  
    4.12 @@ -40,9 +40,9 @@
    4.13  lemmas [symmetric, code inline] = filter_set_def
    4.14  
    4.15  
    4.16 -section {* Operations on lists *}
    4.17 +subsection {* Operations on lists *}
    4.18  
    4.19 -subsection {* Basic definitions *}
    4.20 +subsubsection {* Basic definitions *}
    4.21  
    4.22  definition
    4.23    flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    4.24 @@ -107,7 +107,7 @@
    4.25    by (induct xs) simp_all
    4.26  
    4.27  
    4.28 -subsection {* Derived definitions *}
    4.29 +subsubsection {* Derived definitions *}
    4.30  
    4.31  function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    4.32  where
    4.33 @@ -169,7 +169,7 @@
    4.34    "map_inter xs f = intersects (map f xs)"
    4.35  
    4.36  
    4.37 -section {* Isomorphism proofs *}
    4.38 +subsection {* Isomorphism proofs *}
    4.39  
    4.40  lemma iso_member:
    4.41    "member xs x \<longleftrightarrow> x \<in> set xs"
    4.42 @@ -248,7 +248,7 @@
    4.43    "set (filter P xs) = filter_set P (set xs)"
    4.44    unfolding filter_set_def by (induct xs) auto
    4.45  
    4.46 -section {* code generator setup *}
    4.47 +subsection {* code generator setup *}
    4.48  
    4.49  ML {*
    4.50  nonfix inter;
    4.51 @@ -317,7 +317,7 @@
    4.52    filter_set \<equiv> filter
    4.53  
    4.54  
    4.55 -subsection {* type serializations *}
    4.56 +subsubsection {* type serializations *}
    4.57  
    4.58  types_code
    4.59    set ("_ list")
    4.60 @@ -333,7 +333,7 @@
    4.61  *}
    4.62  
    4.63  
    4.64 -subsection {* const serializations *}
    4.65 +subsubsection {* const serializations *}
    4.66  
    4.67  consts_code
    4.68    "{}"      ("[]")
     5.1 --- a/src/HOL/Library/Graphs.thy	Fri Apr 13 21:26:34 2007 +0200
     5.2 +++ b/src/HOL/Library/Graphs.thy	Fri Apr 13 21:26:35 2007 +0200
     5.3 @@ -3,12 +3,13 @@
     5.4      Author:     Alexander Krauss, TU Muenchen
     5.5  *)
     5.6  
     5.7 +header ""
     5.8 +
     5.9  theory Graphs
    5.10  imports Main SCT_Misc Kleene_Algebras ExecutableSet
    5.11  begin
    5.12  
    5.13 -
    5.14 -section {* Basic types, Size Change Graphs *}
    5.15 +subsection {* Basic types, Size Change Graphs *}
    5.16  
    5.17  datatype ('a, 'b) graph = 
    5.18    Graph "('a \<times> 'b \<times> 'a) set"
    5.19 @@ -40,8 +41,7 @@
    5.20    "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)"
    5.21  
    5.22  
    5.23 -
    5.24 -section {* Graph composition *}
    5.25 +subsection {* Graph composition *}
    5.26  
    5.27  fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph  \<Rightarrow> ('n, 'e) graph"
    5.28  where
    5.29 @@ -131,8 +131,7 @@
    5.30    by (simp add:graph_zero_def has_edge_def)
    5.31  
    5.32  
    5.33 -
    5.34 -subsection {* Multiplicative Structure *}
    5.35 +subsubsection {* Multiplicative Structure *}
    5.36  
    5.37  instance graph :: (type, times) mult_zero
    5.38    graph_mult_def: "G * H == grcomp G H" 
    5.39 @@ -297,8 +296,7 @@
    5.40    done
    5.41  
    5.42  
    5.43 -
    5.44 -section {* Infinite Paths *}
    5.45 +subsection {* Infinite Paths *}
    5.46  
    5.47  types ('n, 'e) ipath = "('n \<times> 'e) sequence"
    5.48  
    5.49 @@ -308,8 +306,7 @@
    5.50    (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))"
    5.51  
    5.52  
    5.53 -
    5.54 -section {* Finite Paths *}
    5.55 +subsection {* Finite Paths *}
    5.56  
    5.57  types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
    5.58  
    5.59 @@ -470,11 +467,7 @@
    5.60  qed
    5.61  
    5.62  
    5.63 -
    5.64 -
    5.65 -
    5.66 -section {* Sub-Paths *}
    5.67 -
    5.68 +subsection {* Sub-Paths *}
    5.69  
    5.70  definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath"
    5.71  ("(_\<langle>_,_\<rangle>)")
    5.72 @@ -710,4 +703,4 @@
    5.73    qed
    5.74  qed
    5.75  
    5.76 -end
    5.77 \ No newline at end of file
    5.78 +end
     6.1 --- a/src/HOL/Library/Kleene_Algebras.thy	Fri Apr 13 21:26:34 2007 +0200
     6.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Fri Apr 13 21:26:35 2007 +0200
     6.3 @@ -3,6 +3,8 @@
     6.4      Author:     Alexander Krauss, TU Muenchen
     6.5  *)
     6.6  
     6.7 +header ""
     6.8 +
     6.9  theory Kleene_Algebras
    6.10  imports Main 
    6.11  begin
     7.1 --- a/src/HOL/Library/Library/document/root.tex	Fri Apr 13 21:26:34 2007 +0200
     7.2 +++ b/src/HOL/Library/Library/document/root.tex	Fri Apr 13 21:26:35 2007 +0200
     7.3 @@ -21,7 +21,8 @@
     7.4  \newpage
     7.5  
     7.6  \renewcommand{\isamarkupheader}[1]%
     7.7 -{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
     7.8 +{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
     7.9 +\markright{THEORY~``\isabellecontext''}}
    7.10  \renewcommand{\isasymguillemotright}{$\gg$}
    7.11  
    7.12  \parindent 0pt \parskip 0.5ex
     8.1 --- a/src/HOL/Library/MLString.thy	Fri Apr 13 21:26:34 2007 +0200
     8.2 +++ b/src/HOL/Library/MLString.thy	Fri Apr 13 21:26:35 2007 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4      Author:     Florian Haftmann, TU Muenchen
     8.5  *)
     8.6  
     8.7 -header {* Monolithic strings for ML  *}
     8.8 +header {* Monolithic strings for ML *}
     8.9  
    8.10  theory MLString
    8.11  imports List
     9.1 --- a/src/HOL/Library/Primes.thy	Fri Apr 13 21:26:34 2007 +0200
     9.2 +++ b/src/HOL/Library/Primes.thy	Fri Apr 13 21:26:35 2007 +0200
     9.3 @@ -48,5 +48,4 @@
     9.4  lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
     9.5    by (rule prime_dvd_square) (simp_all add: power2_eq_square)
     9.6  
     9.7 -
     9.8  end
    10.1 --- a/src/HOL/Library/Pure_term.thy	Fri Apr 13 21:26:34 2007 +0200
    10.2 +++ b/src/HOL/Library/Pure_term.thy	Fri Apr 13 21:26:35 2007 +0200
    10.3 @@ -128,4 +128,4 @@
    10.4  
    10.5  code_reserved SML Term
    10.6  
    10.7 -end
    10.8 \ No newline at end of file
    10.9 +end
    11.1 --- a/src/HOL/Library/Ramsey.thy	Fri Apr 13 21:26:34 2007 +0200
    11.2 +++ b/src/HOL/Library/Ramsey.thy	Fri Apr 13 21:26:35 2007 +0200
    11.3 @@ -7,10 +7,9 @@
    11.4  
    11.5  theory Ramsey imports Main Infinite_Set begin
    11.6  
    11.7 +subsection {* Preliminaries *}
    11.8  
    11.9 -subsection{*Preliminaries*}
   11.10 -
   11.11 -subsubsection{*``Axiom'' of Dependent Choice*}
   11.12 +subsubsection {* ``Axiom'' of Dependent Choice *}
   11.13  
   11.14  consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
   11.15    --{*An integer-indexed chain of choices*}
   11.16 @@ -50,7 +49,7 @@
   11.17  qed
   11.18  
   11.19  
   11.20 -subsubsection {*Partitions of a Set*}
   11.21 +subsubsection {* Partitions of a Set *}
   11.22  
   11.23  definition
   11.24    part :: "nat => nat => 'a set => ('a set => nat) => bool"
   11.25 @@ -72,7 +71,7 @@
   11.26    unfolding part_def by blast
   11.27    
   11.28  
   11.29 -subsection {*Ramsey's Theorem: Infinitary Version*}
   11.30 +subsection {* Ramsey's Theorem: Infinitary Version *}
   11.31  
   11.32  lemma Ramsey_induction: 
   11.33    fixes s and r::nat
   11.34 @@ -231,9 +230,7 @@
   11.35  qed
   11.36  
   11.37  
   11.38 -
   11.39 -
   11.40 -subsection {*Disjunctive Well-Foundedness*}
   11.41 +subsection {* Disjunctive Well-Foundedness *}
   11.42  
   11.43  text {*
   11.44    An application of Ramsey's theorem to program termination. See
   11.45 @@ -336,5 +333,4 @@
   11.46    thus False using wfT less by blast
   11.47  qed
   11.48  
   11.49 -
   11.50  end
    12.1 --- a/src/HOL/Library/SCT_Definition.thy	Fri Apr 13 21:26:34 2007 +0200
    12.2 +++ b/src/HOL/Library/SCT_Definition.thy	Fri Apr 13 21:26:35 2007 +0200
    12.3 @@ -3,14 +3,16 @@
    12.4      Author:     Alexander Krauss, TU Muenchen
    12.5  *)
    12.6  
    12.7 +header ""
    12.8 +
    12.9  theory SCT_Definition
   12.10  imports Graphs Infinite_Set
   12.11  begin
   12.12  
   12.13 -section {* Size-Change Graphs *}
   12.14 +subsection {* Size-Change Graphs *}
   12.15  
   12.16  datatype sedge =
   12.17 -  LESS ("\<down>")
   12.18 +    LESS ("\<down>")
   12.19    | LEQ ("\<Down>")
   12.20  
   12.21  instance sedge :: times ..
   12.22 @@ -42,7 +44,7 @@
   12.23  types acg = "(nat, scg) graph"
   12.24  
   12.25  
   12.26 -section {* Size-Change Termination *}
   12.27 +subsection {* Size-Change Termination *}
   12.28  
   12.29  abbreviation (input)
   12.30    "desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))"
   12.31 @@ -97,5 +99,4 @@
   12.32  where
   12.33    "SCT' A = no_bad_graphs (tcl A)"
   12.34  
   12.35 -
   12.36 -end
   12.37 \ No newline at end of file
   12.38 +end
    13.1 --- a/src/HOL/Library/SCT_Examples.thy	Fri Apr 13 21:26:34 2007 +0200
    13.2 +++ b/src/HOL/Library/SCT_Examples.thy	Fri Apr 13 21:26:35 2007 +0200
    13.3 @@ -3,6 +3,8 @@
    13.4      Author:     Alexander Krauss, TU Muenchen
    13.5  *)
    13.6  
    13.7 +header ""
    13.8 +
    13.9  theory SCT_Examples
   13.10  imports Size_Change_Termination
   13.11  begin
    14.1 --- a/src/HOL/Library/SCT_Implementation.thy	Fri Apr 13 21:26:34 2007 +0200
    14.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Fri Apr 13 21:26:35 2007 +0200
    14.3 @@ -3,6 +3,8 @@
    14.4      Author:     Alexander Krauss, TU Muenchen
    14.5  *)
    14.6  
    14.7 +header ""
    14.8 +
    14.9  theory SCT_Implementation
   14.10  imports ExecutableSet SCT_Definition
   14.11  begin
   14.12 @@ -119,13 +121,4 @@
   14.13  
   14.14  code_gen test_SCT (SML -)
   14.15  
   14.16 -
   14.17  end
   14.18 -
   14.19 -
   14.20 -
   14.21 -
   14.22 -
   14.23 -
   14.24 -
   14.25 -
    15.1 --- a/src/HOL/Library/SCT_Interpretation.thy	Fri Apr 13 21:26:34 2007 +0200
    15.2 +++ b/src/HOL/Library/SCT_Interpretation.thy	Fri Apr 13 21:26:35 2007 +0200
    15.3 @@ -3,6 +3,8 @@
    15.4      Author:     Alexander Krauss, TU Muenchen
    15.5  *)
    15.6  
    15.7 +header ""
    15.8 +
    15.9  theory SCT_Interpretation
   15.10  imports Main SCT_Misc SCT_Definition
   15.11  begin
    16.1 --- a/src/HOL/Library/SCT_Misc.thy	Fri Apr 13 21:26:34 2007 +0200
    16.2 +++ b/src/HOL/Library/SCT_Misc.thy	Fri Apr 13 21:26:35 2007 +0200
    16.3 @@ -3,6 +3,8 @@
    16.4      Author:     Alexander Krauss, TU Muenchen
    16.5  *)
    16.6  
    16.7 +header ""
    16.8 +
    16.9  theory SCT_Misc
   16.10  imports Main
   16.11  begin
   16.12 @@ -22,6 +24,7 @@
   16.13    "(x \<in> set l) = (index_of l x < length l)"
   16.14    by (induct l) auto
   16.15  
   16.16 +
   16.17  subsection {* Some reasoning tools *}
   16.18  
   16.19  lemma inc_induct[consumes 1]:
   16.20 @@ -67,12 +70,14 @@
   16.21    using prems
   16.22    by auto
   16.23  
   16.24 -section {* Sequences *}
   16.25 +
   16.26 +subsection {* Sequences *}
   16.27  
   16.28  types
   16.29    'a sequence = "nat \<Rightarrow> 'a"
   16.30  
   16.31 -subsection {* Increasing sequences *}
   16.32 +
   16.33 +subsubsection {* Increasing sequences *}
   16.34  
   16.35  definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
   16.36  where
   16.37 @@ -115,7 +120,8 @@
   16.38    qed
   16.39  qed (simp add:increasing_strict)
   16.40  
   16.41 -subsection {* Sections induced by an increasing sequence *}
   16.42 +
   16.43 +subsubsection {* Sections induced by an increasing sequence *}
   16.44  
   16.45  abbreviation
   16.46    "section s i == {s i ..< s (Suc i)}"
    17.1 --- a/src/HOL/Library/SCT_Theorem.thy	Fri Apr 13 21:26:34 2007 +0200
    17.2 +++ b/src/HOL/Library/SCT_Theorem.thy	Fri Apr 13 21:26:35 2007 +0200
    17.3 @@ -3,11 +3,13 @@
    17.4      Author:     Alexander Krauss, TU Muenchen
    17.5  *)
    17.6  
    17.7 +header ""
    17.8 +
    17.9  theory SCT_Theorem
   17.10  imports Main Ramsey SCT_Misc SCT_Definition
   17.11  begin
   17.12  
   17.13 -section {* The size change criterion SCT *}
   17.14 +subsection {* The size change criterion SCT *}
   17.15  
   17.16  definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
   17.17  where
   17.18 @@ -33,7 +35,8 @@
   17.19    "has_desc_fth p i j n m = 
   17.20    (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
   17.21  
   17.22 -section {* Bounded graphs and threads *}
   17.23 +
   17.24 +subsection {* Bounded graphs and threads *}
   17.25  
   17.26  definition 
   17.27    "bounded_scg (P::nat) (G::scg) = 
   17.28 @@ -325,9 +328,7 @@
   17.29  qed
   17.30  
   17.31  
   17.32 -
   17.33 -section {* Contraction and more *}
   17.34 -
   17.35 +subsection {* Contraction and more *}
   17.36  
   17.37  abbreviation 
   17.38    "pdesc P == (fst P, prod P, end_node P)"
   17.39 @@ -342,8 +343,6 @@
   17.40    by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def)
   17.41  
   17.42  
   17.43 -
   17.44 -
   17.45  lemma combine_fthreads: 
   17.46    assumes range: "i < j" "j \<le> k"
   17.47    shows 
   17.48 @@ -657,7 +656,7 @@
   17.49    by (auto simp:Lemma7a increasing_weak contract_def)
   17.50  
   17.51  
   17.52 -subsection {* Connecting threads *}
   17.53 +subsubsection {* Connecting threads *}
   17.54  
   17.55  definition
   17.56    "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)"
   17.57 @@ -685,7 +684,6 @@
   17.58  qed
   17.59  
   17.60  
   17.61 -
   17.62  lemma connect_threads:
   17.63    assumes [simp]: "increasing s"
   17.64    assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
   17.65 @@ -889,7 +887,7 @@
   17.66    assume "?A"
   17.67    then obtain \<theta> n 
   17.68      where fr: "\<forall>i\<ge>n. eqlat p \<theta> i" 
   17.69 -    and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
   17.70 +      and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
   17.71      unfolding is_desc_thread_def 
   17.72      by auto
   17.73  
   17.74 @@ -903,18 +901,18 @@
   17.75      proof (intro allI impI)
   17.76        fix i assume "n \<le> i"
   17.77        also have "i \<le> s i" 
   17.78 -	    using increasing_inc by auto
   17.79 +	using increasing_inc by auto
   17.80        finally have "n \<le> s i" .
   17.81  
   17.82        with fr have "is_fthread \<theta> p (s i) (s (Suc i))"
   17.83 -	    unfolding is_fthread_def by auto
   17.84 +	unfolding is_fthread_def by auto
   17.85        hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
   17.86 -	    unfolding has_fth_def by auto
   17.87 +	unfolding has_fth_def by auto
   17.88        with less_imp_le[OF increasing_strict]
   17.89        have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
   17.90 -	    by (simp add:Lemma7a)
   17.91 +	by (simp add:Lemma7a)
   17.92        thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def
   17.93 -	    by auto
   17.94 +	by auto
   17.95      qed
   17.96  
   17.97      show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
   17.98 @@ -924,57 +922,56 @@
   17.99  
  17.100        let ?K = "section_of s (max (s (Suc i)) n)"
  17.101        from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
  17.102 -	    where "s (Suc ?K) < j" "descat p \<theta> j"
  17.103 -	    unfolding INF_nat by blast
  17.104 +	  where "s (Suc ?K) < j" "descat p \<theta> j"
  17.105 +	unfolding INF_nat by blast
  17.106        
  17.107        let ?L = "section_of s j"
  17.108        {
  17.109 -	    fix x assume r: "x \<in> section s ?L"
  17.110 -
  17.111 -	    have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
  17.112 +	fix x assume r: "x \<in> section s ?L"
  17.113 +	
  17.114 +	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
  17.115          note `s (Suc ?K) < j`
  17.116          also have "j < s (Suc ?L)"
  17.117            by (rule section_of2)
  17.118          finally have "Suc ?K \<le> ?L"
  17.119            by (simp add:increasing_bij)          
  17.120 -	    with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
  17.121 -	    with e1 r have "max (s (Suc i)) n < x" by simp
  17.122 +	with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
  17.123 +	with e1 r have "max (s (Suc i)) n < x" by simp
  17.124          
  17.125 -	    hence "(s (Suc i)) < x" "n < x" by auto
  17.126 +	hence "(s (Suc i)) < x" "n < x" by auto
  17.127        }
  17.128        note range_est = this
  17.129        
  17.130        have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))"
  17.131 -	    unfolding is_desc_fthread_def is_fthread_def
  17.132 +	unfolding is_desc_fthread_def is_fthread_def
  17.133        proof
  17.134 -	    show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
  17.135 +	show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
  17.136          proof 
  17.137            fix m assume "m\<in>section s ?L"
  17.138            with range_est(2) have "n < m" . 
  17.139            with fr show "eqlat p \<theta> m" by simp
  17.140          qed
  17.141 -        
  17.142  
  17.143          from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`]
  17.144 -	    have "j \<in> section s ?L" .
  17.145 +	have "j \<in> section s ?L" .
  17.146  
  17.147 -	    with `descat p \<theta> j`
  17.148 -	    show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
  17.149 +	with `descat p \<theta> j`
  17.150 +	show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
  17.151        qed
  17.152        
  17.153        with less_imp_le[OF increasing_strict]
  17.154        have a: "descat (contract s p) ?c\<theta> ?L"
  17.155 -	    unfolding contract_def Lemma7b[symmetric]
  17.156 -	    by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
  17.157 +	unfolding contract_def Lemma7b[symmetric]
  17.158 +	by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
  17.159        
  17.160        have "i < ?L"
  17.161        proof (rule classical)
  17.162 -	    assume "\<not> i < ?L" 
  17.163 -	    hence "s ?L < s (Suc i)" 
  17.164 +	assume "\<not> i < ?L" 
  17.165 +	hence "s ?L < s (Suc i)" 
  17.166            by (simp add:increasing_bij)
  17.167 -	    also have "\<dots> < s ?L"
  17.168 -	      by (rule range_est(1)) (simp add:increasing_strict)
  17.169 -	    finally show ?thesis .
  17.170 +	also have "\<dots> < s ?L"
  17.171 +	  by (rule range_est(1)) (simp add:increasing_strict)
  17.172 +	finally show ?thesis .
  17.173        qed
  17.174        with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l"
  17.175          by blast
  17.176 @@ -994,7 +991,7 @@
  17.177            (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
  17.178                    \<and> \<theta>s i (s i) = \<theta> i 
  17.179                    \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" 
  17.180 -    (is "desc ?alw ?inf") 
  17.181 +      (is "desc ?alw ?inf") 
  17.182      by blast
  17.183  
  17.184    then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast
  17.185 @@ -1004,8 +1001,8 @@
  17.186    let ?j\<theta> = "connect s \<theta>s"
  17.187    
  17.188    from fr ths_spec have ths_spec2:
  17.189 -    "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
  17.190 -    "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  17.191 +      "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
  17.192 +      "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  17.193      by (auto intro:INF_mono)
  17.194    
  17.195    have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
  17.196 @@ -1027,7 +1024,6 @@
  17.197  qed
  17.198  
  17.199  
  17.200 -
  17.201  lemma repeated_edge:
  17.202    assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
  17.203    shows "is_desc_thread (\<lambda>i. k) p"
  17.204 @@ -1050,9 +1046,7 @@
  17.205    by auto
  17.206  
  17.207  
  17.208 -
  17.209 -section {* Ramsey's Theorem *}
  17.210 -
  17.211 +subsection {* Ramsey's Theorem *}
  17.212  
  17.213  definition 
  17.214    "set2pair S = (THE (x,y). x < y \<and> S = {x,y})"
  17.215 @@ -1176,8 +1170,7 @@
  17.216  qed
  17.217  
  17.218  
  17.219 -section {* Main Result *}
  17.220 -
  17.221 +subsection {* Main Result *}
  17.222  
  17.223  theorem LJA_Theorem4: 
  17.224    assumes "bounded_acg P \<A>"
  17.225 @@ -1383,7 +1376,6 @@
  17.226  qed
  17.227  
  17.228  
  17.229 -
  17.230  lemma LJA_apply:
  17.231    assumes fin: "finite_acg A"
  17.232    assumes "SCT' A"
    18.1 --- a/src/HOL/Library/Size_Change_Termination.thy	Fri Apr 13 21:26:34 2007 +0200
    18.2 +++ b/src/HOL/Library/Size_Change_Termination.thy	Fri Apr 13 21:26:35 2007 +0200
    18.3 @@ -3,12 +3,14 @@
    18.4      Author:     Alexander Krauss, TU Muenchen
    18.5  *)
    18.6  
    18.7 +header ""
    18.8 +
    18.9  theory Size_Change_Termination
   18.10  imports SCT_Theorem SCT_Interpretation SCT_Implementation 
   18.11  uses "sct.ML"
   18.12  begin
   18.13  
   18.14 -section {* Simplifier setup *}
   18.15 +subsection {* Simplifier setup *}
   18.16  
   18.17  text {* This is needed to run the SCT algorithm in the simplifier: *}
   18.18