src/HOL/Vimage.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5490 85855f65d0c6
child 7031 972b5f62f476
permissions -rw-r--r--
tidying
paulson@4648
     1
(*  Title:      HOL/Vimage
paulson@4648
     2
    ID:         $Id$
paulson@4648
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4648
     4
    Copyright   1998  University of Cambridge
paulson@4648
     5
paulson@4648
     6
Inverse image of a function
paulson@4648
     7
*)
paulson@4648
     8
paulson@4648
     9
open Vimage;
paulson@4648
    10
paulson@4648
    11
(** Basic rules **)
paulson@4648
    12
paulson@4648
    13
qed_goalw "vimage_eq" thy [vimage_def]
paulson@4648
    14
    "(a : f-``B) = (f a : B)"
paulson@4648
    15
 (fn _ => [ (Blast_tac 1) ]);
paulson@4648
    16
paulson@4680
    17
Addsimps [vimage_eq];
paulson@4680
    18
paulson@4648
    19
qed_goal "vimage_singleton_eq" thy
paulson@4648
    20
    "(a : f-``{b}) = (f a = b)"
paulson@4648
    21
 (fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
paulson@4648
    22
paulson@4648
    23
qed_goalw "vimageI" thy [vimage_def]
paulson@4648
    24
    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B"
paulson@4648
    25
 (fn _ => [ (Blast_tac 1) ]);
paulson@4648
    26
berghofe@5095
    27
Goalw [vimage_def] "f a : A ==> a : f -`` A";
berghofe@5095
    28
by (Fast_tac 1);
berghofe@5095
    29
qed "vimageI2";
berghofe@5095
    30
paulson@4648
    31
qed_goalw "vimageE" thy [vimage_def]
paulson@4648
    32
    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P"
paulson@4648
    33
 (fn major::prems=>
paulson@4648
    34
  [ (rtac (major RS CollectE) 1),
paulson@4648
    35
    (blast_tac (claset() addIs prems) 1) ]);
paulson@4648
    36
berghofe@5095
    37
Goalw [vimage_def] "a : f -`` A ==> f a : A";
berghofe@5095
    38
by (Fast_tac 1);
berghofe@5095
    39
qed "vimageD";
berghofe@5095
    40
paulson@4648
    41
AddIs  [vimageI];
paulson@4648
    42
AddSEs [vimageE];
paulson@4648
    43
paulson@4648
    44
paulson@4648
    45
(*** Simple equalities ***)
paulson@4648
    46
wenzelm@5069
    47
Goal "(%x. x) -`` B = B";
paulson@4680
    48
by (Blast_tac 1);
paulson@4680
    49
qed "ident_vimage";
paulson@4680
    50
Addsimps [ident_vimage];
paulson@4680
    51
wenzelm@5069
    52
Goal "f-``{} = {}";
paulson@4648
    53
by (Blast_tac 1);
paulson@4648
    54
qed "vimage_empty";
paulson@4648
    55
paulson@5490
    56
Goal "f-``(-A) = -(f-``A)";
paulson@4660
    57
by (Blast_tac 1);
paulson@4660
    58
qed "vimage_Compl";
paulson@4660
    59
wenzelm@5069
    60
Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
paulson@4648
    61
by (Blast_tac 1);
paulson@4648
    62
qed "vimage_Un";
paulson@4648
    63
berghofe@5095
    64
Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
berghofe@5095
    65
by (Fast_tac 1);
berghofe@5095
    66
qed "vimage_Int";
berghofe@5095
    67
wenzelm@5069
    68
Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
paulson@4674
    69
by (Blast_tac 1);
paulson@4674
    70
qed "vimage_UN";
paulson@4674
    71
berghofe@5095
    72
bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
berghofe@5095
    73
  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
berghofe@5095
    74
    (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
berghofe@5095
    75
berghofe@5095
    76
Addsimps [vimage_empty, vimage_Un, vimage_Int];
paulson@4660
    77
paulson@4648
    78
(*NOT suitable for rewriting because of the recurrence of {a}*)
wenzelm@5069
    79
Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
paulson@4648
    80
by (Blast_tac 1);
paulson@4648
    81
qed "vimage_insert";
paulson@4648
    82
wenzelm@5069
    83
Goal "f-``(A-B) = (f-``A) - (f-``B)";
paulson@4738
    84
by (Blast_tac 1);
paulson@4738
    85
qed "vimage_Diff";
paulson@4648
    86
wenzelm@5069
    87
Goal "f-``UNIV = UNIV";
paulson@4648
    88
by (Blast_tac 1);
paulson@4648
    89
qed "vimage_UNIV";
paulson@4648
    90
Addsimps [vimage_UNIV];
paulson@4648
    91
wenzelm@5069
    92
Goal "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
paulson@4648
    93
by (Blast_tac 1);
paulson@4648
    94
qed "UN_vimage";
paulson@4648
    95
Addsimps [UN_vimage];
paulson@4648
    96
paulson@4734
    97
(*NOT suitable for rewriting*)
wenzelm@5069
    98
Goal "f-``B = (UN y: B. f-``{y})";
paulson@4734
    99
by (Blast_tac 1);
paulson@4734
   100
qed "vimage_eq_UN";
paulson@4734
   101
paulson@4648
   102
paulson@4648
   103
(** monotonicity **)
paulson@4648
   104
paulson@5143
   105
Goal "A<=B ==> f-``A <= f-``B";
paulson@4648
   106
by (Blast_tac 1);
paulson@4648
   107
qed "vimage_mono";