src/HOL/UNITY/Update.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/Update.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Function updates: like the standard theory Map, but for ordinary functions
     7 *)
     8 
     9 open Update;
    10 
    11 goalw thy [update_def] "(f[x|->y] = f) = (f x = y)";
    12 by Safe_tac;
    13 by (etac subst 1);
    14 by (rtac ext 2);
    15 by Auto_tac;
    16 qed "update_idem_iff";
    17 
    18 (* f x = y ==> f[x|->y] = f *)
    19 bind_thm("update_idem", update_idem_iff RS iffD2);
    20 
    21 AddIffs [refl RS update_idem];
    22 
    23 goal thy "(f[x|->y])z = (if x=z then y else f z)";
    24 by (simp_tac (simpset() addsimps [update_def]) 1);
    25 qed "update_apply";
    26 Addsimps [update_apply];