author wenzelm Tue, 02 Aug 2016 18:44:37 +0200 changeset 63583 a39baba12732 parent 63582 161c5d8ae266 child 63584 68751fe1c036
tuned;
```--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>

theory Knaster_Tarski
-imports Main "~~/src/HOL/Library/Lattice_Syntax"
+  imports Main "~~/src/HOL/Library/Lattice_Syntax"
begin

```
```--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -6,7 +6,7 @@
section \<open>The Mutilated Checker Board Problem\<close>

theory Mutilated_Checkerboard
-imports Main
+  imports Main
begin

text \<open>
@@ -16,11 +16,10 @@

subsection \<open>Tilings\<close>

-inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
-  for A :: "'a set set"
-where
-  empty: "{} \<in> tiling A"
-| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
+inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
+  where
+    empty: "{} \<in> tiling A"
+  | Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"

text \<open>The union of two disjoint tilings is a tiling.\<close>
@@ -114,9 +113,9 @@
subsection \<open>Dominoes\<close>

inductive_set domino :: "(nat \<times> nat) set set"
-where
-  horiz: "{(i, j), (i, j + 1)} \<in> domino"
-| vertl: "{(i, j), (i + 1, j)} \<in> domino"
+  where
+    horiz: "{(i, j), (i, j + 1)} \<in> domino"
+  | vertl: "{(i, j), (i + 1, j)} \<in> domino"

lemma dominoes_tile_row:
"{i} \<times> below (2 * n) \<in> tiling domino"
@@ -242,10 +241,8 @@
subsection \<open>Main theorem\<close>

definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
-  where
-    "mutilated_board m n =
-      below (2 * (m + 1)) \<times> below (2 * (n + 1))
-        - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
+  where "mutilated_board m n =
+    below (2 * (m + 1)) \<times> below (2 * (n + 1)) - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"

theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino"
proof (unfold mutilated_board_def)```
```--- a/src/HOL/Isar_Examples/Puzzle.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -1,7 +1,7 @@
section \<open>An old chestnut\<close>

theory Puzzle
-imports Main
+  imports Main
begin

text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original```
```--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -5,7 +5,7 @@
section \<open>SchrÃ¶der-Bernstein Theorem\<close>

theory Schroeder_Bernstein
-imports Main
+  imports Main
begin

text \<open>```
```--- a/src/HOL/Isar_Examples/Structured_Statements.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Structured statements within Isar proofs\<close>

theory Structured_Statements
-imports Main
+  imports Main
begin

subsection \<open>Introduction steps\<close>```
```--- a/src/HOL/Isar_Examples/Summation.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Summation.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Summing natural numbers\<close>

theory Summation
-imports Main
+  imports Main
begin

text \<open>```