# HG changeset patch
# User wenzelm
# Date 1470156384 -7200
# Node ID f4a308fdf6647a2ef203890264f22b287186eede
# Parent  68751fe1c036b8d5b8fd6f148cd5313159b9f309
tuned;

diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Basic_Logic.thy
--- 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
 
 
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Cantor.thy
--- 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>
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Drinker.thy
--- 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>
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Expr_Compiler.thy
--- 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>
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Fibonacci.thy
--- 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
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/First_Order_Logic.thy
--- 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>
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Group.thy
--- 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> 
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Group_Context.thy
--- 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>
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Group_Notepad.thy
--- 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
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- 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 ..
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Hoare.thy
--- 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)
 
 
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Hoare_Ex.thy
--- 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
diff -r 68751fe1c036 -r f4a308fdf664 src/HOL/Isar_Examples/Peirce.thy
--- 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>