tuned document;
authorwenzelm
Tue Feb 27 00:33:49 2007 +0100 (2007-02-27)
changeset 223676860f09242bf
parent 22366 f4840bfffe5d
child 22368 0e0fe77d4768
tuned document;
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Library/document/root.bib
src/HOL/Library/Ramsey.thy
src/HOL/document/root.bib
     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.18    by (induct k) (simp_all add: add_assoc)
    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.83 -by (simp add: igcd_def)
    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.5 - @InProceedings{Avigad-Donnelly,
     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.13 +@InProceedings{Avigad-Donnelly,
    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