author wenzelm Wed, 14 Mar 2012 00:34:56 +0100 changeset 46914 c2ca2c3d23a6 parent 46913 3444a24dc4e9 child 46915 4b2eccaec3f6 child 46926 3978c15126e7 child 46927 faf4a0b02b71
misc tuning;
 src/HOL/Induct/ABexp.thy file | annotate | diff | comparison | revisions src/HOL/Induct/Ordinals.thy file | annotate | diff | comparison | revisions src/HOL/Induct/Sigma_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Induct/Term.thy file | annotate | diff | comparison | revisions src/HOL/Induct/Tree.thy file | annotate | diff | comparison | revisions
```--- 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 @@

-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 @@

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

-primrec
-  add :: "[brouwer,brouwer] => brouwer"
+primrec add :: "[brouwer,brouwer] => brouwer"
where
@@ -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 @@
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