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