--- a/src/HOL/Product_Type.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Product_Type.thy Mon Dec 07 10:38:04 2015 +0100
@@ -15,7 +15,7 @@
free_constructors case_bool for True | False
by auto
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -23,7 +23,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "bool"\<close>
@@ -35,7 +35,7 @@
setup \<open>Sign.parent_path\<close>
declare case_split [cases type: bool]
- -- "prefer plain propositional version"
+ \<comment> "prefer plain propositional version"
lemma
shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
@@ -57,7 +57,7 @@
| class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) -
-subsection \<open>The @{text unit} type\<close>
+subsection \<open>The \<open>unit\<close> type\<close>
typedef unit = "{True}"
by auto
@@ -82,7 +82,7 @@
free_constructors case_unit for "()"
by auto
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -90,7 +90,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "unit"\<close>
@@ -108,7 +108,7 @@
by (rule triv_forall_equality)
text \<open>
- This rewrite counters the effect of simproc @{text unit_eq} on @{term
+ This rewrite counters the effect of simproc \<open>unit_eq\<close> on @{term
[source] "%u::unit. f u"}, replacing it by @{term [source]
f} rather than by @{term [source] "%u. f ()"}.
\<close>
@@ -253,7 +253,7 @@
by (simp add: Pair_def Abs_prod_inject)
qed
-text \<open>Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}.\<close>
+text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -262,7 +262,7 @@
setup \<open>Sign.parent_path\<close>
-text \<open>But erase the prefix for properties that are not generated by @{text free_constructors}.\<close>
+text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "prod"\<close>
@@ -282,7 +282,7 @@
declare prod.split_asm [no_atp]
text \<open>
- @{thm [source] prod.split} could be declared as @{text "[split]"}
+ @{thm [source] prod.split} could be declared as \<open>[split]\<close>
done after the Splitter has been speeded up significantly;
precompute the constants involved and don't do anything unless the
current goal contains one of those constants.
@@ -314,9 +314,9 @@
"\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)"
"\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)"
"_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t"
- -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}:
- The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
- not @{text pttrn}.\<close>
+ \<comment> \<open>This rule accommodates tuples in \<open>case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>\<close>:
+ The \<open>(x, y)\<close> is parsed as \<open>Pair x y\<close> because it is \<open>logic\<close>,
+ not \<open>pttrn\<close>.\<close>
text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and
@{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
@@ -457,7 +457,7 @@
by (simp add: fun_eq_iff split: prod.split)
lemma case_prod_eta: "(\<lambda>(x, y). f (x, y)) = f"
- -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
+ \<comment> \<open>Subsumes the old \<open>split_Pair\<close> when @{term f} is the identity function.\<close>
by (simp add: fun_eq_iff split: prod.split)
lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
@@ -483,8 +483,8 @@
text \<open>
The rule @{thm [source] split_paired_all} does not work with the
Simplifier because it also affects premises in congrence rules,
- where this can lead to premises of the form @{text "!!a b. ... =
- ?P(a, b)"} which cannot be solved by reflexivity.
+ where this can lead to premises of the form \<open>!!a b. ... =
+ ?P(a, b)\<close> which cannot be solved by reflexivity.
\<close>
lemmas split_tupled_all = split_paired_all unit_all_eq2
@@ -518,22 +518,21 @@
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
- -- \<open>@{text "[iff]"} is not a good idea because it makes @{text blast} loop\<close>
+ \<comment> \<open>\<open>[iff]\<close> is not a good idea because it makes \<open>blast\<close> loop\<close>
by fast
lemma split_paired_Ex [simp, no_atp]: "(EX x. P x) = (EX a b. P (a, b))"
by fast
lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
- -- \<open>Can't be added to simpset: loops!\<close>
+ \<comment> \<open>Can't be added to simpset: loops!\<close>
by (simp add: case_prod_eta)
text \<open>
Simplification procedure for @{thm [source] cond_case_prod_eta}. Using
@{thm [source] case_prod_eta} as a rewrite rule is not general enough,
and using @{thm [source] cond_case_prod_eta} directly would render some
- existing proofs very inefficient; similarly for @{text
- prod.case_eq_if}.
+ existing proofs very inefficient; similarly for \<open>prod.case_eq_if\<close>.
\<close>
ML \<open>
@@ -590,8 +589,8 @@
text \<open>
\medskip @{const case_prod} used as a logical connective or set former.
- \medskip These rules are for use with @{text blast}; could instead
- call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
+ \medskip These rules are for use with \<open>blast\<close>; could instead
+ call \<open>simp\<close> using @{thm [source] prod.split} as rewrite.\<close>
lemma case_prodI2:
"\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> c a b) \<Longrightarrow> case p of (a, b) \<Rightarrow> c a b"
@@ -631,10 +630,10 @@
"\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> z \<in> c a b) \<Longrightarrow> z \<in> (case p of (a, b) \<Rightarrow> c a b)"
by (simp only: split_tupled_all) simp
-declare mem_case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
-declare case_prodI2' [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
-declare case_prodI2 [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
-declare case_prodI [intro!] -- \<open>postponed to maintain traditional declaration order!\<close>
+declare mem_case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI2' [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI2 [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
+declare case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
lemma mem_case_prodE [elim!]:
assumes "z \<in> case_prod c p"
@@ -666,7 +665,7 @@
by (rule ext) fast
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
- -- \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
+ \<comment> \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
by (rule ext) blast
(* Do NOT make this a simp rule as it
@@ -1027,7 +1026,7 @@
"[| c: Sigma A B;
!!x y.[| x:A; y:B(x); c=(x,y) |] ==> P
|] ==> P"
- -- \<open>The general elimination rule.\<close>
+ \<comment> \<open>The general elimination rule.\<close>
by (unfold Sigma_def) blast
text \<open>
@@ -1105,7 +1104,7 @@
lemma UN_Times_distrib:
"(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
- -- \<open>Suggested by Pierre Chartier\<close>
+ \<comment> \<open>Suggested by Pierre Chartier\<close>
by blast
lemma split_paired_Ball_Sigma [simp, no_atp]: