added HOL-Hyperreal-ex;
authorwenzelm
Wed Mar 06 17:47:51 2002 +0100 (2002-03-06)
changeset 1302984e4ba7fb033
parent 13028 81c87faed78b
child 13030 5765aa72afac
added HOL-Hyperreal-ex;
src/HOL/Hyperreal/ex/ROOT.ML
src/HOL/Hyperreal/ex/Sqrt.thy
src/HOL/Hyperreal/ex/Sqrt_Script.thy
src/HOL/Hyperreal/ex/document/root.tex
src/HOL/IsaMakefile
     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.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     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.73 +    add: real_divide_eq_eq prime_not_square
    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.35 +  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
    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.72 -  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
    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