isabelle: src/HOL/Update.ML@82a5ca6290aa (annotated)

4898 68fd1a2b8b7b Removed some traces of UNITY paulson parents: 4896 diff changeset	1	(* Title: HOL/Update.thy
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	2	ID: $Id$
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	5
4898 68fd1a2b8b7b Removed some traces of UNITY paulson parents: 4896 diff changeset	6	Function updates: like theory Map, but for ordinary functions
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	7	*)
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	8
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	9	open Update;
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	10
5195 277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	11	Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	12	by Safe_tac;
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	13	by (etac subst 1);
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	14	by (rtac ext 2);
4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	15	by Auto_tac;
5195 277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	16	qed "fun_upd_idem_iff";
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	17
5070 c42429b3e2f2 Replaced [ := ] syntax by ( := ). nipkow parents: 5069 diff changeset	18	(* f x = y ==> f(x:=y) = f *)
5195 277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	19	bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	20
5154 40fd46f3d3a1 tidying paulson parents: 5133 diff changeset	21	(* f(x := f x) = f *)
5195 277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	22	AddIffs [refl RS fun_upd_idem];
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: diff changeset	23
5133 42a7fe39a63a swapped condition in update_apply. nipkow parents: 5070 diff changeset	24	Goal "(f(x:=y))z = (if z=x then y else f z)";
5195 277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	25	by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	26	qed "fun_upd_apply";
277831ae7eac Map.update -> map_upd, Unpdate.update -> fun_upd nipkow parents: 5154 diff changeset	27	Addsimps [fun_upd_apply];

author	paulson
	Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253	82a5ca6290aa
parent 5195	277831ae7eac
permissions	-rw-r--r--