isabelle: src/HOL/Subst/AList.thy@9a3925c07392 (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
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	13	consts
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	14	alist_rec :: "[('a'b)list, 'c, ['a, 'b, ('a'b)list, 'c]=>'c] => 'c"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	15	assoc :: "['a,'b,('a*'b) list] => 'b"
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	16
8874 3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	17	primrec
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	18	"alist_rec [] c d = c"
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	19	"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	20
8874 3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	21	primrec
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	22	"assoc v d [] = d"
3242637f668c alist_rec and assoc are now defined using primrec and thus no longer berghofe parents: 3842 diff changeset	23	"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	24
15635 8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	25
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	26	lemma alist_induct:
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	27	"[\| P([]);
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	28	!!x y xs. P(xs) ==> P((x,y)#xs) \|] ==> P(l)"
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	29	by (induct_tac "l", auto)
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 12406 diff changeset	30
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	31	end

author	wenzelm
	Sat, 17 Sep 2005 18:11:19 +0200
changeset 17459	9a3925c07392
parent 15635	8408a06590a6
child 24823	bfb619994060
permissions	-rw-r--r--