alist_rec and assoc are now defined using primrec and thus no longer
authorberghofe
Mon May 15 17:32:39 2000 +0200 (2000-05-15)
changeset 88743242637f668c
parent 8873 ab920d8112b4
child 8875 ac86b3d44730
alist_rec and assoc are now defined using primrec and thus no longer
refer to the recursion combinator list_rec, which should be considered
internal.
src/HOL/Subst/AList.ML
src/HOL/Subst/AList.thy
     1.1 --- a/src/HOL/Subst/AList.ML	Mon May 15 17:30:19 2000 +0200
     1.2 +++ b/src/HOL/Subst/AList.ML	Mon May 15 17:32:39 2000 +0200
     1.3 @@ -8,20 +8,6 @@
     1.4  
     1.5  open AList;
     1.6  
     1.7 -let fun prove s = prove_goalw AList.thy [alist_rec_def,assoc_def] s 
     1.8 -			  (fn _ => [Simp_tac 1])
     1.9 -in 
    1.10 -Addsimps 
    1.11 - (
    1.12 -   map prove 
    1.13 -   ["alist_rec [] c d = c",
    1.14 -    "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
    1.15 -    "assoc v d [] = d",
    1.16 -    "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] 
    1.17 - )
    1.18 -end;
    1.19 -
    1.20 -
    1.21  val prems = goal AList.thy
    1.22      "[| P([]);   \
    1.23  \       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
     2.1 --- a/src/HOL/Subst/AList.thy	Mon May 15 17:30:19 2000 +0200
     2.2 +++ b/src/HOL/Subst/AList.thy	Mon May 15 17:32:39 2000 +0200
     2.3 @@ -9,14 +9,15 @@
     2.4  AList = List + 
     2.5  
     2.6  consts
     2.7 -
     2.8    alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
     2.9    assoc      :: "['a,'b,('a*'b) list] => 'b"
    2.10  
    2.11 -defs
    2.12 +primrec
    2.13 +  "alist_rec [] c d = c"
    2.14 +  "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
    2.15  
    2.16 -  alist_rec_def "alist_rec al b c == list_rec b (split c) al"
    2.17 -
    2.18 -  assoc_def   "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
    2.19 +primrec
    2.20 +  "assoc v d [] = d"
    2.21 +  "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    2.22  
    2.23  end