# HG changeset patch
# User wenzelm
# Date 1331681696 -3600
# Node ID c2ca2c3d23a689b3d2065068cae9c93dd071b277
# Parent  3444a24dc4e9fcea3fb61d436824f6733054c169
misc tuning;

diff -r 3444a24dc4e9 -r c2ca2c3d23a6 src/HOL/Induct/ABexp.thy
--- a/src/HOL/Induct/ABexp.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/ABexp.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* Arithmetic and boolean expressions *}
 
-theory ABexp imports Main begin
+theory ABexp
+imports Main
+begin
 
 datatype 'a aexp =
     IF "'a bexp"  "'a aexp"  "'a aexp"
@@ -21,7 +23,8 @@
 text {* \medskip Evaluation of arithmetic and boolean expressions *}
 
 primrec evala :: "('a => nat) => 'a aexp => nat"
-  and evalb :: "('a => nat) => 'a bexp => bool" where
+  and evalb :: "('a => nat) => 'a bexp => bool"
+where
   "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
 | "evala env (Sum a1 a2) = evala env a1 + evala env a2"
 | "evala env (Diff a1 a2) = evala env a1 - evala env a2"
@@ -36,7 +39,8 @@
 text {* \medskip Substitution on arithmetic and boolean expressions *}
 
 primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
-  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where
+  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
+where
   "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
 | "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
 | "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
diff -r 3444a24dc4e9 -r c2ca2c3d23a6 src/HOL/Induct/Ordinals.thy
--- a/src/HOL/Induct/Ordinals.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/Ordinals.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* Ordinals *}
 
-theory Ordinals imports Main begin
+theory Ordinals
+imports Main
+begin
 
 text {*
   Some basic definitions of ordinal numbers.  Draws an Agda
@@ -17,37 +19,38 @@
   | Succ ordinal
   | Limit "nat => ordinal"
 
-primrec pred :: "ordinal => nat => ordinal option" where
+primrec pred :: "ordinal => nat => ordinal option"
+where
   "pred Zero n = None"
 | "pred (Succ a) n = Some a"
 | "pred (Limit f) n = Some (f n)"
 
-abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" where
-  "iter f n \<equiv> f ^^ n"
+abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)"
+  where "iter f n \<equiv> f ^^ n"
+
+definition OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
+  where "OpLim F a = Limit (\<lambda>n. F n a)"
 
-definition
-  OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where
-  "OpLim F a = Limit (\<lambda>n. F n a)"
+definition OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<Squnion>")
+  where "\<Squnion>f = OpLim (iter f)"
 
-definition
-  OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>") where
-  "\<Squnion>f = OpLim (iter f)"
-
-primrec cantor :: "ordinal => ordinal => ordinal" where
+primrec cantor :: "ordinal => ordinal => ordinal"
+where
   "cantor a Zero = Succ a"
 | "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
 | "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
 
-primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>") where
+primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<nabla>")
+where
   "\<nabla>f Zero = f Zero"
 | "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
 | "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
 
-definition
-  deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
-  "deriv f = \<nabla>(\<Squnion>f)"
+definition deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
+  where "deriv f = \<nabla>(\<Squnion>f)"
 
-primrec veblen :: "ordinal => ordinal => ordinal" where
+primrec veblen :: "ordinal => ordinal => ordinal"
+where
   "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
 | "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
 | "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
diff -r 3444a24dc4e9 -r c2ca2c3d23a6 src/HOL/Induct/Sigma_Algebra.thy
--- a/src/HOL/Induct/Sigma_Algebra.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/Sigma_Algebra.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* Sigma algebras *}
 
-theory Sigma_Algebra imports Main begin
+theory Sigma_Algebra
+imports Main
+begin
 
 text {*
   This is just a tiny example demonstrating the use of inductive
@@ -12,14 +14,12 @@
   \<sigma>}-algebra over a given set of sets.
 *}
 
-inductive_set
-  \<sigma>_algebra :: "'a set set => 'a set set"
-  for A :: "'a set set"
-  where
-    basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
-  | UNIV: "UNIV \<in> \<sigma>_algebra A"
-  | complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
-  | Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
+inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set"
+where
+  basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
+| UNIV: "UNIV \<in> \<sigma>_algebra A"
+| complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
+| Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
 
 text {*
   The following basic facts are consequences of the closure properties
@@ -30,7 +30,7 @@
 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
 proof -
   have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
-  hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
+  then have "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
   also have "-UNIV = {}" by simp
   finally show ?thesis .
 qed
@@ -39,9 +39,9 @@
   "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
 proof -
   assume "!!i::nat. a i \<in> \<sigma>_algebra A"
-  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
-  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
-  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
+  then have "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
+  then have "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
+  then have "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
   also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
   finally show ?thesis .
 qed
diff -r 3444a24dc4e9 -r c2ca2c3d23a6 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/Term.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* Terms over a given alphabet *}
 
-theory Term imports Main begin
+theory Term
+imports Main
+begin
 
 datatype ('a, 'b) "term" =
     Var 'a
@@ -14,7 +16,8 @@
 text {* \medskip Substitution function on terms *}
 
 primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
-  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
+  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+where
   "subst_term f (Var a) = f a"
 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
 | "subst_term_list f [] = []"
diff -r 3444a24dc4e9 -r c2ca2c3d23a6 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/Tree.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -13,8 +13,7 @@
     Atom 'a
   | Branch "nat => 'a tree"
 
-primrec
-  map_tree :: "('a => 'b) => 'a tree => 'b tree"
+primrec map_tree :: "('a => 'b) => 'a tree => 'b tree"
 where
   "map_tree f (Atom a) = Atom (f a)"
 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
@@ -22,8 +21,7 @@
 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
   by (induct t) simp_all
 
-primrec
-  exists_tree :: "('a => bool) => 'a tree => bool"
+primrec exists_tree :: "('a => bool) => 'a tree => bool"
 where
   "exists_tree P (Atom a) = P a"
 | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
@@ -39,8 +37,7 @@
 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
 
 text{*Addition of ordinals*}
-primrec
-  add :: "[brouwer,brouwer] => brouwer"
+primrec add :: "[brouwer,brouwer] => brouwer"
 where
   "add i Zero = i"
 | "add i (Succ j) = Succ (add i j)"
@@ -50,8 +47,7 @@
   by (induct k) auto
 
 text{*Multiplication of ordinals*}
-primrec
-  mult :: "[brouwer,brouwer] => brouwer"
+primrec mult :: "[brouwer,brouwer] => brouwer"
 where
   "mult i Zero = Zero"
 | "mult i (Succ j) = add (mult i j) i"
@@ -72,13 +68,11 @@
   ordinals.  Start with a predecessor relation and form its transitive 
   closure. *} 
 
-definition
-  brouwer_pred :: "(brouwer * brouwer) set" where
-  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
+definition brouwer_pred :: "(brouwer * brouwer) set"
+  where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
 
-definition
-  brouwer_order :: "(brouwer * brouwer) set" where
-  "brouwer_order = brouwer_pred^+"
+definition brouwer_order :: "(brouwer * brouwer) set"
+  where "brouwer_order = brouwer_pred^+"
 
 lemma wf_brouwer_pred: "wf brouwer_pred"
   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
@@ -94,8 +88,7 @@
 
 text{*Example of a general function*}
 
-function
-  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
   "add2 i Zero = i"
 | "add2 i (Succ j) = Succ (add2 i j)"