diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Sat Jul 18 21:44:18 2015 +0200 +++ b/src/HOL/Set_Interval.thy Sat Jul 18 22:58:50 2015 +0200 @@ -11,7 +11,7 @@ Examples: Ico = {_ ..< _} and Ici = {_ ..} *) -section {* Set intervals *} +section \Set intervals\ theory Set_Interval imports Lattices_Big Nat_Transfer @@ -55,9 +55,9 @@ end -text{* A note of warning when using @{term"{..A note of warning when using @{term"{.. syntax "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) @@ -84,7 +84,7 @@ "INT iVarious equivalences\ lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i {..< b} = {..< min a b}" by auto -subsection {* Logical Equivalences for Set Inclusion and Equality *} +subsection \Logical Equivalences for Set Inclusion and Equality\ lemma atLeast_subset_iff [iff]: "(atLeast x \ atLeast y) = (y \ (x::'a::order))" @@ -181,7 +181,7 @@ lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b" by auto -subsection {*Two-sided intervals*} +subsection \Two-sided intervals\ context ord begin @@ -202,16 +202,16 @@ "(i : {l..u}) = (l <= i & i <= u)" by (simp add: atLeastAtMost_def) -text {* The above four lemmas could be declared as iffs. Unfortunately this +text \The above four lemmas could be declared as iffs. Unfortunately this breaks many proofs. Since it only helps blast, it is better to leave them -alone. *} +alone.\ lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }" by auto end -subsubsection{* Emptyness, singletons, subset *} +subsubsection\Emptyness, singletons, subset\ context order begin @@ -276,7 +276,7 @@ proof assume "{a..b} = {c}" hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp - with `{a..b} = {c}` have "c \ a \ b \ c" by auto + with \{a..b} = {c}\ have "c \ a \ b \ c" by auto with * show "a = b \ b = c" by auto qed simp @@ -502,7 +502,7 @@ qed -subsection {* Infinite intervals *} +subsection \Infinite intervals\ context dense_linorder begin @@ -513,16 +513,16 @@ proof assume fin: "finite {a<.. {}" - using `a < b` by auto + using \a < b\ by auto ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" using Max_in[of "{a <..< b}"] by auto then obtain x where "Max {a <..< b} < x" "x < b" using dense[of "Max {a<.. {a <..< b}" - using `a < Max {a <..< b}` by auto + using \a < Max {a <..< b}\ by auto then have "x \ Max {a <..< b}" using fin by auto - with `Max {a <..< b} < x` show False by auto + with \Max {a <..< b} < x\ show False by auto qed lemma infinite_Icc: "a < b \ \ finite {a .. b}" @@ -550,11 +550,11 @@ obtain y where "y < Min {..< a}" using lt_ex by auto also have "Min {..< a} \ x" - using `x < a` by fact - also note `x < a` + using \x < a\ by fact + also note \x < a\ finally have "Min {..< a} \ y" by fact - with `y < Min {..< a}` show False by auto + with \y < Min {..< a}\ show False by auto qed lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}" @@ -574,17 +574,17 @@ using gt_ex by auto also then have "x \ Max {a <..}" by fact - also note `Max {a <..} < y` + also note \Max {a <..} < y\ finally have "y \ Max { a <..}" by fact - with `Max {a <..} < y` show False by auto + with \Max {a <..} < y\ show False by auto qed lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}" using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] by (auto simp: subset_eq less_imp_le) -subsubsection {* Intersection *} +subsubsection \Intersection\ context linorder begin @@ -652,9 +652,9 @@ and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x" by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded) -subsection {* Intervals of natural numbers *} +subsection \Intervals of natural numbers\ -subsubsection {* The Constant @{term lessThan} *} +subsubsection \The Constant @{term lessThan}\ lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" by (simp add: lessThan_def) @@ -662,9 +662,9 @@ lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" by (simp add: lessThan_def less_Suc_eq, blast) -text {* The following proof is convenient in induction proofs where +text \The following proof is convenient in induction proofs where new elements get indices at the beginning. So it is used to transform -@{term "{.. lemma zero_notin_Suc_image: "0 \ Suc ` A" by auto @@ -681,7 +681,7 @@ lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" by blast -subsubsection {* The Constant @{term greaterThan} *} +subsubsection \The Constant @{term greaterThan}\ lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" apply (simp add: greaterThan_def) @@ -696,7 +696,7 @@ lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" by blast -subsubsection {* The Constant @{term atLeast} *} +subsubsection \The Constant @{term atLeast}\ lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" by (unfold atLeast_def UNIV_def, simp) @@ -713,7 +713,7 @@ lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" by blast -subsubsection {* The Constant @{term atMost} *} +subsubsection \The Constant @{term atMost}\ lemma atMost_0 [simp]: "atMost (0::nat) = {0}" by (simp add: atMost_def) @@ -726,14 +726,14 @@ lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" by blast -subsubsection {* The Constant @{term atLeastLessThan} *} +subsubsection \The Constant @{term atLeastLessThan}\ -text{*The orientation of the following 2 rules is tricky. The lhs is +text\The orientation of the following 2 rules is tricky. The lhs is defined in terms of the rhs. Hence the chosen orientation makes sense in this theory --- the reverse orientation complicates proofs (eg nontermination). But outside, when the definition of the lhs is rarely used, the opposite orientation seems preferable because it reduces a -specific concept to a more general one. *} +specific concept to a more general one.\ lemma atLeast0LessThan: "{0::nat..Intervals of nats with @{term Suc}\ -text{*Not a simprule because the RHS is too messy.*} +text\Not a simprule because the RHS is too messy.\ lemma atLeastLessThanSuc: "{m.. n then insert n {m.. n \ insert m {Suc m..n} = {m ..n}" by auto -text {* The analogous result is useful on @{typ int}: *} +text \The analogous result is useful on @{typ int}:\ (* here, because we don't have an own int section *) lemma atLeastAtMostPlus1_int_conv: "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}" @@ -791,23 +791,23 @@ apply (simp_all add: atLeastLessThanSuc) done -subsubsection {* Intervals and numerals *} +subsubsection \Intervals and numerals\ -lemma lessThan_nat_numeral: --{*Evaluation for specific numerals*} +lemma lessThan_nat_numeral: --\Evaluation for specific numerals\ "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" by (simp add: numeral_eq_Suc lessThan_Suc) -lemma atMost_nat_numeral: --{*Evaluation for specific numerals*} +lemma atMost_nat_numeral: --\Evaluation for specific numerals\ "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" by (simp add: numeral_eq_Suc atMost_Suc) -lemma atLeastLessThan_nat_numeral: --{*Evaluation for specific numerals*} +lemma atLeastLessThan_nat_numeral: --\Evaluation for specific numerals\ "atLeastLessThan m (numeral k :: nat) = (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastLessThanSuc) -subsubsection {* Image *} +subsubsection \Image\ lemma image_add_atLeastAtMost: fixes k ::"'a::linordered_semidom" @@ -898,7 +898,7 @@ next fix y assume "y \ -x" have "- (-y) \ uminus ` {x..}" - by (rule imageI) (insert `y \ -x`[THEN le_imp_neg_le], simp) + by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp) thus "y \ uminus ` {x..}" by simp qed simp_all @@ -924,7 +924,7 @@ greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) end -subsubsection {* Finiteness *} +subsubsection \Finiteness\ lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\ lemma bounded_nat_set_is_finite: "(ALL i:N. i < (n::nat)) ==> finite N" apply (rule finite_subset) apply (rule_tac [2] finite_lessThan, auto) done -text {* A set of natural numbers is finite iff it is bounded. *} +text \A set of natural numbers is finite iff it is bounded.\ lemma finite_nat_set_iff_bounded: "finite(N::nat set) = (EX m. ALL n:N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast next - assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite) + assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite) qed lemma finite_nat_set_iff_bounded_le: @@ -976,8 +976,8 @@ by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) -text{* Any subset of an interval of natural numbers the size of the -subset is exactly that interval. *} +text\Any subset of an interval of natural numbers the size of the +subset is exactly that interval.\ lemma subset_card_intvl_is_intvl: assumes "A \ {k..Proving Inclusions and Equalities between Unions\ lemma UN_le_eq_Un0: "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B") @@ -1056,7 +1056,7 @@ done -subsubsection {* Cardinality *} +subsubsection \Cardinality\ lemma card_lessThan [simp]: "card {..f. inj_on f A \ f ` A \ B)" by blast qed (insert assms, auto) -subsection {* Intervals of integers *} +subsection \Intervals of integers\ lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\ lemma image_atLeastZeroLessThan_int: "0 \ u ==> {(0::int)..Cardinality\ lemma card_atLeastZeroLessThan_int: "card {(0::int).. u") @@ -1265,13 +1265,13 @@ qed -subsection {*Lemmas useful with the summation operator setsum*} +subsection \Lemmas useful with the summation operator setsum\ -text {* For examples, see Algebra/poly/UnivPoly2.thy *} +text \For examples, see Algebra/poly/UnivPoly2.thy\ -subsubsection {* Disjoint Unions *} +subsubsection \Disjoint Unions\ -text {* Singletons and open intervals *} +text \Singletons and open intervals\ lemma ivl_disj_un_singleton: "{l::'a::linorder} Un {l<..} = {l..}" @@ -1282,7 +1282,7 @@ "(l::'a::linorder) <= u ==> {l..One- and two-sided intervals\ lemma ivl_disj_un_one: "(l::'a::linorder) < u ==> {..l} Un {l<.. {l..Two- and two-sided intervals\ lemma ivl_disj_un_two: "[| (l::'a::linorder) < m; m <= u |] ==> {l<..Disjoint Intersections\ -text {* One- and two-sided intervals *} +text \One- and two-sided intervals\ lemma ivl_disj_int_one: "{..l::'a::order} Int {l<..Two- and two-sided intervals\ lemma ivl_disj_int_two: "{l::'a::order<..Some Differences\ lemma ivl_diff[simp]: "i \ n \ {i..Some Subset Conditions\ lemma ivl_subset [simp]: "({i.. {m.. i | m \ i & j \ (n::'a::linorder))" @@ -1370,7 +1370,7 @@ done -subsection {* Summation indexed over intervals *} +subsection \Summation indexed over intervals\ syntax "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) @@ -1403,7 +1403,7 @@ "\i\n. t" == "CONST setsum (\i. t) {..n}" "\ii. t) {..The above introduces some pretty alternative syntaxes for summation over intervals: \begin{center} \begin{tabular}{lll} @@ -1425,12 +1425,12 @@ Note that for uniformity on @{typ nat} it is better to use @{term"\x::nat=0..x -text{* This congruence rule should be used for sums over intervals as +text\This congruence rule should be used for sums over intervals as the standard theorem @{text[source]setsum.cong} does not work well with the simplifier who adds the unsimplified premise @{term"x:B"} to -the context. *} +the context.\ lemma setsum_ivl_cong: "\a = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \ @@ -1486,7 +1486,7 @@ lemma setsum_ub_add_nat: assumes "(m::nat) \ n + 1" shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" proof- - have "{m .. n+p} = {m..n} \ {n+1..n+p}" using `m \ n+1` by auto + have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto thus ?thesis by (auto simp: ivl_disj_int setsum.union_disjoint atLeastSucAtMost_greaterThanAtMost) qed @@ -1532,7 +1532,7 @@ lemma nat_diff_setsum_reindex: "(\iiShifting bounds\ lemma setsum_shift_bounds_nat_ivl: "setsum f {m+k..The formula for geometric sums\ lemma geometric_sum: assumes "x \ 1" @@ -1611,7 +1611,7 @@ proof - from assms obtain y where "y = x - 1" and "y \ 0" by simp_all moreover have "(\i 0`) + by (induct n) (simp_all add: power_Suc field_simps \y \ 0\) ultimately show ?thesis by simp qed @@ -1635,7 +1635,7 @@ finally show ?case . qed simp -corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *} +corollary power_diff_sumr2: --\@{text COMPLEX_POLYFUN} in HOL Light\ fixes x :: "'a::{comm_ring,monoid_mult}" shows "x^n - y^n = (x - y) * (\iThe formula for arithmetic sums\ lemma gauss_sum: "(2::'a::comm_semiring_1)*(\i\{1..n}. of_nat i) = of_nat n*((of_nat n)+1)" @@ -1721,7 +1721,7 @@ lemma sum_diff_distrib: "\x. Q x \ P x \ (\xxxProducts indexed over intervals\ syntax "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) @@ -1754,7 +1754,7 @@ "\i\n. t" == "CONST setprod (\i. t) {..n}" "\ii. t) {..Transfer setup\ lemma transfer_nat_int_set_functions: "{..n} = nat ` {0..int n}"