--- a/src/HOL/Isar_Examples/Basic_Logic.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Tue Aug 02 18:46:24 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Basic logical reasoning\<close>
theory Basic_Logic
-imports Main
+ imports Main
begin
--- a/src/HOL/Isar_Examples/Cantor.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Cantor's Theorem\<close>
theory Cantor
-imports Main
+ imports Main
begin
subsection \<open>Mathematical statement and proof\<close>
--- a/src/HOL/Isar_Examples/Drinker.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>The Drinker's Principle\<close>
theory Drinker
-imports Main
+ imports Main
begin
text \<open>
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Aug 02 18:46:24 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Correctness of a simple expression compiler\<close>
theory Expr_Compiler
-imports Main
+ imports Main
begin
text \<open>
@@ -46,10 +46,10 @@
\<close>
primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
-where
- "eval (Variable x) env = env x"
-| "eval (Constant c) env = c"
-| "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
+ where
+ "eval (Variable x) env = env x"
+ | "eval (Constant c) env = c"
+ | "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
subsection \<open>Machine\<close>
@@ -69,14 +69,13 @@
\<close>
primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
-where
- "exec [] stack env = stack"
-| "exec (instr # instrs) stack env =
- (case instr of
- Const c \<Rightarrow> exec instrs (c # stack) env
- | Load x \<Rightarrow> exec instrs (env x # stack) env
- | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
- # (tl (tl stack))) env)"
+ where
+ "exec [] stack env = stack"
+ | "exec (instr # instrs) stack env =
+ (case instr of
+ Const c \<Rightarrow> exec instrs (c # stack) env
+ | Load x \<Rightarrow> exec instrs (env x # stack) env
+ | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)"
definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where "execute instrs env = hd (exec instrs [] env)"
@@ -90,10 +89,10 @@
\<close>
primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
-where
- "compile (Variable x) = [Load x]"
-| "compile (Constant c) = [Const c]"
-| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
+ where
+ "compile (Variable x) = [Load x]"
+ | "compile (Constant c) = [Const c]"
+ | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
text \<open>
--- a/src/HOL/Isar_Examples/Fibonacci.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Tue Aug 02 18:46:24 2016 +0200
@@ -15,7 +15,7 @@
section \<open>Fib and Gcd commute\<close>
theory Fibonacci
-imports "../Number_Theory/Primes"
+ imports "../Number_Theory/Primes"
begin
text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
@@ -28,10 +28,10 @@
subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat"
-where
- "fib 0 = 0"
-| "fib (Suc 0) = 1"
-| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+ where
+ "fib 0 = 0"
+ | "fib (Suc 0) = 1"
+ | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "fib (Suc n) > 0"
by (induct n rule: fib.induct) simp_all
--- a/src/HOL/Isar_Examples/First_Order_Logic.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/First_Order_Logic.thy Tue Aug 02 18:46:24 2016 +0200
@@ -10,7 +10,7 @@
\<close>
theory First_Order_Logic
-imports Pure
+ imports Pure
begin
subsection \<open>Abstract syntax\<close>
--- a/src/HOL/Isar_Examples/Group.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Group.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Basic group theory\<close>
theory Group
-imports Main
+ imports Main
begin
subsection \<open>Groups and calculational reasoning\<close>
--- a/src/HOL/Isar_Examples/Group_Context.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Some algebraic identities derived from group axioms -- theory context version\<close>
theory Group_Context
-imports Main
+ imports Main
begin
text \<open>hypothetical group axiomatization\<close>
--- a/src/HOL/Isar_Examples/Group_Notepad.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
theory Group_Notepad
-imports Main
+ imports Main
begin
notepad
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Foundations of HOL\<close>
theory Higher_Order_Logic
-imports Pure
+ imports Pure
begin
text \<open>
@@ -76,7 +76,8 @@
subsubsection \<open>Derived connectives\<close>
-definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
+definition false :: o ("\<bottom>")
+ where "\<bottom> \<equiv> \<forall>A. A"
theorem falseE [elim]:
assumes "\<bottom>"
@@ -87,7 +88,8 @@
qed
-definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o ("\<top>")
+ where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
theorem trueI [intro]: \<top>
unfolding true_def ..
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Tue Aug 02 18:46:24 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Hoare Logic\<close>
theory Hoare
-imports Main
+ imports Main
begin
subsection \<open>Abstract syntax and semantics\<close>
@@ -34,28 +34,24 @@
type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
-where
- "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
-| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
+ where
+ "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
+ | "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
primrec Sem :: "'a com \<Rightarrow> 'a sem"
-where
- "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
-| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
- (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
-| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
+ where
+ "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
+ | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
+ | "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
+ | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
-lemma ValidI [intro?]:
- "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
+lemma ValidI [intro?]: "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
by (simp add: Valid_def)
-lemma ValidD [dest?]:
- "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
+lemma ValidD [dest?]: "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
by (simp add: Valid_def)
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Aug 02 18:46:24 2016 +0200
@@ -1,7 +1,7 @@
section \<open>Using Hoare Logic\<close>
theory Hoare_Ex
-imports Hoare
+ imports Hoare
begin
subsection \<open>State spaces\<close>
@@ -276,11 +276,11 @@
type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
primrec timeit :: "'a time com \<Rightarrow> 'a time com"
-where
- "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
-| "timeit (c1; c2) = (timeit c1; timeit c2)"
-| "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
-| "timeit (While b iv c) = While b iv (timeit c)"
+ where
+ "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
+ | "timeit (c1; c2) = (timeit c1; timeit c2)"
+ | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
+ | "timeit (While b iv c) = While b iv (timeit c)"
record tvars = tstate +
I :: nat
--- a/src/HOL/Isar_Examples/Peirce.thy Tue Aug 02 18:45:34 2016 +0200
+++ b/src/HOL/Isar_Examples/Peirce.thy Tue Aug 02 18:46:24 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Peirce's Law\<close>
theory Peirce
-imports Main
+ imports Main
begin
text \<open>