author berghofe Mon May 15 17:32:39 2000 +0200 (2000-05-15) changeset 8874 3242637f668c 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 file | annotate | diff | revisions src/HOL/Subst/AList.thy file | annotate | diff | revisions
```     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.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
```