author wenzelm Wed Mar 06 17:47:51 2002 +0100 (2002-03-06) changeset 13029 84e4ba7fb033 parent 13028 81c87faed78b child 13030 5765aa72afac
 src/HOL/Hyperreal/ex/ROOT.ML file | annotate | diff | revisions src/HOL/Hyperreal/ex/Sqrt.thy file | annotate | diff | revisions src/HOL/Hyperreal/ex/Sqrt_Script.thy file | annotate | diff | revisions src/HOL/Hyperreal/ex/document/root.tex file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Hyperreal/ex/ROOT.ML	Wed Mar 06 17:47:51 2002 +0100
1.3 @@ -0,0 +1,9 @@
1.4 +(*  Title:      HOL/Hyperreal/ex/ROOT.ML
1.5 +    ID:         $Id$
1.6 +
1.7 +Miscellaneous HOL-Hyperreal Examples.
1.8 +*)
1.9 +
1.10 +no_document use_thy "Primes";
1.11 +use_thy "Sqrt";
1.12 +use_thy "Sqrt_Script";

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Hyperreal/ex/Sqrt.thy	Wed Mar 06 17:47:51 2002 +0100
2.3 @@ -0,0 +1,151 @@
2.4 +(*  Title:      HOL/Hyperreal/ex/Sqrt.thy
2.5 +    ID:         $Id$
2.6 +    Author:     Markus Wenzel, TU Muenchen
2.8 +*)
2.9 +
2.10 +header {*  Square roots of primes are irrational *}
2.11 +
2.12 +theory Sqrt = Primes + Hyperreal:
2.13 +
2.14 +subsection {* Preliminaries *}
2.15 +
2.16 +text {*
2.17 +  The set of rational numbers, including the key representation
2.18 +  theorem.
2.19 +*}
2.20 +
2.21 +constdefs
2.22 +  rationals :: "real set"    ("\<rat>")
2.23 +  "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
2.24 +
2.25 +theorem rationals_rep: "x \<in> \<rat> \<Longrightarrow>
2.26 +  \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
2.27 +proof -
2.28 +  assume "x \<in> \<rat>"
2.29 +  then obtain m n :: nat where n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
2.30 +    by (unfold rationals_def) blast
2.31 +  let ?gcd = "gcd (m, n)"
2.32 +  from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
2.33 +  let ?k = "m div ?gcd"
2.34 +  let ?l = "n div ?gcd"
2.35 +  let ?gcd' = "gcd (?k, ?l)"
2.36 +  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
2.37 +    by (rule dvd_mult_div_cancel)
2.38 +  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
2.39 +    by (rule dvd_mult_div_cancel)
2.40 +
2.41 +  from n and gcd_l have "?l \<noteq> 0"
2.42 +    by (auto iff del: neq0_conv)
2.43 +  moreover
2.44 +  have "\<bar>x\<bar> = real ?k / real ?l"
2.45 +  proof -
2.46 +    from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)"
2.47 +      by (simp add: real_mult_div_cancel1)
2.48 +    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
2.49 +    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
2.50 +    finally show ?thesis ..
2.51 +  qed
2.52 +  moreover
2.53 +  have "?gcd' = 1"
2.54 +  proof -
2.55 +    have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)"
2.56 +      by (rule gcd_mult_distrib2)
2.57 +    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
2.58 +    with gcd show ?thesis by simp
2.59 +  qed
2.60 +  ultimately show ?thesis by blast
2.61 +qed
2.62 +
2.63 +lemma [elim?]: "r \<in> \<rat> \<Longrightarrow>
2.64 +  (\<And>m n. n \<noteq> 0 \<Longrightarrow> \<bar>r\<bar> = real m / real n \<Longrightarrow> gcd (m, n) = 1 \<Longrightarrow> C)
2.65 +    \<Longrightarrow> C"
2.66 +  using rationals_rep by blast
2.67 +
2.68 +
2.69 +subsection {* Main theorem *}
2.70 +
2.71 +text {*
2.72 +  The square root of any prime number (including @{text 2}) is
2.73 +  irrational.
2.74 +*}
2.75 +
2.76 +theorem sqrt_prime_irrational: "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
2.77 +proof
2.78 +  assume p_prime: "p \<in> prime"
2.79 +  then have p: "1 < p" by (simp add: prime_def)
2.80 +  assume "sqrt (real p) \<in> \<rat>"
2.81 +  then obtain m n where
2.82 +      n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
2.83 +    and gcd: "gcd (m, n) = 1" ..
2.84 +  have eq: "m\<twosuperior> = p * n\<twosuperior>"
2.85 +  proof -
2.86 +    from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
2.87 +    then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
2.88 +      by (auto simp add: power_two real_power_two)
2.89 +    also have "(sqrt (real p))\<twosuperior> = real p" by simp
2.90 +    also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
2.91 +    finally show ?thesis ..
2.92 +  qed
2.93 +  have "p dvd m \<and> p dvd n"
2.94 +  proof
2.95 +    from eq have "p dvd m\<twosuperior>" ..
2.96 +    with p_prime show "p dvd m" by (rule prime_dvd_power_two)
2.97 +    then obtain k where "m = p * k" ..
2.98 +    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
2.99 +    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
2.100 +    then have "p dvd n\<twosuperior>" ..
2.101 +    with p_prime show "p dvd n" by (rule prime_dvd_power_two)
2.102 +  qed
2.103 +  then have "p dvd gcd (m, n)" ..
2.104 +  with gcd have "p dvd 1" by simp
2.105 +  then have "p \<le> 1" by (simp add: dvd_imp_le)
2.106 +  with p show False by simp
2.107 +qed
2.108 +
2.109 +text {*
2.110 +  Just for the record: we instantiate the main theorem for the
2.111 +  specific prime number @{text 2} (real mathematicians would never do
2.112 +  this formally :-).
2.113 +*}
2.114 +
2.115 +corollary "sqrt (real (2::nat)) \<notin> \<rat>"
2.116 +  by (rule sqrt_prime_irrational) (rule two_is_prime)
2.117 +
2.118 +
2.119 +subsection {* Variations *}
2.120 +
2.121 +text {*
2.122 +  Here is an alternative version of the main proof, using mostly
2.123 +  linear forward-reasoning.  While this results in less top-down
2.124 +  structure, it is probably closer to proofs seen in mathematics.
2.125 +*}
2.126 +
2.127 +theorem "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
2.128 +proof
2.129 +  assume p_prime: "p \<in> prime"
2.130 +  then have p: "1 < p" by (simp add: prime_def)
2.131 +  assume "sqrt (real p) \<in> \<rat>"
2.132 +  then obtain m n where
2.133 +      n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
2.134 +    and gcd: "gcd (m, n) = 1" ..
2.135 +  from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
2.136 +  then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
2.137 +    by (auto simp add: power_two real_power_two)
2.138 +  also have "(sqrt (real p))\<twosuperior> = real p" by simp
2.139 +  also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
2.140 +  finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
2.141 +  then have "p dvd m\<twosuperior>" ..
2.142 +  with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
2.143 +  then obtain k where "m = p * k" ..
2.144 +  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
2.145 +  with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
2.146 +  then have "p dvd n\<twosuperior>" ..
2.147 +  with p_prime have "p dvd n" by (rule prime_dvd_power_two)
2.148 +  with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
2.149 +  with gcd have "p dvd 1" by simp
2.150 +  then have "p \<le> 1" by (simp add: dvd_imp_le)
2.151 +  with p show False by simp
2.152 +qed
2.153 +
2.154 +end

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 17:47:51 2002 +0100
3.3 @@ -0,0 +1,76 @@
3.4 +(*  Title:      HOL/Hyperreal/ex/Sqrt_Script.thy
3.5 +    ID:         $Id$
3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3.7 +    Copyright   2001  University of Cambridge
3.8 +*)
3.9 +
3.10 +header {*  Square roots of primes are irrational (script version) *}
3.11 +
3.12 +theory Sqrt_Script = Primes + Hyperreal:
3.13 +
3.14 +text {*
3.15 +  \medskip Contrast this linear Isabelle/Isar script with Markus
3.16 +  Wenzel's more mathematical version.
3.17 +*}
3.18 +
3.19 +subsection {* Preliminaries *}
3.20 +
3.21 +lemma prime_nonzero:  "p \<in> prime \<Longrightarrow> p \<noteq> 0"
3.22 +  by (force simp add: prime_def)
3.23 +
3.24 +lemma prime_dvd_other_side: "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
3.25 +  apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
3.26 +  apply (rule_tac j = "k * k" in dvd_mult_left, simp)
3.27 +  done
3.28 +
3.29 +lemma reduction:
3.30 +    "p \<in> prime \<Longrightarrow> 0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
3.31 +  apply (rule ccontr)
3.32 +  apply (simp add: linorder_not_less)
3.33 +  apply (erule disjE)
3.34 +   apply (frule mult_le_mono, assumption)
3.35 +   apply auto
3.36 +  apply (force simp add: prime_def)
3.37 +  done
3.38 +
3.39 +lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
3.40 +  by (simp add: mult_ac)
3.41 +
3.42 +lemma prime_not_square:
3.43 +    "p \<in> prime \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
3.44 +  apply (induct m rule: nat_less_induct)
3.45 +  apply clarify
3.46 +  apply (frule prime_dvd_other_side, assumption)
3.47 +  apply (erule dvdE)
3.48 +  apply (simp add: nat_mult_eq_cancel_disj prime_nonzero)
3.49 +  apply (blast dest: rearrange reduction)
3.50 +  done
3.51 +
3.52 +
3.53 +subsection {* The set of rational numbers *}
3.54 +
3.55 +constdefs
3.56 +  rationals :: "real set"    ("\<rat>")
3.57 +  "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
3.58 +
3.59 +
3.60 +subsection {* Main theorem *}
3.61 +
3.62 +text {*
3.63 +  The square root of any prime number (including @{text 2}) is
3.64 +  irrational.
3.65 +*}
3.66 +
3.67 +theorem prime_sqrt_irrational:
3.68 +    "p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
3.69 +  apply (simp add: rationals_def real_abs_def)
3.70 +  apply clarify
3.71 +  apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
3.72 +  apply (simp del: real_of_nat_mult
3.74 +    real_of_nat_mult [symmetric])
3.75 +  done
3.76 +
3.77 +lemmas two_sqrt_irrational = prime_sqrt_irrational [OF two_is_prime]
3.78 +
3.79 +end

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Hyperreal/ex/document/root.tex	Wed Mar 06 17:47:51 2002 +0100
4.3 @@ -0,0 +1,20 @@
4.4 +
4.5 +\documentclass[11pt,a4paper]{article}
4.6 +\usepackage[latin1]{inputenc}
4.7 +\usepackage{isabelle,isabellesym}
4.8 +\usepackage{pdfsetup}
4.9 +
4.10 +\urlstyle{rm}
4.11 +\isabellestyle{it}
4.12 +
4.13 +\begin{document}
4.14 +
4.15 +\title{Miscellaneous HOL-Hyperreal Examples}
4.16 +\maketitle
4.17 +
4.18 +\tableofcontents
4.19 +
4.20 +\parindent 0pt\parskip 0.5ex
4.21 +\input{session}
4.22 +
4.23 +\end{document}

     5.1 --- a/src/HOL/IsaMakefile	Wed Mar 06 16:18:45 2002 +0100
