src/HOL/Bali/Basis.thy
 changeset 37956 ee939247b2fb parent 36176 3fe7e97ccca8 child 44011 f67c93f52d13
```     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Jul 26 13:50:52 2010 +0200
1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jul 26 17:41:26 2010 +0200
1.3 @@ -180,31 +180,34 @@
1.4
1.5  notation sum_case  (infixr "'(+')"80)
1.6
1.7 -consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
1.8 -          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
1.9 -primrec  "the_Inl (Inl a) = a"
1.10 -primrec  "the_Inr (Inr b) = b"
1.11 +primrec the_Inl  :: "'a + 'b \<Rightarrow> 'a"
1.12 +  where "the_Inl (Inl a) = a"
1.13 +
1.14 +primrec the_Inr  :: "'a + 'b \<Rightarrow> 'b"
1.15 +  where "the_Inr (Inr b) = b"
1.16
1.17  datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
1.18
1.19 -consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
1.20 -          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
1.21 -          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
1.22 -primrec  "the_In1 (In1 a) = a"
1.23 -primrec  "the_In2 (In2 b) = b"
1.24 -primrec  "the_In3 (In3 c) = c"
1.25 +primrec the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
1.26 +  where "the_In1 (In1 a) = a"
1.27 +
1.28 +primrec the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
1.29 +  where "the_In2 (In2 b) = b"
1.30 +
1.31 +primrec the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
1.32 +  where "the_In3 (In3 c) = c"
1.33
1.34  abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
1.35 -      where "In1l e == In1 (Inl e)"
1.36 +  where "In1l e == In1 (Inl e)"
1.37
1.38  abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
1.39 -      where "In1r c == In1 (Inr c)"
1.40 +  where "In1r c == In1 (Inr c)"
1.41
1.42  abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
1.43 -      where "the_In1l == the_Inl \<circ> the_In1"
1.44 +  where "the_In1l == the_Inl \<circ> the_In1"
1.45
1.46  abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
1.47 -      where "the_In1r == the_Inr \<circ> the_In1"
1.48 +  where "the_In1r == the_Inr \<circ> the_In1"
1.49
1.50  ML {*
1.51  fun sum3_instantiate ctxt thm = map (fn s =>
1.52 @@ -232,8 +235,9 @@
1.53
1.54  text{* Deemed too special for theory Map. *}
1.55
1.56 -definition chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" where
1.57 - "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
1.58 +definition
1.59 +  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
1.60 +  where "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"
1.61
1.62  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
1.63  by (unfold chg_map_def, auto)
1.64 @@ -247,8 +251,9 @@
1.65
1.66  section "unique association lists"
1.67
1.68 -definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" where
1.69 - "unique \<equiv> distinct \<circ> map fst"
1.70 +definition
1.71 +  unique :: "('a \<times> 'b) list \<Rightarrow> bool"
1.72 +  where "unique = distinct \<circ> map fst"
1.73
1.74  lemma uniqueD [rule_format (no_asm)]:
1.75  "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
1.76 @@ -296,11 +301,11 @@
1.77
1.78  section "list patterns"
1.79
1.80 -consts
1.81 -  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
1.82 -defs
1.83 -  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
1.84 -(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
1.85 +definition
1.86 +  lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" where
1.87 +  "lsplit = (\<lambda>f l. f (hd l) (tl l))"
1.88 +
1.89 +text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
1.90  syntax
1.91    "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
1.92  translations
```