src/ZF/Update.ML
author paulson
Fri, 17 Jul 1998 11:13:59 +0200
changeset 5157 6e03de8ec2b4
child 5168 adafef6eb295
permissions -rw-r--r--
as in HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5157
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     1
(*  Title:      ZF/Update.thy
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     2
    ID:         $Id$
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     5
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     6
Function updates: like theory Map, but for ordinary functions
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     7
*)
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     8
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     9
open Update;
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    10
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    11
Goal "f(x:=y) ` z = if(z=x, y, f`z)";
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    12
by (simp_tac (simpset() addsimps [update_def]) 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    13
by (case_tac "z : domain(f)" 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    14
by (Asm_simp_tac 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    15
by (asm_simp_tac (simpset() addsimps [apply_0]) 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    16
qed "update_apply";
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    17
Addsimps [update_apply];
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    18
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    19
Goalw [update_def] "[| f`x = y;  f: Pi(A,B);  x: A |] ==> f(x:=y) = f";
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    20
by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    21
by (rtac fun_extension 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    22
by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    23
ba 1;
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    24
by (Asm_simp_tac 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    25
qed "update_idem";
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    26
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    27
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    28
(* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *)
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    29
Addsimps [refl RS update_idem];
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    30
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    31
Goalw [update_def] "domain(f(x:=y)) = cons(x, domain(f))";
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    32
by (Asm_simp_tac 1);
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    33
qed "domain_update";
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    34
Addsimps [domain_update];
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
    35