--- 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)"
--- 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)))"
--- 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
--- 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 [] = []"
--- 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)"