--- a/src/HOL/Lattice/Bounds.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Lattice/Bounds.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,19 +2,19 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Bounds *}
+section \<open>Bounds\<close>
theory Bounds imports Orders begin
hide_const (open) inf sup
-subsection {* Infimum and supremum *}
+subsection \<open>Infimum and supremum\<close>
-text {*
+text \<open>
Given a partial order, we define infimum (greatest lower bound) and
- supremum (least upper bound) wrt.\ @{text \<sqsubseteq>} for two and for any
+ supremum (least upper bound) wrt.\ \<open>\<sqsubseteq>\<close> for two and for any
number of elements.
-*}
+\<close>
definition
is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
@@ -32,10 +32,10 @@
is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool" where
"is_Sup A sup = ((\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z))"
-text {*
+text \<open>
These definitions entail the following basic properties of boundary
elements.
-*}
+\<close>
lemma is_infI [intro?]: "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow>
(\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_inf x y inf"
@@ -89,11 +89,11 @@
by (unfold is_Sup_def) blast
-subsection {* Duality *}
+subsection \<open>Duality\<close>
-text {*
+text \<open>
Infimum and supremum are dual to each other.
-*}
+\<close>
theorem dual_inf [iff?]:
"is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"
@@ -112,12 +112,12 @@
by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
-subsection {* Uniqueness *}
+subsection \<open>Uniqueness\<close>
-text {*
+text \<open>
Infima and suprema on partial orders are unique; this is mainly due
to anti-symmetry of the underlying relation.
-*}
+\<close>
theorem is_inf_uniq: "is_inf x y inf \<Longrightarrow> is_inf x y inf' \<Longrightarrow> inf = inf'"
proof -
@@ -180,11 +180,11 @@
qed
-subsection {* Related elements *}
+subsection \<open>Related elements\<close>
-text {*
+text \<open>
The binary bound of related elements is either one of the argument.
-*}
+\<close>
theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
proof -
@@ -210,11 +210,11 @@
qed
-subsection {* General versus binary bounds \label{sec:gen-bin-bounds} *}
+subsection \<open>General versus binary bounds \label{sec:gen-bin-bounds}\<close>
-text {*
+text \<open>
General bounds of two-element sets coincide with binary bounds.
-*}
+\<close>
theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"
proof -
@@ -284,14 +284,14 @@
qed
-subsection {* Connecting general bounds \label{sec:connect-bounds} *}
+subsection \<open>Connecting general bounds \label{sec:connect-bounds}\<close>
-text {*
+text \<open>
Either kind of general bounds is sufficient to express the other.
The least upper bound (supremum) is the same as the the greatest
lower bound of the set of all upper bounds; the dual statements
holds as well; the dual statement holds as well.
-*}
+\<close>
theorem Inf_Sup: "is_Inf {b. \<forall>a \<in> A. a \<sqsubseteq> b} sup \<Longrightarrow> is_Sup A sup"
proof -
--- a/src/HOL/Lattice/CompleteLattice.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,18 +2,18 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Complete lattices *}
+section \<open>Complete lattices\<close>
theory CompleteLattice imports Lattice begin
-subsection {* Complete lattice operations *}
+subsection \<open>Complete lattice operations\<close>
-text {*
+text \<open>
A \emph{complete lattice} is a partial order with general
(infinitary) infimum of any set of elements. General supremum
exists as well, as a consequence of the connection of infinitary
bounds (see \S\ref{sec:connect-bounds}).
-*}
+\<close>
class complete_lattice =
assumes ex_Inf: "\<exists>inf. is_Inf A inf"
@@ -25,10 +25,10 @@
then show ?thesis ..
qed
-text {*
- The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
+text \<open>
+ The general \<open>\<Sqinter>\<close> (meet) and \<open>\<Squnion>\<close> (join) operations select
such infimum and supremum elements.
-*}
+\<close>
definition
Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) where
@@ -37,16 +37,16 @@
Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) where
"\<Squnion>A = (THE sup. is_Sup A sup)"
-text {*
+text \<open>
Due to unique existence of bounds, the complete lattice operations
may be exhibited as follows.
-*}
+\<close>
lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
proof (unfold Meet_def)
assume "is_Inf A inf"
then show "(THE inf. is_Inf A inf) = inf"
- by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
+ by (rule the_equality) (rule is_Inf_uniq [OF _ \<open>is_Inf A inf\<close>])
qed
lemma MeetI [intro?]:
@@ -59,7 +59,7 @@
proof (unfold Join_def)
assume "is_Sup A sup"
then show "(THE sup. is_Sup A sup) = sup"
- by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
+ by (rule the_equality) (rule is_Sup_uniq [OF _ \<open>is_Sup A sup\<close>])
qed
lemma JoinI [intro?]:
@@ -69,16 +69,16 @@
by (rule Join_equality, rule is_SupI) blast+
-text {*
- \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
+text \<open>
+ \medskip The \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations indeed determine
bounds on a complete lattice structure.
-*}
+\<close>
lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
proof (unfold Meet_def)
from ex_Inf obtain inf where "is_Inf A inf" ..
then show "is_Inf A (THE inf. is_Inf A inf)"
- by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
+ by (rule theI) (rule is_Inf_uniq [OF _ \<open>is_Inf A inf\<close>])
qed
lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -92,7 +92,7 @@
proof (unfold Join_def)
from ex_Sup obtain sup where "is_Sup A sup" ..
then show "is_Sup A (THE sup. is_Sup A sup)"
- by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
+ by (rule theI) (rule is_Sup_uniq [OF _ \<open>is_Sup A sup\<close>])
qed
lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
@@ -101,15 +101,15 @@
by (rule is_Sup_upper) (rule is_Sup_Join)
-subsection {* The Knaster-Tarski Theorem *}
+subsection \<open>The Knaster-Tarski Theorem\<close>
-text {*
+text \<open>
The Knaster-Tarski Theorem (in its simplest formulation) states that
any monotone function on a complete lattice has a least fixed-point
(see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example). This
is a consequence of the basic boundary properties of the complete
lattice operations.
-*}
+\<close>
theorem Knaster_Tarski:
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
@@ -176,12 +176,12 @@
qed
-subsection {* Bottom and top elements *}
+subsection \<open>Bottom and top elements\<close>
-text {*
+text \<open>
With general bounds available, complete lattices also have least and
greatest elements.
-*}
+\<close>
definition
bottom :: "'a::complete_lattice" ("\<bottom>") where
@@ -232,12 +232,12 @@
qed
-subsection {* Duality *}
+subsection \<open>Duality\<close>
-text {*
+text \<open>
The class of complete lattices is closed under formation of dual
structures.
-*}
+\<close>
instance dual :: (complete_lattice) complete_lattice
proof
@@ -250,10 +250,10 @@
qed
qed
-text {*
- Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
+text \<open>
+ Apparently, the \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations are dual to each
other.
-*}
+\<close>
theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
proof -
@@ -269,9 +269,9 @@
then show ?thesis ..
qed
-text {*
- Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
-*}
+text \<open>
+ Likewise are \<open>\<bottom>\<close> and \<open>\<top>\<close> duals of each other.
+\<close>
theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
proof -
@@ -296,14 +296,14 @@
qed
-subsection {* Complete lattices are lattices *}
+subsection \<open>Complete lattices are lattices\<close>
-text {*
+text \<open>
Complete lattices (with general bounds available) are indeed plain
lattices as well. This holds due to the connection of general
versus binary bounds that has been formally established in
\S\ref{sec:gen-bin-bounds}.
-*}
+\<close>
lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
proof -
@@ -331,12 +331,12 @@
by (rule join_equality) (rule is_sup_binary)
-subsection {* Complete lattices and set-theory operations *}
+subsection \<open>Complete lattices and set-theory operations\<close>
-text {*
+text \<open>
The complete lattice operations are (anti) monotone wrt.\ set
inclusion.
-*}
+\<close>
theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
proof (rule Meet_greatest)
@@ -355,9 +355,9 @@
then show ?thesis by (simp only: dual_leq)
qed
-text {*
+text \<open>
Bounds over unions of sets may be obtained separately.
-*}
+\<close>
theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
proof
@@ -404,9 +404,9 @@
finally show ?thesis ..
qed
-text {*
+text \<open>
Bounds over singleton sets are trivial.
-*}
+\<close>
theorem Meet_singleton: "\<Sqinter>{x} = x"
proof
@@ -425,9 +425,9 @@
finally show ?thesis ..
qed
-text {*
+text \<open>
Bounds over the empty and universal set correspond to each other.
-*}
+\<close>
theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"
proof
--- a/src/HOL/Lattice/Lattice.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Lattice/Lattice.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,26 +2,26 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Lattices *}
+section \<open>Lattices\<close>
theory Lattice imports Bounds begin
-subsection {* Lattice operations *}
+subsection \<open>Lattice operations\<close>
-text {*
+text \<open>
A \emph{lattice} is a partial order with infimum and supremum of any
two elements (thus any \emph{finite} number of elements have bounds
as well).
-*}
+\<close>
class lattice =
assumes ex_inf: "\<exists>inf. is_inf x y inf"
assumes ex_sup: "\<exists>sup. is_sup x y sup"
-text {*
- The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
+text \<open>
+ The \<open>\<sqinter>\<close> (meet) and \<open>\<squnion>\<close> (join) operations select such
infimum and supremum elements.
-*}
+\<close>
definition
meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) where
@@ -30,16 +30,16 @@
join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) where
"x \<squnion> y = (THE sup. is_sup x y sup)"
-text {*
+text \<open>
Due to unique existence of bounds, the lattice operations may be
exhibited as follows.
-*}
+\<close>
lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
proof (unfold meet_def)
assume "is_inf x y inf"
then show "(THE inf. is_inf x y inf) = inf"
- by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`])
+ by (rule the_equality) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])
qed
lemma meetI [intro?]:
@@ -50,7 +50,7 @@
proof (unfold join_def)
assume "is_sup x y sup"
then show "(THE sup. is_sup x y sup) = sup"
- by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`])
+ by (rule the_equality) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])
qed
lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
@@ -58,16 +58,16 @@
by (rule join_equality, rule is_supI) blast+
-text {*
- \medskip The @{text \<sqinter>} and @{text \<squnion>} operations indeed determine
+text \<open>
+ \medskip The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations indeed determine
bounds on a lattice structure.
-*}
+\<close>
lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
proof (unfold meet_def)
from ex_inf obtain inf where "is_inf x y inf" ..
then show "is_inf x y (THE inf. is_inf x y inf)"
- by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`])
+ by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])
qed
lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
@@ -84,7 +84,7 @@
proof (unfold join_def)
from ex_sup obtain sup where "is_sup x y sup" ..
then show "is_sup x y (THE sup. is_sup x y sup)"
- by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`])
+ by (rule theI) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])
qed
lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
@@ -97,14 +97,14 @@
by (rule is_sup_upper) (rule is_sup_join)
-subsection {* Duality *}
+subsection \<open>Duality\<close>
-text {*
+text \<open>
The class of lattices is closed under formation of dual structures.
This means that for any theorem of lattice theory, the dualized
statement holds as well; this important fact simplifies many proofs
of lattice theory.
-*}
+\<close>
instance dual :: (lattice) lattice
proof
@@ -125,10 +125,10 @@
qed
qed
-text {*
- Apparently, the @{text \<sqinter>} and @{text \<squnion>} operations are dual to each
+text \<open>
+ Apparently, the \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are dual to each
other.
-*}
+\<close>
theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
proof -
@@ -145,13 +145,13 @@
qed
-subsection {* Algebraic properties \label{sec:lattice-algebra} *}
+subsection \<open>Algebraic properties \label{sec:lattice-algebra}\<close>
-text {*
- The @{text \<sqinter>} and @{text \<squnion>} operations have the following
+text \<open>
+ The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations have the following
characteristic algebraic properties: associative (A), commutative
(C), and absorptive (AB).
-*}
+\<close>
theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
proof
@@ -239,10 +239,10 @@
then show ?thesis ..
qed
-text {*
+text \<open>
\medskip Some further algebraic properties hold as well. The
property idempotent (I) is a basic algebraic consequence of (AB).
-*}
+\<close>
theorem meet_idem: "x \<sqinter> x = x"
proof -
@@ -260,9 +260,9 @@
then show ?thesis ..
qed
-text {*
+text \<open>
Meet and join are trivial for related elements.
-*}
+\<close>
theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
proof
@@ -283,12 +283,12 @@
qed
-subsection {* Order versus algebraic structure *}
+subsection \<open>Order versus algebraic structure\<close>
-text {*
- The @{text \<sqinter>} and @{text \<squnion>} operations are connected with the
- underlying @{text \<sqsubseteq>} relation in a canonical manner.
-*}
+text \<open>
+ The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are connected with the
+ underlying \<open>\<sqsubseteq>\<close> relation in a canonical manner.
+\<close>
theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
proof
@@ -312,28 +312,28 @@
finally show "x \<sqsubseteq> y" .
qed
-text {*
+text \<open>
\medskip The most fundamental result of the meta-theory of lattices
is as follows (we do not prove it here).
- Given a structure with binary operations @{text \<sqinter>} and @{text \<squnion>}
+ Given a structure with binary operations \<open>\<sqinter>\<close> and \<open>\<squnion>\<close>
such that (A), (C), and (AB) hold (cf.\
\S\ref{sec:lattice-algebra}). This structure represents a lattice,
if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}
(alternatively as @{term "x \<squnion> y = y"}). Furthermore, infimum and
supremum with respect to this ordering coincide with the original
- @{text \<sqinter>} and @{text \<squnion>} operations.
-*}
+ \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations.
+\<close>
-subsection {* Example instances *}
+subsection \<open>Example instances\<close>
-subsubsection {* Linear orders *}
+subsubsection \<open>Linear orders\<close>
-text {*
+text \<open>
Linear orders with @{term minimum} and @{term maximum} operations
are a (degenerate) example of lattice structures.
-*}
+\<close>
definition
minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
@@ -367,10 +367,10 @@
from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
qed
-text {*
+text \<open>
The lattice operations on linear orders indeed coincide with @{term
minimum} and @{term maximum}.
-*}
+\<close>
theorem meet_mimimum: "x \<sqinter> y = minimum x y"
by (rule meet_equality) (rule is_inf_minimum)
@@ -380,12 +380,12 @@
-subsubsection {* Binary products *}
+subsubsection \<open>Binary products\<close>
-text {*
+text \<open>
The class of lattices is closed under direct binary products (cf.\
\S\ref{sec:prod-order}).
-*}
+\<close>
lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
proof
@@ -456,10 +456,10 @@
from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
qed
-text {*
+text \<open>
The lattice operations on a binary product structure indeed coincide
with the products of the original ones.
-*}
+\<close>
theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
by (rule meet_equality) (rule is_inf_prod)
@@ -468,12 +468,12 @@
by (rule join_equality) (rule is_sup_prod)
-subsubsection {* General products *}
+subsubsection \<open>General products\<close>
-text {*
+text \<open>
The class of lattices is closed under general products (function
spaces) as well (cf.\ \S\ref{sec:fun-order}).
-*}
+\<close>
lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"
proof
@@ -526,10 +526,10 @@
show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
qed
-text {*
+text \<open>
The lattice operations on a general product structure (function
space) indeed emerge by point-wise lifting of the original ones.
-*}
+\<close>
theorem meet_fun: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
by (rule meet_equality) (rule is_inf_fun)
@@ -538,13 +538,13 @@
by (rule join_equality) (rule is_sup_fun)
-subsection {* Monotonicity and semi-morphisms *}
+subsection \<open>Monotonicity and semi-morphisms\<close>
-text {*
+text \<open>
The lattice operations are monotone in both argument positions. In
fact, monotonicity of the second position is trivial due to
commutativity.
-*}
+\<close>
theorem meet_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"
proof -
@@ -576,12 +576,12 @@
then show ?thesis ..
qed
-text {*
- \medskip A semi-morphisms is a function @{text f} that preserves the
+text \<open>
+ \medskip A semi-morphisms is a function \<open>f\<close> that preserves the
lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
\<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively. Any of
these properties is equivalent with monotonicity.
-*}
+\<close>
theorem meet_semimorph:
"(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
@@ -615,7 +615,7 @@
assume "x \<sqsubseteq> y" then have "x \<squnion> y = y" ..
have "f x \<sqsubseteq> f x \<squnion> f y" ..
also have "\<dots> \<sqsubseteq> f (x \<squnion> y)" by (rule morph)
- also from `x \<sqsubseteq> y` have "x \<squnion> y = y" ..
+ also from \<open>x \<sqsubseteq> y\<close> have "x \<squnion> y = y" ..
finally show "f x \<sqsubseteq> f y" .
next
assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
--- a/src/HOL/Lattice/Orders.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Lattice/Orders.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,20 +2,20 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Orders *}
+section \<open>Orders\<close>
theory Orders imports Main begin
-subsection {* Ordered structures *}
+subsection \<open>Ordered structures\<close>
-text {*
+text \<open>
We define several classes of ordered structures over some type @{typ
- 'a} with relation @{text "\<sqsubseteq> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}. For a
+ 'a} with relation \<open>\<sqsubseteq> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>. For a
\emph{quasi-order} that relation is required to be reflexive and
transitive, for a \emph{partial order} it also has to be
anti-symmetric, while for a \emph{linear order} all elements are
required to be related (in either direction).
-*}
+\<close>
class leq =
fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
@@ -35,13 +35,13 @@
by (insert leq_linear) blast
-subsection {* Duality *}
+subsection \<open>Duality\<close>
-text {*
+text \<open>
The \emph{dual} of an ordered structure is an isomorphic copy of the
- underlying type, with the @{text \<sqsubseteq>} relation defined as the inverse
+ underlying type, with the \<open>\<sqsubseteq>\<close> relation defined as the inverse
of the original one.
-*}
+\<close>
datatype 'a dual = dual 'a
@@ -64,10 +64,10 @@
lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"
by (simp add: leq_dual_def)
-text {*
+text \<open>
\medskip Functions @{term dual} and @{term undual} are inverse to
each other; this entails the following fundamental properties.
-*}
+\<close>
lemma dual_undual [simp]: "dual (undual x') = x'"
by (cases x') simp
@@ -78,11 +78,11 @@
lemma dual_undual_id [simp]: "dual o undual = id"
by (rule ext) simp
-text {*
+text \<open>
\medskip Since @{term dual} (and @{term undual}) are both injective
and surjective, the basic logical connectives (equality,
quantification etc.) are transferred as follows.
-*}
+\<close>
lemma undual_equality [iff?]: "(undual x' = undual y') = (x' = y')"
by (cases x', cases y') simp
@@ -143,14 +143,14 @@
qed
-subsection {* Transforming orders *}
+subsection \<open>Transforming orders\<close>
-subsubsection {* Duals *}
+subsubsection \<open>Duals\<close>
-text {*
+text \<open>
The classes of quasi, partial, and linear orders are all closed
under formation of dual structures.
-*}
+\<close>
instance dual :: (quasi_order) quasi_order
proof
@@ -183,13 +183,13 @@
qed
-subsubsection {* Binary products \label{sec:prod-order} *}
+subsubsection \<open>Binary products \label{sec:prod-order}\<close>
-text {*
+text \<open>
The classes of quasi and partial orders are closed under binary
products. Note that the direct product of linear orders need
\emph{not} be linear in general.
-*}
+\<close>
instantiation prod :: (leq, leq) leq
begin
@@ -245,13 +245,13 @@
qed
-subsubsection {* General products \label{sec:fun-order} *}
+subsubsection \<open>General products \label{sec:fun-order}\<close>
-text {*
+text \<open>
The classes of quasi and partial orders are closed under general
products (function spaces). Note that the direct product of linear
orders need \emph{not} be linear in general.
-*}
+\<close>
instantiation "fun" :: (type, leq) leq
begin
--- a/src/HOL/Proofs/Extraction/Euclid.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Wed Dec 30 18:25:39 2015 +0100
@@ -4,7 +4,7 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* Euclid's theorem *}
+section \<open>Euclid's theorem\<close>
theory Euclid
imports
@@ -13,10 +13,10 @@
"~~/src/HOL/Library/Code_Target_Numeral"
begin
-text {*
+text \<open>
A constructive version of the proof of Euclid's theorem by
Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
-*}
+\<close>
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
by (induct m) auto
@@ -109,10 +109,10 @@
then show ?case by simp
next
case (Suc n)
- from `m \<le> Suc n` show ?case
+ from \<open>m \<le> Suc n\<close> show ?case
proof (rule le_SucE)
assume "m \<le> n"
- with `0 < m` have "m dvd fact n" by (rule Suc)
+ with \<open>0 < m\<close> have "m dvd fact n" by (rule Suc)
then have "m dvd (fact n * Suc n)" by (rule dvd_mult2)
then show ?thesis by (simp add: mult.commute)
next
@@ -155,13 +155,13 @@
lemma all_prime_nempty_g_one:
assumes "all_prime ps" and "ps \<noteq> []"
shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)"
- using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
+ using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close> unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
(simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
proof (induct n rule: nat_wf_ind)
case (1 n)
- from `Suc 0 < n`
+ from \<open>Suc 0 < n\<close>
have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
by (rule not_prime_ex_mk)
then show ?case
@@ -175,7 +175,7 @@
from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" by (rule 1)
then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k"
by iprover
- from `all_prime ps1` `all_prime ps2`
+ from \<open>all_prime ps1\<close> \<open>all_prime ps2\<close>
have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) =
(\<Prod>m::nat \<in># mset ps1. m) * (\<Prod>m::nat \<in># mset ps2. m)"
by (rule split_all_prime)
@@ -198,15 +198,15 @@
with N have "ps \<noteq> []"
by (auto simp add: all_prime_nempty_g_one msetprod_empty)
then obtain p qs where ps: "ps = p # qs" by (cases ps) simp
- with `all_prime ps` have "prime p" by (simp add: all_prime_simps)
- moreover from `all_prime ps` ps prod_ps
+ with \<open>all_prime ps\<close> have "prime p" by (simp add: all_prime_simps)
+ moreover from \<open>all_prime ps\<close> ps prod_ps
have "p dvd n" by (simp only: dvd_prod)
ultimately show ?thesis by iprover
qed
-text {*
+text \<open>
Euclid's theorem: there are infinitely many primes.
-*}
+\<close>
lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
proof -
@@ -218,7 +218,7 @@
have "\<not> p \<le> n"
proof
assume pn: "p \<le> n"
- from `prime p` have "0 < p" by (rule prime_gt_0_nat)
+ from \<open>prime p\<close> have "0 < p" by (rule prime_gt_0_nat)
then have "p dvd fact n" using pn by (rule dvd_factorial)
with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat)
then have "p dvd 1" by simp
@@ -231,12 +231,12 @@
extract Euclid
-text {*
+text \<open>
The program extracted from the proof of Euclid's theorem looks as follows.
@{thm [display] Euclid_def}
The program corresponding to the proof of the factorization theorem is
@{thm [display] factor_exists_def}
-*}
+\<close>
instantiation nat :: default
begin
--- a/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,7 +3,7 @@
Author: Helmut Schwichtenberg, LMU Muenchen
*)
-section {* Greatest common divisor *}
+section \<open>Greatest common divisor\<close>
theory Greatest_Common_Divisor
imports QuotRem
@@ -55,10 +55,10 @@
extract greatest_common_divisor
-text {*
+text \<open>
The extracted program for computing the greatest common divisor is
@{thm [display] greatest_common_divisor_def}
-*}
+\<close>
instantiation nat :: default
begin
--- a/src/HOL/Proofs/Extraction/Higman.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,16 +3,16 @@
Author: Monika Seisenberger, LMU Muenchen
*)
-section {* Higman's lemma *}
+section \<open>Higman's lemma\<close>
theory Higman
imports Old_Datatype
begin
-text {*
+text \<open>
Formalization by Stefan Berghofer and Monika Seisenberger,
based on Coquand and Fridlender @{cite Coquand93}.
-*}
+\<close>
datatype letter = A | B
@@ -279,9 +279,9 @@
thus ?case by (rule bar2)
qed
-text {*
+text \<open>
Strong version: yields indices of words that can be embedded into each other.
-*}
+\<close>
theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"
proof (rule bar_idx)
@@ -289,10 +289,10 @@
show "is_prefix [] f" by simp
qed
-text {*
+text \<open>
Weak version: only yield sequence containing words
that can be embedded into each other.
-*}
+\<close>
theorem good_prefix_lemma:
assumes bar: "bar ws"
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Wed Dec 30 18:25:39 2015 +0100
@@ -9,7 +9,7 @@
begin
(*>*)
-subsection {* Extracting the program *}
+subsection \<open>Extracting the program\<close>
declare R.induct [ind_realizer]
declare T.induct [ind_realizer]
@@ -19,23 +19,23 @@
extract higman_idx
-text {*
- Program extracted from the proof of @{text higman_idx}:
+text \<open>
+ Program extracted from the proof of \<open>higman_idx\<close>:
@{thm [display] higman_idx_def [no_vars]}
Corresponding correctness theorem:
@{thm [display] higman_idx_correctness [no_vars]}
- Program extracted from the proof of @{text higman}:
+ Program extracted from the proof of \<open>higman\<close>:
@{thm [display] higman_def [no_vars]}
- Program extracted from the proof of @{text prop1}:
+ Program extracted from the proof of \<open>prop1\<close>:
@{thm [display] prop1_def [no_vars]}
- Program extracted from the proof of @{text prop2}:
+ Program extracted from the proof of \<open>prop2\<close>:
@{thm [display] prop2_def [no_vars]}
- Program extracted from the proof of @{text prop3}:
+ Program extracted from the proof of \<open>prop3\<close>:
@{thm [display] prop3_def [no_vars]}
-*}
+\<close>
-subsection {* Some examples *}
+subsection \<open>Some examples\<close>
instantiation LT and TT :: default
begin
@@ -88,7 +88,7 @@
| "f2 (Suc (Suc 0)) = [B, A]"
| "f2 _ = []"
-ML_val {*
+ML_val \<open>
local
val higman_idx = @{code higman_idx};
val g1 = @{code g1};
@@ -105,6 +105,6 @@
val (i4, j4) = higman_idx f2;
val (v4, w4) = (f2 i4, f2 j4);
end;
-*}
+\<close>
end
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,20 +2,20 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* The pigeonhole principle *}
+section \<open>The pigeonhole principle\<close>
theory Pigeonhole
imports Util "~~/src/HOL/Library/Code_Target_Numeral"
begin
-text {*
+text \<open>
We formalize two proofs of the pigeonhole principle, which lead
to extracted programs of quite different complexity. The original
formalization of these proofs in {\sc Nuprl} is due to
Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
This proof yields a polynomial program.
-*}
+\<close>
theorem pigeonhole:
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
@@ -131,10 +131,10 @@
show ?case by (rule r) simp_all
qed
-text {*
+text \<open>
The following proof, although quite elegant from a mathematical point of view,
leads to an exponential program:
-*}
+\<close>
theorem pigeonhole_slow:
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
@@ -205,7 +205,7 @@
extract pigeonhole pigeonhole_slow
-text {*
+text \<open>
The programs extracted from the above proofs look as follows:
@{thm [display] pigeonhole_def}
@{thm [display] pigeonhole_slow_def}
@@ -216,7 +216,7 @@
In order to analyze the speed of the above programs,
we generate ML code from them.
-*}
+\<close>
instantiation nat :: default
begin
--- a/src/HOL/Proofs/Extraction/QuotRem.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,13 +2,13 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* Quotient and remainder *}
+section \<open>Quotient and remainder\<close>
theory QuotRem
imports Util
begin
-text {* Derivation of quotient and remainder using program extraction. *}
+text \<open>Derivation of quotient and remainder using program extraction.\<close>
theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
proof (induct a)
@@ -25,7 +25,7 @@
thus ?case by iprover
next
assume "r \<noteq> b"
- with `r \<le> b` have "r < b" by (simp add: order_less_le)
+ with \<open>r \<le> b\<close> have "r < b" by (simp add: order_less_le)
with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
thus ?case by iprover
qed
@@ -33,12 +33,12 @@
extract division
-text {*
+text \<open>
The program extracted from the above proof looks as follows
@{thm [display] division_def [no_vars]}
The corresponding correctness theorem is
@{thm [display] division_correctness [no_vars]}
-*}
+\<close>
lemma "division 9 2 = (0, 3)" by eval
--- a/src/HOL/Proofs/Extraction/Util.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Util.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,15 +2,15 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* Auxiliary lemmas used in program extraction examples *}
+section \<open>Auxiliary lemmas used in program extraction examples\<close>
theory Util
imports "~~/src/HOL/Library/Old_Datatype"
begin
-text {*
+text \<open>
Decidability of equality on natural numbers.
-*}
+\<close>
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
apply (induct m)
@@ -19,10 +19,10 @@
apply (simp only: nat.simps, iprover?)+
done
-text {*
+text \<open>
Well-founded induction on natural numbers, derived using the standard
structural induction rule.
-*}
+\<close>
lemma nat_wf_ind:
assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
@@ -48,9 +48,9 @@
qed
qed
-text {*
+text \<open>
Bounded search for a natural number satisfying a decidable predicate.
-*}
+\<close>
lemma search:
assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
--- a/src/HOL/Proofs/Extraction/Warshall.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,16 +2,16 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* Warshall's algorithm *}
+section \<open>Warshall's algorithm\<close>
theory Warshall
imports Old_Datatype
begin
-text {*
+text \<open>
Derivation of Warshall's algorithm using program extraction,
based on Berger, Schwichtenberg and Seisenberger @{cite "Berger-JAR-2001"}.
-*}
+\<close>
datatype b = T | F
@@ -251,12 +251,12 @@
extract warshall
-text {*
+text \<open>
The program extracted from the above proof looks as follows
@{thm [display, eta_contract=false] warshall_def [no_vars]}
The corresponding correctness theorem is
@{thm [display] warshall_correctness [no_vars]}
-*}
+\<close>
ML_val "@{code warshall}"
--- a/src/HOL/Proofs/Lambda/Commutation.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/Commutation.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,7 +3,7 @@
Copyright 1995 TU Muenchen
*)
-section {* Abstract commutation and confluence notions *}
+section \<open>Abstract commutation and confluence notions\<close>
theory Commutation
imports Main
@@ -12,7 +12,7 @@
declare [[syntax_ambiguity_warning = false]]
-subsection {* Basic definitions *}
+subsection \<open>Basic definitions\<close>
definition
square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
@@ -37,9 +37,9 @@
"confluent R == diamond (R^**)"
-subsection {* Basic lemmas *}
+subsection \<open>Basic lemmas\<close>
-subsubsection {* @{text "square"} *}
+subsubsection \<open>\<open>square\<close>\<close>
lemma square_sym: "square R S T U ==> square S R U T"
apply (unfold square_def)
@@ -74,7 +74,7 @@
done
-subsubsection {* @{text "commute"} *}
+subsubsection \<open>\<open>commute\<close>\<close>
lemma commute_sym: "commute R S ==> commute S R"
apply (unfold commute_def)
@@ -93,7 +93,7 @@
done
-subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
+subsubsection \<open>\<open>diamond\<close>, \<open>confluence\<close>, and \<open>union\<close>\<close>
lemma diamond_Un:
"[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
@@ -125,25 +125,25 @@
done
-subsection {* Church-Rosser *}
+subsection \<open>Church-Rosser\<close>
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
apply (unfold square_def commute_def diamond_def Church_Rosser_def)
- apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
- apply (tactic {*
+ apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
+ apply (tactic \<open>
blast_tac (put_claset HOL_cs @{context} addIs
[@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
@{thm rtranclp_converseI}, @{thm conversepI},
- @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
+ @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1\<close>)
apply (erule rtranclp_induct)
apply blast
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
done
-subsection {* Newman's lemma *}
+subsection \<open>Newman's lemma\<close>
-text {* Proof by Stefan Berghofer *}
+text \<open>Proof by Stefan Berghofer\<close>
theorem newman:
assumes wf: "wfP (R\<inverse>\<inverse>)"
@@ -189,12 +189,12 @@
qed
qed
-text {*
+text \<open>
Alternative version. Partly automated by Tobias
Nipkow. Takes 2 minutes (2002).
- This is the maximal amount of automation possible using @{text blast}.
-*}
+ This is the maximal amount of automation possible using \<open>blast\<close>.
+\<close>
theorem newman':
assumes wf: "wfP (R\<inverse>\<inverse>)"
@@ -205,8 +205,8 @@
using wf
proof induct
case (less x b c)
- note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
- \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+ note IH = \<open>\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+ \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d\<close>
have xc: "R\<^sup>*\<^sup>* x c" by fact
have xb: "R\<^sup>*\<^sup>* x b" by fact
thus ?case
@@ -237,10 +237,10 @@
qed
qed
-text {*
+text \<open>
Using the coherent logic prover, the proof of the induction step
is completely automatic.
-*}
+\<close>
lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
by simp
@@ -254,11 +254,11 @@
using wf
proof induct
case (less x b c)
- note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
- \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+ note IH = \<open>\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+ \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d\<close>
show ?case
by (coherent
- `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
+ \<open>R\<^sup>*\<^sup>* x c\<close> \<open>R\<^sup>*\<^sup>* x b\<close>
refl [where 'a='a] sym
eq_imp_rtranclp
r_into_rtranclp [of R]
--- a/src/HOL/Proofs/Lambda/Eta.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/Eta.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,12 +3,12 @@
Copyright 1995, 2005 TU Muenchen
*)
-section {* Eta-reduction *}
+section \<open>Eta-reduction\<close>
theory Eta imports ParRed begin
-subsection {* Definition of eta-reduction and relatives *}
+subsection \<open>Definition of eta-reduction and relatives\<close>
primrec
free :: "dB => nat => bool"
@@ -39,7 +39,7 @@
"Var i \<rightarrow>\<^sub>\<eta> t"
-subsection {* Properties of @{text "eta"}, @{text "subst"} and @{text "free"} *}
+subsection \<open>Properties of \<open>eta\<close>, \<open>subst\<close> and \<open>free\<close>\<close>
lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
by (induct s arbitrary: i t u) (simp_all add: subst_Var)
@@ -77,7 +77,7 @@
by (induct s arbitrary: i dummy) simp_all
-subsection {* Confluence of @{text "eta"} *}
+subsection \<open>Confluence of \<open>eta\<close>\<close>
lemma square_eta: "square eta eta (eta^==) (eta^==)"
apply (unfold square_def id_def)
@@ -95,7 +95,7 @@
done
-subsection {* Congruence rules for @{text "eta\<^sup>*"} *}
+subsection \<open>Congruence rules for \<open>eta\<^sup>*\<close>\<close>
lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'"
by (induct set: rtranclp)
@@ -113,7 +113,7 @@
by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans)
-subsection {* Commutation of @{text "beta"} and @{text "eta"} *}
+subsection \<open>Commutation of \<open>beta\<close> and \<open>eta\<close>\<close>
lemma free_beta:
"s \<rightarrow>\<^sub>\<beta> t ==> free t i \<Longrightarrow> free s i"
@@ -167,9 +167,9 @@
done
-subsection {* Implicit definition of @{text "eta"} *}
+subsection \<open>Implicit definition of \<open>eta\<close>\<close>
-text {* @{term "Abs (lift s 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s"} *}
+text \<open>@{term "Abs (lift s 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s"}\<close>
lemma not_free_iff_lifted:
"(\<not> free s i) = (\<exists>t. s = lift t i)"
@@ -226,13 +226,13 @@
by (auto simp add: not_free_iff_lifted)
-subsection {* Eta-postponement theorem *}
+subsection \<open>Eta-postponement theorem\<close>
-text {*
+text \<open>
Based on a paper proof due to Andreas Abel.
Unlike the proof by Masako Takahashi @{cite "Takahashi-IandC"}, it does not
use parallel eta reduction, which only seems to complicate matters unnecessarily.
-*}
+\<close>
theorem eta_case:
fixes s :: dB
@@ -260,17 +260,17 @@
next
case (abs s' t)
note abs' = this
- from `s \<rightarrow>\<^sub>\<eta> Abs s'` show ?case
+ from \<open>s \<rightarrow>\<^sub>\<eta> Abs s'\<close> show ?case
proof cases
case (eta s'' dummy)
from abs have "Abs s' => Abs t" by simp
with eta have "s''[dummy/0] => Abs t" by simp
- with `\<not> free s'' 0` have "\<exists>t'. Abs (s'' \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t"
+ with \<open>\<not> free s'' 0\<close> have "\<exists>t'. Abs (s'' \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t"
by (rule eta_case)
with eta show ?thesis by simp
next
case (abs r)
- from `r \<rightarrow>\<^sub>\<eta> s'`
+ from \<open>r \<rightarrow>\<^sub>\<eta> s'\<close>
obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
from r have "Abs r => Abs t'" ..
moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs)
@@ -278,24 +278,24 @@
qed
next
case (app u u' t t')
- from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case
+ from \<open>s \<rightarrow>\<^sub>\<eta> u \<degree> t\<close> show ?case
proof cases
case (eta s' dummy)
from app have "u \<degree> t => u' \<degree> t'" by simp
with eta have "s'[dummy/0] => u' \<degree> t'" by simp
- with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'"
+ with \<open>\<not> free s' 0\<close> have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'"
by (rule eta_case)
with eta show ?thesis by simp
next
case (appL s')
- from `s' \<rightarrow>\<^sub>\<eta> u`
+ from \<open>s' \<rightarrow>\<^sub>\<eta> u\<close>
obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
from s' and app have "s' \<degree> t => r \<degree> t'" by simp
moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL)
ultimately show ?thesis using appL by simp iprover
next
case (appR s')
- from `s' \<rightarrow>\<^sub>\<eta> t`
+ from \<open>s' \<rightarrow>\<^sub>\<eta> t\<close>
obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
from s' and app have "u \<degree> s' => u' \<degree> r" by simp
moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR)
@@ -303,17 +303,17 @@
qed
next
case (beta u u' t t')
- from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case
+ from \<open>s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t\<close> show ?case
proof cases
case (eta s' dummy)
from beta have "Abs u \<degree> t => u'[t'/0]" by simp
with eta have "s'[dummy/0] => u'[t'/0]" by simp
- with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
+ with \<open>\<not> free s' 0\<close> have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
by (rule eta_case)
with eta show ?thesis by simp
next
case (appL s')
- from `s' \<rightarrow>\<^sub>\<eta> Abs u` show ?thesis
+ from \<open>s' \<rightarrow>\<^sub>\<eta> Abs u\<close> show ?thesis
proof cases
case (eta s'' dummy)
have "Abs (lift u 1) = lift (Abs u) 0" by simp
@@ -323,12 +323,12 @@
hence "Abs (lift u 1) \<degree> Var 0 => lift u' 1[Var 0/0]"
using par_beta.var ..
hence "Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t => lift u' 1[Var 0/0][t'/0]"
- using `t => t'` ..
+ using \<open>t => t'\<close> ..
with s have "s => u'[t'/0]" by simp
thus ?thesis by iprover
next
case (abs r)
- from `r \<rightarrow>\<^sub>\<eta> u`
+ from \<open>r \<rightarrow>\<^sub>\<eta> u\<close>
obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp
moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
@@ -337,7 +337,7 @@
qed
next
case (appR s')
- from `s' \<rightarrow>\<^sub>\<eta> t`
+ from \<open>s' \<rightarrow>\<^sub>\<eta> t\<close>
obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp
moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
--- a/src/HOL/Proofs/Lambda/InductTermi.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/InductTermi.thy Wed Dec 30 18:25:39 2015 +0100
@@ -7,11 +7,11 @@
rediscovered by Matthes and Joachimski.
*)
-section {* Inductive characterization of terminating lambda terms *}
+section \<open>Inductive characterization of terminating lambda terms\<close>
theory InductTermi imports ListBeta begin
-subsection {* Terminating lambda terms *}
+subsection \<open>Terminating lambda terms\<close>
inductive IT :: "dB => bool"
where
@@ -20,7 +20,7 @@
| Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
-subsection {* Every term in @{text "IT"} terminates *}
+subsection \<open>Every term in \<open>IT\<close> terminates\<close>
lemma double_induction_lemma [rule_format]:
"termip beta s ==> \<forall>t. termip beta t -->
@@ -54,7 +54,7 @@
done
-subsection {* Every terminating term is in @{text "IT"} *}
+subsection \<open>Every terminating term is in \<open>IT\<close>\<close>
declare Var_apps_neq_Abs_apps [symmetric, simp]
--- a/src/HOL/Proofs/Lambda/Lambda.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/Lambda.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,7 +3,7 @@
Copyright 1995 TU Muenchen
*)
-section {* Basic definitions of Lambda-calculus *}
+section \<open>Basic definitions of Lambda-calculus\<close>
theory Lambda
imports Main
@@ -12,7 +12,7 @@
declare [[syntax_ambiguity_warning = false]]
-subsection {* Lambda-terms in de Bruijn notation and substitution *}
+subsection \<open>Lambda-terms in de Bruijn notation and substitution\<close>
datatype dB =
Var nat
@@ -36,7 +36,7 @@
declare subst_Var [simp del]
-text {* Optimized versions of @{term subst} and @{term lift}. *}
+text \<open>Optimized versions of @{term subst} and @{term lift}.\<close>
primrec
liftn :: "[nat, dB, nat] => dB"
@@ -54,7 +54,7 @@
| "substn (Abs t) s k = Abs (substn t s (k + 1))"
-subsection {* Beta-reduction *}
+subsection \<open>Beta-reduction\<close>
inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
where
@@ -76,10 +76,10 @@
"s \<degree> t \<rightarrow>\<^sub>\<beta> u"
declare if_not_P [simp] not_less_eq [simp]
- -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
+ \<comment> \<open>don't add \<open>r_into_rtrancl[intro!]\<close>\<close>
-subsection {* Congruence rules *}
+subsection \<open>Congruence rules\<close>
lemma rtrancl_beta_Abs [intro!]:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
@@ -98,7 +98,7 @@
by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
-subsection {* Substitution-lemmas *}
+subsection \<open>Substitution-lemmas\<close>
lemma subst_eq [simp]: "(Var k)[u/k] = u"
by (simp add: subst_Var)
@@ -133,7 +133,7 @@
split: nat.split)
-subsection {* Equivalence proof for optimized substitution *}
+subsection \<open>Equivalence proof for optimized substitution\<close>
lemma liftn_0 [simp]: "liftn 0 t k = t"
by (induct t arbitrary: k) (simp_all add: subst_Var)
@@ -148,10 +148,10 @@
by simp
-subsection {* Preservation theorems *}
+subsection \<open>Preservation theorems\<close>
-text {* Not used in Church-Rosser proof, but in Strong
- Normalization. \medskip *}
+text \<open>Not used in Church-Rosser proof, but in Strong
+ Normalization. \medskip\<close>
theorem subst_preserves_beta [simp]:
"r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
--- a/src/HOL/Proofs/Lambda/LambdaType.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,12 +3,12 @@
Copyright 2000 TU Muenchen
*)
-section {* Simply-typed lambda terms *}
+section \<open>Simply-typed lambda terms\<close>
theory LambdaType imports ListApplication begin
-subsection {* Environments *}
+subsection \<open>Environments\<close>
definition
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) where
@@ -27,7 +27,7 @@
by (rule ext) (simp_all add: shift_def split: nat.split)
-subsection {* Types and typing rules *}
+subsection \<open>Types and typing rules\<close>
datatype type =
Atom nat
@@ -69,7 +69,7 @@
funs (infixr "\<Rrightarrow>" 200)
-subsection {* Some examples *}
+subsection \<open>Some examples\<close>
schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
by force
@@ -78,7 +78,7 @@
by force
-subsection {* Lists of types *}
+subsection \<open>Lists of types\<close>
lemma lists_typings:
"e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts"
@@ -114,8 +114,8 @@
lemma rev_exhaust2 [extraction_expand]:
obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]"
- -- {* Cannot use @{text rev_exhaust} from the @{text List}
- theory, since it is not constructive *}
+ \<comment> \<open>Cannot use \<open>rev_exhaust\<close> from the \<open>List\<close>
+ theory, since it is not constructive\<close>
apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis")
apply (erule_tac x="rev xs" in allE)
apply simp
@@ -135,7 +135,7 @@
done
-subsection {* n-ary function types *}
+subsection \<open>n-ary function types\<close>
lemma list_app_typeD:
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
@@ -178,12 +178,12 @@
apply blast
done
-text {*
+text \<open>
For the specific case where the head of the term is a variable,
the following theorems allow to infer the types of the arguments
without analyzing the typing derivation. This is crucial
for program extraction.
-*}
+\<close>
theorem var_app_type_eq:
"e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
@@ -275,7 +275,7 @@
done
-subsection {* Lifting preserves well-typedness *}
+subsection \<open>Lifting preserves well-typedness\<close>
lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
by (induct arbitrary: i U set: typing) auto
@@ -289,7 +289,7 @@
done
-subsection {* Substitution lemmas *}
+subsection \<open>Substitution lemmas\<close>
lemma subst_lemma:
"e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
@@ -316,7 +316,7 @@
done
-subsection {* Subject reduction *}
+subsection \<open>Subject reduction\<close>
lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T"
apply (induct arbitrary: t' set: typing)
@@ -338,7 +338,7 @@
by (induct set: rtranclp) (iprover intro: subject_reduction)+
-subsection {* Alternative induction rule for types *}
+subsection \<open>Alternative induction rule for types\<close>
lemma type_induct [induct type]:
assumes
--- a/src/HOL/Proofs/Lambda/ListApplication.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,7 +3,7 @@
Copyright 1998 TU Muenchen
*)
-section {* Application of a term to a list of terms *}
+section \<open>Application of a term to a list of terms\<close>
theory ListApplication imports Lambda begin
@@ -93,7 +93,7 @@
by simp
-text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
+text \<open>\medskip A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close>
lemma lem:
assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
--- a/src/HOL/Proofs/Lambda/ListBeta.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/ListBeta.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,13 +3,13 @@
Copyright 1998 TU Muenchen
*)
-section {* Lifting beta-reduction to lists *}
+section \<open>Lifting beta-reduction to lists\<close>
theory ListBeta imports ListApplication ListOrder begin
-text {*
+text \<open>
Lifting beta-reduction to lists of terms, reducing exactly one element.
-*}
+\<close>
abbreviation
list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where
--- a/src/HOL/Proofs/Lambda/ListOrder.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/ListOrder.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,7 +3,7 @@
Copyright 1998 TU Muenchen
*)
-section {* Lifting an order to lists of elements *}
+section \<open>Lifting an order to lists of elements\<close>
theory ListOrder
imports Main
@@ -12,10 +12,10 @@
declare [[syntax_ambiguity_warning = false]]
-text {*
+text \<open>
Lifting an order to lists of elements, relating exactly one
element.
-*}
+\<close>
definition
step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
--- a/src/HOL/Proofs/Lambda/NormalForm.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,13 +2,13 @@
Author: Stefan Berghofer, TU Muenchen, 2003
*)
-section {* Inductive characterization of lambda terms in normal form *}
+section \<open>Inductive characterization of lambda terms in normal form\<close>
theory NormalForm
imports ListBeta
begin
-subsection {* Terms in normal form *}
+subsection \<open>Terms in normal form\<close>
definition
listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
@@ -64,13 +64,13 @@
lemma listall_cong [cong, extraction_expand]:
"xs = ys \<Longrightarrow> listall P xs = listall P ys"
- -- {* Currently needed for strange technical reasons *}
+ \<comment> \<open>Currently needed for strange technical reasons\<close>
by (unfold listall_def) simp
-text {*
+text \<open>
@{term "listsp"} is equivalent to @{term "listall"}, but cannot be
used for program extraction.
-*}
+\<close>
lemma listall_listsp_eq: "listall P xs = listsp P xs"
by (induct xs) (auto intro: listsp.intros)
@@ -100,7 +100,7 @@
by cases simp_all
-subsection {* Properties of @{text NF} *}
+subsection \<open>Properties of \<open>NF\<close>\<close>
lemma Var_NF: "NF (Var n)"
apply (subgoal_tac "NF (Var n \<degree>\<degree> [])")
@@ -146,7 +146,7 @@
lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
apply (induct set: NF)
- apply (simplesubst app_last) --{*Using @{text subst} makes extraction fail*}
+ apply (simplesubst app_last) \<comment>\<open>Using \<open>subst\<close> makes extraction fail\<close>
apply (rule exI)
apply (rule conjI)
apply (rule rtranclp.rtrancl_refl)
@@ -185,9 +185,9 @@
apply simp
done
-text {*
+text \<open>
@{term NF} characterizes exactly the terms that are in normal form.
-*}
+\<close>
lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')"
proof
--- a/src/HOL/Proofs/Lambda/ParRed.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/ParRed.thy Wed Dec 30 18:25:39 2015 +0100
@@ -6,12 +6,12 @@
confluence of beta.
*)
-section {* Parallel reduction and a complete developments *}
+section \<open>Parallel reduction and a complete developments\<close>
theory ParRed imports Lambda Commutation begin
-subsection {* Parallel reduction *}
+subsection \<open>Parallel reduction\<close>
inductive par_beta :: "[dB, dB] => bool" (infixl "=>" 50)
where
@@ -28,9 +28,9 @@
"Abs s => t"
-subsection {* Inclusions *}
+subsection \<open>Inclusions\<close>
-text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
+text \<open>\<open>beta \<subseteq> par_beta \<subseteq> beta^*\<close> \medskip\<close>
lemma par_beta_varL [simp]:
"(Var n => t) = (t = Var n)"
@@ -50,11 +50,11 @@
apply (erule par_beta.induct)
apply blast
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
- -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
+ \<comment> \<open>@{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor\<close>
done
-subsection {* Misc properties of @{text "par_beta"} *}
+subsection \<open>Misc properties of \<open>par_beta\<close>\<close>
lemma par_beta_lift [simp]:
"t => t' \<Longrightarrow> lift t n => lift t' n"
@@ -72,7 +72,7 @@
done
-subsection {* Confluence (directly) *}
+subsection \<open>Confluence (directly)\<close>
lemma diamond_par_beta: "diamond par_beta"
apply (unfold diamond_def commute_def square_def)
@@ -82,7 +82,7 @@
done
-subsection {* Complete developments *}
+subsection \<open>Complete developments\<close>
fun
cd :: "dB => dB"
@@ -100,7 +100,7 @@
done
-subsection {* Confluence (via complete developments) *}
+subsection \<open>Confluence (via complete developments)\<close>
lemma diamond_par_beta2: "diamond par_beta"
apply (unfold diamond_def commute_def square_def)
--- a/src/HOL/Proofs/Lambda/Standardization.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/Standardization.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,19 +3,19 @@
Copyright 2005 TU Muenchen
*)
-section {* Standardization *}
+section \<open>Standardization\<close>
theory Standardization
imports NormalForm
begin
-text {*
+text \<open>
Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"},
original proof idea due to Ralph Loader @{cite Loader1998}.
-*}
+\<close>
-subsection {* Standard reduction relation *}
+subsection \<open>Standard reduction relation\<close>
declare listrel_mono [mono_set]
@@ -63,7 +63,7 @@
from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1)
moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app)
- with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
+ with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
by (rule sred.Abs)
thus ?case by (simp only: app_last)
next
@@ -199,7 +199,7 @@
with r'' show ?case by simp
next
case (Abs r r' ss ss')
- from `Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''` show ?case
+ from \<open>Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case
proof
fix s
assume r'': "r'' = s \<degree>\<degree> ss'"
@@ -213,7 +213,7 @@
fix rs'
assume "ss' => rs'"
with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux)
- with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
+ with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
moreover assume "r'' = Abs r' \<degree>\<degree> rs'"
ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
next
@@ -240,7 +240,7 @@
by induct (iprover intro: refl_sred lemma4)+
-subsection {* Leftmost reduction and weakly normalizing terms *}
+subsection \<open>Leftmost reduction and weakly normalizing terms\<close>
inductive
lred :: "dB \<Rightarrow> dB \<Rightarrow> bool" (infixl "\<rightarrow>\<^sub>l" 50)
@@ -261,13 +261,13 @@
then show ?case by (rule sred.Var)
next
case (Abs r r')
- from `r \<rightarrow>\<^sub>s r'`
+ from \<open>r \<rightarrow>\<^sub>s r'\<close>
have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil
by (rule sred.Abs)
then show ?case by simp
next
case (Beta r s ss t)
- from `r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t`
+ from \<open>r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close>
show ?case by (rule sred.Beta)
qed
@@ -310,7 +310,7 @@
shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r
proof induct
case (Var rs rs' x)
- from `NF (Var x \<degree>\<degree> rs')` have "listall NF rs'"
+ from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listall NF rs'"
by cases simp_all
with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'"
proof induct
@@ -324,7 +324,7 @@
thus ?case by (rule lred.Var)
next
case (Abs r r' ss ss')
- from `NF (Abs r' \<degree>\<degree> ss')`
+ from \<open>NF (Abs r' \<degree>\<degree> ss')\<close>
have ss': "ss' = []" by (rule Abs_NF)
from Abs(3) have ss: "ss = []" using ss'
by cases simp_all
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,17 +3,17 @@
Copyright 2000 TU Muenchen
*)
-section {* Strong normalization for simply-typed lambda calculus *}
+section \<open>Strong normalization for simply-typed lambda calculus\<close>
theory StrongNorm imports LambdaType InductTermi begin
-text {*
+text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
-*}
+\<close>
-subsection {* Properties of @{text IT} *}
+subsection \<open>Properties of \<open>IT\<close>\<close>
lemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)"
apply (induct arbitrary: i set: IT)
@@ -36,7 +36,7 @@
lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])"
apply (induct arbitrary: i j set: IT)
- txt {* Case @{term Var}: *}
+ txt \<open>Case @{term Var}:\<close>
apply (simp (no_asm) add: subst_Var)
apply
((rule conjI impI)+,
@@ -47,12 +47,12 @@
rule listsp.Cons,
fast,
assumption)+
- txt {* Case @{term Lambda}: *}
+ txt \<open>Case @{term Lambda}:\<close>
apply atomize
apply simp
apply (rule IT.Lambda)
apply fast
- txt {* Case @{term Beta}: *}
+ txt \<open>Case @{term Beta}:\<close>
apply atomize
apply (simp (no_asm_use) add: subst_subst [symmetric])
apply (rule IT.Beta)
@@ -85,7 +85,7 @@
done
-subsection {* Well-typed substitution preserves termination *}
+subsection \<open>Well-typed substitution preserves termination\<close>
lemma subst_type_IT:
"\<And>t e T u i. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
@@ -241,7 +241,7 @@
qed
-subsection {* Well-typed terms are strongly normalizing *}
+subsection \<open>Well-typed terms are strongly normalizing\<close>
lemma type_implies_IT:
assumes "e \<turnstile> t : T"
@@ -257,7 +257,7 @@
case (App e s T U t)
have "IT ((Var 0 \<degree> lift t 0)[s/0])"
proof (rule subst_type_IT)
- have "IT (lift t 0)" using `IT t` by (rule lift_IT)
+ have "IT (lift t 0)" using \<open>IT t\<close> by (rule lift_IT)
hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
hence "IT (Var 0 \<degree>\<degree> [lift t 0])" by (rule IT.Var)
also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,20 +3,20 @@
Copyright 2003 TU Muenchen
*)
-section {* Weak normalization for simply-typed lambda calculus *}
+section \<open>Weak normalization for simply-typed lambda calculus\<close>
theory WeakNorm
imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
"~~/src/HOL/Library/Code_Target_Int"
begin
-text {*
+text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
-*}
+\<close>
-subsection {* Main theorems *}
+subsection \<open>Main theorems\<close>
lemma norm_list:
assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
@@ -191,7 +191,7 @@
case (Abs r e1 T'1 u1 i1)
assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp
- moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
+ moreover have "NF (lift u 0)" using \<open>NF u\<close> by (rule lift_NF)
moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
@@ -201,7 +201,7 @@
qed
--- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
+\<comment> \<open>A computationally relevant copy of @{term "e \<turnstile> t : T"}\<close>
inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
where
Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
@@ -257,7 +257,7 @@
qed
-subsection {* Extracting the program *}
+subsection \<open>Extracting the program\<close>
declare NF.induct [ind_realizer]
declare rtranclp.induct [ind_realizer irrelevant]
@@ -285,12 +285,12 @@
apply (erule NF.intros)
done
-text_raw {*
+text_raw \<open>
\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
\renewcommand{\isastyle}{\small\it}%
-\caption{Program extracted from @{text subst_type_NF}}
+\caption{Program extracted from \<open>subst_type_NF\<close>}
\label{fig:extr-subst-type-nf}
\end{figure}
@@ -304,33 +304,33 @@
\caption{Program extracted from lemmas and main theorem}
\label{fig:extr-type-nf}
\end{figure}
-*}
+\<close>
-text {*
+text \<open>
The program corresponding to the proof of the central lemma, which
performs substitution and normalization, is shown in Figure
\ref{fig:extr-subst-type-nf}. The correctness
-theorem corresponding to the program @{text "subst_type_NF"} is
+theorem corresponding to the program \<open>subst_type_NF\<close> is
@{thm [display,margin=100] subst_type_NF_correctness
[simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
-where @{text NFR} is the realizability predicate corresponding to
-the datatype @{text NFT}, which is inductively defined by the rules
+where \<open>NFR\<close> is the realizability predicate corresponding to
+the datatype \<open>NFT\<close>, which is inductively defined by the rules
\pagebreak
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}
-The programs corresponding to the main theorem @{text "type_NF"}, as
+The programs corresponding to the main theorem \<open>type_NF\<close>, as
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
-The correctness statement for the main function @{text "type_NF"} is
+The correctness statement for the main function \<open>type_NF\<close> is
@{thm [display,margin=100] type_NF_correctness
[simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
-where the realizability predicate @{text "rtypingR"} corresponding to the
+where the realizability predicate \<open>rtypingR\<close> corresponding to the
computationally relevant version of the typing judgement is inductively
defined by the rules
@{thm [display,margin=100] rtypingR.Var [no_vars]
rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
-*}
+\<close>
-subsection {* Generating executable code *}
+subsection \<open>Generating executable code\<close>
instantiation NFT :: default
begin
@@ -380,14 +380,14 @@
definition int_of_nat :: "nat \<Rightarrow> int" where
"int_of_nat = of_nat"
-text {*
+text \<open>
The following functions convert between Isabelle's built-in {\tt term}
datatype and the generated {\tt dB} datatype. This allows to
generate example terms using Isabelle's parser and inspect
normalized terms using Isabelle's pretty printer.
-*}
+\<close>
-ML {*
+ML \<open>
val nat_of_integer = @{code nat} o @{code int_of_integer};
fun dBtype_of_typ (Type ("fun", [T, U])) =
@@ -438,6 +438,6 @@
val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
-*}
+\<close>
end
--- a/src/HOL/Proofs/ex/Hilbert_Classical.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/ex/Hilbert_Classical.thy Wed Dec 30 18:25:39 2015 +0100
@@ -2,19 +2,19 @@
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
*)
-section {* Hilbert's choice and classical logic *}
+section \<open>Hilbert's choice and classical logic\<close>
theory Hilbert_Classical
imports Main
begin
-text {*
+text \<open>
Derivation of the classical law of tertium-non-datur by means of
Hilbert's choice operator (due to M. J. Beeson and J. Harrison).
-*}
+\<close>
-subsection {* Proof text *}
+subsection \<open>Proof text\<close>
theorem tnd: "A \<or> \<not> A"
proof -
@@ -94,12 +94,12 @@
qed
-subsection {* Proof term of text *}
+subsection \<open>Proof term of text\<close>
prf tnd
-subsection {* Proof script *}
+subsection \<open>Proof script\<close>
theorem tnd': "A \<or> \<not> A"
apply (subgoal_tac
@@ -153,7 +153,7 @@
done
-subsection {* Proof term of script *}
+subsection \<open>Proof term of script\<close>
prf tnd'
--- a/src/HOL/Proofs/ex/XML_Data.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy Wed Dec 30 18:25:39 2015 +0100
@@ -9,9 +9,9 @@
imports "~~/src/HOL/Isar_Examples/Drinker"
begin
-subsection {* Export and re-import of global proof terms *}
+subsection \<open>Export and re-import of global proof terms\<close>
-ML {*
+ML \<open>
fun export_proof thy thm =
let
val (_, prop) =
@@ -30,36 +30,36 @@
val prf = Proofterm.decode xml;
val (prf', _) = Proofterm.freeze_thaw_prf prf;
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
-*}
+\<close>
-subsection {* Examples *}
+subsection \<open>Examples\<close>
-ML {* val thy1 = @{theory} *}
+ML \<open>val thy1 = @{theory}\<close>
lemma ex: "A \<longrightarrow> A" ..
-ML_val {*
+ML_val \<open>
val xml = export_proof @{theory} @{thm ex};
val thm = import_proof thy1 xml;
-*}
+\<close>
-ML_val {*
+ML_val \<open>
val xml = export_proof @{theory} @{thm de_Morgan};
val thm = import_proof thy1 xml;
-*}
+\<close>
-ML_val {*
+ML_val \<open>
val xml = export_proof @{theory} @{thm Drinker's_Principle};
val thm = import_proof thy1 xml;
-*}
+\<close>
-text {* Some fairly large proof: *}
+text \<open>Some fairly large proof:\<close>
-ML_val {*
+ML_val \<open>
val xml = export_proof @{theory} @{thm abs_less_iff};
val thm = import_proof thy1 xml;
@{assert} (size (YXML.string_of_body xml) > 1000000);
-*}
+\<close>
end