5.2 +++ b/src/HOL/IsaMakefile	Wed Mar 06 17:47:51 2002 +0100
5.3 @@ -22,6 +22,7 @@
5.4        HOL-Real-ex \
5.5    HOL-Hoare \
5.6    HOL-HoareParallel \
5.7 +  HOL-Hyperreal-ex \
5.8    HOL-IMP \
5.9    HOL-IMPP \
5.10    HOL-IOA \
5.11 @@ -123,7 +124,33 @@
5.12  	@cd Real; $(ISATOOL) usedir -b$(OUT)/HOL HOL-Real
5.13
5.14
5.15 -## HOL-Real-Hyperreal
5.16 +## HOL-Real-ex
5.17 +
5.18 +HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz 5.19 + 5.20 +$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \ 5.21 + Real/ex/BinEx.thy Real/ex/document/root.tex 5.22 + @cd Real;$(ISATOOL) usedir $(OUT)/HOL-Real ex 5.23 + 5.24 + 5.25 +## HOL-Real-HahnBanach 5.26 + 5.27 +HOL-Real-HahnBanach: HOL-Real$(LOG)/HOL-Real-HahnBanach.gz
5.28 +
5.29 +$(LOG)/HOL-Real-HahnBanach.gz:$(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
5.30 +  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
5.31 +  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
5.32 +  Real/HahnBanach/HahnBanachExtLemmas.thy	\
5.33 +  Real/HahnBanach/HahnBanachSupLemmas.thy	\
5.34 +  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
5.36 +  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
5.37 +  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
5.38 +  Real/HahnBanach/document/root.tex
5.39 +	@cd Real; $(ISATOOL) usedir -g true$(OUT)/HOL-Real HahnBanach
5.40 +
5.41 +
5.42 +## HOL-Hyperreal
5.43
5.44  HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal 5.45 5.46 @@ -151,31 +178,14 @@ 5.47 @cd Hyperreal;$(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Hyperreal 5.48 5.49 5.50 -## HOL-Real-ex 5.51 - 5.52 -HOL-Real-ex: HOL-Real$(LOG)/HOL-Real-ex.gz
5.53 +## HOL-Hyperreal-ex
5.54
5.55 -$(LOG)/HOL-Real-ex.gz:$(OUT)/HOL-Real Real/ex/ROOT.ML \
5.56 -  Real/ex/BinEx.thy Real/ex/document/root.tex Real/ex/Sqrt.thy \
5.57 -  Real/ex/Sqrt_Script.thy
5.58 -	@cd Real; $(ISATOOL) usedir$(OUT)/HOL-Real ex
5.59 -
5.60 -
5.61 -## HOL-Real-HahnBanach
5.62 +HOL-Hyperreal-ex: HOL-Hyperreal $(LOG)/HOL-Hyperreal-ex.gz 5.63 5.64 -HOL-Real-HahnBanach: HOL-Real$(LOG)/HOL-Real-HahnBanach.gz
5.65 -
5.66 -$(LOG)/HOL-Real-HahnBanach.gz:$(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
5.67 -  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
5.68 -  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
5.69 -  Real/HahnBanach/HahnBanachExtLemmas.thy	\
5.70 -  Real/HahnBanach/HahnBanachSupLemmas.thy	\
5.71 -  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
5.73 -  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
5.74 -  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
5.75 -  Real/HahnBanach/document/root.tex
5.76 -	@cd Real; $(ISATOOL) usedir -g true$(OUT)/HOL-Real HahnBanach
5.77 +$(LOG)/HOL-Hyperreal-ex.gz:$(OUT)/HOL-Hyperreal Hyperreal/ex/ROOT.ML \
5.78 +  Hyperreal/ex/document/root.tex Hyperreal/ex/Sqrt.thy \
5.79 +  Hyperreal/ex/Sqrt_Script.thy
5.80 +	@cd Hyperreal; $(ISATOOL) usedir$(OUT)/HOL-Hyperreal ex
5.81
5.82
5.83  ## HOL-Library
5.84 @@ -301,7 +311,7 @@
5.85    HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy	   \
5.86    HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML		   \
5.87    HoareParallel/document/root.tex
5.88 -	@$(ISATOOL) usedir$(OUT)/HOL HoareParallel
5.89 +	@$(ISATOOL) usedir -g true$(OUT)/HOL HoareParallel
5.90
5.91
5.92  ## HOL-Lex
5.93 @@ -652,6 +662,7 @@
5.94  		$(LOG)/HOL-MicroJava.gz$(LOG)/HOL-NanoJava.gz \
5.95  		$(LOG)/HOL-IOA.gz$(LOG)/HOL-AxClasses \
5.96  		$(LOG)/HOL-Lattice$(LOG)/HOL-Real-ex.gz \
5.97 +		$(LOG)/HOL-Hyperreal-ex.gz \ 5.98$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \ 5.99$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \ 5.100$(LOG)/HOL-Library.gz \$(LOG)/HOL-Unix.gz