# HG changeset patch
# User wenzelm
# Date 1434810236 -7200
# Node ID 7fb5b7dc8332d14e441f473a5ec74dd10ea15e13
# Parent  9cc91b8a6489c0617f52c2bdc7d45b250dedc4b9
misc tuning;

diff -r 9cc91b8a6489 -r 7fb5b7dc8332 src/HOL/Induct/ABexp.thy
--- a/src/HOL/Induct/ABexp.thy	Sat Jun 20 16:08:47 2015 +0200
+++ b/src/HOL/Induct/ABexp.thy	Sat Jun 20 16:23:56 2015 +0200
@@ -22,8 +22,8 @@
 
 text \<open>\medskip Evaluation of arithmetic and boolean expressions\<close>
 
-primrec evala :: "('a => nat) => 'a aexp => nat"
-  and evalb :: "('a => nat) => 'a bexp => bool"
+primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
+  and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> 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"
@@ -38,8 +38,8 @@
 
 text \<open>\medskip Substitution on arithmetic and boolean expressions\<close>
 
-primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
-  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
+primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
+  and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> '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)"
diff -r 9cc91b8a6489 -r 7fb5b7dc8332 src/HOL/Induct/Ordinals.thy
--- a/src/HOL/Induct/Ordinals.thy	Sat Jun 20 16:08:47 2015 +0200
+++ b/src/HOL/Induct/Ordinals.thy	Sat Jun 20 16:23:56 2015 +0200
@@ -17,39 +17,39 @@
 datatype ordinal =
     Zero
   | Succ ordinal
-  | Limit "nat => ordinal"
+  | Limit "nat \<Rightarrow> ordinal"
 
-primrec pred :: "ordinal => nat => ordinal option"
+primrec pred :: "ordinal \<Rightarrow> nat \<Rightarrow> 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)"
+abbreviation (input) iter :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a)"
   where "iter f n \<equiv> f ^^ n"
 
-definition OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
+definition OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
   where "OpLim F a = Limit (\<lambda>n. F n a)"
 
-definition OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<Squnion>")
+definition OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"  ("\<Squnion>")
   where "\<Squnion>f = OpLim (iter f)"
 
-primrec cantor :: "ordinal => ordinal => ordinal"
+primrec cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> 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>")
+primrec Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> 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)"
+definition deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
   where "deriv f = \<nabla>(\<Squnion>f)"
 
-primrec veblen :: "ordinal => ordinal => ordinal"
+primrec veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
 where
   "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
 | "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
diff -r 9cc91b8a6489 -r 7fb5b7dc8332 src/HOL/Induct/Sigma_Algebra.thy
--- a/src/HOL/Induct/Sigma_Algebra.thy	Sat Jun 20 16:08:47 2015 +0200
+++ b/src/HOL/Induct/Sigma_Algebra.thy	Sat Jun 20 16:23:56 2015 +0200
@@ -14,12 +14,12 @@
   \<sigma>}-algebra over a given set of sets.
 \<close>
 
-inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set"
+inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
 where
-  basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
+  basic: "a \<in> A \<Longrightarrow> 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"
+| complement: "a \<in> \<sigma>_algebra A \<Longrightarrow> -a \<in> \<sigma>_algebra A"
+| Union: "(\<And>i::nat. a i \<in> \<sigma>_algebra A) \<Longrightarrow> (\<Union>i. a i) \<in> \<sigma>_algebra A"
 
 text \<open>
   The following basic facts are consequences of the closure properties
@@ -36,10 +36,10 @@
 qed
 
 theorem sigma_algebra_Inter:
-  "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
+  "(\<And>i::nat. a i \<in> \<sigma>_algebra A) \<Longrightarrow> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
 proof -
-  assume "!!i::nat. a i \<in> \<sigma>_algebra A"
-  then have "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
+  assume "\<And>i::nat. a i \<in> \<sigma>_algebra A"
+  then have "\<And>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
diff -r 9cc91b8a6489 -r 7fb5b7dc8332 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Sat Jun 20 16:08:47 2015 +0200
+++ b/src/HOL/Induct/Term.thy	Sat Jun 20 16:23:56 2015 +0200
@@ -15,8 +15,8 @@
 
 text \<open>\medskip Substitution function on terms\<close>
 
