author wenzelm Sat, 22 Nov 2014 14:57:04 +0100 changeset 59031 4c3bb56b8ce7 parent 59030 67baff6f697c child 59032 f36496364ce1
misc tuning and modernization;
 src/HOL/ex/Abstract_NAT.thy file | annotate | diff | comparison | revisions src/HOL/ex/Antiquote.thy file | annotate | diff | comparison | revisions src/HOL/ex/Guess.thy file | annotate | diff | comparison | revisions src/HOL/ex/Hebrew.thy file | annotate | diff | comparison | revisions src/HOL/ex/Higher_Order_Logic.thy file | annotate | diff | comparison | revisions src/HOL/ex/Multiquote.thy file | annotate | diff | comparison | revisions src/HOL/ex/PER.thy file | annotate | diff | comparison | revisions src/HOL/ex/Sqrt.thy file | annotate | diff | comparison | revisions
--- 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) *}

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
-
+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>"

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)"