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