--- 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]"
--- 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"
--- 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
--- 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)
--- 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",