# HG changeset patch
# User wenzelm
# Date 1329861028 -3600
# Node ID dcc312f22ee8699accdb77b0131330487e1517f8
# Parent  1544a8703787bfd16d1d30861a1ebee82f11a240
misc tuning;

diff -r 1544a8703787 -r dcc312f22ee8 src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 21 21:15:57 2012 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Feb 21 22:50:28 2012 +0100
@@ -59,9 +59,7 @@
 text {* Execution of a list of stack machine instructions is easily
   defined as follows. *}
 
-primrec
-  exec :: "(('adr, 'val) instr) list
-    => 'val list => ('adr => 'val) => 'val list"
+primrec exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"
 where
   "exec [] stack env = stack"
 | "exec (instr # instrs) stack env =
@@ -71,8 +69,7 @@
     | Apply f => exec instrs (f (hd stack) (hd (tl stack))
                    # (tl (tl stack))) env)"
 
-definition
-  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
   where "execute instrs env = hd (exec instrs [] env)"
 
 
@@ -81,8 +78,7 @@
 text {* We are ready to define the compilation function of expressions
   to lists of stack machine instructions. *}
 
-primrec
-  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
+primrec compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
 where
   "compile (Variable x) = [Load x]"
 | "compile (Constant c) = [Const c]"
diff -r 1544a8703787 -r dcc312f22ee8 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 21 21:15:57 2012 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 21 22:50:28 2012 +0100
@@ -46,8 +46,7 @@
     (if s : b then Sem c1 s s' else Sem c2 s s')"
 | "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
 
-definition
-  Valid :: "'a bexp => 'a com => 'a bexp => bool"
+definition Valid :: "'a bexp => 'a com => 'a bexp => bool"
     ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
   where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
 
@@ -113,9 +112,10 @@
   which cases apply. *}
 
 theorem cond:
-  "|- (P Int b) c1 Q ==> |- (P Int -b) c2 Q ==> |- P (Cond b c1 c2) Q"
+  assumes case_b: "|- (P Int b) c1 Q"
+    and case_nb: "|- (P Int -b) c2 Q"
+  shows "|- P (Cond b c1 c2) Q"
 proof
-  assume case_b: "|- (P Int b) c1 Q" and case_nb: "|- (P Int -b) c2 Q"
   fix s s' assume s: "s : P"
   assume sem: "Sem (Cond b c1 c2) s s'"
   show "s' : Q"
diff -r 1544a8703787 -r dcc312f22ee8 src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Feb 21 21:15:57 2012 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Feb 21 22:50:28 2012 +0100
@@ -62,9 +62,9 @@
   by hoare simp
 
 lemma
-"|- .{\<acute>M = a & \<acute>N = b}.
-    \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
-    .{\<acute>M = b & \<acute>N = a}."
+  "|- .{\<acute>M = a & \<acute>N = b}.
+      \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
+      .{\<acute>M = b & \<acute>N = a}."
   by hoare simp
 
 text {* It is important to note that statements like the following one
@@ -272,18 +272,19 @@
 lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)"
   by (induct n) simp_all
 
-lemma "|- .{i = \<acute>I & \<acute>time = 0}.
- timeit(
- WHILE \<acute>I \<noteq> 0
- INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}.
- DO
-   \<acute>J := \<acute>I;
-   WHILE \<acute>J \<noteq> 0
-   INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}.
-   DO \<acute>J := \<acute>J - 1 OD;
-   \<acute>I := \<acute>I - 1
- OD
- ) .{2*\<acute>time = i*i + 5*i}."
+lemma
+  "|- .{i = \<acute>I & \<acute>time = 0}.
+    timeit (
+    WHILE \<acute>I \<noteq> 0
+    INV .{2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i}.
+    DO
+      \<acute>J := \<acute>I;
+      WHILE \<acute>J \<noteq> 0
+      INV .{0 < \<acute>I & 2 * \<acute>time + \<acute>I * \<acute>I + 3 * \<acute>I + 2 * \<acute>J - 2 = i * i + 5 * i}.
+      DO \<acute>J := \<acute>J - 1 OD;
+        \<acute>I := \<acute>I - 1
+    OD
+    ) .{2*\<acute>time = i*i + 5*i}."
   apply simp
   apply hoare
       apply simp
diff -r 1544a8703787 -r dcc312f22ee8 src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Feb 21 21:15:57 2012 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Feb 21 22:50:28 2012 +0100
@@ -242,10 +242,10 @@
 subsection {* Main theorem *}
 
 definition mutilated_board :: "nat => nat => (nat * nat) set"
-where
-  "mutilated_board m n =
-    below (2 * (m + 1)) <*> below (2 * (n + 1))
-      - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
+  where
+    "mutilated_board m n =
+      below (2 * (m + 1)) <*> below (2 * (n + 1))
+        - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
 
 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
 proof (unfold mutilated_board_def)
@@ -253,7 +253,7 @@
   let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
   let ?t' = "?t - {(0, 0)}"
   let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
-  
+
   show "?t'' ~: ?T"
   proof
     have t: "?t : ?T" by (rule dominoes_tile_matrix)
diff -r 1544a8703787 -r dcc312f22ee8 src/HOL/Isar_Examples/ROOT.ML
--- a/src/HOL/Isar_Examples/ROOT.ML	Tue Feb 21 21:15:57 2012 +0100
+++ b/src/HOL/Isar_Examples/ROOT.ML	Tue Feb 21 22:50:28 2012 +0100
@@ -1,6 +1,6 @@
 (* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
 
-no_document use_thys ["../Number_Theory/Primes"];
+no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"];
 
 use_thys [
   "Basic_Logic",