# HG changeset patch # User wenzelm # Date 1172532829 -3600 # Node ID 6860f09242bf230e2ec68810c871e047ab177991 # Parent f4840bfffe5d03e3785ab1724bac50c89acc5509 tuned document; diff -r f4840bfffe5d -r 6860f09242bf src/HOL/Library/Coinductive_List.thy --- a/src/HOL/Library/Coinductive_List.thy Tue Feb 27 00:32:52 2007 +0100 +++ b/src/HOL/Library/Coinductive_List.thy Tue Feb 27 00:33:49 2007 +0100 @@ -280,7 +280,7 @@ qed -subsection {* Equality as greatest fixed-point; the bisimulation principle. *} +subsection {* Equality as greatest fixed-point -- the bisimulation principle *} consts EqLList :: "('a Datatype.item \ 'a Datatype.item) set \ diff -r f4840bfffe5d -r 6860f09242bf src/HOL/Library/Continuity.thy --- a/src/HOL/Library/Continuity.thy Tue Feb 27 00:32:52 2007 +0100 +++ b/src/HOL/Library/Continuity.thy Tue Feb 27 00:33:49 2007 +0100 @@ -9,20 +9,22 @@ imports Main begin -subsection{*Continuity for complete lattices*} +subsection {* Continuity for complete lattices *} -constdefs - chain :: "(nat \ 'a::order) \ bool" -"chain M == !i. M i \ M(Suc i)" - continuous :: "('a::order \ 'a::order) \ bool" -"continuous F == !M. chain M \ F(SUP i. M i) = (SUP i. F(M i))" +definition + chain :: "(nat \ 'a::order) \ bool" where + "chain M \ (\i. M i \ M (Suc i))" + +definition + continuous :: "('a::order \ 'a::order) \ bool" where + "continuous F \ (\M. chain M \ F (SUP i. M i) = (SUP i. F (M i)))" abbreviation bot :: "'a::order" where - "bot == Sup {}" + "bot \ Sup {}" lemma SUP_nat_conv: - "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))" + "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))" apply(rule order_antisym) apply(rule SUP_leI) apply(case_tac n) diff -r f4840bfffe5d -r 6860f09242bf src/HOL/Library/GCD.thy --- a/src/HOL/Library/GCD.thy Tue Feb 27 00:32:52 2007 +0100 +++ b/src/HOL/Library/GCD.thy Tue Feb 27 00:33:49 2007 +0100 @@ -180,10 +180,10 @@ lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" proof - - have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) + have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) also have "... = gcd (n + m, m)" by (simp add: add_commute) also have "... = gcd (n, m)" by simp - also have "... = gcd (m, n)" by (rule gcd_commute) + also have "... = gcd (m, n)" by (rule gcd_commute) finally show ?thesis . qed @@ -195,110 +195,124 @@ lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" by (induct k) (simp_all add: add_assoc) - (* Division by gcd yields rrelatively primes *) +text {* + \medskip Division by gcd yields rrelatively primes. +*} lemma div_gcd_relprime: - assumes nz:"a\0 \ b\0" + assumes nz: "a \ 0 \ b \ 0" shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1" -proof- - let ?g = "gcd (a,b)" +proof - + let ?g = "gcd (a, b)" let ?a' = "a div ?g" let ?b' = "b div ?g" let ?g' = "gcd (?a', ?b')" have dvdg: "?g dvd a" "?g dvd b" by simp_all have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all - from dvdg dvdg' obtain ka kb ka' kb' where - kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'" + from dvdg dvdg' obtain ka kb ka' kb' where + kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" unfolding dvd_def by blast - hence "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all - hence dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" - by (auto simp add: dvd_mult_div_cancel[OF dvdg(1)] - dvd_mult_div_cancel[OF dvdg(2)] dvd_def) + then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all + then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" + by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] + dvd_mult_div_cancel [OF dvdg(2)] dvd_def) have "?g \ 0" using nz by (simp add: gcd_zero) - hence gp: "?g > 0" by simp - from gcd_greatest[OF dvdgg'] have "?g * ?g' dvd ?g" . - with dvd_mult_cancel1[OF gp] show "?g' = 1" by simp + then have gp: "?g > 0" by simp + from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . + with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp qed - (* gcd on integers *) -constdefs igcd:: "int \ int \ int" - "igcd i j \ int (gcd (nat (abs i),nat (abs j)))" -lemma igcd_dvd1[simp]:"igcd i j dvd i" + +text {* + \medskip Gcd on integers. +*} + +definition + igcd :: "int \ int \ int" where + "igcd i j = int (gcd (nat (abs i), nat (abs j)))" + +lemma igcd_dvd1 [simp]: "igcd i j dvd i" by (simp add: igcd_def int_dvd_iff) -lemma igcd_dvd2[simp]:"igcd i j dvd j" -by (simp add: igcd_def int_dvd_iff) +lemma igcd_dvd2 [simp]: "igcd i j dvd j" + by (simp add: igcd_def int_dvd_iff) lemma igcd_pos: "igcd i j \ 0" -by (simp add: igcd_def) -lemma igcd0[simp]: "(igcd i j = 0) = (i = 0 \ j = 0)" -by (simp add: igcd_def gcd_zero) arith + by (simp add: igcd_def) + +lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \ j = 0)" + by (simp add: igcd_def gcd_zero) arith lemma igcd_commute: "igcd i j = igcd j i" unfolding igcd_def by (simp add: gcd_commute) -lemma igcd_neg1[simp]: "igcd (- i) j = igcd i j" + +lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j" unfolding igcd_def by simp -lemma igcd_neg2[simp]: "igcd i (- j) = igcd i j" + +lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j" unfolding igcd_def by simp + lemma zrelprime_dvd_mult: "igcd i j = 1 \ i dvd k * j \ i dvd k" unfolding igcd_def -proof- - assume H: "int (gcd (nat \i\, nat \j\)) = 1" "i dvd k * j" - hence g: "gcd (nat \i\, nat \j\) = 1" by simp - from H(2) obtain h where h:"k*j = i*h" unfolding dvd_def by blast +proof - + assume "int (gcd (nat \i\, nat \j\)) = 1" "i dvd k * j" + then have g: "gcd (nat \i\, nat \j\) = 1" by simp + from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast have th: "nat \i\ dvd nat \k\ * nat \j\" - unfolding dvd_def - by (rule_tac x= "nat \h\" in exI,simp add: h nat_abs_mult_distrib[symmetric]) - from relprime_dvd_mult[OF g th] obtain h' where h': "nat \k\ = nat \i\ * h'" + unfolding dvd_def + by (rule_tac x= "nat \h\" in exI, simp add: h nat_abs_mult_distrib [symmetric]) + from relprime_dvd_mult [OF g th] obtain h' where h': "nat \k\ = nat \i\ * h'" unfolding dvd_def by blast from h' have "int (nat \k\) = int (nat \i\ * h')" by simp - hence "\k\ = \i\ * int h'" by (simp add: int_mult) + then have "\k\ = \i\ * int h'" by (simp add: int_mult) then show ?thesis - apply (subst zdvd_abs1[symmetric]) - apply (subst zdvd_abs2[symmetric]) + apply (subst zdvd_abs1 [symmetric]) + apply (subst zdvd_abs2 [symmetric]) apply (unfold dvd_def) - apply (rule_tac x="int h'" in exI, simp) + apply (rule_tac x = "int h'" in exI, simp) done qed lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith -lemma igcd_greatest: assumes km:"k dvd m" and kn:"k dvd n" shows "k dvd igcd m n" -proof- + +lemma igcd_greatest: + assumes "k dvd m" and "k dvd n" + shows "k dvd igcd m n" +proof - let ?k' = "nat \k\" let ?m' = "nat \m\" let ?n' = "nat \n\" - from km kn have dvd': "?k' dvd ?m'" "?k' dvd ?n'" + from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'" unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2) - from gcd_greatest[OF dvd'] have "int (nat \k\) dvd igcd m n" + from gcd_greatest [OF dvd'] have "int (nat \k\) dvd igcd m n" unfolding igcd_def by (simp only: zdvd_int) - hence "\k\ dvd igcd m n" by (simp only: int_nat_abs) - thus "k dvd igcd m n" by (simp add: zdvd_abs1) + then have "\k\ dvd igcd m n" by (simp only: int_nat_abs) + then show "k dvd igcd m n" by (simp add: zdvd_abs1) qed lemma div_igcd_relprime: - assumes nz:"a\0 \ b\0" + assumes nz: "a \ 0 \ b \ 0" shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1" -proof- +proof - from nz have nz': "nat \a\ \ 0 \ nat \b\ \ 0" by simp - have th1: "(1::int) = int 1" by simp let ?g = "igcd a b" let ?a' = "a div ?g" let ?b' = "b div ?g" let ?g' = "igcd ?a' ?b'" have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2) have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2) - from dvdg dvdg' obtain ka kb ka' kb' where - kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'" + from dvdg dvdg' obtain ka kb ka' kb' where + kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'" unfolding dvd_def by blast - hence "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all - hence dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" - by (auto simp add: zdvd_mult_div_cancel[OF dvdg(1)] - zdvd_mult_div_cancel[OF dvdg(2)] dvd_def) + then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all + then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" + by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)] + zdvd_mult_div_cancel [OF dvdg(2)] dvd_def) have "?g \ 0" using nz by simp - hence gp: "?g \ 0" using igcd_pos[where i="a" and j="b"] by arith - from igcd_greatest[OF dvdgg'] have "?g * ?g' dvd ?g" . - with zdvd_mult_cancel1[OF gp] have "\?g'\ = 1" by simp + then have gp: "?g \ 0" using igcd_pos[where i="a" and j="b"] by arith + from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . + with zdvd_mult_cancel1 [OF gp] have "\?g'\ = 1" by simp with igcd_pos show "?g' = 1" by simp qed diff -r f4840bfffe5d -r 6860f09242bf src/HOL/Library/Library/document/root.bib --- a/src/HOL/Library/Library/document/root.bib Tue Feb 27 00:32:52 2007 +0100 +++ b/src/HOL/Library/Library/document/root.bib Tue Feb 27 00:33:49 2007 +0100 @@ -1,5 +1,12 @@ - @InProceedings{Avigad-Donnelly, +@Unpublished{Abrial-Laffitte, + author = {Abrial and Laffitte}, + title = {Towards the Mechanization of the Proofs of + Some Classical Theorems of Set Theory}, + note = {Unpublished} +} + +@InProceedings{Avigad-Donnelly, author = {Jeremy Avigad and Kevin Donnelly}, title = {Formalizing {O} notation in {Isabelle/HOL}}, booktitle = {Automated Reasoning: second international conference, IJCAR 2004}, @@ -9,13 +16,6 @@ publisher = {Springer} } -@Unpublished{Abrial-Laffitte, - author = {Abrial and Laffitte}, - title = {Towards the Mechanization of the Proofs of - Some Classical Theorems of Set Theory}, - note = {Unpublished} -} - @Book{Oberschelp:1993, author = {Arnold Oberschelp}, title = {Rekursionstheorie}, @@ -23,6 +23,21 @@ year = 1993 } +@InProceedings{Podelski-Rybalchenko, + author = {Andreas Podelski and Andrey Rybalchenko}, + title = {Transition Invariants}, + booktitle = {19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)}, + pages = {32--41}, + year = 2004 +} + +@Book{davenport92, + author = {H. Davenport}, + title = {The Higher Arithmetic}, + publisher = {Cambridge University Press}, + year = 1992 +} + @InProceedings{paulin-tlca, author = {Christine Paulin-Mohring}, title = {Inductive Definitions in the System {Coq}: Rules and diff -r f4840bfffe5d -r 6860f09242bf src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Tue Feb 27 00:32:52 2007 +0100 +++ b/src/HOL/Library/Ramsey.thy Tue Feb 27 00:33:49 2007 +0100 @@ -235,10 +235,9 @@ subsection {*Disjunctive Well-Foundedness*} -text{*An application of Ramsey's theorem to program termination. See - -Andreas Podelski and Andrey Rybalchenko, Transition Invariants, 19th Annual -IEEE Symposium on Logic in Computer Science (LICS'04), pages 32--41 (2004). +text {* + An application of Ramsey's theorem to program termination. See + \cite{Podelski-Rybalchenko}. *} definition diff -r f4840bfffe5d -r 6860f09242bf src/HOL/document/root.bib --- a/src/HOL/document/root.bib Tue Feb 27 00:32:52 2007 +0100 +++ b/src/HOL/document/root.bib Tue Feb 27 00:33:49 2007 +0100 @@ -1,9 +1,3 @@ -@Book{davenport92, - author = {H. Davenport}, - title = {The Higher Arithmetic}, - publisher = {Cambridge University Press}, - year = 1992 -} @book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory}, publisher={American Mathematical Society},year=1979} \ No newline at end of file