author wenzelm Wed Mar 14 00:34:56 2012 +0100 (2012-03-14) 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 | revisions src/HOL/Induct/Ordinals.thy file | annotate | diff | revisions src/HOL/Induct/Sigma_Algebra.thy file | annotate | diff | revisions src/HOL/Induct/Term.thy file | annotate | diff | revisions src/HOL/Induct/Tree.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Induct/ABexp.thy	Tue Mar 13 23:45:34 2012 +0100
1.2 +++ b/src/HOL/Induct/ABexp.thy	Wed Mar 14 00:34:56 2012 +0100
1.3 @@ -4,7 +4,9 @@
1.4
1.5  header {* Arithmetic and boolean expressions *}
1.6
1.7 -theory ABexp imports Main begin
1.8 +theory ABexp
1.9 +imports Main
1.10 +begin
1.11
1.12  datatype 'a aexp =
1.13      IF "'a bexp"  "'a aexp"  "'a aexp"
1.14 @@ -21,7 +23,8 @@
1.15  text {* \medskip Evaluation of arithmetic and boolean expressions *}
1.16
1.17  primrec evala :: "('a => nat) => 'a aexp => nat"
1.18 -  and evalb :: "('a => nat) => 'a bexp => bool" where
1.19 +  and evalb :: "('a => nat) => 'a bexp => bool"
1.20 +where
1.21    "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
1.22  | "evala env (Sum a1 a2) = evala env a1 + evala env a2"
1.23  | "evala env (Diff a1 a2) = evala env a1 - evala env a2"
1.24 @@ -36,7 +39,8 @@
1.25  text {* \medskip Substitution on arithmetic and boolean expressions *}
1.26
1.27  primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
1.28 -  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where
1.29 +  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
1.30 +where
1.31    "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
1.32  | "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
1.33  | "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
```
```     2.1 --- a/src/HOL/Induct/Ordinals.thy	Tue Mar 13 23:45:34 2012 +0100
2.2 +++ b/src/HOL/Induct/Ordinals.thy	Wed Mar 14 00:34:56 2012 +0100
2.3 @@ -4,7 +4,9 @@
2.4
2.6
2.7 -theory Ordinals imports Main begin
2.8 +theory Ordinals
2.9 +imports Main
2.10 +begin
2.11
2.12  text {*
2.13    Some basic definitions of ordinal numbers.  Draws an Agda
2.14 @@ -17,37 +19,38 @@
2.15    | Succ ordinal
2.16    | Limit "nat => ordinal"
2.17
2.18 -primrec pred :: "ordinal => nat => ordinal option" where
2.19 +primrec pred :: "ordinal => nat => ordinal option"
2.20 +where
2.21    "pred Zero n = None"
2.22  | "pred (Succ a) n = Some a"
2.23  | "pred (Limit f) n = Some (f n)"
2.24
2.25 -abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" where
2.26 -  "iter f n \<equiv> f ^^ n"
2.27 +abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)"
2.28 +  where "iter f n \<equiv> f ^^ n"
2.29 +
2.30 +definition OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
2.31 +  where "OpLim F a = Limit (\<lambda>n. F n a)"
2.32
2.33 -definition
2.34 -  OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where
2.35 -  "OpLim F a = Limit (\<lambda>n. F n a)"
2.36 +definition OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<Squnion>")
2.37 +  where "\<Squnion>f = OpLim (iter f)"
2.38
2.39 -definition
2.40 -  OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>") where
2.41 -  "\<Squnion>f = OpLim (iter f)"
2.42 -
2.43 -primrec cantor :: "ordinal => ordinal => ordinal" where
2.44 +primrec cantor :: "ordinal => ordinal => ordinal"
2.45 +where
2.46    "cantor a Zero = Succ a"
2.47  | "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
2.48  | "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
2.49
2.50 -primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>") where
2.51 +primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"  ("\<nabla>")
2.52 +where
2.53    "\<nabla>f Zero = f Zero"
2.54  | "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
2.55  | "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
2.56
2.57 -definition
2.58 -  deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
2.59 -  "deriv f = \<nabla>(\<Squnion>f)"
2.60 +definition deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
2.61 +  where "deriv f = \<nabla>(\<Squnion>f)"
2.62
2.63 -primrec veblen :: "ordinal => ordinal => ordinal" where
2.64 +primrec veblen :: "ordinal => ordinal => ordinal"
2.65 +where
2.66    "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
2.67  | "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
2.68  | "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
```
```     3.1 --- a/src/HOL/Induct/Sigma_Algebra.thy	Tue Mar 13 23:45:34 2012 +0100
3.2 +++ b/src/HOL/Induct/Sigma_Algebra.thy	Wed Mar 14 00:34:56 2012 +0100
3.3 @@ -4,7 +4,9 @@
3.4
3.5  header {* Sigma algebras *}
3.6
3.7 -theory Sigma_Algebra imports Main begin
3.8 +theory Sigma_Algebra
3.9 +imports Main
3.10 +begin
3.11
3.12  text {*
3.13    This is just a tiny example demonstrating the use of inductive
3.14 @@ -12,14 +14,12 @@
3.15    \<sigma>}-algebra over a given set of sets.
3.16  *}
3.17
3.18 -inductive_set
3.19 -  \<sigma>_algebra :: "'a set set => 'a set set"
3.20 -  for A :: "'a set set"
3.21 -  where
3.22 -    basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
3.23 -  | UNIV: "UNIV \<in> \<sigma>_algebra A"
3.24 -  | complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
3.25 -  | Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
3.26 +inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set"
3.27 +where
3.28 +  basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
3.29 +| UNIV: "UNIV \<in> \<sigma>_algebra A"
3.30 +| complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
3.31 +| Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
3.32
3.33  text {*
3.34    The following basic facts are consequences of the closure properties
3.35 @@ -30,7 +30,7 @@
3.36  theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
3.37  proof -
3.38    have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
3.39 -  hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
3.40 +  then have "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
3.41    also have "-UNIV = {}" by simp
3.42    finally show ?thesis .
3.43  qed
3.44 @@ -39,9 +39,9 @@
3.45    "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
3.46  proof -
3.47    assume "!!i::nat. a i \<in> \<sigma>_algebra A"
3.48 -  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
3.49 -  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
3.50 -  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
3.51 +  then have "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
3.52 +  then have "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
3.53 +  then have "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
3.54    also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
3.55    finally show ?thesis .
3.56  qed
```
```     4.1 --- a/src/HOL/Induct/Term.thy	Tue Mar 13 23:45:34 2012 +0100
4.2 +++ b/src/HOL/Induct/Term.thy	Wed Mar 14 00:34:56 2012 +0100
4.3 @@ -4,7 +4,9 @@
4.4
4.5  header {* Terms over a given alphabet *}
4.6
4.7 -theory Term imports Main begin
4.8 +theory Term
4.9 +imports Main
4.10 +begin
4.11
4.12  datatype ('a, 'b) "term" =
4.13      Var 'a
4.14 @@ -14,7 +16,8 @@
4.15  text {* \medskip Substitution function on terms *}
4.16
4.17  primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
4.18 -  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
4.19 +  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
4.20 +where
4.21    "subst_term f (Var a) = f a"
4.22  | "subst_term f (App b ts) = App b (subst_term_list f ts)"
4.23  | "subst_term_list f [] = []"
```
```     5.1 --- a/src/HOL/Induct/Tree.thy	Tue Mar 13 23:45:34 2012 +0100
5.2 +++ b/src/HOL/Induct/Tree.thy	Wed Mar 14 00:34:56 2012 +0100
5.3 @@ -13,8 +13,7 @@
5.4      Atom 'a
5.5    | Branch "nat => 'a tree"
5.6
5.7 -primrec
5.8 -  map_tree :: "('a => 'b) => 'a tree => 'b tree"
5.9 +primrec map_tree :: "('a => 'b) => 'a tree => 'b tree"
5.10  where
5.11    "map_tree f (Atom a) = Atom (f a)"
5.12  | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
5.13 @@ -22,8 +21,7 @@
5.14  lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
5.15    by (induct t) simp_all
5.16
5.17 -primrec
5.18 -  exists_tree :: "('a => bool) => 'a tree => bool"
5.19 +primrec exists_tree :: "('a => bool) => 'a tree => bool"
5.20  where
5.21    "exists_tree P (Atom a) = P a"
5.22  | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
5.23 @@ -39,8 +37,7 @@
5.24  datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
5.25
5.27 -primrec
5.28 -  add :: "[brouwer,brouwer] => brouwer"
5.29 +primrec add :: "[brouwer,brouwer] => brouwer"
5.30  where
5.31    "add i Zero = i"
5.33 @@ -50,8 +47,7 @@
5.34    by (induct k) auto
5.35
5.36  text{*Multiplication of ordinals*}
5.37 -primrec
5.38 -  mult :: "[brouwer,brouwer] => brouwer"
5.39 +primrec mult :: "[brouwer,brouwer] => brouwer"
5.40  where
5.41    "mult i Zero = Zero"
5.42  | "mult i (Succ j) = add (mult i j) i"
5.43 @@ -72,13 +68,11 @@
5.45    closure. *}
5.46
5.47 -definition
5.48 -  brouwer_pred :: "(brouwer * brouwer) set" where
5.49 -  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
5.50 +definition brouwer_pred :: "(brouwer * brouwer) set"
5.51 +  where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
5.52
5.53 -definition
5.54 -  brouwer_order :: "(brouwer * brouwer) set" where
5.55 -  "brouwer_order = brouwer_pred^+"
5.56 +definition brouwer_order :: "(brouwer * brouwer) set"
5.57 +  where "brouwer_order = brouwer_pred^+"
5.58
5.59  lemma wf_brouwer_pred: "wf brouwer_pred"
5.60    by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
5.61 @@ -94,8 +88,7 @@
5.62
5.63  text{*Example of a general function*}
5.64
5.65 -function
5.66 -  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
5.67 +function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
5.68  where
5.69    "add2 i Zero = i"