--- a/src/Doc/Isar_Ref/Generic.thy Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Apr 01 23:59:56 2015 +0200
@@ -18,12 +18,14 @@
this:
\<close>
+(*<*)experiment begin(*>*)
declare [[show_main_goal = false]]
notepad
begin
note [[show_main_goal = true]]
end
+(*<*)end(*>*)
text \<open>For historical reasons, some tools cannot take the full proof
context into account and merely refer to the background theory.
@@ -816,7 +818,7 @@
lexicographically --- the rewriting engine imitates bubble-sort.
\<close>
-locale AC_example =
+experiment
fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<bullet>" 60)
assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
assumes commute: "x \<bullet> y = y \<bullet> x"
@@ -922,8 +924,10 @@
\end{description}
\<close>
+(*<*)experiment begin(*>*)
declare conjI [simp_break]
declare [[simp_break "?x \<and> ?y"]]
+(*<*)end(*>*)
subsection \<open>Simplification procedures \label{sec:simproc}\<close>
@@ -996,10 +1000,12 @@
the Simplifier loop! Note that a version of this simplification
procedure is already active in Isabelle/HOL.\<close>
+(*<*)experiment begin(*>*)
simproc_setup unit ("x::unit") =
\<open>fn _ => fn _ => fn ct =>
if HOLogic.is_unit (Thm.term_of ct) then NONE
else SOME (mk_meta_eq @{thm unit_eq})\<close>
+(*<*)end(*>*)
text \<open>Since the Simplifier applies simplification procedures
frequently, it is important to make the failure check in ML
@@ -1049,7 +1055,7 @@
As an example, consider the following alternative subgoaler:
\<close>
-ML \<open>
+ML_val \<open>
fun subgoaler_tac ctxt =
assume_tac ctxt ORELSE'
resolve_tac ctxt (Simplifier.prems_of ctxt) ORELSE'
@@ -1873,7 +1879,7 @@
Initially the two wrapper lists are empty, which means no
modification of the step tactics. Safe and unsafe wrappers are added
- to a claset with the functions given below, supplying them with
+ to the context with the functions given below, supplying them with
wrapper names. These names may be used to selectively delete
wrappers.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Wed Apr 01 23:59:56 2015 +0200
@@ -220,6 +220,7 @@
text \<open>The finite powerset operator can be defined inductively like this:\<close>
+(*<*)experiment begin(*>*)
inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
where
empty: "{} \<in> Fin A"
@@ -230,11 +231,13 @@
inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
+(*<*)end(*>*)
text \<open>Common logical connectives can be easily characterized as
non-recursive inductive definitions with parameters, but without
arguments.\<close>
+(*<*)experiment begin(*>*)
inductive AND for A B :: bool
where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
@@ -244,6 +247,7 @@
inductive EXISTS for B :: "'a \<Rightarrow> bool"
where "B a \<Longrightarrow> EXISTS B"
+(*<*)end(*>*)
text \<open>Here the @{text "cases"} or @{text "induct"} rules produced by
the @{command inductive} package coincide with the expected
@@ -378,6 +382,7 @@
boolean expressions, and use @{command primrec} for evaluation
functions that follow the same recursive structure.\<close>
+(*<*)experiment begin(*>*)
datatype 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
@@ -442,6 +447,7 @@
"evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
"evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
by (induct a and b) simp_all
+(*<*)end(*>*)
subsubsection \<open>Example: a substitution function for terms\<close>
@@ -449,6 +455,7 @@
text \<open>Functions on datatypes with nested recursion are also defined
by mutual primitive recursion.\<close>
+(*<*)experiment begin(*>*)
datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
text \<open>A substitution function on type @{typ "('a, 'b) term"} can be
@@ -468,9 +475,12 @@
substitution function, mutual induction is needed:
\<close>
-lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
- "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
+lemma "subst_term (subst_term f1 \<circ> f2) t =
+ subst_term f1 (subst_term f2 t)" and
+ "subst_term_list (subst_term f1 \<circ> f2) ts =
+ subst_term_list f1 (subst_term_list f2 ts)"
by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
+(*<*)end(*>*)
subsubsection \<open>Example: a map function for infinitely branching trees\<close>
@@ -479,6 +489,7 @@
primitive recursion is just as easy.
\<close>
+(*<*)experiment begin(*>*)
datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
@@ -494,6 +505,7 @@
lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
by (induct t) simp_all
+(*<*)end(*>*)
subsection \<open>Proof methods related to recursive definitions\<close>
@@ -748,6 +760,7 @@
names than the existing @{typ "'a list"} that is already in @{theory
Main}:\<close>
+(*<*)experiment begin(*>*)
datatype 'a seq = Empty | Seq 'a "'a seq"
text \<open>We can now prove some simple lemma by structural induction:\<close>
@@ -771,6 +784,7 @@
lemma "Seq x xs \<noteq> xs"
by (induct xs arbitrary: x) simp_all
+(*<*)end(*>*)
section \<open>Records \label{sec:hol-record}\<close>
@@ -1118,6 +1132,7 @@
\end{description}
\<close>
+
subsubsection \<open>Examples\<close>
text \<open>Type definitions permit the introduction of abstract data
@@ -1142,6 +1157,7 @@
\medskip The following trivial example pulls a three-element type
into existence within the formal logical environment of HOL.\<close>
+(*<*)experiment begin(*>*)
typedef three = "{(True, True), (True, False), (False, True)}"
by blast
@@ -1155,11 +1171,14 @@
lemma three_cases:
fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
+(*<*)end(*>*)
text \<open>Note that such trivial constructions are better done with
derived specification mechanisms such as @{command datatype}:\<close>
-datatype three' = One' | Two' | Three'
+(*<*)experiment begin(*>*)
+datatype three = One | Two | Three
+(*<*)end(*>*)
text \<open>This avoids re-doing basic definitions and proofs from the
primitive @{command typedef} above.\<close>
@@ -1988,6 +2007,7 @@
text \<open>The subsequent example is from geometry: collinearity is
invariant by rotation.\<close>
+(*<*)experiment begin(*>*)
type_synonym point = "int \<times> int"
fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
@@ -1999,6 +2019,7 @@
shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
(Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
using assms by (algebra add: collinear.simps)
+(*<*)end(*>*)
text \<open>
See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
--- a/src/Doc/Isar_Ref/Proof.thy Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Apr 01 23:59:56 2015 +0200
@@ -952,6 +952,7 @@
\end{description}
\<close>
+(*<*)experiment begin(*>*)
method_setup my_method1 =
\<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close>
"my first method (without any arguments)"
@@ -965,6 +966,7 @@
\<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
SIMPLE_METHOD' (fn i: int => no_tac))\<close>
"my third method (with theorem arguments and context)"
+(*<*)end(*>*)
section \<open>Generalized elimination \label{sec:obtain}\<close>
--- a/src/Doc/Isar_Ref/Spec.thy Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Apr 01 23:59:56 2015 +0200
@@ -260,10 +260,12 @@
Here is an artificial example of bundling various configuration
options:\<close>
+(*<*)experiment begin(*>*)
bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
lemma "x = x"
including trace by metis
+(*<*)end(*>*)
section \<open>Term definitions \label{sec:term-definitions}\<close>
@@ -1205,6 +1207,7 @@
\end{description}
\<close>
+(*<*)experiment begin(*>*)
attribute_setup my_rule =
\<open>Attrib.thms >> (fn ths =>
Thm.rule_attribute
@@ -1218,6 +1221,7 @@
(fn th: thm => fn context: Context.generic =>
let val context' = context
in context' end))\<close>
+(*<*)end(*>*)
text \<open>
\begin{description}