-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"
+primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
+  and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('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)"
@@ -37,8 +37,8 @@
 text \<open>\medskip Alternative induction rule\<close>
 
 lemma
-  assumes var: "!!v. P (Var v)"
-    and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
+  assumes var: "\<And>v. P (Var v)"
+    and app: "\<And>f ts. (\<forall>t \<in> set ts. P t) \<Longrightarrow> P (App f ts)"
   shows term_induct2: "P t"
     and "\<forall>t \<in> set ts. P t"
   apply (induct t and ts rule: subst_term.induct subst_term_list.induct)
diff -r 9cc91b8a6489 -r 7fb5b7dc8332 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Sat Jun 20 16:08:47 2015 +0200
+++ b/src/HOL/Induct/Tree.thy	Sat Jun 20 16:23:56 2015 +0200
@@ -11,9 +11,9 @@
 
 datatype 'a tree =
     Atom 'a
-  | Branch "nat => 'a tree"
+  | Branch "nat \<Rightarrow> 'a tree"
 
-primrec map_tree :: "('a => 'b) => 'a tree => 'b tree"
+primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
 where
   "map_tree f (Atom a) = Atom (f a)"
 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
@@ -21,37 +21,37 @@
 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 \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool"
 where
   "exists_tree P (Atom a) = P a"
 | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
 
 lemma exists_map:
-  "(!!x. P x ==> Q (f x)) ==>
-    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
+  "(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow>
+    exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)"
   by (induct ts) auto
 
 
 subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
 
-datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
+datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer"
 
-text\<open>Addition of ordinals\<close>
-primrec add :: "[brouwer,brouwer] => brouwer"
+text \<open>Addition of ordinals\<close>
+primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
   "add i Zero = i"
 | "add i (Succ j) = Succ (add i j)"
-| "add i (Lim f) = Lim (%n. add i (f n))"
+| "add i (Lim f) = Lim (\<lambda>n. add i (f n))"
 
 lemma add_assoc: "add (add i j) k = add i (add j k)"
   by (induct k) auto
 
-text\<open>Multiplication of ordinals\<close>
-primrec mult :: "[brouwer,brouwer] => brouwer"
+text \<open>Multiplication of ordinals\<close>
+primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
   "mult i Zero = Zero"
 | "mult i (Succ j) = add (mult i j) i"
-| "mult i (Lim f) = Lim (%n. mult i (f n))"
+| "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))"
 
 lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
   by (induct k) (auto simp add: add_assoc)
@@ -59,35 +59,40 @@
 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
   by (induct k) (auto simp add: add_mult_distrib)
 
-text\<open>We could probably instantiate some axiomatic type classes and use
-the standard infix operators.\<close>
+text \<open>We could probably instantiate some axiomatic type classes and use
+  the standard infix operators.\<close>
 
-subsection\<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
+
+subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
 
-text\<open>To use the function package we need an ordering on the Brouwer
-  ordinals.  Start with a predecessor relation and form its transitive 
-  closure.\<close> 
+text \<open>To use the function package we need an ordering on the Brouwer
+  ordinals.  Start with a predecessor relation and form its transitive
+  closure.\<close>
 
-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 \<times> brouwer) set"
+  where "brouwer_pred = (\<Union>i. {(m, n). n = Succ m \<or> (\<exists>f. n = Lim f \<and> m = f i)})"
 
-definition brouwer_order :: "(brouwer * brouwer) set"
+definition brouwer_order :: "(brouwer \<times> 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+)
+  unfolding wf_def brouwer_pred_def
+  apply clarify
+  apply (induct_tac x)
+  apply blast+
+  done
 
 lemma wf_brouwer_order[simp]: "wf brouwer_order"
-  by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
-
-lemma [simp]: "(j, Succ j) : brouwer_order"
-  by(auto simp add: brouwer_order_def brouwer_pred_def)
+  unfolding brouwer_order_def
+  by (rule wf_trancl[OF wf_brouwer_pred])
 
-lemma [simp]: "(f n, Lim f) : brouwer_order"
-  by(auto simp add: brouwer_order_def brouwer_pred_def)
+lemma [simp]: "(j, Succ j) \<in> brouwer_order"
+  by (auto simp add: brouwer_order_def brouwer_pred_def)
 
-text\<open>Example of a general function\<close>
+lemma [simp]: "(f n, Lim f) \<in> brouwer_order"
+  by (auto simp add: brouwer_order_def brouwer_pred_def)
 
+text \<open>Example of a general function\<close>
 function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
   "add2 i Zero = i"