--- a/src/HOL/ex/Abstract_NAT.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy Sat Nov 22 14:57:04 2014 +0100
@@ -2,18 +2,18 @@
Author: Makarius
*)
-section {* Abstract Natural Numbers primitive recursion *}
+section \<open>Abstract Natural Numbers primitive recursion\<close>
theory Abstract_NAT
imports Main
begin
-text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
+text \<open>Axiomatic Natural Numbers (Peano) -- a monomorphic theory.\<close>
locale NAT =
fixes zero :: 'n
and succ :: "'n \<Rightarrow> 'n"
- assumes succ_inject [simp]: "(succ m = succ n) = (m = n)"
+ assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n"
and succ_neq_zero [simp]: "succ m \<noteq> zero"
and induct [case_names zero succ, induct type: 'n]:
"P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
@@ -23,7 +23,7 @@
by (rule succ_neq_zero [symmetric])
-text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *}
+text \<open>\medskip Primitive recursion as a (functional) relation -- polymorphic!\<close>
inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -47,7 +47,7 @@
qed
next
case (succ m)
- from `\<exists>!y. ?R m y`
+ from \<open>\<exists>!y. ?R m y\<close>
obtain y where y: "?R m y"
and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
show "\<exists>!z. ?R (succ m) z"
@@ -61,7 +61,7 @@
qed
-text {* \medskip The recursion operator -- polymorphic! *}
+text \<open>\medskip The recursion operator -- polymorphic!\<close>
definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
where "rec e r x = (THE y. Rec e r x y)"
@@ -86,7 +86,7 @@
qed
-text {* \medskip Example: addition (monomorphic) *}
+text \<open>\medskip Example: addition (monomorphic)\<close>
definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
where "add m n = rec n (\<lambda>_ k. succ k) m"
@@ -109,7 +109,7 @@
by simp
-text {* \medskip Example: replication (polymorphic) *}
+text \<open>\medskip Example: replication (polymorphic)\<close>
definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
@@ -124,12 +124,12 @@
end
-text {* \medskip Just see that our abstract specification makes sense \dots *}
+text \<open>\medskip Just see that our abstract specification makes sense \dots\<close>
interpretation NAT 0 Suc
proof (rule NAT.intro)
fix m n
- show "(Suc m = Suc n) = (m = n)" by simp
+ show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
show "Suc m \<noteq> 0" by simp
fix P
assume zero: "P 0"
--- a/src/HOL/ex/Antiquote.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Antiquote.thy Sat Nov 22 14:57:04 2014 +0100
@@ -2,16 +2,13 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Antiquotations *}
+section \<open>Antiquotations\<close>
theory Antiquote
imports Main
begin
-text {*
- A simple example on quote / antiquote in higher-order abstract
- syntax.
-*}
+text \<open>A simple example on quote / antiquote in higher-order abstract syntax.\<close>
definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" ("VAR _" [1000] 999)
where "var x env = env x"
@@ -22,23 +19,21 @@
syntax
"_Expr" :: "'a \<Rightarrow> 'a" ("EXPR _" [1000] 999)
-parse_translation {*
- [Syntax_Trans.quote_antiquote_tr
- @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
-*}
+parse_translation
+ \<open>[Syntax_Trans.quote_antiquote_tr
+ @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close>
-print_translation {*
- [Syntax_Trans.quote_antiquote_tr'
- @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
-*}
+print_translation
+ \<open>[Syntax_Trans.quote_antiquote_tr'
+ @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close>
term "EXPR (a + b + c)"
term "EXPR (a + b + c + VAR x + VAR y + 1)"
term "EXPR (VAR (f w) + VAR x)"
-term "Expr (\<lambda>env. env x)" -- {* improper *}
+term "Expr (\<lambda>env. env x)" -- \<open>improper\<close>
term "Expr (\<lambda>env. f env)"
-term "Expr (\<lambda>env. f env + env x)" -- {* improper *}
+term "Expr (\<lambda>env. f env + env x)" -- \<open>improper\<close>
term "Expr (\<lambda>env. f env y z)"
term "Expr (\<lambda>env. f env + g y env)"
term "Expr (\<lambda>env. f env + g env y + h a env z)"
--- a/src/HOL/ex/Guess.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Guess.thy Sat Nov 22 14:57:04 2014 +0100
@@ -8,9 +8,8 @@
imports Main
begin
-lemma True
-proof
-
+notepad
+begin
have 1: "\<exists>x. x = x" by simp
from 1 guess ..
@@ -18,13 +17,12 @@
from 1 guess x :: 'a ..
from 1 guess x :: nat ..
- have 2: "\<exists>x y. x = x & y = y" by simp
+ have 2: "\<exists>x y. x = x \<and> y = y" by simp
from 2 guess apply - apply (erule exE conjE)+ done
from 2 guess x apply - apply (erule exE conjE)+ done
from 2 guess x y apply - apply (erule exE conjE)+ done
from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
-
-qed
+end
end
--- a/src/HOL/ex/Hebrew.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Hebrew.thy Sat Nov 22 14:57:04 2014 +0100
@@ -4,13 +4,13 @@
formal and informal ones.
*)
-section {* A Hebrew theory *}
+section \<open>A Hebrew theory\<close>
theory Hebrew
imports Main
begin
-text {* The Hebrew Alef-Bet (א-ב). *}
+text \<open>The Hebrew Alef-Bet (א-ב).\<close>
datatype alef_bet =
Alef ("א")
@@ -39,9 +39,10 @@
thm alef_bet.induct
-text {* Interpreting Hebrew letters as numbers. *}
+text \<open>Interpreting Hebrew letters as numbers.\<close>
-primrec mispar :: "alef_bet => nat" where
+primrec mispar :: "alef_bet => nat"
+where
"mispar א = 1"
| "mispar ב = 2"
| "mispar ג = 3"
--- a/src/HOL/ex/Higher_Order_Logic.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy Sat Nov 22 14:57:04 2014 +0100
@@ -2,21 +2,21 @@
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
*)
-section {* Foundations of HOL *}
+section \<open>Foundations of HOL\<close>
theory Higher_Order_Logic imports Pure begin
-text {*
+text \<open>
The following theory development demonstrates Higher-Order Logic
itself, represented directly within the Pure framework of Isabelle.
The ``HOL'' logic given here is essentially that of Gordon
@{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
in a slightly more conventional manner oriented towards plain
Natural Deduction.
-*}
+\<close>
-subsection {* Pure Logic *}
+subsection \<open>Pure Logic\<close>
class type
default_sort type
@@ -26,7 +26,7 @@
instance "fun" :: (type, type) type ..
-subsubsection {* Basic logical connectives *}
+subsubsection \<open>Basic logical connectives\<close>
judgment
Trueprop :: "o \<Rightarrow> prop" ("_" 5)
@@ -41,7 +41,7 @@
allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
-subsubsection {* Extensional equality *}
+subsubsection \<open>Extensional equality\<close>
axiomatization
equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50)
@@ -75,35 +75,26 @@
by (rule subst) (rule sym)
-subsubsection {* Derived connectives *}
+subsubsection \<open>Derived connectives\<close>
-definition
- false :: o ("\<bottom>") where
- "\<bottom> \<equiv> \<forall>A. A"
+definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
-definition
- true :: o ("\<top>") where
- "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
-definition
- not :: "o \<Rightarrow> o" ("\<not> _" [40] 40) where
- "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
+definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
+ where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
-definition
- conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35) where
- "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
+ where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-definition
- disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30) where
- "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
+ where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-definition
- Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10) where
- "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
+ where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-abbreviation
- not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50) where
- "x \<noteq> y \<equiv> \<not> (x = y)"
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)
+ where "x \<noteq> y \<equiv> \<not> (x = y)"
theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
proof (unfold false_def)
@@ -133,7 +124,7 @@
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
by (rule notE)
-lemmas contradiction = notE notE' -- {* proof by contradiction in any order *}
+lemmas contradiction = notE notE' -- \<open>proof by contradiction in any order\<close>
theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
proof (unfold conj_def)
@@ -143,8 +134,8 @@
fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "A \<longrightarrow> B \<longrightarrow> C"
- also note `A`
- also note `B`
+ also note \<open>A\<close>
+ also note \<open>B\<close>
finally show C .
qed
qed
@@ -180,7 +171,7 @@
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "A \<longrightarrow> C"
- also note `A`
+ also note \<open>A\<close>
finally have C .
then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
qed
@@ -197,7 +188,7 @@
show "(B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "B \<longrightarrow> C"
- also note `B`
+ also note \<open>B\<close>
finally show C .
qed
qed
@@ -229,7 +220,7 @@
proof
assume "\<forall>x. P x \<longrightarrow> C"
then have "P a \<longrightarrow> C" ..
- also note `P a`
+ also note \<open>P a\<close>
finally show C .
qed
qed
@@ -252,7 +243,7 @@
qed
-subsection {* Classical logic *}
+subsection \<open>Classical logic\<close>
locale classical =
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
@@ -267,7 +258,7 @@
have "A \<longrightarrow> B"
proof
assume A
- with `\<not> A` show B by (rule contradiction)
+ with \<open>\<not> A\<close> show B by (rule contradiction)
qed
with a show A ..
qed
@@ -280,7 +271,7 @@
show A
proof (rule classical)
assume "\<not> A"
- with `\<not> \<not> A` show ?thesis by (rule contradiction)
+ with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
qed
qed
@@ -293,10 +284,10 @@
have "\<not> A"
proof
assume A then have "A \<or> \<not> A" ..
- with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
+ with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
qed
then have "A \<or> \<not> A" ..
- with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
+ with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
qed
qed
--- a/src/HOL/ex/Multiquote.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Multiquote.thy Sat Nov 22 14:57:04 2014 +0100
@@ -2,22 +2,22 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Multiple nested quotations and anti-quotations *}
+section \<open>Multiple nested quotations and anti-quotations\<close>
theory Multiquote
imports Main
begin
-text {*
+text \<open>
Multiple nested quotations and anti-quotations -- basically a
generalized version of de-Bruijn representation.
-*}
+\<close>
syntax
"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
"_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
-parse_translation {*
+parse_translation \<open>
let
fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
(t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
@@ -33,15 +33,15 @@
fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
| quote_tr ts = raise TERM ("quote_tr", ts);
in [(@{syntax_const "_quote"}, K quote_tr)] end
-*}
+\<close>
-text {* basic examples *}
+text \<open>basic examples\<close>
term "\<guillemotleft>a + b + c\<guillemotright>"
term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
-text {* advanced examples *}
+text \<open>advanced examples\<close>
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
--- a/src/HOL/ex/PER.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/PER.thy Sat Nov 22 14:57:04 2014 +0100
@@ -2,11 +2,13 @@
Author: Oscar Slotosch and Markus Wenzel, TU Muenchen
*)
-section {* Partial equivalence relations *}
+section \<open>Partial equivalence relations\<close>
-theory PER imports Main begin
+theory PER
+imports Main
+begin
-text {*
+text \<open>
Higher-order quotients are defined over partial equivalence
relations (PERs) instead of total ones. We provide axiomatic type
classes @{text "equiv < partial_equiv"} and a type constructor
@@ -17,41 +19,41 @@
Implementation in Isabelle HOL.} Elsa L. Gunter and Amy Felty,
editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
Springer LNCS 1275, 1997.
-*}
+\<close>
-subsection {* Partial equivalence *}
+subsection \<open>Partial equivalence\<close>
-text {*
+text \<open>
Type class @{text partial_equiv} models partial equivalence
- relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
+ relations (PERs) using the polymorphic @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
bool"} relation, which is required to be symmetric and transitive,
but not necessarily reflexive.
-*}
+\<close>
class partial_equiv =
- fixes eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)
- assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
- assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+ fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50)
+ assumes partial_equiv_sym [elim?]: "x \<sim> y \<Longrightarrow> y \<sim> x"
+ assumes partial_equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
-text {*
+text \<open>
\medskip The domain of a partial equivalence relation is the set of
reflexive elements. Due to symmetry and transitivity this
characterizes exactly those elements that are connected with
\emph{any} other one.
-*}
+\<close>
definition
"domain" :: "'a::partial_equiv set" where
"domain = {x. x \<sim> x}"
-lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
+lemma domainI [intro]: "x \<sim> x \<Longrightarrow> x \<in> domain"
unfolding domain_def by blast
-lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
+lemma domainD [dest]: "x \<in> domain \<Longrightarrow> x \<sim> x"
unfolding domain_def by blast
-theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
+theorem domainI' [elim?]: "x \<sim> y \<Longrightarrow> x \<in> domain"
proof
assume xy: "x \<sim> y"
also from xy have "y \<sim> x" ..
@@ -59,35 +61,34 @@
qed
-subsection {* Equivalence on function spaces *}
+subsection \<open>Equivalence on function spaces\<close>
-text {*
+text \<open>
The @{text \<sim>} relation is lifted to function spaces. It is
important to note that this is \emph{not} the direct product, but a
structural one corresponding to the congruence property.
-*}
+\<close>
instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
begin
-definition
- eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
+definition "f \<sim> g \<longleftrightarrow> (\<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y \<longrightarrow> f x \<sim> g y)"
lemma partial_equiv_funI [intro?]:
- "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
+ "(\<And>x y. x \<in> domain \<Longrightarrow> y \<in> domain \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g y) \<Longrightarrow> f \<sim> g"
unfolding eqv_fun_def by blast
lemma partial_equiv_funD [dest?]:
- "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
+ "f \<sim> g \<Longrightarrow> x \<in> domain \<Longrightarrow> y \<in> domain \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g y"
unfolding eqv_fun_def by blast
-text {*
+text \<open>
The class of partial equivalence relations is closed under function
spaces (in \emph{both} argument positions).
-*}
+\<close>
instance proof
- fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
+ fix f g h :: "'a::partial_equiv \<Rightarrow> 'b::partial_equiv"
assume fg: "f \<sim> g"
show "g \<sim> f"
proof
@@ -112,29 +113,29 @@
end
-subsection {* Total equivalence *}
+subsection \<open>Total equivalence\<close>
-text {*
+text \<open>
The class of total equivalence relations on top of PERs. It
coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
- :: 'a => 'a => bool"} is required to be reflexive, transitive and
+ :: 'a \<Rightarrow> 'a \<Rightarrow> bool"} is required to be reflexive, transitive and
symmetric.
-*}
+\<close>
class equiv =
assumes eqv_refl [intro]: "x \<sim> x"
-text {*
+text \<open>
On total equivalences all elements are reflexive, and congruence
holds unconditionally.
-*}
+\<close>
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
proof
show "x \<sim> x" ..
qed
-theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
+theorem equiv_cong [dest?]: "f \<sim> g \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g (y::'a::equiv)"
proof -
assume "f \<sim> g"
moreover have "x \<in> domain" ..
@@ -144,12 +145,12 @@
qed
-subsection {* Quotient types *}
+subsection \<open>Quotient types\<close>
-text {*
+text \<open>
The quotient type @{text "'a quot"} consists of all
\emph{equivalence classes} over elements of the base type @{typ 'a}.
-*}
+\<close>
definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
@@ -159,17 +160,16 @@
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
unfolding quot_def by blast
-lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
+lemma quotE [elim]: "R \<in> quot \<Longrightarrow> (\<And>a. R = {x. a \<sim> x} \<Longrightarrow> C) \<Longrightarrow> C"
unfolding quot_def by blast
-text {*
+text \<open>
\medskip Abstracted equivalence classes are the canonical
representation of elements of a quotient type.
-*}
+\<close>
-definition
- eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") where
- "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
+definition eqv_class :: "('a::partial_equiv) \<Rightarrow> 'a quot" ("\<lfloor>_\<rfloor>")
+ where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
proof (cases A)
@@ -184,19 +184,19 @@
using quot_rep by blast
-subsection {* Equality on quotients *}
+subsection \<open>Equality on quotients\<close>
-text {*
+text \<open>
Equality of canonical quotient elements corresponds to the original
relation as follows.
-*}
+\<close>
-theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
+theorem eqv_class_eqI [intro]: "a \<sim> b \<Longrightarrow> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
proof -
assume ab: "a \<sim> b"
have "{x. a \<sim> x} = {x. b \<sim> x}"
proof (rule Collect_cong)
- fix x show "(a \<sim> x) = (b \<sim> x)"
+ fix x show "a \<sim> x \<longleftrightarrow> b \<sim> x"
proof
from ab have "b \<sim> a" ..
also assume "a \<sim> x"
@@ -210,7 +210,7 @@
then show ?thesis by (simp only: eqv_class_def)
qed
-theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"
+theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<Longrightarrow> a \<in> domain \<Longrightarrow> a \<sim> b"
proof (unfold eqv_class_def)
assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
then have "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
@@ -220,25 +220,24 @@
then show "a \<sim> b" ..
qed
-theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"
+theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<Longrightarrow> a \<sim> (b::'a::equiv)"
proof (rule eqv_class_eqD')
show "a \<in> domain" ..
qed
-lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
+lemma eqv_class_eq' [simp]: "a \<in> domain \<Longrightarrow> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"
using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl)
-lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
+lemma eqv_class_eq [simp]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> (b::'a::equiv)"
using eqv_class_eqI eqv_class_eqD by blast
-subsection {* Picking representing elements *}
+subsection \<open>Picking representing elements\<close>
-definition
- pick :: "'a::partial_equiv quot => 'a" where
- "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
+definition pick :: "'a::partial_equiv quot \<Rightarrow> 'a"
+ where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
-theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a"
+theorem pick_eqv' [intro?, simp]: "a \<in> domain \<Longrightarrow> pick \<lfloor>a\<rfloor> \<sim> a"
proof (unfold pick_def)
assume a: "a \<in> domain"
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
--- a/src/HOL/ex/Sqrt.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Sqrt.thy Sat Nov 22 14:57:04 2014 +0100
@@ -2,19 +2,19 @@
Author: Markus Wenzel, Tobias Nipkow, TU Muenchen
*)
-section {* Square roots of primes are irrational *}
+section \<open>Square roots of primes are irrational\<close>
theory Sqrt
imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
begin
-text {* The square root of any prime number (including 2) is irrational. *}
+text \<open>The square root of any prime number (including 2) is irrational.\<close>
theorem sqrt_prime_irrational:
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from `prime p` have p: "1 < p" by (simp add: prime_nat_def)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -31,12 +31,12 @@
have "p dvd m \<and> p dvd n"
proof
from eq have "p dvd m\<^sup>2" ..
- with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
+ with \<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
then have "p dvd n\<^sup>2" ..
- with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
+ with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
qed
then have "p dvd gcd m n" ..
with gcd have "p dvd 1" by simp
@@ -47,19 +47,20 @@
corollary sqrt_2_not_rat: "sqrt 2 \<notin> \<rat>"
using sqrt_prime_irrational[of 2] by simp
-subsection {* Variations *}
-text {*
+subsection \<open>Variations\<close>
+
+text \<open>
Here is an alternative version of the main proof, using mostly
linear forward-reasoning. While this results in less top-down
structure, it is probably closer to proofs seen in mathematics.
-*}
+\<close>
theorem
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from `prime p` have p: "1 < p" by (simp add: prime_nat_def)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -71,12 +72,12 @@
also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
then have "p dvd m\<^sup>2" ..
- with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
+ with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
then have "p dvd n\<^sup>2" ..
- with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
+ with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
with gcd have "p dvd 1" by simp
then have "p \<le> 1" by (simp add: dvd_imp_le)
@@ -84,9 +85,9 @@
qed
-text {* Another old chestnut, which is a consequence of the irrationality of 2. *}
+text \<open>Another old chestnut, which is a consequence of the irrationality of 2.\<close>
-lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b")
+lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "\<exists>a b. ?P a b")
proof cases
assume "sqrt 2 powr sqrt 2 \<in> \<rat>"
then have "?P (sqrt 2) (sqrt 2)"