misc tuning;
authorwenzelm
Wed Mar 14 00:34:56 2012 +0100 (2012-03-14)
changeset 46914c2ca2c3d23a6
parent 46913 3444a24dc4e9
child 46915 4b2eccaec3f6
child 46926 3978c15126e7
child 46927 faf4a0b02b71
misc tuning;
src/HOL/Induct/ABexp.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Induct/Sigma_Algebra.thy
src/HOL/Induct/Term.thy
src/HOL/Induct/Tree.thy
     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.5  header {* Ordinals *}
     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.26  text{*Addition of ordinals*}
    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.32  | "add i (Succ j) = Succ (add i j)"
    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.44    ordinals.  Start with a predecessor relation and form its transitive 
    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"
    5.70  | "add2 i (Succ j) = Succ (add2 i j)"