author wenzelm Tue Feb 27 00:33:49 2007 +0100 (2007-02-27) changeset 22367 6860f09242bf parent 22366 f4840bfffe5d child 22368 0e0fe77d4768
tuned document;
 src/HOL/Library/Coinductive_List.thy file | annotate | diff | revisions src/HOL/Library/Continuity.thy file | annotate | diff | revisions src/HOL/Library/GCD.thy file | annotate | diff | revisions src/HOL/Library/Library/document/root.bib file | annotate | diff | revisions src/HOL/Library/Ramsey.thy file | annotate | diff | revisions src/HOL/document/root.bib file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Library/Coinductive_List.thy	Tue Feb 27 00:32:52 2007 +0100
1.2 +++ b/src/HOL/Library/Coinductive_List.thy	Tue Feb 27 00:33:49 2007 +0100
1.3 @@ -280,7 +280,7 @@
1.4  qed
1.5
1.6
1.7 -subsection {* Equality as greatest fixed-point; the bisimulation principle. *}
1.8 +subsection {* Equality as greatest fixed-point -- the bisimulation principle *}
1.9
1.10  consts
1.11    EqLList :: "('a Datatype.item \<times> 'a Datatype.item) set \<Rightarrow>
```
```     2.1 --- a/src/HOL/Library/Continuity.thy	Tue Feb 27 00:32:52 2007 +0100
2.2 +++ b/src/HOL/Library/Continuity.thy	Tue Feb 27 00:33:49 2007 +0100
2.3 @@ -9,20 +9,22 @@
2.4  imports Main
2.5  begin
2.6
2.7 -subsection{*Continuity for complete lattices*}
2.8 +subsection {* Continuity for complete lattices *}
2.9
2.10 -constdefs
2.11 - chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
2.12 -"chain M == !i. M i \<le> M(Suc i)"
2.13 - continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
2.14 -"continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
2.15 +definition
2.16 +  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
2.17 +  "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
2.18 +
2.19 +definition
2.20 +  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where
2.21 +  "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
2.22
2.23  abbreviation
2.24    bot :: "'a::order" where
2.25 -  "bot == Sup {}"
2.26 +  "bot \<equiv> Sup {}"
2.27
2.28  lemma SUP_nat_conv:
2.29 - "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
2.30 +  "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
2.31  apply(rule order_antisym)
2.32   apply(rule SUP_leI)
2.33   apply(case_tac n)
```
```     3.1 --- a/src/HOL/Library/GCD.thy	Tue Feb 27 00:32:52 2007 +0100
3.2 +++ b/src/HOL/Library/GCD.thy	Tue Feb 27 00:33:49 2007 +0100
3.3 @@ -180,10 +180,10 @@
3.4
3.5  lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
3.6  proof -
3.7 -  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute)
3.8 +  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute)
3.9    also have "... = gcd (n + m, m)" by (simp add: add_commute)
3.10    also have "... = gcd (n, m)" by simp
3.11 -  also have  "... = gcd (m, n)" by (rule gcd_commute)
3.12 +  also have  "... = gcd (m, n)" by (rule gcd_commute)
3.13    finally show ?thesis .
3.14  qed
3.15
3.16 @@ -195,110 +195,124 @@
3.17  lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
3.19
3.20 -  (* Division by gcd yields rrelatively primes *)
3.21
3.22 +text {*
3.23 +  \medskip Division by gcd yields rrelatively primes.
3.24 +*}
3.25
3.26  lemma div_gcd_relprime:
3.27 -  assumes nz:"a\<noteq>0 \<or> b\<noteq>0"
3.28 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
3.29    shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1"
3.30 -proof-
3.31 -  let ?g = "gcd (a,b)"
3.32 +proof -
3.33 +  let ?g = "gcd (a, b)"
3.34    let ?a' = "a div ?g"
3.35    let ?b' = "b div ?g"
3.36    let ?g' = "gcd (?a', ?b')"
3.37    have dvdg: "?g dvd a" "?g dvd b" by simp_all
3.38    have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
3.39 -  from dvdg dvdg' obtain ka kb ka' kb' where
3.40 -   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
3.41 +  from dvdg dvdg' obtain ka kb ka' kb' where
3.42 +      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
3.43      unfolding dvd_def by blast
3.44 -  hence	"?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
3.45 -  hence dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
3.46 -    by (auto simp add: dvd_mult_div_cancel[OF dvdg(1)]
3.47 -      dvd_mult_div_cancel[OF dvdg(2)] dvd_def)
3.48 +  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
3.49 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
3.50 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
3.51 +      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
3.52    have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
3.53 -  hence gp: "?g > 0" by simp
3.54 -  from gcd_greatest[OF dvdgg'] have "?g * ?g' dvd ?g" .
3.55 -  with dvd_mult_cancel1[OF gp] show "?g' = 1" by simp
3.56 +  then have gp: "?g > 0" by simp
3.57 +  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
3.58 +  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
3.59  qed
3.60
3.61 -  (* gcd on integers *)
3.62 -constdefs igcd:: "int \<Rightarrow> int \<Rightarrow> int"
3.63 -  "igcd i j \<equiv> int (gcd (nat (abs i),nat (abs j)))"
3.64 -lemma igcd_dvd1[simp]:"igcd i j dvd i"
3.65 +
3.66 +text {*
3.67 +  \medskip Gcd on integers.
3.68 +*}
3.69 +
3.70 +definition
3.71 +  igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
3.72 +  "igcd i j = int (gcd (nat (abs i), nat (abs j)))"
3.73 +
3.74 +lemma igcd_dvd1 [simp]: "igcd i j dvd i"
3.75    by (simp add: igcd_def int_dvd_iff)
3.76
3.77 -lemma igcd_dvd2[simp]:"igcd i j dvd j"
3.78 -by (simp add: igcd_def int_dvd_iff)
3.79 +lemma igcd_dvd2 [simp]: "igcd i j dvd j"
3.80 +  by (simp add: igcd_def int_dvd_iff)
3.81
3.82  lemma igcd_pos: "igcd i j \<ge> 0"
3.84 -lemma igcd0[simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
3.85 -by (simp add: igcd_def gcd_zero) arith
3.86 +  by (simp add: igcd_def)
3.87 +
3.88 +lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
3.89 +  by (simp add: igcd_def gcd_zero) arith
3.90
3.91  lemma igcd_commute: "igcd i j = igcd j i"
3.92    unfolding igcd_def by (simp add: gcd_commute)
3.93 -lemma igcd_neg1[simp]: "igcd (- i) j = igcd i j"
3.94 +
3.95 +lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j"
3.96    unfolding igcd_def by simp
3.97 -lemma igcd_neg2[simp]: "igcd i (- j) = igcd i j"
3.98 +
3.99 +lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j"
3.100    unfolding igcd_def by simp
3.101 +
3.102  lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
3.103    unfolding igcd_def
3.104 -proof-
3.105 -  assume H: "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
3.106 -  hence g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
3.107 -  from H(2) obtain h where h:"k*j = i*h" unfolding dvd_def by blast
3.108 +proof -
3.109 +  assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
3.110 +  then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
3.111 +  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
3.112    have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
3.113 -    unfolding dvd_def
3.114 -    by (rule_tac x= "nat \<bar>h\<bar>" in exI,simp add: h nat_abs_mult_distrib[symmetric])
3.115 -  from relprime_dvd_mult[OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
3.116 +    unfolding dvd_def
3.117 +    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
3.118 +  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
3.119      unfolding dvd_def by blast
3.120    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
3.121 -  hence "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
3.122 +  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
3.123    then show ?thesis
3.124 -    apply (subst zdvd_abs1[symmetric])
3.125 -    apply (subst zdvd_abs2[symmetric])
3.126 +    apply (subst zdvd_abs1 [symmetric])
3.127 +    apply (subst zdvd_abs2 [symmetric])
3.128      apply (unfold dvd_def)
3.129 -    apply (rule_tac x="int h'" in exI, simp)
3.130 +    apply (rule_tac x = "int h'" in exI, simp)
3.131      done
3.132  qed
3.133
3.134  lemma int_nat_abs: "int (nat (abs x)) = abs x"  by arith
3.135 -lemma igcd_greatest: assumes km:"k dvd m" and kn:"k dvd n"  shows "k dvd igcd m n"
3.136 -proof-
3.137 +
3.138 +lemma igcd_greatest:
3.139 +  assumes "k dvd m" and "k dvd n"
3.140 +  shows "k dvd igcd m n"
3.141 +proof -
3.142    let ?k' = "nat \<bar>k\<bar>"
3.143    let ?m' = "nat \<bar>m\<bar>"
3.144    let ?n' = "nat \<bar>n\<bar>"
3.145 -  from km kn have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
3.146 +  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
3.147      unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
3.148 -  from gcd_greatest[OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
3.149 +  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
3.150      unfolding igcd_def by (simp only: zdvd_int)
3.151 -  hence "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
3.152 -  thus "k dvd igcd m n" by (simp add: zdvd_abs1)
3.153 +  then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
3.154 +  then show "k dvd igcd m n" by (simp add: zdvd_abs1)
3.155  qed
3.156
3.157  lemma div_igcd_relprime:
3.158 -  assumes nz:"a\<noteq>0 \<or> b\<noteq>0"
3.159 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
3.160    shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
3.161 -proof-
3.162 +proof -
3.163    from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by simp
3.164 -  have th1: "(1::int) = int 1" by simp
3.165    let ?g = "igcd a b"
3.166    let ?a' = "a div ?g"
3.167    let ?b' = "b div ?g"
3.168    let ?g' = "igcd ?a' ?b'"
3.169    have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
3.170    have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2)
3.171 -  from dvdg dvdg' obtain ka kb ka' kb' where
3.172 -   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
3.173 +  from dvdg dvdg' obtain ka kb ka' kb' where
3.174 +   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
3.175      unfolding dvd_def by blast
3.176 -  hence	"?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
3.177 -  hence dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
3.178 -    by (auto simp add: zdvd_mult_div_cancel[OF dvdg(1)]
3.179 -      zdvd_mult_div_cancel[OF dvdg(2)] dvd_def)
3.180 +  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
3.181 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
3.182 +    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
3.183 +      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
3.184    have "?g \<noteq> 0" using nz by simp
3.185 -  hence gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
3.186 -  from igcd_greatest[OF dvdgg'] have "?g * ?g' dvd ?g" .
3.187 -  with zdvd_mult_cancel1[OF gp] have "\<bar>?g'\<bar> = 1" by simp
3.188 +  then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
3.189 +  from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
3.190 +  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
3.191    with igcd_pos show "?g' = 1" by simp
3.192  qed
3.193
```
```     4.1 --- a/src/HOL/Library/Library/document/root.bib	Tue Feb 27 00:32:52 2007 +0100
4.2 +++ b/src/HOL/Library/Library/document/root.bib	Tue Feb 27 00:33:49 2007 +0100
4.3 @@ -1,5 +1,12 @@
4.4
4.6 +@Unpublished{Abrial-Laffitte,
4.7 +  author = 	 {Abrial and Laffitte},
4.8 +  title = 	 {Towards the Mechanization of the Proofs of
4.9 +                  Some Classical Theorems of Set Theory},
4.10 +  note = 	 {Unpublished}
4.11 +}
4.12 +
4.14    author = 	 {Jeremy Avigad and Kevin Donnelly},
4.15    title = 	 {Formalizing {O} notation in {Isabelle/HOL}},
4.16    booktitle = 	 {Automated Reasoning: second international conference, IJCAR 2004},
4.17 @@ -9,13 +16,6 @@
4.18    publisher =	 {Springer}
4.19  }
4.20
4.21 -@Unpublished{Abrial-Laffitte,
4.22 -  author = 	 {Abrial and Laffitte},
4.23 -  title = 	 {Towards the Mechanization of the Proofs of
4.24 -                  Some Classical Theorems of Set Theory},
4.25 -  note = 	 {Unpublished}
4.26 -}
4.27 -
4.28  @Book{Oberschelp:1993,
4.29    author =	 {Arnold Oberschelp},
4.30    title = 	 {Rekursionstheorie},
4.31 @@ -23,6 +23,21 @@
4.32    year = 	 1993
4.33  }
4.34
4.35 +@InProceedings{Podelski-Rybalchenko,
4.36 +  author = 	 {Andreas Podelski and Andrey Rybalchenko},
4.37 +  title = 	 {Transition Invariants},
4.38 +  booktitle = 	 {19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)},
4.39 +  pages =	 {32--41},
4.40 +  year =	 2004
4.41 +}
4.42 +
4.43 +@Book{davenport92,
4.44 +  author =	 {H. Davenport},
4.45 +  title = 	 {The Higher Arithmetic},
4.46 +  publisher = 	 {Cambridge University Press},
4.47 +  year = 	 1992
4.48 +}
4.49 +
4.50  @InProceedings{paulin-tlca,
4.51    author	= {Christine Paulin-Mohring},
4.52    title		= {Inductive Definitions in the System {Coq}: Rules and
```
```     5.1 --- a/src/HOL/Library/Ramsey.thy	Tue Feb 27 00:32:52 2007 +0100
5.2 +++ b/src/HOL/Library/Ramsey.thy	Tue Feb 27 00:33:49 2007 +0100
5.3 @@ -235,10 +235,9 @@
5.4
5.5  subsection {*Disjunctive Well-Foundedness*}
5.6
5.7 -text{*An application of Ramsey's theorem to program termination. See
5.8 -
5.9 -Andreas Podelski and Andrey Rybalchenko, Transition Invariants, 19th Annual
5.10 -IEEE Symposium on Logic in Computer Science (LICS'04), pages 32--41 (2004).
5.11 +text {*
5.12 +  An application of Ramsey's theorem to program termination. See
5.13 +  \cite{Podelski-Rybalchenko}.
5.14  *}
5.15
5.16  definition
```
```     6.1 --- a/src/HOL/document/root.bib	Tue Feb 27 00:32:52 2007 +0100
6.2 +++ b/src/HOL/document/root.bib	Tue Feb 27 00:33:49 2007 +0100
6.3 @@ -1,9 +1,3 @@
6.4 -@Book{davenport92,
6.5 -  author =	 {H. Davenport},
6.6 -  title = 	 {The Higher Arithmetic},
6.7 -  publisher = 	 {Cambridge University Press},
6.8 -  year = 	 1992
6.9 -}
6.10
6.11  @book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
6.12  publisher={American Mathematical Society},year=1979}
6.13 \ No newline at end of file
```