# HG changeset patch # User wenzelm # Date 1176492395 -7200 # Node ID cf152ff55d162d4652dbf3d2b51bff41316c3129 # Parent e965391e28646bd2991f8fad6018613f35b6a1e0 tuned document (headers, sections, spacing); diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/BigO.thy Fri Apr 13 21:26:35 2007 +0200 @@ -59,11 +59,11 @@ apply (rule mult_right_mono) apply (rule abs_ge_self) apply (rule abs_ge_zero) -done + done lemma bigo_alt_def: "O(f) = {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" -by (auto simp add: bigo_def bigo_pos_const) + by (auto simp add: bigo_def bigo_pos_const) lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)" apply (auto simp add: bigo_alt_def) @@ -78,25 +78,25 @@ apply (simp add: mult_ac) apply (rule mult_left_mono, assumption) apply (rule order_less_imp_le, assumption) -done + done lemma bigo_refl [intro]: "f : O(f)" apply(auto simp add: bigo_def) apply(rule_tac x = 1 in exI) apply simp -done + done lemma bigo_zero: "0 : O(g)" apply (auto simp add: bigo_def func_zero) apply (rule_tac x = 0 in exI) apply auto -done + done lemma bigo_zero2: "O(%x.0) = {%x.0}" apply (auto simp add: bigo_def) apply (rule ext) apply auto -done + done lemma bigo_plus_self_subset [intro]: "O(f) + O(f) <= O(f)" @@ -116,7 +116,7 @@ apply (rule bigo_plus_self_subset) apply (rule set_zero_plus2) apply (rule bigo_zero) -done + done lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)" apply (rule subsetI) @@ -168,17 +168,17 @@ apply simp apply (rule ext) apply (auto simp add: if_splits linorder_not_le) -done + done lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)" apply (subgoal_tac "A + B <= O(f) + O(f)") apply (erule order_trans) apply simp apply (auto del: subsetI simp del: bigo_plus_idemp) -done + done lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> - O(f + g) = O(f) + O(g)" + O(f + g) = O(f) + O(g)" apply (rule equalityI) apply (rule bigo_plus_subset) apply (simp add: bigo_alt_def set_plus func_plus) @@ -211,7 +211,7 @@ apply (rule abs_triangle_ineq) apply (rule add_nonneg_nonneg) apply assumption+ -done + done lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" @@ -220,13 +220,13 @@ apply auto apply (drule_tac x = x in spec)+ apply (simp add: abs_mult [symmetric]) -done + done lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> f : O(g)" apply (erule bigo_bounded_alt [of f 1 g]) apply simp -done + done lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==> f : lb +o O(g)" @@ -237,21 +237,21 @@ apply force apply (drule_tac x = x in spec)+ apply force -done + done lemma bigo_abs: "(%x. abs(f x)) =o O(f)" apply (unfold bigo_def) apply auto apply (rule_tac x = 1 in exI) apply auto -done + done lemma bigo_abs2: "f =o O(%x. abs(f x))" apply (unfold bigo_def) apply auto apply (rule_tac x = 1 in exI) apply auto -done + done lemma bigo_abs3: "O(f) = O(%x. abs(f x))" apply (rule equalityI) @@ -259,7 +259,7 @@ apply (rule bigo_abs2) apply (rule bigo_elt_subset) apply (rule bigo_abs) -done + done lemma bigo_abs4: "f =o g +o O(h) ==> (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" @@ -288,7 +288,7 @@ qed lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" -by (unfold bigo_def, auto) + by (unfold bigo_def, auto) lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)" proof - @@ -326,7 +326,7 @@ apply (rule mult_nonneg_nonneg) apply auto apply (simp add: mult_ac abs_mult) -done + done lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) @@ -337,20 +337,20 @@ apply (force simp add: mult_ac) apply (rule mult_left_mono, assumption) apply (rule abs_ge_zero) -done + done lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)" apply (rule subsetD) apply (rule bigo_mult) apply (erule set_times_intro, assumption) -done + done lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)" apply (drule set_plus_imp_minus) apply (rule set_minus_imp_plus) apply (drule bigo_mult3 [where g = g and j = g]) apply (auto simp add: ring_eq_simps mult_ac) -done + done lemma bigo_mult5: "ALL x. f x ~= 0 ==> O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)" @@ -386,7 +386,7 @@ apply (rule equalityI) apply (erule bigo_mult5) apply (rule bigo_mult2) -done + done lemma bigo_mult7: "ALL x. f x ~= 0 ==> O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)" @@ -394,14 +394,14 @@ apply assumption apply (rule set_times_mono3) apply (rule bigo_refl) -done + done lemma bigo_mult8: "ALL x. f x ~= 0 ==> O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)" apply (rule equalityI) apply (erule bigo_mult7) apply (rule bigo_mult) -done + done lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" by (auto simp add: bigo_def func_minus) @@ -411,7 +411,7 @@ apply (drule set_plus_imp_minus) apply (drule bigo_minus) apply (simp add: diff_minus) -done + done lemma bigo_minus3: "O(-f) = O(f)" by (auto simp add: bigo_def func_minus abs_minus_cancel) @@ -452,12 +452,12 @@ apply (rule equalityI) apply (erule bigo_plus_absorb_lemma1) apply (erule bigo_plus_absorb_lemma2) -done + done lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)" apply (subgoal_tac "f +o A <= f +o O(g)") apply force+ -done + done lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)" apply (subst set_minus_plus [symmetric]) @@ -467,56 +467,56 @@ apply (subst set_minus_plus) apply assumption apply (simp add: diff_minus add_ac) -done + done lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))" apply (rule iffI) apply (erule bigo_add_commute_imp)+ -done + done lemma bigo_const1: "(%x. c) : O(%x. 1)" -by (auto simp add: bigo_def mult_ac) + by (auto simp add: bigo_def mult_ac) lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)" apply (rule bigo_elt_subset) apply (rule bigo_const1) -done + done lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)" apply (simp add: bigo_def) apply (rule_tac x = "abs(inverse c)" in exI) apply (simp add: abs_mult [symmetric]) -done + done lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" -by (rule bigo_elt_subset, rule bigo_const3, assumption) + by (rule bigo_elt_subset, rule bigo_const3, assumption) lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> O(%x. c) = O(%x. 1)" -by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) + by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) lemma bigo_const_mult1: "(%x. c * f x) : O(f)" apply (simp add: bigo_def) apply (rule_tac x = "abs(c)" in exI) apply (auto simp add: abs_mult [symmetric]) -done + done lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" -by (rule bigo_elt_subset, rule bigo_const_mult1) + by (rule bigo_elt_subset, rule bigo_const_mult1) lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)" apply (simp add: bigo_def) apply (rule_tac x = "abs(inverse c)" in exI) apply (simp add: abs_mult [symmetric] mult_assoc [symmetric]) -done + done lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> O(f) <= O(%x. c * f x)" -by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) + by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> O(%x. c * f x) = O(f)" -by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) + by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> (%x. c) *o O(f) = O(f)" @@ -533,7 +533,7 @@ apply (rule mult_left_mono) apply (erule spec) apply force -done + done lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)" apply (auto intro!: subsetI @@ -547,7 +547,7 @@ apply (erule spec) apply simp apply(simp add: mult_ac) -done + done lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)" proof - @@ -571,6 +571,7 @@ apply (erule bigo_compose1) done + subsection {* Setsum *} lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> @@ -595,7 +596,7 @@ apply (rule mult_right_mono) apply (rule abs_ge_self) apply force -done + done lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> EX c. ALL x y. abs(f x y) <= c * (h x y) ==> @@ -605,12 +606,12 @@ apply clarsimp apply (rule_tac x = c in exI) apply force -done + done lemma bigo_setsum2: "ALL y. 0 <= h y ==> EX c. ALL y. abs(f y) <= c * (h y) ==> (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)" -by (rule bigo_setsum1, auto) + by (rule bigo_setsum1, auto) lemma bigo_setsum3: "f =o O(h) ==> (%x. SUM y : A x. (l x y) * f(k x y)) =o @@ -627,7 +628,7 @@ apply (rule mult_left_mono) apply (erule spec) apply (rule abs_ge_zero) -done + done lemma bigo_setsum4: "f =o g +o O(h) ==> (%x. SUM y : A x. l x y * f(k x y)) =o @@ -640,7 +641,7 @@ apply (rule bigo_setsum3) apply (subst func_diff [symmetric]) apply (erule set_plus_imp_minus) -done + done lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> ALL x. 0 <= h x ==> @@ -655,7 +656,7 @@ apply (subst abs_of_nonneg) apply (rule mult_nonneg_nonneg) apply auto -done + done lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==> ALL x. 0 <= h x ==> @@ -670,7 +671,8 @@ apply (subst func_diff [symmetric]) apply (drule set_plus_imp_minus) apply auto -done + done + subsection {* Misc useful stuff *} @@ -679,13 +681,13 @@ apply (subst bigo_plus_idemp [symmetric]) apply (rule set_plus_mono2) apply assumption+ -done + done lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)" apply (subst bigo_plus_idemp [symmetric]) apply (rule set_plus_intro) apply assumption+ -done + done lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> (%x. c) * f =o O(h) ==> f =o O(h)" @@ -701,7 +703,7 @@ apply (subst times_divide_eq_left [symmetric]) apply (subst divide_self) apply (assumption, simp) -done + done lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==> f =o O(h)" @@ -718,7 +720,7 @@ apply (erule ssubst) back apply (erule spec) apply simp -done + done lemma bigo_fix2: "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> @@ -730,7 +732,8 @@ apply (rule set_plus_imp_minus) apply simp apply (simp add: func_diff) -done + done + subsection {* Less than or equal to *} @@ -747,7 +750,7 @@ apply (rule allI) apply (rule order_trans) apply (erule spec)+ -done + done lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==> g =o O(h)" @@ -757,15 +760,15 @@ apply (rule order_trans) apply assumption apply (rule abs_ge_self) -done + done lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==> - g =o O(h)" + g =o O(h)" apply (erule bigo_lesseq2) apply (rule allI) apply (subst abs_of_nonneg) apply (erule spec)+ -done + done lemma bigo_lesseq4: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==> @@ -774,7 +777,7 @@ apply (rule allI) apply (subst abs_of_nonneg) apply (erule spec)+ -done + done lemma bigo_lesso1: "ALL x. f x <= g x ==> f ALL x. 0 <= k x ==> ALL x. k x <= f x ==> @@ -808,7 +811,7 @@ prefer 2 apply (rule abs_ge_zero) apply (simp add: compare_rls) -done + done lemma bigo_lesso3: "f =o g +o O(h) ==> ALL x. 0 <= k x ==> ALL x. g x <= k x ==> @@ -833,7 +836,7 @@ prefer 2 apply (rule abs_ge_zero) apply (simp add: compare_rls) -done + done lemma bigo_lesso4: "f 'b::ordered_field) ==> g =o h +o O(k) ==> f EX C. ALL x. f x <= g x + C * abs(h x)" @@ -860,7 +863,7 @@ apply (clarsimp simp add: compare_rls add_ac) apply (rule abs_of_nonneg) apply (rule le_maxI2) -done + done lemma lesso_add: "f k (f + k) 'b \ 'c) \ 'b \ 'a \ 'c" where @@ -107,7 +107,7 @@ by (induct xs) simp_all -subsection {* Derived definitions *} +subsubsection {* Derived definitions *} function unionl :: "'a list \ 'a list \ 'a list" where @@ -169,7 +169,7 @@ "map_inter xs f = intersects (map f xs)" -section {* Isomorphism proofs *} +subsection {* Isomorphism proofs *} lemma iso_member: "member xs x \ x \ set xs" @@ -248,7 +248,7 @@ "set (filter P xs) = filter_set P (set xs)" unfolding filter_set_def by (induct xs) auto -section {* code generator setup *} +subsection {* code generator setup *} ML {* nonfix inter; @@ -317,7 +317,7 @@ filter_set \ filter -subsection {* type serializations *} +subsubsection {* type serializations *} types_code set ("_ list") @@ -333,7 +333,7 @@ *} -subsection {* const serializations *} +subsubsection {* const serializations *} consts_code "{}" ("[]") diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Graphs.thy --- a/src/HOL/Library/Graphs.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Graphs.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,12 +3,13 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory Graphs imports Main SCT_Misc Kleene_Algebras ExecutableSet begin - -section {* Basic types, Size Change Graphs *} +subsection {* Basic types, Size Change Graphs *} datatype ('a, 'b) graph = Graph "('a \ 'b \ 'a) set" @@ -40,8 +41,7 @@ "has_edge G n e n' = ((n, e, n') \ dest_graph G)" - -section {* Graph composition *} +subsection {* Graph composition *} fun grcomp :: "('n, 'e::times) graph \ ('n, 'e) graph \ ('n, 'e) graph" where @@ -131,8 +131,7 @@ by (simp add:graph_zero_def has_edge_def) - -subsection {* Multiplicative Structure *} +subsubsection {* Multiplicative Structure *} instance graph :: (type, times) mult_zero graph_mult_def: "G * H == grcomp G H" @@ -297,8 +296,7 @@ done - -section {* Infinite Paths *} +subsection {* Infinite Paths *} types ('n, 'e) ipath = "('n \ 'e) sequence" @@ -308,8 +306,7 @@ (\i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))" - -section {* Finite Paths *} +subsection {* Finite Paths *} types ('n, 'e) fpath = "('n \ ('e \ 'n) list)" @@ -470,11 +467,7 @@ qed - - - -section {* Sub-Paths *} - +subsection {* Sub-Paths *} definition sub_path :: "('n, 'e) ipath \ nat \ nat \ ('n, 'e) fpath" ("(_\_,_\)") @@ -710,4 +703,4 @@ qed qed -end \ No newline at end of file +end diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Kleene_Algebras.thy --- a/src/HOL/Library/Kleene_Algebras.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Kleene_Algebras.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,6 +3,8 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory Kleene_Algebras imports Main begin diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Library/document/root.tex --- a/src/HOL/Library/Library/document/root.tex Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Library/document/root.tex Fri Apr 13 21:26:35 2007 +0200 @@ -21,7 +21,8 @@ \newpage \renewcommand{\isamarkupheader}[1]% -{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}} +{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}% +\markright{THEORY~``\isabellecontext''}} \renewcommand{\isasymguillemotright}{$\gg$} \parindent 0pt \parskip 0.5ex diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/MLString.thy --- a/src/HOL/Library/MLString.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/MLString.thy Fri Apr 13 21:26:35 2007 +0200 @@ -2,7 +2,7 @@ Author: Florian Haftmann, TU Muenchen *) -header {* Monolithic strings for ML *} +header {* Monolithic strings for ML *} theory MLString imports List diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Primes.thy --- a/src/HOL/Library/Primes.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Primes.thy Fri Apr 13 21:26:35 2007 +0200 @@ -48,5 +48,4 @@ lemma prime_dvd_power_two: "prime p ==> p dvd m\ ==> p dvd m" by (rule prime_dvd_square) (simp_all add: power2_eq_square) - end diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Pure_term.thy --- a/src/HOL/Library/Pure_term.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Pure_term.thy Fri Apr 13 21:26:35 2007 +0200 @@ -128,4 +128,4 @@ code_reserved SML Term -end \ No newline at end of file +end diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Ramsey.thy Fri Apr 13 21:26:35 2007 +0200 @@ -7,10 +7,9 @@ theory Ramsey imports Main Infinite_Set begin +subsection {* Preliminaries *} -subsection{*Preliminaries*} - -subsubsection{*``Axiom'' of Dependent Choice*} +subsubsection {* ``Axiom'' of Dependent Choice *} consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a" --{*An integer-indexed chain of choices*} @@ -50,7 +49,7 @@ qed -subsubsection {*Partitions of a Set*} +subsubsection {* Partitions of a Set *} definition part :: "nat => nat => 'a set => ('a set => nat) => bool" @@ -72,7 +71,7 @@ unfolding part_def by blast -subsection {*Ramsey's Theorem: Infinitary Version*} +subsection {* Ramsey's Theorem: Infinitary Version *} lemma Ramsey_induction: fixes s and r::nat @@ -231,9 +230,7 @@ qed - - -subsection {*Disjunctive Well-Foundedness*} +subsection {* Disjunctive Well-Foundedness *} text {* An application of Ramsey's theorem to program termination. See @@ -336,5 +333,4 @@ thus False using wfT less by blast qed - end diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Definition.thy --- a/src/HOL/Library/SCT_Definition.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/SCT_Definition.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,14 +3,16 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory SCT_Definition imports Graphs Infinite_Set begin -section {* Size-Change Graphs *} +subsection {* Size-Change Graphs *} datatype sedge = - LESS ("\") + LESS ("\") | LEQ ("\") instance sedge :: times .. @@ -42,7 +44,7 @@ types acg = "(nat, scg) graph" -section {* Size-Change Termination *} +subsection {* Size-Change Termination *} abbreviation (input) "desc P Q == ((\n.\i\n. P i) \ (\\<^sub>\i. Q i))" @@ -97,5 +99,4 @@ where "SCT' A = no_bad_graphs (tcl A)" - -end \ No newline at end of file +end diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Examples.thy --- a/src/HOL/Library/SCT_Examples.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/SCT_Examples.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,6 +3,8 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory SCT_Examples imports Size_Change_Termination begin diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Implementation.thy --- a/src/HOL/Library/SCT_Implementation.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/SCT_Implementation.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,6 +3,8 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory SCT_Implementation imports ExecutableSet SCT_Definition begin @@ -119,13 +121,4 @@ code_gen test_SCT (SML -) - end - - - - - - - - diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Interpretation.thy --- a/src/HOL/Library/SCT_Interpretation.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/SCT_Interpretation.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,6 +3,8 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory SCT_Interpretation imports Main SCT_Misc SCT_Definition begin diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Misc.thy --- a/src/HOL/Library/SCT_Misc.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/SCT_Misc.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,6 +3,8 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory SCT_Misc imports Main begin @@ -22,6 +24,7 @@ "(x \ set l) = (index_of l x < length l)" by (induct l) auto + subsection {* Some reasoning tools *} lemma inc_induct[consumes 1]: @@ -67,12 +70,14 @@ using prems by auto -section {* Sequences *} + +subsection {* Sequences *} types 'a sequence = "nat \ 'a" -subsection {* Increasing sequences *} + +subsubsection {* Increasing sequences *} definition increasing :: "(nat \ nat) \ bool" where @@ -115,7 +120,8 @@ qed qed (simp add:increasing_strict) -subsection {* Sections induced by an increasing sequence *} + +subsubsection {* Sections induced by an increasing sequence *} abbreviation "section s i == {s i ..< s (Suc i)}" diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Theorem.thy --- a/src/HOL/Library/SCT_Theorem.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/SCT_Theorem.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,11 +3,13 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory SCT_Theorem imports Main Ramsey SCT_Misc SCT_Definition begin -section {* The size change criterion SCT *} +subsection {* The size change criterion SCT *} definition is_thread :: "nat \ nat sequence \ (nat, scg) ipath \ bool" where @@ -33,7 +35,8 @@ "has_desc_fth p i j n m = (\\. is_desc_fthread \ p i j \ \ i = n \ \ j = m)" -section {* Bounded graphs and threads *} + +subsection {* Bounded graphs and threads *} definition "bounded_scg (P::nat) (G::scg) = @@ -325,9 +328,7 @@ qed - -section {* Contraction and more *} - +subsection {* Contraction and more *} abbreviation "pdesc P == (fst P, prod P, end_node P)" @@ -342,8 +343,6 @@ by (auto intro:sub_path_is_path[of "\" p i j] simp:sub_path_def) - - lemma combine_fthreads: assumes range: "i < j" "j \ k" shows @@ -657,7 +656,7 @@ by (auto simp:Lemma7a increasing_weak contract_def) -subsection {* Connecting threads *} +subsubsection {* Connecting threads *} definition "connect s \s = (\k. \s (section_of s k) k)" @@ -685,7 +684,6 @@ qed - lemma connect_threads: assumes [simp]: "increasing s" assumes connected: "\s i (s (Suc i)) = \s (Suc i) (s (Suc i))" @@ -889,7 +887,7 @@ assume "?A" then obtain \ n where fr: "\i\n. eqlat p \ i" - and ds: "\\<^sub>\i. descat p \ i" + and ds: "\\<^sub>\i. descat p \ i" unfolding is_desc_thread_def by auto @@ -903,18 +901,18 @@ proof (intro allI impI) fix i assume "n \ i" also have "i \ s i" - using increasing_inc by auto + using increasing_inc by auto finally have "n \ s i" . with fr have "is_fthread \ p (s i) (s (Suc i))" - unfolding is_fthread_def by auto + unfolding is_fthread_def by auto hence "has_fth p (s i) (s (Suc i)) (\ (s i)) (\ (s (Suc i)))" - unfolding has_fth_def by auto + unfolding has_fth_def by auto with less_imp_le[OF increasing_strict] have "eql (prod (p\s i,s (Suc i)\)) (\ (s i)) (\ (s (Suc i)))" - by (simp add:Lemma7a) + by (simp add:Lemma7a) thus "eqlat (contract s p) ?c\ i" unfolding contract_def - by auto + by auto qed show "\\<^sub>\i. descat (contract s p) ?c\ i" @@ -924,57 +922,56 @@ let ?K = "section_of s (max (s (Suc i)) n)" from `\\<^sub>\i. descat p \ i` obtain j - where "s (Suc ?K) < j" "descat p \ j" - unfolding INF_nat by blast + where "s (Suc ?K) < j" "descat p \ j" + unfolding INF_nat by blast let ?L = "section_of s j" { - fix x assume r: "x \ section s ?L" - - have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) + fix x assume r: "x \ section s ?L" + + have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) note `s (Suc ?K) < j` also have "j < s (Suc ?L)" by (rule section_of2) finally have "Suc ?K \ ?L" by (simp add:increasing_bij) - with increasing_weak have "s (Suc ?K) \ s ?L" by simp - with e1 r have "max (s (Suc i)) n < x" by simp + with increasing_weak have "s (Suc ?K) \ s ?L" by simp + with e1 r have "max (s (Suc i)) n < x" by simp - hence "(s (Suc i)) < x" "n < x" by auto + hence "(s (Suc i)) < x" "n < x" by auto } note range_est = this have "is_desc_fthread \ p (s ?L) (s (Suc ?L))" - unfolding is_desc_fthread_def is_fthread_def + unfolding is_desc_fthread_def is_fthread_def proof - show "\m\section s ?L. eqlat p \ m" + show "\m\section s ?L. eqlat p \ m" proof fix m assume "m\section s ?L" with range_est(2) have "n < m" . with fr show "eqlat p \ m" by simp qed - from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`] - have "j \ section s ?L" . + have "j \ section s ?L" . - with `descat p \ j` - show "\m\section s ?L. descat p \ m" .. + with `descat p \ j` + show "\m\section s ?L. descat p \ m" .. qed with less_imp_le[OF increasing_strict] have a: "descat (contract s p) ?c\ ?L" - unfolding contract_def Lemma7b[symmetric] - by (auto simp:Lemma7b[symmetric] has_desc_fth_def) + unfolding contract_def Lemma7b[symmetric] + by (auto simp:Lemma7b[symmetric] has_desc_fth_def) have "i < ?L" proof (rule classical) - assume "\ i < ?L" - hence "s ?L < s (Suc i)" + assume "\ i < ?L" + hence "s ?L < s (Suc i)" by (simp add:increasing_bij) - also have "\ < s ?L" - by (rule range_est(1)) (simp add:increasing_strict) - finally show ?thesis . + also have "\ < s ?L" + by (rule range_est(1)) (simp add:increasing_strict) + finally show ?thesis . qed with a show "\l. i < l \ descat (contract s p) ?c\ l" by blast @@ -994,7 +991,7 @@ (\i. is_desc_fthread (\s i) p (s i) (s (Suc i)) \ \s i (s i) = \ i \ \s i (s (Suc i)) = \ (Suc i))" - (is "desc ?alw ?inf") + (is "desc ?alw ?inf") by blast then obtain n where fr: "\i\n. ?alw i" by blast @@ -1004,8 +1001,8 @@ let ?j\ = "connect s \s" from fr ths_spec have ths_spec2: - "\i. i > n \ is_fthread (\s i) p (s i) (s (Suc i))" - "\\<^sub>\i. is_desc_fthread (\s i) p (s i) (s (Suc i))" + "\i. i > n \ is_fthread (\s i) p (s i) (s (Suc i))" + "\\<^sub>\i. is_desc_fthread (\s i) p (s i) (s (Suc i))" by (auto intro:INF_mono) have p1: "\i. i > n \ is_fthread ?j\ p (s i) (s (Suc i))" @@ -1027,7 +1024,6 @@ qed - lemma repeated_edge: assumes "\i. i > n \ dsc (snd (p i)) k k" shows "is_desc_thread (\i. k) p" @@ -1050,9 +1046,7 @@ by auto - -section {* Ramsey's Theorem *} - +subsection {* Ramsey's Theorem *} definition "set2pair S = (THE (x,y). x < y \ S = {x,y})" @@ -1176,8 +1170,7 @@ qed -section {* Main Result *} - +subsection {* Main Result *} theorem LJA_Theorem4: assumes "bounded_acg P \" @@ -1383,7 +1376,6 @@ qed - lemma LJA_apply: assumes fin: "finite_acg A" assumes "SCT' A" diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/Size_Change_Termination.thy --- a/src/HOL/Library/Size_Change_Termination.thy Fri Apr 13 21:26:34 2007 +0200 +++ b/src/HOL/Library/Size_Change_Termination.thy Fri Apr 13 21:26:35 2007 +0200 @@ -3,12 +3,14 @@ Author: Alexander Krauss, TU Muenchen *) +header "" + theory Size_Change_Termination imports SCT_Theorem SCT_Interpretation SCT_Implementation uses "sct.ML" begin -section {* Simplifier setup *} +subsection {* Simplifier setup *} text {* This is needed to run the SCT algorithm in the simplifier: *}