isabelle: src/HOL/Subst/AList.thy@24d0e890b432 (annotated)

15635 8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	1	(* ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 968 diff changeset	2	Author: Martin Coen, Cambridge University Computer Laboratory
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	3	Copyright 1993 University of Cambridge
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	4
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	5	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	6
15635 8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	7	header{Association Lists}
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	8
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	9	theory AList
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	10	imports Main
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	11	begin
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	12
24823 bfb619994060 modernized specifications; wenzelm parents: 15635 diff changeset	13	consts alist_rec :: "[('a'b)list, 'c, ['a, 'b, ('a'b)list, 'c]=>'c] => 'c"
8874 3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	14	primrec
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	15	"alist_rec [] c d = c"
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	16	"alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	17
24823 bfb619994060 modernized specifications; wenzelm parents: 15635 diff changeset	18	consts assoc :: "['a,'b,('a*'b) list] => 'b"
8874 3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	19	primrec
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	20	"assoc v d [] = d"
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	21	"assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	22
15635 8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	23	lemma alist_induct:
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	24	"[\| P([]);
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	25	!!x y xs. P(xs) ==> P((x,y)#xs) \|] ==> P(l)"
24823 bfb619994060 modernized specifications; wenzelm parents: 15635 diff changeset	26	by (induct l) auto
15635 8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	27
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	28	end

author	wenzelm
	Wed, 06 Aug 2008 00:12:26 +0200
changeset 27756	24d0e890b432
parent 24823	bfb619994060
child 38140	05691ad74079
permissions	-rw-r--r--