--- a/src/Doc/Logics_ZF/ZF_examples.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Logics_ZF/ZF_examples.thy Sat Nov 01 14:20:38 2014 +0100
@@ -42,7 +42,7 @@
text {*
@{thm[display] Br_in_bt[no_vars]}
-*};
+*}
subsection{*Primitive recursion*}
@@ -92,7 +92,7 @@
consts
- llist :: "i=>i";
+ llist :: "i=>i"
codatatype
"llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Sat Nov 01 14:20:38 2014 +0100
@@ -298,8 +298,8 @@
\end{quote}
Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
just not true. The correct generalization is
-*};
-(*<*)oops;(*>*)
+*}
+(*<*)oops(*>*)
lemma "itrev xs ys = rev xs @ ys"
(*<*)apply(induction xs, auto)(*>*)
txt{*
--- a/src/Doc/Tutorial/Advanced/Partial.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Advanced/Partial.thy Sat Nov 01 14:20:38 2014 +0100
@@ -138,7 +138,7 @@
*}
lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
-apply(induct_tac f x rule: find.induct);
+apply(induct_tac f x rule: find.induct)
apply simp
done
@@ -191,7 +191,7 @@
\<exists>y. while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x) = (y,y) \<and>
f y = y"
apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
- r = "inv_image (step1 f) fst" in while_rule);
+ r = "inv_image (step1 f) fst" in while_rule)
apply auto
apply(simp add: inv_image_def step1_def)
done
--- a/src/Doc/Tutorial/CTL/Base.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/CTL/Base.thy Sat Nov 01 14:20:38 2014 +0100
@@ -69,7 +69,7 @@
transition system, i.e.\ a relation between states:
*}
-consts M :: "(state \<times> state)set";
+consts M :: "(state \<times> state)set"
text{*\noindent
This is Isabelle's way of declaring a constant without defining it.
--- a/src/Doc/Tutorial/CTL/CTL.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/CTL/CTL.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,6 +1,6 @@
(*<*)theory CTL imports Base begin(*>*)
-subsection{*Computation Tree Logic --- CTL*};
+subsection{*Computation Tree Logic --- CTL*}
text{*\label{sec:CTL}
\index{CTL|(}%
@@ -8,21 +8,21 @@
Let us be adventurous and introduce a more expressive temporal operator.
We extend the datatype
@{text formula} by a new constructor
-*};
+*}
(*<*)
datatype formula = Atom "atom"
| Neg formula
| And formula formula
| AX formula
| EF formula(*>*)
- | AF formula;
+ | AF formula
text{*\noindent
which stands for ``\emph{A}lways in the \emph{F}uture'':
on all infinite paths, at some point the formula holds.
Formalizing the notion of an infinite path is easy
in HOL: it is simply a function from @{typ nat} to @{typ state}.
-*};
+*}
definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where
"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"
@@ -33,7 +33,7 @@
extended by new constructors or equations. This is just a trick of the
presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
a new datatype and a new function.}
-*};
+*}
(*<*)
primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
"s \<Turnstile> Atom a = (a \<in> L s)" |
@@ -47,7 +47,7 @@
text{*\noindent
Model checking @{const AF} involves a function which
is just complicated enough to warrant a separate definition:
-*};
+*}
definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"
@@ -55,7 +55,7 @@
text{*\noindent
Now we define @{term "mc(AF f)"} as the least set @{term T} that includes
@{term"mc f"} and all states all of whose direct successors are in @{term T}:
-*};
+*}
(*<*)
primrec mc :: "formula \<Rightarrow> state set" where
"mc(Atom a) = {s. a \<in> L s}" |
@@ -63,45 +63,45 @@
"mc(And f g) = mc f \<inter> mc g" |
"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
"mc(EF f) = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"|(*>*)
-"mc(AF f) = lfp(af(mc f))";
+"mc(AF f) = lfp(af(mc f))"
text{*\noindent
Because @{const af} is monotone in its second argument (and also its first, but
that is irrelevant), @{term"af A"} has a least fixed point:
-*};
+*}
-lemma mono_af: "mono(af A)";
-apply(simp add: mono_def af_def);
-apply blast;
+lemma mono_af: "mono(af A)"
+apply(simp add: mono_def af_def)
+apply blast
done
(*<*)
-lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)";
-apply(rule monoI);
-by(blast);
+lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)"
+apply(rule monoI)
+by(blast)
lemma EF_lemma:
- "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}";
-apply(rule equalityI);
- apply(rule subsetI);
- apply(simp);
- apply(erule lfp_induct_set);
- apply(rule mono_ef);
- apply(simp);
- apply(blast intro: rtrancl_trans);
-apply(rule subsetI);
-apply(simp, clarify);
-apply(erule converse_rtrancl_induct);
- apply(subst lfp_unfold[OF mono_ef]);
- apply(blast);
-apply(subst lfp_unfold[OF mono_ef]);
-by(blast);
+ "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
+apply(rule equalityI)
+ apply(rule subsetI)
+ apply(simp)
+ apply(erule lfp_induct_set)
+ apply(rule mono_ef)
+ apply(simp)
+ apply(blast intro: rtrancl_trans)
+apply(rule subsetI)
+apply(simp, clarify)
+apply(erule converse_rtrancl_induct)
+ apply(subst lfp_unfold[OF mono_ef])
+ apply(blast)
+apply(subst lfp_unfold[OF mono_ef])
+by(blast)
(*>*)
text{*
All we need to prove now is @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.
This time we prove the two inclusions separately, starting
with the easy one:
-*};
+*}
theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}"
@@ -114,9 +114,9 @@
\end{center}
The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
a decision that \isa{auto} takes for us:
-*};
-apply(rule lfp_lowerbound);
-apply(auto simp add: af_def Paths_def);
+*}
+apply(rule lfp_lowerbound)
+apply(auto simp add: af_def Paths_def)
txt{*
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
@@ -124,11 +124,11 @@
The rest is automatic, which is surprising because it involves
finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
for @{text"\<forall>p"}.
-*};
+*}
-apply(erule_tac x = "p 1" in allE);
-apply(auto);
-done;
+apply(erule_tac x = "p 1" in allE)
+apply(auto)
+done
text{*
@@ -143,14 +143,14 @@
The one-step argument in the sketch above
is proved by a variant of contraposition:
-*};
+*}
lemma not_in_lfp_afD:
- "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
-apply(erule contrapos_np);
-apply(subst lfp_unfold[OF mono_af]);
-apply(simp add: af_def);
-done;
+ "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))"
+apply(erule contrapos_np)
+apply(subst lfp_unfold[OF mono_af])
+apply(simp add: af_def)
+done
text{*\noindent
We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
@@ -159,7 +159,7 @@
Now we iterate this process. The following construction of the desired
path is parameterized by a predicate @{term Q} that should hold along the path:
-*};
+*}
primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where
"path s Q 0 = s" |
@@ -175,41 +175,41 @@
Let us show that if each state @{term s} that satisfies @{term Q}
has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path:
-*};
+*}
lemma infinity_lemma:
"\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow>
- \<exists>p\<in>Paths s. \<forall>i. Q(p i)";
+ \<exists>p\<in>Paths s. \<forall>i. Q(p i)"
txt{*\noindent
First we rephrase the conclusion slightly because we need to prove simultaneously
both the path property and the fact that @{term Q} holds:
-*};
+*}
apply(subgoal_tac
- "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))");
+ "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))")
txt{*\noindent
From this proposition the original goal follows easily:
-*};
+*}
- apply(simp add: Paths_def, blast);
+ apply(simp add: Paths_def, blast)
txt{*\noindent
The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
-*};
+*}
-apply(rule_tac x = "path s Q" in exI);
-apply(clarsimp);
+apply(rule_tac x = "path s Q" in exI)
+apply(clarsimp)
txt{*\noindent
After simplification and clarification, the subgoal has the following form:
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
It invites a proof by induction on @{term i}:
-*};
+*}
-apply(induct_tac i);
- apply(simp);
+apply(induct_tac i)
+ apply(simp)
txt{*\noindent
After simplification, the base case boils down to
@@ -223,9 +223,9 @@
two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and
@{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
@{text fast} can prove the base case quickly:
-*};
+*}
- apply(fast intro: someI2_ex);
+ apply(fast intro: someI2_ex)
txt{*\noindent
What is worth noting here is that we have used \methdx{fast} rather than
@@ -242,15 +242,15 @@
occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely
show the proof commands but do not describe the details:
-*};
+*}
-apply(simp);
-apply(rule someI2_ex);
- apply(blast);
-apply(rule someI2_ex);
- apply(blast);
-apply(blast);
-done;
+apply(simp)
+apply(rule someI2_ex)
+ apply(blast)
+apply(rule someI2_ex)
+ apply(blast)
+apply(blast)
+done
text{*
Function @{const path} has fulfilled its purpose now and can be forgotten.
@@ -261,58 +261,58 @@
@{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
is extensionally equal to @{term"path s Q"},
where @{term rec_nat} is the predefined primitive recursor on @{typ nat}.
-*};
+*}
(*<*)
lemma
"\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>
- \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
+ \<exists> p\<in>Paths s. \<forall> i. Q(p i)"
apply(subgoal_tac
- "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
- apply(simp add: Paths_def);
- apply(blast);
-apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
-apply(simp);
-apply(intro strip);
-apply(induct_tac i);
- apply(simp);
- apply(fast intro: someI2_ex);
-apply(simp);
-apply(rule someI2_ex);
- apply(blast);
-apply(rule someI2_ex);
- apply(blast);
-by(blast);
+ "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))")
+ apply(simp add: Paths_def)
+ apply(blast)
+apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI)
+apply(simp)
+apply(intro strip)
+apply(induct_tac i)
+ apply(simp)
+ apply(fast intro: someI2_ex)
+apply(simp)
+apply(rule someI2_ex)
+ apply(blast)
+apply(rule someI2_ex)
+ apply(blast)
+by(blast)
(*>*)
text{*
At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
-*};
+*}
-theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)";
+theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)"
txt{*\noindent
The proof is again pointwise and then by contraposition:
-*};
+*}
-apply(rule subsetI);
-apply(erule contrapos_pp);
-apply simp;
+apply(rule subsetI)
+apply(erule contrapos_pp)
+apply simp
txt{*
@{subgoals[display,indent=0,goals_limit=1]}
Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
premise of @{thm[source]infinity_lemma} and the original subgoal:
-*};
+*}
-apply(drule infinity_lemma);
+apply(drule infinity_lemma)
txt{*
@{subgoals[display,indent=0,margin=65]}
Both are solved automatically:
-*};
+*}
- apply(auto dest: not_in_lfp_afD);
-done;
+ apply(auto dest: not_in_lfp_afD)
+done
text{*
If you find these proofs too complicated, we recommend that you read
@@ -324,9 +324,9 @@
@{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
*}
-theorem "mc f = {s. s \<Turnstile> f}";
-apply(induct_tac f);
-apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
+theorem "mc f = {s. s \<Turnstile> f}"
+apply(induct_tac f)
+apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
done
text{*
@@ -377,22 +377,22 @@
apply simp
done
-lemma mono_eufix: "mono(eufix A B)";
-apply(simp add: mono_def eufix_def);
-apply blast;
+lemma mono_eufix: "mono(eufix A B)"
+apply(simp add: mono_def eufix_def)
+apply blast
done
-lemma "eusem A B \<subseteq> lfp(eufix A B)";
-apply(clarsimp simp add: eusem_def);
-apply(erule rev_mp);
-apply(rule_tac x = x in spec);
-apply(induct_tac p);
+lemma "eusem A B \<subseteq> lfp(eufix A B)"
+apply(clarsimp simp add: eusem_def)
+apply(erule rev_mp)
+apply(rule_tac x = x in spec)
+apply(induct_tac p)
apply(subst lfp_unfold[OF mono_eufix])
- apply(simp add: eufix_def);
-apply(clarsimp);
+ apply(simp add: eufix_def)
+apply(clarsimp)
apply(subst lfp_unfold[OF mono_eufix])
-apply(simp add: eufix_def);
-apply blast;
+apply(simp add: eufix_def)
+apply blast
done
(*
--- a/src/Doc/Tutorial/CTL/CTLind.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/CTL/CTLind.thy Sat Nov 01 14:20:38 2014 +0100
@@ -29,7 +29,7 @@
for s :: state and A :: "state set"
where
"s \<in> Avoid s A"
- | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
+ | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A"
text{*
It is easy to see that for any infinite @{term A}-avoiding path @{term f}
@@ -44,12 +44,12 @@
lemma ex_infinite_path[rule_format]:
"t \<in> Avoid s A \<Longrightarrow>
- \<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)";
-apply(erule Avoid.induct);
- apply(blast);
-apply(clarify);
-apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec);
-apply(simp_all add: Paths_def split: nat.split);
+ \<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)"
+apply(erule Avoid.induct)
+ apply(blast)
+apply(clarify)
+apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec)
+apply(simp_all add: Paths_def split: nat.split)
done
text{*\noindent
@@ -69,7 +69,7 @@
*}
lemma Avoid_in_lfp[rule_format(no_asm)]:
- "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
+ "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)"
txt{*\noindent
The proof is by induction on the ``distance'' between @{term t} and @{term
@@ -87,9 +87,9 @@
moment we assume this and proceed with the induction:
*}
-apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}");
- apply(erule_tac a = t in wf_induct);
- apply(clarsimp);
+apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}")
+ apply(erule_tac a = t in wf_induct)
+ apply(clarsimp)
(*<*)apply(rename_tac t)(*>*)
txt{*\noindent
@@ -106,9 +106,9 @@
@{term"lfp(af A)"}. Mechanically:
*}
- apply(subst lfp_unfold[OF mono_af]);
- apply(simp (no_asm) add: af_def);
- apply(blast intro: Avoid.intros);
+ apply(subst lfp_unfold[OF mono_af])
+ apply(simp (no_asm) add: af_def)
+ apply(blast intro: Avoid.intros)
txt{*
Having proved the main goal, we return to the proof obligation that the
@@ -121,11 +121,11 @@
@{term A}-avoiding path starting in @{term s} follows, contradiction.
*}
-apply(erule contrapos_pp);
-apply(simp add: wf_iff_no_infinite_down_chain);
-apply(erule exE);
-apply(rule ex_infinite_path);
-apply(auto simp add: Paths_def);
+apply(erule contrapos_pp)
+apply(simp add: wf_iff_no_infinite_down_chain)
+apply(erule exE)
+apply(rule ex_infinite_path)
+apply(auto simp add: Paths_def)
done
text{*
@@ -141,8 +141,8 @@
by the first @{const Avoid}-rule. Isabelle confirms this:%
\index{CTL|)}*}
-theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
-by(auto elim: Avoid_in_lfp intro: Avoid.intros);
+theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)"
+by(auto elim: Avoid_in_lfp intro: Avoid.intros)
(*<*)end(*>*)
--- a/src/Doc/Tutorial/CodeGen/CodeGen.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy Sat Nov 01 14:20:38 2014 +0100
@@ -15,10 +15,10 @@
appropriate function itself.
*}
-type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
+type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
datatype (dead 'a, 'v) expr = Cex 'v
| Vex 'a
- | Bex "'v binop" "('a,'v)expr" "('a,'v)expr";
+ | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"
text{*\noindent
The three constructors represent constants, variables and the application of
@@ -42,7 +42,7 @@
datatype (dead 'a, 'v) instr = Const 'v
| Load 'a
- | Apply "'v binop";
+ | Apply "'v binop"
text{*
The execution of the stack machine is modelled by a function
@@ -83,22 +83,22 @@
Now we have to prove the correctness of the compiler, i.e.\ that the
execution of a compiled expression results in the value of the expression:
*}
-theorem "exec (compile e) s [] = [value e s]";
-(*<*)oops;(*>*)
+theorem "exec (compile e) s [] = [value e s]"
+(*<*)oops(*>*)
text{*\noindent
This theorem needs to be generalized:
*}
-theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
+theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs"
txt{*\noindent
It will be proved by induction on @{term"e"} followed by simplification.
First, we must prove a lemma about executing the concatenation of two
instruction sequences:
*}
-(*<*)oops;(*>*)
+(*<*)oops(*>*)
lemma exec_app[simp]:
- "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
+ "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"
txt{*\noindent
This requires induction on @{term"xs"} and ordinary simplification for the
@@ -106,7 +106,7 @@
that contains two @{text"case"}-expressions over instructions. Thus we add
automatic case splitting, which finishes the proof:
*}
-apply(induct_tac xs, simp, simp split: instr.split);
+apply(induct_tac xs, simp, simp split: instr.split)
(*<*)done(*>*)
text{*\noindent
Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
@@ -114,10 +114,10 @@
rewritten as
*}
(*<*)
-declare exec_app[simp del];
-lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
+declare exec_app[simp del]
+lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"
(*>*)
-apply(induct_tac xs, simp_all split: instr.split);
+apply(induct_tac xs, simp_all split: instr.split)
(*<*)done(*>*)
text{*\noindent
Although this is more compact, it is less clear for the reader of the proof.
@@ -129,7 +129,7 @@
\index{compiling expressions example|)}
*}
(*<*)
-theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
-by(induct_tac e, auto);
+theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs"
+by(induct_tac e, auto)
end
(*>*)
--- a/src/Doc/Tutorial/Datatype/ABexpr.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Datatype/ABexpr.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory ABexpr imports Main begin;
+theory ABexpr imports Main begin
(*>*)
text{*
@@ -24,7 +24,7 @@
| Num nat
and 'a bexp = Less "'a aexp" "'a aexp"
| And "'a bexp" "'a bexp"
- | Neg "'a bexp";
+ | Neg "'a bexp"
text{*\noindent
Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
@@ -92,13 +92,13 @@
*}
lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
- evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
-apply(induct_tac a and b);
+ evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"
+apply(induct_tac a and b)
txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:
*}
-apply simp_all;
+apply simp_all
(*<*)done(*>*)
text{*
--- a/src/Doc/Tutorial/Datatype/Fundata.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Datatype/Fundata.thy Sat Nov 01 14:20:38 2014 +0100
@@ -34,10 +34,10 @@
The following lemma has a simple proof by induction: *}
-lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
+lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
apply(induct_tac T, simp_all)
done
-(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
+(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
apply(induct_tac T, rename_tac[2] F)(*>*)
txt{*\noindent
Because of the function type, the proof state after induction looks unusual.
--- a/src/Doc/Tutorial/Datatype/Nested.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Datatype/Nested.thy Sat Nov 01 14:20:38 2014 +0100
@@ -12,7 +12,7 @@
where function symbols can be applied to a list of arguments:
*}
(*<*)hide_const Var(*>*)
-datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
+datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"
text{*\noindent
Note that we need to quote @{text term} on the left to avoid confusion with
@@ -66,8 +66,8 @@
*}
lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and>
- substs Var ts = (ts::('v,'f)term list)";
-apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all);
+ substs Var ts = (ts::('v,'f)term list)"
+apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all)
done
text{*\noindent
--- a/src/Doc/Tutorial/Datatype/unfoldnested.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Datatype/unfoldnested.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory unfoldnested imports Main begin;
+theory unfoldnested imports Main begin
(*>*)
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
--- a/src/Doc/Tutorial/Fun/fun0.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Fun/fun0.thy Sat Nov 01 14:20:38 2014 +0100
@@ -27,7 +27,7 @@
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"sep a [] = []" |
"sep a [x] = [x]" |
-"sep a (x#y#zs) = x # a # sep a (y#zs)";
+"sep a (x#y#zs) = x # a # sep a (y#zs)"
text{*\noindent
This time the length of the list decreases with the
@@ -217,7 +217,7 @@
this lemma by recursion induction over @{term"sep"}:
*}
-apply(induct_tac x xs rule: sep.induct);
+apply(induct_tac x xs rule: sep.induct)
txt{*\noindent
The resulting proof state has three subgoals corresponding to the three
@@ -226,7 +226,7 @@
The rest is pure simplification:
*}
-apply simp_all;
+apply simp_all
done
text{*\noindent The proof goes smoothly because the induction rule
--- a/src/Doc/Tutorial/Ifexpr/Ifexpr.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Ifexpr/Ifexpr.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory Ifexpr imports Main begin;
+theory Ifexpr imports Main begin
(*>*)
subsection{*Case Study: Boolean Expressions*}
@@ -19,7 +19,7 @@
*}
datatype boolex = Const bool | Var nat | Neg boolex
- | And boolex boolex;
+ | And boolex boolex
text{*\noindent
The two constants are represented by @{term"Const True"} and
@@ -51,7 +51,7 @@
(@{term"IF"}):
*}
-datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
text{*\noindent
The evaluation of If-expressions proceeds as for @{typ"boolex"}:
@@ -82,14 +82,14 @@
value of its argument:
*}
-lemma "valif (bool2if b) env = value b env";
+lemma "valif (bool2if b) env = value b env"
txt{*\noindent
The proof is canonical:
*}
-apply(induct_tac b);
-apply(auto);
+apply(induct_tac b)
+apply(auto)
done
text{*\noindent
@@ -120,7 +120,7 @@
transformation preserves the value of the expression:
*}
-theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
+theorem "valif (norm b) env = valif b env"(*<*)oops(*>*)
text{*\noindent
The proof is canonical, provided we first show the following simplification
@@ -128,14 +128,14 @@
*}
lemma [simp]:
- "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
+ "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env"
(*<*)
-apply(induct_tac b);
-by(auto);
+apply(induct_tac b)
+by(auto)
-theorem "valif (norm b) env = valif b env";
-apply(induct_tac b);
-by(auto);
+theorem "valif (norm b) env = valif b env"
+apply(induct_tac b)
+by(auto)
(*>*)
text{*\noindent
Note that the lemma does not have a name, but is implicitly used in the proof
@@ -156,14 +156,14 @@
normality of @{term"normif"}:
*}
-lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
+lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)"
(*<*)
-apply(induct_tac b);
-by(auto);
+apply(induct_tac b)
+by(auto)
-theorem "normal(norm b)";
-apply(induct_tac b);
-by(auto);
+theorem "normal(norm b)"
+apply(induct_tac b)
+by(auto)
(*>*)
text{*\medskip
--- a/src/Doc/Tutorial/Inductive/Star.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Inductive/Star.thy Sat Nov 01 14:20:38 2014 +0100
@@ -39,7 +39,7 @@
*}
lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
-by(blast intro: rtc_step);
+by(blast intro: rtc_step)
text{*\noindent
Although the lemma itself is an unremarkable consequence of the basic rules,
@@ -110,8 +110,8 @@
@{subgoals[display,indent=0]}
*}
- apply(blast);
-apply(blast intro: rtc_step);
+ apply(blast)
+apply(blast intro: rtc_step)
done
text{*
@@ -134,16 +134,16 @@
*}
lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
-apply(erule rtc2.induct);
- apply(blast);
- apply(blast);
-apply(blast intro: rtc_trans);
+apply(erule rtc2.induct)
+ apply(blast)
+ apply(blast)
+apply(blast intro: rtc_trans)
done
lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"
-apply(erule rtc.induct);
- apply(blast intro: rtc2.intros);
-apply(blast intro: rtc2.intros);
+apply(erule rtc.induct)
+ apply(blast intro: rtc2.intros)
+apply(blast intro: rtc2.intros)
done
text{*
@@ -167,8 +167,8 @@
*}
(*<*)
lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
-apply(erule rtc.induct);
- apply blast;
+apply(erule rtc.induct)
+ apply blast
apply(blast intro: rtc_step)
done
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory AdvancedInd imports Main begin;
+theory AdvancedInd imports Main begin
(*>*)
text{*\noindent
@@ -9,9 +9,9 @@
(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
with an extended example of induction (\S\ref{sec:CTL-revisited}).
-*};
+*}
-subsection{*Massaging the Proposition*};
+subsection{*Massaging the Proposition*}
text{*\label{sec:ind-var-in-prems}
Often we have assumed that the theorem to be proved is already in a form
@@ -19,7 +19,7 @@
Here is an example.
Since @{term"hd"} and @{term"last"} return the first and last element of a
non-empty list, this lemma looks easy to prove:
-*};
+*}
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
apply(induct_tac xs)
@@ -51,11 +51,11 @@
implication~(@{text"\<longrightarrow>"}), letting
\attrdx{rule_format} (\S\ref{sec:forward}) convert the
result to the usual @{text"\<Longrightarrow>"} form:
-*};
-(*<*)oops;(*>*)
-lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
+*}
+(*<*)oops(*>*)
+lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs"
(*<*)
-apply(induct_tac xs);
+apply(induct_tac xs)
(*>*)
txt{*\noindent
@@ -112,7 +112,7 @@
*}
(*<*)by auto(*>*)
-subsection{*Beyond Structural and Recursion Induction*};
+subsection{*Beyond Structural and Recursion Induction*}
text{*\label{sec:complete-ind}
So far, inductive proofs were by structural induction for
@@ -130,7 +130,7 @@
@{thm[display]"nat_less_induct"[no_vars]}
As an application, we prove a property of the following
function:
-*};
+*}
axiomatization f :: "nat \<Rightarrow> nat"
where f_ax: "f(f(n)) < f(Suc(n))"
@@ -148,17 +148,17 @@
The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
above, we have to phrase the proposition as follows to allow induction:
-*};
+*}
-lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
+lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
txt{*\noindent
To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
the same general induction method as for recursion induction (see
\S\ref{sec:fun-induction}):
-*};
+*}
-apply(induct_tac k rule: nat_less_induct);
+apply(induct_tac k rule: nat_less_induct)
txt{*\noindent
We get the following proof state:
@@ -203,17 +203,17 @@
proofs are easy to write but hard to read and understand.
The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:
-*};
+*}
-lemmas f_incr = f_incr_lem[rule_format, OF refl];
+lemmas f_incr = f_incr_lem[rule_format, OF refl]
text{*\noindent
The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}.
We could have included this derivation in the original statement of the lemma:
-*};
+*}
-lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
-(*<*)oops;(*>*)
+lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
+(*<*)oops(*>*)
text{*
\begin{exercise}
@@ -237,7 +237,7 @@
where @{term f} may be any function into type @{typ nat}.
*}
-subsection{*Derivation of New Induction Schemas*};
+subsection{*Derivation of New Induction Schemas*}
text{*\label{sec:derive-ind}
\index{induction!deriving new schemas}%
@@ -246,18 +246,18 @@
of @{thm[source]nat_less_induct}. Assume we only have structural induction
available for @{typ"nat"} and want to derive complete induction. We
must generalize the statement as shown:
-*};
+*}
-lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
-apply(induct_tac n);
+lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m"
+apply(induct_tac n)
txt{*\noindent
The base case is vacuously true. For the induction step (@{prop"m <
Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
hypothesis and case @{prop"m = n"} follows from the assumption, again using
the induction hypothesis:
-*};
- apply(blast);
+*}
+ apply(blast)
by(blast elim: less_SucE)
text{*\noindent
@@ -270,10 +270,10 @@
and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
happens automatically when we add the lemma as a new premise to the
desired goal:
-*};
+*}
-theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
-by(insert induct_lem, blast);
+theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"
+by(insert induct_lem, blast)
text{*
HOL already provides the mother of
--- a/src/Doc/Tutorial/Misc/Itrev.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Itrev.thy Sat Nov 01 14:20:38 2014 +0100
@@ -58,15 +58,15 @@
Naturally, we would like to show that @{term"itrev"} does indeed reverse
its first argument provided the second one is empty:
-*};
+*}
-lemma "itrev xs [] = rev xs";
+lemma "itrev xs [] = rev xs"
txt{*\noindent
There is no choice as to the induction variable, and we immediately simplify:
-*};
+*}
-apply(induct_tac xs, simp_all);
+apply(induct_tac xs, simp_all)
txt{*\noindent
Unfortunately, this attempt does not prove
@@ -80,9 +80,9 @@
\end{quote}
Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
just not true. The correct generalization is
-*};
-(*<*)oops;(*>*)
-lemma "itrev xs ys = rev xs @ ys";
+*}
+(*<*)oops(*>*)
+lemma "itrev xs ys = rev xs @ ys"
(*<*)apply(induct_tac xs, simp_all)(*>*)
txt{*\noindent
If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
@@ -100,11 +100,11 @@
the subgoal, but the induction hypothesis needs to be applied with
@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
for all @{term"ys"} instead of a fixed one:
-*};
-(*<*)oops;(*>*)
-lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
+*}
+(*<*)oops(*>*)
+lemma "\<forall>ys. itrev xs ys = rev xs @ ys"
(*<*)
-by(induct_tac xs, simp_all);
+by(induct_tac xs, simp_all)
(*>*)
text{*\noindent
--- a/src/Doc/Tutorial/Misc/Option2.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Option2.thy Sat Nov 01 14:20:38 2014 +0100
@@ -9,7 +9,7 @@
Our final datatype is very simple but still eminently useful:
*}
-datatype 'a option = None | Some 'a;
+datatype 'a option = None | Some 'a
text{*\noindent
Frequently one needs to add a distinguished element to some existing type.
--- a/src/Doc/Tutorial/Misc/Tree.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Tree.thy Sat Nov 01 14:20:38 2014 +0100
@@ -6,25 +6,25 @@
Define the datatype of \rmindex{binary trees}:
*}
-datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*)
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
"mirror Tip = Tip" |
-"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
+"mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
text{*\noindent
Define a function @{term"mirror"} that mirrors a binary tree
by swapping subtrees recursively. Prove
*}
-lemma mirror_mirror: "mirror(mirror t) = t";
+lemma mirror_mirror: "mirror(mirror t) = t"
(*<*)
-apply(induct_tac t);
-by(auto);
+apply(induct_tac t)
+by(auto)
primrec flatten :: "'a tree => 'a list" where
"flatten Tip = []" |
-"flatten (Node l x r) = flatten l @ [x] @ flatten r";
+"flatten (Node l x r) = flatten l @ [x] @ flatten r"
(*>*)
text{*\noindent
@@ -32,10 +32,10 @@
by traversing it in infix order. Prove
*}
-lemma "flatten(mirror t) = rev(flatten t)";
+lemma "flatten(mirror t) = rev(flatten t)"
(*<*)
-apply(induct_tac t);
-by(auto);
+apply(induct_tac t)
+by(auto)
end
(*>*)
--- a/src/Doc/Tutorial/Misc/Tree2.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Tree2.thy Sat Nov 01 14:20:38 2014 +0100
@@ -16,7 +16,7 @@
(*<*)
lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs"
apply(induct_tac t)
-by(auto);
+by(auto)
(*>*)
lemma "flatten2 t [] = flatten t"
(*<*)
--- a/src/Doc/Tutorial/Misc/case_exprs.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/case_exprs.thy Sat Nov 01 14:20:38 2014 +0100
@@ -52,8 +52,8 @@
by \methdx{case_tac}. Here is a trivial example:
*}
-lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
-apply(case_tac xs);
+lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs"
+apply(case_tac xs)
txt{*\noindent
results in the proof state
--- a/src/Doc/Tutorial/Misc/fakenat.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/fakenat.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory fakenat imports Main begin;
+theory fakenat imports Main begin
(*>*)
text{*\noindent
--- a/src/Doc/Tutorial/Misc/pairs2.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/pairs2.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory pairs2 imports Main begin;
+theory pairs2 imports Main begin
(*>*)
text{*\label{sec:pairs}\index{pairs and tuples}
HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
--- a/src/Doc/Tutorial/Misc/prime_def.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/prime_def.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory prime_def imports Main begin;
+theory prime_def imports Main begin
consts prime :: "nat \<Rightarrow> bool"
(*>*)
text{*
--- a/src/Doc/Tutorial/Protocol/Event.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy Sat Nov 01 14:20:38 2014 +0100
@@ -278,7 +278,7 @@
text{*For proving @{text new_keys_not_used}*}
lemma keysFor_parts_insert:
"[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |]
- ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H";
+ ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"
by (force
dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
--- a/src/Doc/Tutorial/Protocol/Message.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sat Nov 01 14:20:38 2014 +0100
@@ -743,7 +743,7 @@
lemma Fake_parts_insert_in_Un:
"[|Z \<in> parts (insert X H); X: synth (analz H)|]
- ==> Z \<in> synth (analz H) \<union> parts H";
+ ==> Z \<in> synth (analz H) \<union> parts H"
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
text{*@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put
@@ -882,24 +882,24 @@
apply (drule synth_mono)
apply (simp add: synth_idem)
apply (rule equalityI)
-apply (simp add: );
+apply (simp add: )
apply (rule synth_analz_mono, blast)
done
text{*Two generalizations of @{text analz_insert_eq}*}
lemma gen_analz_insert_eq [rule_format]:
- "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
+ "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
lemma synth_analz_insert_eq [rule_format]:
"X \<in> synth (analz H)
- ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
+ ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
apply (erule synth.induct)
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
done
lemma Fake_parts_sing:
- "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
+ "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
apply (rule subset_trans)
apply (erule_tac [2] Fake_parts_insert)
apply (rule parts_mono, blast)
--- a/src/Doc/Tutorial/Recdef/Induction.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Recdef/Induction.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory Induction imports examples simplification begin;
+theory Induction imports examples simplification begin
(*>*)
text{*
@@ -19,7 +19,7 @@
involving the predefined @{term"map"} functional on lists:
*}
-lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
+lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
txt{*\noindent
Note that @{term"map f xs"}
@@ -27,7 +27,7 @@
this lemma by recursion induction over @{term"sep"}:
*}
-apply(induct_tac x xs rule: sep.induct);
+apply(induct_tac x xs rule: sep.induct)
txt{*\noindent
The resulting proof state has three subgoals corresponding to the three
@@ -36,7 +36,7 @@
The rest is pure simplification:
*}
-apply simp_all;
+apply simp_all
done
text{*
--- a/src/Doc/Tutorial/Recdef/examples.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Recdef/examples.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,16 +1,16 @@
(*<*)
-theory examples imports Main begin;
+theory examples imports Main begin
(*>*)
text{*
Here is a simple example, the \rmindex{Fibonacci function}:
*}
-consts fib :: "nat \<Rightarrow> nat";
+consts fib :: "nat \<Rightarrow> nat"
recdef fib "measure(\<lambda>n. n)"
"fib 0 = 0"
"fib (Suc 0) = 1"
- "fib (Suc(Suc x)) = fib x + fib (Suc x)";
+ "fib (Suc(Suc x)) = fib x + fib (Suc x)"
text{*\noindent
\index{measure functions}%
@@ -27,11 +27,11 @@
between any two elements of a list:
*}
-consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
+consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"
recdef sep "measure (\<lambda>(a,xs). length xs)"
"sep(a, []) = []"
"sep(a, [x]) = [x]"
- "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
+ "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
text{*\noindent
This time the measure is the length of the list, which decreases with the
@@ -43,20 +43,20 @@
need not be exhaustive:
*}
-consts last :: "'a list \<Rightarrow> 'a";
+consts last :: "'a list \<Rightarrow> 'a"
recdef last "measure (\<lambda>xs. length xs)"
"last [x] = x"
- "last (x#y#zs) = last (y#zs)";
+ "last (x#y#zs) = last (y#zs)"
text{*
Overlapping patterns are disambiguated by taking the order of equations into
account, just as in functional programming:
*}
-consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
+consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"
recdef sep1 "measure (\<lambda>(a,xs). length xs)"
"sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
- "sep1(a, xs) = xs";
+ "sep1(a, xs) = xs"
text{*\noindent
To guarantee that the second equation can only be applied if the first
@@ -74,10 +74,10 @@
arguments as in the following definition:
\end{warn}
*}
-consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
+consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
recdef sep2 "measure length"
"sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
- "sep2 xs = (\<lambda>a. xs)";
+ "sep2 xs = (\<lambda>a. xs)"
text{*
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
@@ -85,10 +85,10 @@
degenerates to the empty set @{term"{}"}:
*}
-consts swap12 :: "'a list \<Rightarrow> 'a list";
+consts swap12 :: "'a list \<Rightarrow> 'a list"
recdef swap12 "{}"
"swap12 (x#y#zs) = y#x#zs"
- "swap12 zs = zs";
+ "swap12 zs = zs"
(*<*)
end
--- a/src/Doc/Tutorial/Recdef/simplification.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Recdef/simplification.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory simplification imports Main begin;
+theory simplification imports Main begin
(*>*)
text{*
@@ -12,9 +12,9 @@
Let us look at an example:
*}
-consts gcd :: "nat\<times>nat \<Rightarrow> nat";
+consts gcd :: "nat\<times>nat \<Rightarrow> nat"
recdef gcd "measure (\<lambda>(m,n).n)"
- "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
+ "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
text{*\noindent
According to the measure function, the second argument should decrease with
@@ -50,10 +50,10 @@
following alternative definition suggests itself:
*}
-consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
+consts gcd1 :: "nat\<times>nat \<Rightarrow> nat"
recdef gcd1 "measure (\<lambda>(m,n).n)"
"gcd1 (m, 0) = m"
- "gcd1 (m, n) = gcd1(n, m mod n)";
+ "gcd1 (m, n) = gcd1(n, m mod n)"
text{*\noindent
@@ -65,9 +65,9 @@
which is also available for @{typ bool} and is not split automatically:
*}
-consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
+consts gcd2 :: "nat\<times>nat \<Rightarrow> nat"
recdef gcd2 "measure (\<lambda>(m,n).n)"
- "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
+ "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))"
text{*\noindent
This is probably the neatest solution next to pattern matching, and it is
@@ -78,12 +78,12 @@
these lemmas:
*}
-lemma [simp]: "gcd (m, 0) = m";
-apply(simp);
+lemma [simp]: "gcd (m, 0) = m"
+apply(simp)
done
-lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
-apply(simp);
+lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"
+apply(simp)
done
text{*\noindent
--- a/src/Doc/Tutorial/Rules/Blast.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Rules/Blast.thy Sat Nov 01 14:20:38 2014 +0100
@@ -13,7 +13,7 @@
(\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
(\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
(\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
- \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
+ \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"
by blast
lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
@@ -26,12 +26,12 @@
@{thm[display] finite_Un}
\rulename{finite_Un}}
-*};
+*}
lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])"
apply (induct_tac xs)
- by (simp_all);
+ by (simp_all)
(*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*)
end
--- a/src/Doc/Tutorial/Rules/Force.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Rules/Force.thy Sat Nov 01 14:20:38 2014 +0100
@@ -2,7 +2,7 @@
(*Use Divides rather than Main to experiment with the first proof.
Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
-declare div_mult_self_is_m [simp del];
+declare div_mult_self_is_m [simp del]
lemma div_mult_self_is_m:
"0<n \<Longrightarrow> (m*n) div n = (m::nat)"
@@ -21,14 +21,14 @@
goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ Q\ x{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\isanewline
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ xa{\isachardot}\ {\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x{\isacharsemicolon}\ Q\ xa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ {\isasymand}\ Q\ x
-*};
+*}
text {*
couldn't find a good example of clarsimp
@{thm[display]"someI"}
\rulename{someI}
-*};
+*}
lemma "\<lbrakk>Q a; P a\<rbrakk> \<Longrightarrow> P (SOME x. P x \<and> Q x) \<and> Q (SOME x. P x \<and> Q x)"
apply (rule someI)
--- a/src/Doc/Tutorial/Rules/Forward.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Rules/Forward.thy Sat Nov 01 14:20:38 2014 +0100
@@ -11,7 +11,7 @@
(** Commutativity **)
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
-apply (auto simp add: is_gcd_def);
+apply (auto simp add: is_gcd_def)
done
lemma gcd_commute: "gcd m n = gcd n m"
@@ -48,15 +48,15 @@
text {*
@{thm[display] gcd_mult_distrib2}
\rulename{gcd_mult_distrib2}
-*};
+*}
text{*\noindent
of, simplified
*}
-lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
-lemmas gcd_mult_1 = gcd_mult_0 [simplified];
+lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
+lemmas gcd_mult_1 = gcd_mult_0 [simplified]
lemmas where1 = gcd_mult_distrib2 [where m=1]
@@ -82,23 +82,23 @@
@{thm[display] sym}
\rulename{sym}
-*};
+*}
-lemmas gcd_mult0 = gcd_mult_1 [THEN sym];
+lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
(*not quite right: we need ?k but this gives k*)
-lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
+lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
(*better in one step!*)
text {*
more legible, and variables properly generalized
-*};
+*}
lemma gcd_mult [simp]: "gcd k (k*n) = k"
by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
-lemmas gcd_self0 = gcd_mult [of k 1, simplified];
+lemmas gcd_self0 = gcd_mult [of k 1, simplified]
text {*
@@ -107,7 +107,7 @@
@{thm[display] gcd_self0}
\rulename{gcd_self0}
-*};
+*}
text {*
Rules handy with THEN
@@ -117,12 +117,12 @@
@{thm[display] iffD2}
\rulename{iffD2}
-*};
+*}
text {*
again: more legible, and variables properly generalized
-*};
+*}
lemma gcd_self [simp]: "gcd k k = k"
by (rule gcd_mult [of k 1, simplified])
@@ -143,12 +143,12 @@
txt{*
before using arg_cong
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (drule_tac f="\<lambda>x. x mod u" in arg_cong)
txt{*
after using arg_cong
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (simp add: mod_Suc)
done
@@ -172,7 +172,7 @@
txt{*@{subgoals[display,indent=0,margin=65]}*}
apply simp
txt{*@{subgoals[display,indent=0,margin=65]}*}
-apply (erule_tac t="m" in ssubst);
+apply (erule_tac t="m" in ssubst)
apply simp
done
@@ -185,16 +185,16 @@
@{thm[display] mod_div_equality}
\rulename{mod_div_equality}
-*};
+*}
(*MOVED to Force.thy, which now depends only on Divides.thy
lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
*)
-lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
+lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"
by (auto intro: relprime_dvd_mult elim: dvdE)
-lemma relprime_20_81: "gcd 20 81 = 1";
+lemma relprime_20_81: "gcd 20 81 = 1"
by (simp add: gcd.simps)
text {*
@@ -214,20 +214,20 @@
@{thm[display] dvd_add [OF dvd_refl dvd_refl]}
@{thm[display] dvd_add [OF _ dvd_refl]}
-*};
+*}
-lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)";
+lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)"
apply (subgoal_tac "z = 34 \<or> z = 36")
txt{*
the tactic leaves two subgoals:
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply blast
apply (subgoal_tac "z \<noteq> 35")
txt{*
the tactic leaves two subgoals:
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply arith
apply force
done
--- a/src/Doc/Tutorial/Rules/TPrimes.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Rules/TPrimes.thy Sat Nov 01 14:20:38 2014 +0100
@@ -11,20 +11,20 @@
text {*Now in Basic.thy!
@{thm[display]"dvd_def"}
\rulename{dvd_def}
-*};
+*}
(*** Euclid's Algorithm ***)
lemma gcd_0 [simp]: "gcd m 0 = m"
-apply (simp);
+apply (simp)
done
lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd m n = gcd n (m mod n)"
apply (simp)
-done;
+done
-declare gcd.simps [simp del];
+declare gcd.simps [simp del]
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
lemma gcd_dvd_both: "(gcd m n dvd m) \<and> (gcd m n dvd n)"
@@ -33,7 +33,7 @@
apply (case_tac "n=0")
txt{*subgoals after the case tac
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (simp_all)
--{* @{subgoals[display,indent=0,margin=65]} *}
by (blast dest: dvd_mod_imp_dvd)
@@ -49,7 +49,7 @@
*}
lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
-lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
+lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]
text {*
@@ -60,7 +60,7 @@
@{thm[display] gcd_dvd2}
\rulename{gcd_dvd2}
\end{quote}
-*};
+*}
(*Maximality: for all m,n,k naturals,
if k divides m and k divides n then k divides gcd(m,n)*)
@@ -70,7 +70,7 @@
apply (case_tac "n=0")
txt{*subgoals after the case tac
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (simp_all add: dvd_mod)
done
@@ -100,12 +100,12 @@
(*Function gcd yields the Greatest Common Divisor*)
lemma is_gcd: "is_gcd (gcd m n) m n"
-apply (simp add: is_gcd_def gcd_greatest);
+apply (simp add: is_gcd_def gcd_greatest)
done
(*uniqueness of GCDs*)
lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n"
-apply (simp add: is_gcd_def);
+apply (simp add: is_gcd_def)
apply (blast intro: dvd_antisym)
done
@@ -123,13 +123,13 @@
\ \ \ \ \ \ \ n\ dvd\ a\ \isasymand \ n\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ n)\isasymrbrakk \isanewline
\ \ \ \ \isasymLongrightarrow \ m\ =\ n
\end{isabelle}
-*};
+*}
lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
apply (rule is_gcd_unique)
apply (rule is_gcd)
- apply (simp add: is_gcd_def);
- apply (blast intro: dvd_trans);
+ apply (simp add: is_gcd_def)
+ apply (blast intro: dvd_trans)
done
text{*
--- a/src/Doc/Tutorial/Sets/Functions.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Sets/Functions.thy Sat Nov 01 14:20:38 2014 +0100
@@ -73,7 +73,7 @@
\rulename{fun_eq_iff}
*}
-lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
+lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"
apply (simp add: fun_eq_iff inj_on_def)
apply (auto)
done
--- a/src/Doc/Tutorial/Sets/Relations.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Sets/Relations.thy Sat Nov 01 14:20:38 2014 +0100
@@ -91,7 +91,7 @@
apply (erule rtrancl_induct)
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (rule rtrancl_refl)
apply (blast intro: rtrancl_trans)
done
@@ -112,12 +112,12 @@
after intro rules
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply clarify
txt{*
after splitting
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
oops
@@ -127,13 +127,13 @@
@{subgoals[display,indent=0,margin=65]}
after subsetI
-*};
+*}
apply clarify
txt{*
@{subgoals[display,indent=0,margin=65]}
subgoals after clarify
-*};
+*}
by blast
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Sat Nov 01 14:20:38 2014 +0100
@@ -12,7 +12,7 @@
*}
datatype 'a list = Nil ("[]")
- | Cons 'a "'a list" (infixr "#" 65);
+ | Cons 'a "'a list" (infixr "#" 65)
text{*\noindent
The datatype\index{datatype@\isacommand {datatype} (command)}
@@ -140,7 +140,7 @@
list.
*}
-theorem rev_rev [simp]: "rev(rev xs) = xs";
+theorem rev_rev [simp]: "rev(rev xs) = xs"
txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
\noindent
@@ -179,7 +179,7 @@
nothing obvious except induction on @{term"xs"}:
*}
-apply(induct_tac xs);
+apply(induct_tac xs)
txt{*\noindent\index{*induct_tac (method)}%
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
@@ -211,7 +211,7 @@
Let us try to solve both goals automatically:
*}
-apply(auto);
+apply(auto)
txt{*\noindent
This command tells Isabelle to apply a proof strategy called
@@ -234,7 +234,7 @@
\commdx{oops}) we start a new proof:
*}
-lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
txt{*\noindent The keywords \commdx{theorem} and
\commdx{lemma} are interchangeable and merely indicate
@@ -246,13 +246,13 @@
the first argument, @{term"xs"} is the correct one:
*}
-apply(induct_tac xs);
+apply(induct_tac xs)
txt{*\noindent
This time not even the base case is solved automatically:
*}
-apply(auto);
+apply(auto)
txt{*
@{subgoals[display,indent=0,goals_limit=1]}
@@ -270,9 +270,9 @@
We again try the canonical proof procedure:
*}
-lemma app_Nil2 [simp]: "xs @ [] = xs";
-apply(induct_tac xs);
-apply(auto);
+lemma app_Nil2 [simp]: "xs @ [] = xs"
+apply(induct_tac xs)
+apply(auto)
txt{*
\noindent
@@ -298,9 +298,9 @@
Going back to the proof of the first lemma
*}
-lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
-apply(induct_tac xs);
-apply(auto);
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
+apply(induct_tac xs)
+apply(auto)
txt{*
\noindent
@@ -324,9 +324,9 @@
succeeds without further ado.
*}
-lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
-apply(induct_tac xs);
-apply(auto);
+lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
+apply(induct_tac xs)
+apply(auto)
done
text{*
@@ -334,18 +334,18 @@
Now we can prove the first lemma:
*}
-lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
-apply(induct_tac xs);
-apply(auto);
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
+apply(induct_tac xs)
+apply(auto)
done
text{*\noindent
Finally, we prove our main theorem:
*}
-theorem rev_rev [simp]: "rev(rev xs) = xs";
-apply(induct_tac xs);
-apply(auto);
+theorem rev_rev [simp]: "rev(rev xs) = xs"
+apply(induct_tac xs)
+apply(auto)
done
text{*\noindent
--- a/src/Doc/Tutorial/Trie/Trie.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Trie/Trie.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory Trie imports Main begin;
+theory Trie imports Main begin
(*>*)
text{*
To minimize running time, each node of a trie should contain an array that maps
@@ -7,9 +7,9 @@
representation where the subtries are held in an association list, i.e.\ a
list of (letter,trie) pairs. Abstracting over the alphabet @{typ"'a"} and the
values @{typ"'v"} we define a trie as follows:
-*};
+*}
-datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list";
+datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list"
text{*\noindent
\index{datatypes!and nested recursion}%
@@ -17,7 +17,7 @@
association list of subtries. This is an example of nested recursion involving products,
which is fine because products are datatypes as well.
We define two selector functions:
-*};
+*}
primrec "value" :: "('a,'v)trie \<Rightarrow> 'v option" where
"value(Trie ov al) = ov"
@@ -27,7 +27,7 @@
text{*\noindent
Association lists come with a generic lookup function. Its result
involves type @{text option} because a lookup can fail:
-*};
+*}
primrec assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option" where
"assoc [] x = None" |
@@ -39,7 +39,7 @@
examining the letters of the search string one by one. As
recursion on lists is simpler than on tries, let us express this as primitive
recursion on the search string argument:
-*};
+*}
primrec lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option" where
"lookup t [] = value t" |
@@ -51,17 +51,17 @@
As a first simple property we prove that looking up a string in the empty
trie @{term"Trie None []"} always returns @{const None}. The proof merely
distinguishes the two cases whether the search string is empty or not:
-*};
+*}
-lemma [simp]: "lookup (Trie None []) as = None";
-apply(case_tac as, simp_all);
+lemma [simp]: "lookup (Trie None []) as = None"
+apply(case_tac as, simp_all)
done
text{*
Things begin to get interesting with the definition of an update function
that adds a new (string, value) pair to a trie, overwriting the old value
associated with that string:
-*};
+*}
primrec update:: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie" where
"update t [] v = Trie (Some v) (alist t)" |
@@ -81,7 +81,7 @@
Before we start on any proofs about @{const update} we tell the simplifier to
expand all @{text let}s and to split all @{text case}-constructs over
options:
-*};
+*}
declare Let_def[simp] option.split[split]
@@ -92,10 +92,10 @@
Our main goal is to prove the correct interaction of @{const update} and
@{const lookup}:
-*};
+*}
theorem "\<forall>t v bs. lookup (update t as v) bs =
- (if as=bs then Some v else lookup t bs)";
+ (if as=bs then Some v else lookup t bs)"
txt{*\noindent
Our plan is to induct on @{term as}; hence the remaining variables are
@@ -105,8 +105,8 @@
if @{const update} has already been simplified, which can only happen if
@{term as} is instantiated.
The start of the proof is conventional:
-*};
-apply(induct_tac as, auto);
+*}
+apply(induct_tac as, auto)
txt{*\noindent
Unfortunately, this time we are left with three intimidating looking subgoals:
@@ -118,8 +118,8 @@
Clearly, if we want to make headway we have to instantiate @{term bs} as
well now. It turns out that instead of induction, case distinction
suffices:
-*};
-apply(case_tac[!] bs, auto);
+*}
+apply(case_tac[!] bs, auto)
done
text{*\noindent
@@ -158,7 +158,7 @@
with @{typ"'a \<Rightarrow> ('a,'v)trie option"}.
\end{exercise}
-*};
+*}
(*<*)
@@ -174,9 +174,9 @@
in Trie (value t) ((a, update1 tt as vo) # alist t))"
theorem [simp]: "\<forall>t v bs. lookup (update1 t as v) bs =
- (if as = bs then v else lookup t bs)";
-apply (induct_tac as, auto);
-apply (case_tac[!] bs, auto);
+ (if as = bs then v else lookup t bs)"
+apply (induct_tac as, auto)
+apply (case_tac[!] bs, auto)
done
@@ -198,17 +198,17 @@
(let tt = (case assoc (alist t) a of
None \<Rightarrow> Trie None []
| Some at \<Rightarrow> at)
- in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))";
+ in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))"
theorem "\<forall>t v bs. lookup (update2 t as vo) bs =
- (if as = bs then vo else lookup t bs)";
-apply (induct_tac as, auto);
-apply (case_tac[!] bs, auto);
+ (if as = bs then vo else lookup t bs)"
+apply (induct_tac as, auto)
+apply (case_tac[!] bs, auto)
done
(* Exercise 3. Solution by Getrud Bauer *)
-datatype ('a,dead 'v) triem = Triem "'v option" "'a \<Rightarrow> ('a,'v) triem option";
+datatype ('a,dead 'v) triem = Triem "'v option" "'a \<Rightarrow> ('a,'v) triem option"
primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
"valuem (Triem ov m) = ov"
@@ -220,10 +220,10 @@
"lookupm t [] = valuem t" |
"lookupm t (a#as) = (case mapping t a of
None \<Rightarrow> None
- | Some at \<Rightarrow> lookupm at as)";
+ | Some at \<Rightarrow> lookupm at as)"
-lemma [simp]: "lookupm (Triem None (\<lambda>c. None)) as = None";
-apply (case_tac as, simp_all);
+lemma [simp]: "lookupm (Triem None (\<lambda>c. None)) as = None"
+apply (case_tac as, simp_all)
done
primrec updatem :: "('a,'v)triem \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)triem" where
@@ -233,13 +233,13 @@
None \<Rightarrow> Triem None (\<lambda>c. None)
| Some at \<Rightarrow> at)
in Triem (valuem t)
- (\<lambda>c. if c = a then Some (updatem tt as v) else mapping t c))";
+ (\<lambda>c. if c = a then Some (updatem tt as v) else mapping t c))"
theorem "\<forall>t v bs. lookupm (updatem t as v) bs =
- (if as = bs then Some v else lookupm t bs)";
-apply (induct_tac as, auto);
-apply (case_tac[!] bs, auto);
+ (if as = bs then Some v else lookupm t bs)"
+apply (induct_tac as, auto)
+apply (case_tac[!] bs, auto)
done
-end;
+end
(*>*)
--- a/src/Doc/Tutorial/Types/Numbers.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Types/Numbers.thy Sat Nov 01 14:20:38 2014 +0100
@@ -10,7 +10,7 @@
lemma "2 * m = m + m"
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
oops
fun h :: "nat \<Rightarrow> nat" where
@@ -46,11 +46,11 @@
lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (simp add: ac_simps ac_simps)
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
oops
text{*
@@ -213,21 +213,21 @@
lemma "P ((3/4) * (8/15 :: real))"
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply simp
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
oops
lemma "(3/4) * (8/15) < (x :: real)"
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply simp
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
oops
text{*
--- a/src/Doc/Tutorial/Types/Pairs.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Types/Pairs.thy Sat Nov 01 14:20:38 2014 +0100
@@ -77,7 +77,7 @@
*}
lemma "(\<lambda>(x,y).y) p = snd p"
-apply(split split_split);
+apply(split split_split)
txt{*
@{subgoals[display,indent=0]}
@@ -93,7 +93,7 @@
Let us look at a second example:
*}
-lemma "let (x,y) = p in fst p = x";
+lemma "let (x,y) = p in fst p = x"
apply(simp only: Let_def)
txt{*
@@ -189,7 +189,7 @@
*}
lemma "\<forall>p. \<exists>q. swap p = swap q"
-by simp;
+by simp
text{*\noindent
To turn off this automatic splitting, disable the
--- a/src/FOLP/ex/Classical.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/FOLP/ex/Classical.thy Sat Nov 01 14:20:38 2014 +0100
@@ -145,7 +145,7 @@
by (tactic "fast_tac FOLP_cs 1")
text "Problem 21"
-schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
+schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
by (tactic "best_tac FOLP_dup_cs 1")
text "Problem 22"
@@ -173,7 +173,7 @@
text "Problem 26"
schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &
(ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
- --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
+ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
by (tactic "fast_tac FOLP_cs 1")
text "Problem 27"
--- a/src/HOL/Algebra/FiniteProduct.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Sat Nov 01 14:20:38 2014 +0100
@@ -33,7 +33,7 @@
lemma foldSetD_closed:
"[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D
- |] ==> z \<in> D";
+ |] ==> z \<in> D"
by (erule foldSetD.cases) auto
lemma Diff1_foldSetD:
@@ -72,7 +72,7 @@
and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D"
lemma (in LCD) foldSetD_closed [dest]:
- "(A, z) \<in> foldSetD D f e ==> z \<in> D";
+ "(A, z) \<in> foldSetD D f e ==> z \<in> D"
by (erule foldSetD.cases) auto
lemma (in LCD) Diff1_foldSetD:
--- a/src/HOL/Algebra/Module.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Algebra/Module.thy Sat Nov 01 14:20:38 2014 +0100
@@ -118,7 +118,7 @@
qed
lemma (in algebra) smult_r_null [simp]:
- "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
+ "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
proof -
assume R: "a \<in> carrier R"
note facts = R smult_closed
--- a/src/HOL/Auth/Guard/Extensions.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Sat Nov 01 14:20:38 2014 +0100
@@ -508,7 +508,7 @@
apply (induct evs, simp)
apply (rename_tac a b)
apply (case_tac a, simp_all)
-apply (blast dest: parts_trans)+;
+apply (blast dest: parts_trans)+
done
subsubsection{*monotonicity of used*}
--- a/src/HOL/Auth/NS_Shared.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Sat Nov 01 14:20:38 2014 +0100
@@ -231,7 +231,7 @@
apply (drule_tac [8] Says_Server_message_form)
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
txt{*NS2, NS3*}
-apply blast+;
+apply blast+
done
@@ -468,7 +468,7 @@
Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
Key K \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
- \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs";
+ \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
--- a/src/HOL/Auth/Smartcard/EventSC.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Sat Nov 01 14:20:38 2014 +0100
@@ -407,7 +407,7 @@
text{*For proving @{text new_keys_not_used}*}
lemma keysFor_parts_insert:
"\<lbrakk> K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) \<rbrakk>
- \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H";
+ \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H"
by (force
dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
--- a/src/HOL/Hoare/Examples.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Hoare/Examples.thy Sat Nov 01 14:20:38 2014 +0100
@@ -224,7 +224,7 @@
OD
{leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
(* expand and delete abbreviations first *)
-apply (simp);
+apply (simp)
apply (erule thin_rl)+
apply vcg_simp
apply (force simp: neq_Nil_conv)
--- a/src/HOL/Hoare_Parallel/Graph.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy Sat Nov 01 14:20:38 2014 +0100
@@ -90,7 +90,7 @@
subsubsection{* Graph 2 *}
lemma Ex_first_occurrence [rule_format]:
- "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))";
+ "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))"
apply(rule nat_less_induct)
apply clarify
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Sat Nov 01 14:20:38 2014 +0100
@@ -220,7 +220,7 @@
apply(force intro:tl_of_cptn_is_cptn)
done
-lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))";
+lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))"
apply(rule nat_less_induct)
apply clarify
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
--- a/src/HOL/Induct/QuoNestedDataType.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Sat Nov 01 14:20:38 2014 +0100
@@ -259,7 +259,7 @@
qed
lemma listset_Rep_Exp_Abs_Exp:
- "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
+ "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"
by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def)
lemma FnCall:
--- a/src/HOL/MicroJava/BV/Correct.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Sat Nov 01 14:20:38 2014 +0100
@@ -299,7 +299,7 @@
hp a = Some (C,fs) \<longrightarrow>
map_of (fields (G, C)) fl = Some fd \<longrightarrow>
G,hp\<turnstile>v::\<preceq>fd
- \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
+ \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs"
apply (induct frs)
apply simp
apply clarify
--- a/src/HOL/MicroJava/BV/JVMType.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sat Nov 01 14:20:38 2014 +0100
@@ -363,7 +363,7 @@
theorem sup_state_length [simp]:
"G \<turnstile> s2 <=s s1 \<Longrightarrow>
length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
- by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
+ by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def)
theorem sup_state_append_snd:
"length a = length b \<Longrightarrow>
--- a/src/HOL/MicroJava/Comp/TypeInf.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy Sat Nov 01 14:20:38 2014 +0100
@@ -10,7 +10,7 @@
(**********************************************************************)
-;
+
(*** Inversion of typing rules -- to be moved into WellType.thy
Also modify the wtpd_expr_\<dots> proofs in CorrComp.thy ***)
--- a/src/HOL/MicroJava/DFA/Err.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy Sat Nov 01 14:20:38 2014 +0100
@@ -117,7 +117,7 @@
"OK x <=_(le r) e = (e = Err | (? y. e = OK y & x <=_r y))"
by (simp add: unfold_lesub_err le_def split: err.split)
-lemma top_Err [iff]: "top (le r) Err";
+lemma top_Err [iff]: "top (le r) Err"
by (simp add: top_def)
lemma OK_less_conv [rule_format, iff]:
@@ -231,7 +231,7 @@
lemma semilat_le_err_OK1:
"\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk>
- \<Longrightarrow> x <=_r z";
+ \<Longrightarrow> x <=_r z"
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply (simp add: Semilat.ub1 [OF Semilat.intro])
--- a/src/HOL/MicroJava/DFA/Kildall.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Sat Nov 01 14:20:38 2014 +0100
@@ -355,7 +355,7 @@
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
- prefer 2; apply (fast intro: someI)
+ prefer 2 apply (fast intro: someI)
apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
prefer 2
apply clarify
@@ -406,7 +406,7 @@
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
- prefer 2; apply (fast intro: someI)
+ prefer 2 apply (fast intro: someI)
apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
prefer 2
apply clarify
--- a/src/HOL/MicroJava/DFA/Listn.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Sat Nov 01 14:20:38 2014 +0100
@@ -80,7 +80,7 @@
done
lemma list_update_le_cong:
- "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
+ "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]"
apply (unfold unfold_lesub_list)
apply (unfold Listn.le_def)
apply (simp add: list_all2_conv_all_nth nth_list_update)
@@ -189,12 +189,12 @@
done
lemma Cons_in_list_Suc [iff]:
- "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)";
+ "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)"
apply (simp add: in_list_Suc_iff)
done
lemma list_not_empty:
- "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A";
+ "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A"
apply (induct "n")
apply simp
apply (simp add: in_list_Suc_iff)
--- a/src/HOL/MicroJava/DFA/Opt.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Opt.thy Sat Nov 01 14:20:38 2014 +0100
@@ -69,7 +69,7 @@
done
lemma le_None [iff]:
- "(ox <=_(le r) None) = (ox = None)";
+ "(ox <=_(le r) None) = (ox = None)"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
@@ -282,7 +282,7 @@
lemma option_map_in_optionI:
"\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk>
- \<Longrightarrow> map_option f ox : opt S";
+ \<Longrightarrow> map_option f ox : opt S"
apply (unfold map_option_case)
apply (simp split: option.split)
apply blast
--- a/src/HOL/MicroJava/DFA/Product.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy Sat Nov 01 14:20:38 2014 +0100
@@ -57,7 +57,7 @@
lemma closed_lift2_sup:
"\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow>
- closed (err(A<*>B)) (lift2(sup f g))";
+ closed (err(A<*>B)) (lift2(sup f g))"
apply (unfold closed_def plussub_def lift2_def err_def sup_def)
apply (simp split: err.split)
apply blast
--- a/src/HOL/MicroJava/DFA/Semilat.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Sat Nov 01 14:20:38 2014 +0100
@@ -145,7 +145,7 @@
(*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
lemma (in Semilat) lub [simp, intro?]:
- "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z";
+ "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"
(*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
lemma (in Semilat) plus_le_conv [simp]:
@@ -299,7 +299,7 @@
lemma is_lub_some_lub:
"\<lbrakk> single_valued r; acyclic r; (x,u)\<in>r^*; (y,u)\<in>r^* \<rbrakk>
- \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+ \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"
(*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
subsection{*An executable lub-finder*}
@@ -331,7 +331,7 @@
lemma exec_lub_conv:
"\<lbrakk> acyclic r; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
- exec_lub r f x y = u";
+ exec_lub r f x y = u"
(*<*)
apply(unfold exec_lub_def)
apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and
@@ -343,9 +343,9 @@
apply(blast dest:rtrancl_into_rtrancl)
apply(rename_tac s)
apply(subgoal_tac "is_ub (r\<^sup>*) x y s")
- prefer 2; apply(simp add:is_ub_def)
+ prefer 2 apply(simp add:is_ub_def)
apply(subgoal_tac "(u, s) \<in> r\<^sup>*")
- prefer 2; apply(blast dest:is_lubD)
+ prefer 2 apply(blast dest:is_lubD)
apply(erule converse_rtranclE)
apply blast
apply(simp only:acyclic_def)
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Nov 01 14:20:38 2014 +0100
@@ -357,7 +357,7 @@
apply(unfold is_class_def)
apply(clarsimp)
-apply(rule Call_type_sound);
+apply(rule Call_type_sound)
prefer 11
apply blast
apply (simp (no_asm_simp))+
--- a/src/HOL/MicroJava/J/WellForm.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Sat Nov 01 14:20:38 2014 +0100
@@ -260,9 +260,9 @@
done
qed
-lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma];
+lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma]
-lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
+lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma]
lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk>
\<Longrightarrow> field (G, C) =
--- a/src/HOL/NSA/CLim.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/NSA/CLim.thy Sat Nov 01 14:20:38 2014 +0100
@@ -19,7 +19,7 @@
by (simp add: numeral_2_eq_2)
text{*Changing the quantified variable. Install earlier?*}
-lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
+lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"
apply auto
apply (drule_tac x="x+a" in spec)
apply (simp add: add.assoc)
--- a/src/HOL/NanoJava/TypeRel.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Sat Nov 01 14:20:38 2014 +0100
@@ -114,7 +114,7 @@
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
apply (unfold method_def)
-apply (erule (1) class_rec [THEN trans]);
+apply (erule (1) class_rec [THEN trans])
apply simp
done
@@ -126,7 +126,7 @@
lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
apply (unfold field_def)
-apply (erule (1) class_rec [THEN trans]);
+apply (erule (1) class_rec [THEN trans])
apply simp
done
--- a/src/HOL/Number_Theory/Cong.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Sat Nov 01 14:20:38 2014 +0100
@@ -161,7 +161,7 @@
lemma cong_diff_nat:
assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d"
shows "[a - c = b - d] (mod m)"
- using assms by (rule cong_diff_aux_int [transferred]);
+ using assms by (rule cong_diff_aux_int [transferred])
lemma cong_mult_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
--- a/src/HOL/SET_Protocol/Message_SET.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Sat Nov 01 14:20:38 2014 +0100
@@ -765,7 +765,7 @@
lemma Fake_parts_insert_in_Un:
"[|Z \<in> parts (insert X H); X: synth (analz H)|]
- ==> Z \<in> synth (analz H) \<union> parts H";
+ ==> Z \<in> synth (analz H) \<union> parts H"
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
@@ -906,18 +906,18 @@
text{*Two generalizations of @{text analz_insert_eq}*}
lemma gen_analz_insert_eq [rule_format]:
- "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
+ "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
lemma synth_analz_insert_eq [rule_format]:
"X \<in> synth (analz H)
- ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
+ ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
apply (erule synth.induct)
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
done
lemma Fake_parts_sing:
- "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
+ "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
apply (rule subset_trans)
apply (erule_tac [2] Fake_parts_insert)
apply (simp add: parts_mono)
--- a/src/HOL/UNITY/Comp/PriorityAux.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy Sat Nov 01 14:20:38 2014 +0100
@@ -131,7 +131,7 @@
done
lemma above_lemma_b:
- "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})";
+ "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})"
apply (drule above_lemma_a)
apply (auto simp add: image0_trancl_iff_image0_r)
done
--- a/src/Pure/Pure.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Pure/Pure.thy Sat Nov 01 14:20:38 2014 +0100
@@ -105,8 +105,8 @@
ML_file "Isar/calculation.ML"
ML_file "Tools/bibtex.ML"
ML_file "Tools/rail.ML"
-ML_file "Tools/rule_insts.ML";
-ML_file "Tools/thm_deps.ML";
+ML_file "Tools/rule_insts.ML"
+ML_file "Tools/thm_deps.ML"
ML_file "Tools/class_deps.ML"
ML_file "Tools/find_theorems.ML"
ML_file "Tools/find_consts.ML"
--- a/src/Sequents/LK0.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Sequents/LK0.thy Sat Nov 01 14:20:38 2014 +0100
@@ -359,7 +359,7 @@
apply fast
done
-lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y";
+lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y"
apply (unfold If_def)
apply (erule thinR [THEN cut])
apply fast
--- a/src/ZF/AC/AC16_WO4.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Sat Nov 01 14:20:38 2014 +0100
@@ -45,7 +45,7 @@
(* There exists a well ordered set y such that ... *)
(* ********************************************************************** *)
-lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll];
+lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]
lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)"
apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI)
--- a/src/ZF/AC/WO2_AC16.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Sat Nov 01 14:20:38 2014 +0100
@@ -309,13 +309,13 @@
apply (rule Finite_def [THEN def_imp_iff, THEN iffD2])
apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)
apply (blast intro: Card_is_Ord)
-done;
+done
(* back to the proof *)
lemmas disj_Un_eqpoll_nat_sum =
eqpoll_trans [THEN eqpoll_trans,
- OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum];
+ OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]
lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;
--- a/src/ZF/Arith.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Arith.thy Sat Nov 01 14:20:38 2014 +0100
@@ -413,12 +413,12 @@
"i \<in> nat ==> pred(i) \<in> nat"
by (simp add: pred_def split: split_nat_case)
-lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)";
+lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)"
apply (rule_tac m=i and n=j in diff_induct)
apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case)
done
-lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)";
+lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)"
apply (insert nat_diff_pred [of "natify(i)" "natify(j)"])
apply (simp add: natify_succ [symmetric])
done
@@ -435,7 +435,7 @@
text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
lemma diff_diff_left [simplified]:
- "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)";
+ "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)"
by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto)
--- a/src/ZF/Coind/Values.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Coind/Values.thy Sat Nov 01 14:20:38 2014 +0100
@@ -10,7 +10,7 @@
consts
Val :: i
ValEnv :: i
- Val_ValEnv :: i;
+ Val_ValEnv :: i
codatatype
"Val" = v_const ("c \<in> Const")
--- a/src/ZF/Constructible/Datatype_absolute.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy Sat Nov 01 14:20:38 2014 +0100
@@ -969,7 +969,7 @@
"M(g) ==>
strong_replacement
(M, \<lambda>x y. x \<in> formula &
- y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)";
+ y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)"
lemma (in Formula_Rec) formula_rec_case_closed:
"[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
--- a/src/ZF/Constructible/Formula.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/Formula.thy Sat Nov 01 14:20:38 2014 +0100
@@ -42,7 +42,7 @@
definition
Exists :: "i=>i" where
- "Exists(p) == Neg(Forall(Neg(p)))";
+ "Exists(p) == Neg(Forall(Neg(p)))"
lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
by (simp add: Neg_def)
@@ -107,7 +107,7 @@
==> sats(A, Forall(p), env) \<longleftrightarrow> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
by simp
-declare satisfies.simps [simp del];
+declare satisfies.simps [simp del]
subsection{*Dividing line between primitive and derived connectives*}
@@ -601,10 +601,10 @@
lemma Lset: "Lset(i) = (\<Union>j\<in>i. DPow(Lset(j)))"
by (subst Lset_def [THEN def_transrec], simp)
-lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
+lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)"
by (subst Lset, blast)
-lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
+lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))"
apply (insert Lset [of x])
apply (blast intro: elim: equalityE)
done
@@ -888,7 +888,7 @@
declare Ord_lrank [THEN lrank_of_Ord, simp]
text{*Kunen's VI 1.10 *}
-lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
+lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))"
apply (simp add: Lset_succ DPow_def)
apply (rule_tac x=Nil in bexI)
apply (rule_tac x="Equal(0,0)" in bexI)
@@ -907,7 +907,7 @@
done
text{*Kunen's VI 1.11 *}
-lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) \<subseteq> Vset(i)";
+lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) \<subseteq> Vset(i)"
apply (erule trans_induct)
apply (subst Lset)
apply (subst Vset)
@@ -917,7 +917,7 @@
done
text{*Kunen's VI 1.12 *}
-lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
+lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)"
apply (erule nat_induct)
apply (simp add: Vfrom_0)
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
@@ -1002,7 +1002,7 @@
\<exists>env \<in> list(A). \<exists>p \<in> formula.
X = {x\<in>A. sats(A, p, Cons(x,env))}}"
-lemma DPow_subset_DPow': "DPow(A) \<subseteq> DPow'(A)";
+lemma DPow_subset_DPow': "DPow(A) \<subseteq> DPow'(A)"
by (simp add: DPow_def DPow'_def, blast)
lemma DPow'_0: "DPow'(0) = {0}"
--- a/src/ZF/Constructible/Rank.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/Rank.thy Sat Nov 01 14:20:38 2014 +0100
@@ -566,7 +566,7 @@
subsubsection{*Ordinal Multiplication*}
lemma omult_eqns_unique:
- "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
+ "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"
apply (simp add: omult_eqns_def, clarify)
apply (erule Ord_cases, simp_all)
done
--- a/src/ZF/Constructible/Reflection.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/Reflection.thy Sat Nov 01 14:20:38 2014 +0100
@@ -6,10 +6,10 @@
theory Reflection imports Normal begin
-lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))";
+lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))"
by blast
-lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))";
+lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))"
by blast
text{*From the notes of A. S. Kechris, page 6, and from
@@ -339,14 +339,14 @@
schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
- \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
+ \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"
by fast
text{*Example 3''*}
schematic_lemma (in reflection)
"Reflects(?Cl,
\<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
- \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
+ \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
by fast
text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs
--- a/src/ZF/Constructible/Relative.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/Relative.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1336,7 +1336,7 @@
text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
lemma (in M_basic) is_funspace_abs [simp]:
- "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B";
+ "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B"
apply (simp add: is_funspace_def)
apply (rule iffI)
prefer 2 apply blast
--- a/src/ZF/Constructible/WFrec.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/WFrec.thy Sat Nov 01 14:20:38 2014 +0100
@@ -135,7 +135,7 @@
"[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |]
==> is_recfun(r,a,H,f) \<longleftrightarrow>
(\<forall>z[M]. z \<in> f \<longleftrightarrow>
- (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))";
+ (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))"
apply (simp add: is_recfun_def lam_def)
apply (safe intro!: equalityI)
apply (drule equalityD1 [THEN subsetD], assumption)
--- a/src/ZF/Epsilon.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Epsilon.thy Sat Nov 01 14:20:38 2014 +0100
@@ -117,14 +117,14 @@
done
text{*A transitive set either is empty or contains the empty set.*}
-lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A";
+lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A"
apply (simp add: Transset_def)
apply (rule_tac a=x in eps_induct, clarify)
apply (drule bspec, assumption)
apply (case_tac "x=0", auto)
done
-lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
+lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A"
by (blast dest: Transset_0_lemma)
--- a/src/ZF/List_ZF.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/List_ZF.thy Sat Nov 01 14:20:38 2014 +0100
@@ -1216,7 +1216,7 @@
lemma sublist_upt_eq_take [rule_format, simp]:
"xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
apply (erule list.induct, simp)
-apply (clarify );
+apply (clarify )
apply (erule natE)
apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
done
--- a/src/ZF/Nat_ZF.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Nat_ZF.thy Sat Nov 01 14:20:38 2014 +0100
@@ -244,7 +244,7 @@
lemma nat_case_type [TC]:
"[| n \<in> nat; a \<in> C(0); !!m. m \<in> nat ==> b(m): C(succ(m)) |]
- ==> nat_case(a,b,n) \<in> C(n)";
+ ==> nat_case(a,b,n) \<in> C(n)"
by (erule nat_induct, auto)
lemma split_nat_case:
--- a/src/ZF/OrdQuant.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/OrdQuant.thy Sat Nov 01 14:20:38 2014 +0100
@@ -273,7 +273,7 @@
lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
by blast
-lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))";
+lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))"
by (simp add: rall_def atomize_all atomize_imp)
declare atomize_rall [symmetric, rulify]
--- a/src/ZF/Sum.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Sum.thy Sat Nov 01 14:20:38 2014 +0100
@@ -109,10 +109,10 @@
lemma sum_iff: "u \<in> A+B \<longleftrightarrow> (\<exists>x. x \<in> A & u=Inl(x)) | (\<exists>y. y \<in> B & u=Inr(y))"
by blast
-lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
+lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)"
by auto
-lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)";
+lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)"
by auto
lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
--- a/src/ZF/Trancl.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Trancl.thy Sat Nov 01 14:20:38 2014 +0100
@@ -90,7 +90,7 @@
lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
by (unfold trans_def trans_on_def, blast)
-lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)";
+lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)"
by (simp add: trans_on_def trans_def, blast)
--- a/src/ZF/UNITY/AllocImpl.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Sat Nov 01 14:20:38 2014 +0100
@@ -415,7 +415,7 @@
prefer 2 apply (force)
apply (subgoal_tac "x`available_tok =
NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
-apply (simp add: );
+apply (simp add: )
apply (auto split add: nat_diff_split dest: lt_trans2)
done
--- a/src/ZF/UNITY/ClientImpl.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Sat Nov 01 14:20:38 2014 +0100
@@ -105,14 +105,14 @@
lemma preserves_lift_imp_stable:
- "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})";
+ "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"
apply (drule preserves_imp_stable)
apply (simp add: lift_def)
done
lemma preserves_imp_prefix:
"G \<in> preserves(lift(ff))
- ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})";
+ ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
by (erule preserves_lift_imp_stable)
(*Safety property 1 \<in> ask, rel are increasing: (24) *)
--- a/src/ZF/Univ.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Univ.thy Sat Nov 01 14:20:38 2014 +0100
@@ -453,7 +453,7 @@
Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
done
-lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
+lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))"
apply (erule nat_induct)
apply (simp add: Vfrom_0)
apply (simp add: Vset_succ)
--- a/src/ZF/equalities.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/equalities.thy Sat Nov 01 14:20:38 2014 +0100
@@ -22,10 +22,10 @@
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}.*}
-lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
+lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"
by blast
-lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
+lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))"
by blast
lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
--- a/src/ZF/ex/Group.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/ex/Group.thy Sat Nov 01 14:20:38 2014 +0100
@@ -383,7 +383,7 @@
apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)")
prefer 2 apply (simp add: bij_converse_bij bij_is_fun)
apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"]
- simp add: hom_def bij_is_inj right_inverse_bij);
+ simp add: hom_def bij_is_inj right_inverse_bij)
done
lemma (in group) iso_trans:
@@ -658,7 +658,7 @@
by (simp add: normal_def subgroup_def)
lemma (in group) normalI:
- "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
+ "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
by (simp add: normal_def normal_axioms_def)
lemma (in normal) inv_op_closed1:
@@ -1086,7 +1086,7 @@
definition
kernel :: "[i,i,i] => i" where
--{*the kernel of a homomorphism*}
- "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
+ "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}"
lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
apply (rule subgroup.intro)
--- a/src/ZF/ex/LList.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/ex/LList.thy Sat Nov 01 14:20:38 2014 +0100
@@ -16,7 +16,7 @@
theory LList imports Main begin
consts
- llist :: "i=>i";
+ llist :: "i=>i"
codatatype
"llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
--- a/src/ZF/func.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/func.thy Sat Nov 01 14:20:38 2014 +0100
@@ -249,7 +249,7 @@
lemma Repfun_function_if:
"function(f)
- ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))";
+ ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))"
apply simp
apply (intro conjI impI)
apply (blast dest: function_apply_equality intro: function_apply_Pair)
@@ -261,7 +261,7 @@
(*For this lemma and the next, the right-hand side could equivalently
be written \<Union>x\<in>C. {f`x} *)
lemma image_function:
- "[| function(f); C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}";
+ "[| function(f); C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}"
by (simp add: Repfun_function_if)
lemma image_fun: "[| f \<in> Pi(A,B); C \<subseteq> A |] ==> f``C = {f`x. x \<in> C}"