--- a/src/HOL/Set.thy Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Set.thy Sat Jul 18 22:58:50 2015 +0200
@@ -1,12 +1,12 @@
(* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel *)
-section {* Set theory for higher-order logic *}
+section \<open>Set theory for higher-order logic\<close>
theory Set
imports Lattices
begin
-subsection {* Sets as predicates *}
+subsection \<open>Sets as predicates\<close>
typedecl 'a set
@@ -40,7 +40,7 @@
not_member ("(_/ \<notin> _)" [51, 51] 50)
-text {* Set comprehensions *}
+text \<open>Set comprehensions\<close>
syntax
"_Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")
@@ -63,12 +63,12 @@
lemma Collect_cong: "(\<And>x. P x = Q x) ==> {x. P x} = {x. Q x}"
by simp
-text {*
+text \<open>
Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
to the front (and similarly for @{text "t=x"}):
-*}
-
-simproc_setup defined_Collect ("{x. P x & Q x}") = {*
+\<close>
+
+simproc_setup defined_Collect ("{x. P x & Q x}") = \<open>
fn _ => Quantifier1.rearrange_Collect
(fn ctxt =>
resolve_tac ctxt @{thms Collect_cong} 1 THEN
@@ -76,7 +76,7 @@
ALLGOALS
(EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
-*}
+\<close>
lemmas CollectE = CollectD [elim_format]
@@ -92,7 +92,7 @@
"A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
by (auto intro:set_eqI)
-text {* Lifting of predicate class instances *}
+text \<open>Lifting of predicate class instances\<close>
instantiation set :: (type) boolean_algebra
begin
@@ -130,7 +130,7 @@
end
-text {* Set enumerations *}
+text \<open>Set enumerations\<close>
abbreviation empty :: "'a set" ("{}") where
"{} \<equiv> bot"
@@ -145,7 +145,7 @@
"{x}" == "CONST insert x {}"
-subsection {* Subsets and bounded quantifiers *}
+subsection \<open>Subsets and bounded quantifiers\<close>
abbreviation
subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -256,7 +256,7 @@
"\<exists>A\<subseteq>B. P" => "EX A. A \<subseteq> B & P"
"\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P"
-print_translation {*
+print_translation \<open>
let
val All_binder = Mixfix.binder_name @{const_syntax All};
val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
@@ -287,19 +287,19 @@
in
[tr' All_binder, tr' Ex_binder]
end
-*}
-
-
-text {*
+\<close>
+
+
+text \<open>
\medskip Translate between @{text "{e | x1...xn. P}"} and @{text
"{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
only translated if @{text "[0..n] subset bvs(e)"}.
-*}
+\<close>
syntax
"_Setcompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
-parse_translation {*
+parse_translation \<open>
let
val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));
@@ -314,14 +314,14 @@
in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
-*}
-
-print_translation {*
+\<close>
+
+print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
-*} -- {* to avoid eta-contraction of body *}
-
-print_translation {*
+\<close> -- \<open>to avoid eta-contraction of body\<close>
+
+print_translation \<open>
let
val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
@@ -353,21 +353,21 @@
end
end;
in [(@{const_syntax Collect}, setcompr_tr')] end;
-*}
-
-simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
+\<close>
+
+simproc_setup defined_Bex ("EX x:A. P x & Q x") = \<open>
fn _ => Quantifier1.rearrange_bex
(fn ctxt =>
unfold_tac ctxt @{thms Bex_def} THEN
Quantifier1.prove_one_point_ex_tac ctxt)
-*}
-
-simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
+\<close>
+
+simproc_setup defined_All ("ALL x:A. P x --> Q x") = \<open>
fn _ => Quantifier1.rearrange_ball
(fn ctxt =>
unfold_tac ctxt @{thms Ball_def} THEN
Quantifier1.prove_one_point_all_tac ctxt)
-*}
+\<close>
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
by (simp add: Ball_def)
@@ -377,16 +377,16 @@
lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
by (simp add: Ball_def)
-text {*
+text \<open>
Gives better instantiation for bound:
-*}
-
-setup {*
+\<close>
+
+setup \<open>
map_theory_claset (fn ctxt =>
ctxt addbefore ("bspec", fn ctxt' => dresolve_tac ctxt' @{thms bspec} THEN' assume_tac ctxt'))
-*}
-
-ML {*
+\<close>
+
+ML \<open>
structure Simpdata =
struct
@@ -397,22 +397,22 @@
end;
open Simpdata;
-*}
-
-declaration {* fn _ =>
+\<close>
+
+declaration \<open>fn _ =>
Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
-*}
+\<close>
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
by (unfold Ball_def) blast
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
- -- {* Normally the best argument order: @{prop "P x"} constrains the
- choice of @{prop "x:A"}. *}
+ -- \<open>Normally the best argument order: @{prop "P x"} constrains the
+ choice of @{prop "x:A"}.\<close>
by (unfold Bex_def) blast
lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x"
- -- {* The best argument order when there is only one @{prop "x:A"}. *}
+ -- \<open>The best argument order when there is only one @{prop "x:A"}.\<close>
by (unfold Bex_def) blast
lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"
@@ -422,11 +422,11 @@
by (unfold Bex_def) blast
lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"
- -- {* Trival rewrite rule. *}
+ -- \<open>Trival rewrite rule.\<close>
by (simp add: Ball_def)
lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"
- -- {* Dual form for existentials. *}
+ -- \<open>Dual form for existentials.\<close>
by (simp add: Bex_def)
lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"
@@ -456,7 +456,7 @@
by blast
-text {* Congruence rules *}
+text \<open>Congruence rules\<close>
lemma ball_cong:
"A = B ==> (!!x. x:B ==> P x = Q x) ==>
@@ -481,34 +481,34 @@
lemma bex1_def: "(\<exists>!x\<in>X. P x) \<longleftrightarrow> (\<exists>x\<in>X. P x) \<and> (\<forall>x\<in>X. \<forall>y\<in>X. P x \<longrightarrow> P y \<longrightarrow> x = y)"
by auto
-subsection {* Basic operations *}
-
-subsubsection {* Subsets *}
+subsection \<open>Basic operations\<close>
+
+subsubsection \<open>Subsets\<close>
lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
by (simp add: less_eq_set_def le_fun_def)
-text {*
+text \<open>
\medskip Map the type @{text "'a set => anything"} to just @{typ
'a}; for overloading constants whose first argument has type @{typ
"'a set"}.
-*}
+\<close>
lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
by (simp add: less_eq_set_def le_fun_def)
- -- {* Rule in Modus Ponens style. *}
+ -- \<open>Rule in Modus Ponens style.\<close>
lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
- -- {* The same, with reversed premises for use with @{text erule} --
- cf @{text rev_mp}. *}
+ -- \<open>The same, with reversed premises for use with @{text erule} --
+ cf @{text rev_mp}.\<close>
by (rule subsetD)
-text {*
+text \<open>
\medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
-*}
+\<close>
lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
- -- {* Classical elimination rule. *}
+ -- \<open>Classical elimination rule.\<close>
by (auto simp add: less_eq_set_def le_fun_def)
lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
@@ -539,16 +539,16 @@
order_trans_rules set_rev_mp set_mp eq_mem_trans
-subsubsection {* Equality *}
+subsubsection \<open>Equality\<close>
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
- -- {* Anti-symmetry of the subset relation. *}
+ -- \<open>Anti-symmetry of the subset relation.\<close>
by (iprover intro: set_eqI subsetD)
-text {*
+text \<open>
\medskip Equality rules from ZF set theory -- are they appropriate
here?
-*}
+\<close>
lemma equalityD1: "A = B ==> A \<subseteq> B"
by simp
@@ -556,11 +556,11 @@
lemma equalityD2: "A = B ==> B \<subseteq> A"
by simp
-text {*
+text \<open>
\medskip Be careful when adding this to the claset as @{text
subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
\<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
-*}
+\<close>
lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
by simp
@@ -576,7 +576,7 @@
by simp
-subsubsection {* The empty set *}
+subsubsection \<open>The empty set\<close>
lemma empty_def:
"{} = {x. False}"
@@ -589,14 +589,14 @@
by simp
lemma empty_subsetI [iff]: "{} \<subseteq> A"
- -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
+ -- \<open>One effect is to delete the ASSUMPTION @{prop "{} <= A"}\<close>
by blast
lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
by blast
lemma equals0D: "A = {} ==> a \<notin> A"
- -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
+ -- \<open>Use for reasoning about disjointness: @{text "A Int B = {}"}\<close>
by blast
lemma ball_empty [simp]: "Ball {} P = True"
@@ -606,7 +606,7 @@
by (simp add: Bex_def)
-subsubsection {* The universal set -- UNIV *}
+subsubsection \<open>The universal set -- UNIV\<close>
abbreviation UNIV :: "'a set" where
"UNIV \<equiv> top"
@@ -618,7 +618,7 @@
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
-declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *}
+declare UNIV_I [intro] -- \<open>unsafe makes it less likely to cause problems\<close>
lemma UNIV_witness [intro?]: "EX x. x : UNIV"
by simp
@@ -626,11 +626,11 @@
lemma subset_UNIV: "A \<subseteq> UNIV"
by (fact top_greatest) (* already simp *)
-text {*
+text \<open>
\medskip Eta-contracting these two rules (to remove @{text P})
causes them to be ignored because of their interaction with
congruence rules.
-*}
+\<close>
lemma ball_UNIV [simp]: "Ball UNIV P = All P"
by (simp add: Ball_def)
@@ -647,7 +647,7 @@
lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
by blast
-subsubsection {* The Powerset operator -- Pow *}
+subsubsection \<open>The Powerset operator -- Pow\<close>
definition Pow :: "'a set => 'a set set" where
Pow_def: "Pow A = {B. B \<le> A}"
@@ -671,7 +671,7 @@
using Pow_top by blast
-subsubsection {* Set complement *}
+subsubsection \<open>Set complement\<close>
lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
by (simp add: fun_Compl_def uminus_set_def)
@@ -679,10 +679,10 @@
lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
by (simp add: fun_Compl_def uminus_set_def) blast
-text {*
+text \<open>
\medskip This form, with negated conclusion, works well with the
Classical prover. Negated assumptions behave like formulae on the
- right side of the notional turnstile ... *}
+ right side of the notional turnstile ...\<close>
lemma ComplD [dest!]: "c : -A ==> c~:A"
by simp
@@ -693,7 +693,7 @@
by blast
-subsubsection {* Binary intersection *}
+subsubsection \<open>Binary intersection\<close>
abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
"op Int \<equiv> inf"
@@ -727,7 +727,7 @@
by (fact mono_inf)
-subsubsection {* Binary union *}
+subsubsection \<open>Binary union\<close>
abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
"union \<equiv> sup"
@@ -751,10 +751,10 @@
lemma UnI2 [elim?]: "c:B ==> c : A Un B"
by simp
-text {*
+text \<open>
\medskip Classical introduction rule: no commitment to @{prop A} vs
@{prop B}.
-*}
+\<close>
lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
by auto
@@ -769,7 +769,7 @@
by (fact mono_sup)
-subsubsection {* Set difference *}
+subsubsection \<open>Set difference\<close>
lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
by (simp add: minus_set_def fun_diff_def)
@@ -792,7 +792,7 @@
by blast
-subsubsection {* Augmenting a set -- @{const insert} *}
+subsubsection \<open>Augmenting a set -- @{const insert}\<close>
lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
by (unfold insert_def) blast
@@ -807,7 +807,7 @@
by (unfold insert_def) blast
lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
- -- {* Classical introduction rule. *}
+ -- \<open>Classical introduction rule.\<close>
by auto
lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
@@ -833,13 +833,13 @@
assume ?L
show ?R
proof cases
- assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)
+ assume "a=b" with assms \<open>?L\<close> show ?R by (simp add: insert_ident)
next
assume "a\<noteq>b"
let ?C = "A - {b}"
have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
- using assms `?L` `a\<noteq>b` by auto
- thus ?R using `a\<noteq>b` by auto
+ using assms \<open>?L\<close> \<open>a\<noteq>b\<close> by auto
+ thus ?R using \<open>a\<noteq>b\<close> by auto
qed
next
assume ?R thus ?L by (auto split: if_splits)
@@ -848,10 +848,10 @@
lemma insert_UNIV: "insert x UNIV = UNIV"
by auto
-subsubsection {* Singletons, using insert *}
+subsubsection \<open>Singletons, using insert\<close>
lemma singletonI [intro!]: "a : {a}"
- -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
+ -- \<open>Redundant? But unlike @{text insertCI}, it proves the subgoal immediately!\<close>
by (rule insertI1)
lemma singletonD [dest!]: "b : {a} ==> b = a"
@@ -897,11 +897,11 @@
by auto
-subsubsection {* Image of a set under a function *}
-
-text {*
+subsubsection \<open>Image of a set under a function\<close>
+
+text \<open>
Frequently @{term b} does not have the syntactic form of @{term "f x"}.
-*}
+\<close>
definition image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "`" 90)
where
@@ -917,12 +917,12 @@
lemma rev_image_eqI:
"x \<in> A \<Longrightarrow> b = f x \<Longrightarrow> b \<in> f ` A"
- -- {* This version's more effective when we already have the
- required @{term x}. *}
+ -- \<open>This version's more effective when we already have the
+ required @{term x}.\<close>
by (rule image_eqI)
lemma imageE [elim!]:
- assumes "b \<in> (\<lambda>x. f x) ` A" -- {* The eta-expansion gives variable-name preservation. *}
+ assumes "b \<in> (\<lambda>x. f x) ` A" -- \<open>The eta-expansion gives variable-name preservation.\<close>
obtains x where "b = f x" and "x \<in> A"
using assms by (unfold image_def) blast
@@ -940,13 +940,13 @@
lemma image_subsetI:
"(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` A \<subseteq> B"
- -- {* Replaces the three steps @{text subsetI}, @{text imageE},
- @{text hypsubst}, but breaks too many existing proofs. *}
+ -- \<open>Replaces the three steps @{text subsetI}, @{text imageE},
+ @{text hypsubst}, but breaks too many existing proofs.\<close>
by blast
lemma image_subset_iff:
"f ` A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
- -- {* This rewrite rule would confuse users if made default. *}
+ -- \<open>This rewrite rule would confuse users if made default.\<close>
by blast
lemma subset_imageE:
@@ -1000,9 +1000,9 @@
lemma image_Collect:
"f ` {x. P x} = {f x | x. P x}"
- -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
+ -- \<open>NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
with its implicit quantifier and conjunction. Also image enjoys better
- equational properties than does the RHS. *}
+ equational properties than does the RHS.\<close>
by blast
lemma if_image_distrib [simp]:
@@ -1036,9 +1036,9 @@
using assms by auto
-text {*
+text \<open>
\medskip Range of a function -- just a translation for image!
-*}
+\<close>
abbreviation range :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set"
where -- "of function"
@@ -1065,9 +1065,9 @@
by auto
-subsubsection {* Some rules with @{text "if"} *}
-
-text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
+subsubsection \<open>Some rules with @{text "if"}\<close>
+
+text\<open>Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}.\<close>
lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
by auto
@@ -1075,10 +1075,10 @@
lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
by auto
-text {*
+text \<open>
Rewrite rules for boolean case-splitting: faster than @{text
"split_if [split]"}.
-*}
+\<close>
lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
by (rule split_if)
@@ -1086,10 +1086,10 @@
lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
by (rule split_if)
-text {*
+text \<open>
Split ifs on either side of the membership relation. Not for @{text
"[simp]"} -- can cause goals to blow up!
-*}
+\<close>
lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
by (rule split_if)
@@ -1109,9 +1109,9 @@
*)
-subsection {* Further operations and lemmas *}
-
-subsubsection {* The ``proper subset'' relation *}
+subsection \<open>Further operations and lemmas\<close>
+
+subsubsection \<open>The ``proper subset'' relation\<close>
lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
by (unfold less_le) blast
@@ -1167,9 +1167,9 @@
using assms by (blast elim: subset_imageE)
-subsubsection {* Derived rules involving subsets. *}
-
-text {* @{text insert}. *}
+subsubsection \<open>Derived rules involving subsets.\<close>
+
+text \<open>@{text insert}.\<close>
lemma subset_insertI: "B \<subseteq> insert a B"
by (rule subsetI) (erule insertI2)
@@ -1181,7 +1181,7 @@
by blast
-text {* \medskip Finite Union -- the least upper bound of two sets. *}
+text \<open>\medskip Finite Union -- the least upper bound of two sets.\<close>
lemma Un_upper1: "A \<subseteq> A \<union> B"
by (fact sup_ge1)
@@ -1193,7 +1193,7 @@
by (fact sup_least)
-text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
+text \<open>\medskip Finite Intersection -- the greatest lower bound of two sets.\<close>
lemma Int_lower1: "A \<inter> B \<subseteq> A"
by (fact inf_le1)
@@ -1205,7 +1205,7 @@
by (fact inf_greatest)
-text {* \medskip Set difference. *}
+text \<open>\medskip Set difference.\<close>
lemma Diff_subset: "A - B \<subseteq> A"
by blast
@@ -1214,12 +1214,12 @@
by blast
-subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
-
-text {* @{text "{}"}. *}
+subsubsection \<open>Equalities involving union, intersection, inclusion, etc.\<close>
+
+text \<open>@{text "{}"}.\<close>
lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
- -- {* supersedes @{text "Collect_False_empty"} *}
+ -- \<open>supersedes @{text "Collect_False_empty"}\<close>
by auto
lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
@@ -1250,10 +1250,10 @@
by blast
-text {* \medskip @{text insert}. *}
+text \<open>\medskip @{text insert}.\<close>
lemma insert_is_Un: "insert a A = {a} Un A"
- -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
+ -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"}\<close>
by blast
lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
@@ -1263,8 +1263,8 @@
declare empty_not_insert [simp]
lemma insert_absorb: "a \<in> A ==> insert a A = A"
- -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
- -- {* with \emph{quadratic} running time *}
+ -- \<open>@{text "[simp]"} causes recursive calls when there are nested inserts\<close>
+ -- \<open>with \emph{quadratic} running time\<close>
by blast
lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
@@ -1277,7 +1277,7 @@
by blast
lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
- -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
+ -- \<open>use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding\<close>
apply (rule_tac x = "A - {a}" in exI, blast)
done
@@ -1298,7 +1298,7 @@
by auto
-text {* \medskip @{text Int} *}
+text \<open>\medskip @{text Int}\<close>
lemma Int_absorb: "A \<inter> A = A"
by (fact inf_idem) (* already simp *)
@@ -1316,7 +1316,7 @@
by (fact inf_assoc)
lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
- -- {* Intersection is an AC-operator *}
+ -- \<open>Intersection is an AC-operator\<close>
lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
by (fact inf_absorb2)
@@ -1358,7 +1358,7 @@
by blast
-text {* \medskip @{text Un}. *}
+text \<open>\medskip @{text Un}.\<close>
lemma Un_absorb: "A \<union> A = A"
by (fact sup_idem) (* already simp *)
@@ -1376,7 +1376,7 @@
by (fact sup_assoc)
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
- -- {* Union is an AC-operator *}
+ -- \<open>Union is an AC-operator\<close>
lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
by (fact sup_absorb2)
@@ -1452,7 +1452,7 @@
by blast
-text {* \medskip Set complement *}
+text \<open>\medskip Set complement\<close>
lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
by (fact inf_compl_bot)
@@ -1479,7 +1479,7 @@
by blast
lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
- -- {* Halmos, Naive Set Theory, page 16. *}
+ -- \<open>Halmos, Naive Set Theory, page 16.\<close>
by blast
lemma Compl_UNIV_eq: "-UNIV = {}"
@@ -1497,10 +1497,10 @@
lemma Compl_insert: "- insert x A = (-A) - {x}"
by blast
-text {* \medskip Bounded quantifiers.
+text \<open>\medskip Bounded quantifiers.
The following are not added to the default simpset because
- (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
+ (a) they duplicate the body and (b) there are no similar rules for @{text Int}.\<close>
lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
by blast
@@ -1509,7 +1509,7 @@
by blast
-text {* \medskip Set difference. *}
+text \<open>\medskip Set difference.\<close>
lemma Diff_eq: "A - B = A \<inter> (-B)"
by blast
@@ -1539,11 +1539,11 @@
by blast
lemma Diff_insert: "A - insert a B = A - B - {a}"
- -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
+ -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"}\<close>
by blast
lemma Diff_insert2: "A - insert a B = A - {a} - B"
- -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
+ -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"}\<close>
by blast
lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
@@ -1601,7 +1601,7 @@
by blast
-text {* \medskip Quantification over type @{typ bool}. *}
+text \<open>\medskip Quantification over type @{typ bool}.\<close>
lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
by (cases x) auto
@@ -1618,7 +1618,7 @@
lemma UNIV_bool: "UNIV = {False, True}"
by (auto intro: bool_induct)
-text {* \medskip @{text Pow} *}
+text \<open>\medskip @{text Pow}\<close>
lemma Pow_empty [simp]: "Pow {} = {{}}"
by (auto simp add: Pow_def)
@@ -1642,7 +1642,7 @@
by blast
-text {* \medskip Miscellany. *}
+text \<open>\medskip Miscellany.\<close>
lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
by blast
@@ -1684,7 +1684,7 @@
by auto
-subsubsection {* Monotonicity of various operations *}
+subsubsection \<open>Monotonicity of various operations\<close>
lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
by blast
@@ -1707,7 +1707,7 @@
lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
by (fact compl_mono)
-text {* \medskip Monotonicity of implications. *}
+text \<open>\medskip Monotonicity of implications.\<close>
lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
apply (rule impI)
@@ -1749,7 +1749,7 @@
by iprover
-subsubsection {* Inverse image of a function *}
+subsubsection \<open>Inverse image of a function\<close>
definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
"f -` B == {x. f x : B}"
@@ -1791,7 +1791,7 @@
by blast
lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
- -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
+ -- \<open>NOT suitable for rewriting because of the recurrence of @{term "{a}"}.\<close>
by blast
lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
@@ -1801,7 +1801,7 @@
by blast
lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
- -- {* monotonicity *}
+ -- \<open>monotonicity\<close>
by blast
lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
@@ -1832,7 +1832,7 @@
by blast
-subsubsection {* Getting the Contents of a Singleton Set *}
+subsubsection \<open>Getting the Contents of a Singleton Set\<close>
definition the_elem :: "'a set \<Rightarrow> 'a" where
"the_elem X = (THE x. X = {x})"
@@ -1845,20 +1845,20 @@
assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
shows "the_elem (f ` A) = f x"
unfolding the_elem_def proof (rule the1_equality)
- from `A \<noteq> {}` obtain y where "y \<in> A" by auto
+ from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
with * have "f x = f y" by simp
- with `y \<in> A` have "f x \<in> f ` A" by blast
+ with \<open>y \<in> A\<close> have "f x \<in> f ` A" by blast
with * show "f ` A = {f x}" by auto
then show "\<exists>!x. f ` A = {x}" by auto
qed
-subsubsection {* Least value operator *}
+subsubsection \<open>Least value operator\<close>
lemma Least_mono:
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
- -- {* Courtesy of Stephan Merz *}
+ -- \<open>Courtesy of Stephan Merz\<close>
apply clarify
apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
apply (rule LeastI2_order)
@@ -1866,7 +1866,7 @@
done
-subsubsection {* Monad operation *}
+subsubsection \<open>Monad operation\<close>
definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
"bind A f = {x. \<exists>B \<in> f`A. x \<in> B}"
@@ -1892,7 +1892,7 @@
lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
by(auto simp add: bind_def)
-subsubsection {* Operations for execution *}
+subsubsection \<open>Operations for execution\<close>
definition is_empty :: "'a set \<Rightarrow> bool" where
[code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
@@ -1929,13 +1929,13 @@
end
-text {* Misc *}
+text \<open>Misc\<close>
hide_const (open) member not_member
lemmas equalityI = subset_antisym
-ML {*
+ML \<open>
val Ball_def = @{thm Ball_def}
val Bex_def = @{thm Bex_def}
val CollectD = @{thm CollectD}
@@ -1988,7 +1988,7 @@
val vimage_Collect = @{thm vimage_Collect}
val vimage_Int = @{thm vimage_Int}
val vimage_Un = @{thm vimage_Un}
-*}
+\<close>
end