src/HOL/Vimage.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7516 a1d476251238
child 7823 742715638a01
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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
(** Basic rules **)
paulson@4648
    10
paulson@7031
    11
Goalw [vimage_def] "(a : f-``B) = (f a : B)";
paulson@7031
    12
by (Blast_tac 1) ;
paulson@7031
    13
qed "vimage_eq";
paulson@4648
    14
paulson@4680
    15
Addsimps [vimage_eq];
paulson@4680
    16
paulson@7031
    17
Goal "(a : f-``{b}) = (f a = b)";
paulson@7031
    18
by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
paulson@7031
    19
qed "vimage_singleton_eq";
paulson@4648
    20
paulson@7031
    21
Goalw [vimage_def]
paulson@7031
    22
    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
paulson@7031
    23
by (Blast_tac 1) ;
paulson@7031
    24
qed "vimageI";
paulson@4648
    25
berghofe@5095
    26
Goalw [vimage_def] "f a : A ==> a : f -`` A";
berghofe@5095
    27
by (Fast_tac 1);
berghofe@5095
    28
qed "vimageI2";
berghofe@5095
    29
paulson@7031
    30
val major::prems = Goalw [vimage_def]
paulson@7031
    31
    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
paulson@7031
    32
by (rtac (major RS CollectE) 1);
paulson@7031
    33
by (blast_tac (claset() addIs prems) 1) ;
paulson@7031
    34
qed "vimageE";
paulson@4648
    35
berghofe@5095
    36
Goalw [vimage_def] "a : f -`` A ==> f a : A";
berghofe@5095
    37
by (Fast_tac 1);
berghofe@5095
    38
qed "vimageD";
berghofe@5095
    39
paulson@4648
    40
AddIs  [vimageI];
paulson@4648
    41
AddSEs [vimageE];
paulson@4648
    42
paulson@4648
    43
paulson@4648
    44
(*** Simple equalities ***)
paulson@4648
    45
wenzelm@5069
    46
Goal "f-``{} = {}";
paulson@4648
    47
by (Blast_tac 1);
paulson@4648
    48
qed "vimage_empty";
paulson@4648
    49
paulson@5490
    50
Goal "f-``(-A) = -(f-``A)";
paulson@4660
    51
by (Blast_tac 1);
paulson@4660
    52
qed "vimage_Compl";
paulson@4660
    53
wenzelm@5069
    54
Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
paulson@4648
    55
by (Blast_tac 1);
paulson@4648
    56
qed "vimage_Un";
paulson@4648
    57
berghofe@5095
    58
Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
berghofe@5095
    59
by (Fast_tac 1);
berghofe@5095
    60
qed "vimage_Int";
berghofe@5095
    61
wenzelm@5069
    62
Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
paulson@4674
    63
by (Blast_tac 1);
paulson@4674
    64
qed "vimage_UN";
paulson@4674
    65
berghofe@5095
    66
bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
berghofe@5095
    67
  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
berghofe@5095
    68
    (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
berghofe@5095
    69
berghofe@5095
    70
Addsimps [vimage_empty, vimage_Un, vimage_Int];
paulson@4660
    71
paulson@4648
    72
(*NOT suitable for rewriting because of the recurrence of {a}*)
wenzelm@5069
    73
Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
paulson@4648
    74
by (Blast_tac 1);
paulson@4648
    75
qed "vimage_insert";
paulson@4648
    76
wenzelm@5069
    77
Goal "f-``(A-B) = (f-``A) - (f-``B)";
paulson@4738
    78
by (Blast_tac 1);
paulson@4738
    79
qed "vimage_Diff";
paulson@4648
    80
wenzelm@5069
    81
Goal "f-``UNIV = UNIV";
paulson@4648
    82
by (Blast_tac 1);
paulson@4648
    83
qed "vimage_UNIV";
paulson@4648
    84
Addsimps [vimage_UNIV];
paulson@4648
    85
wenzelm@5069
    86
Goal "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
paulson@4648
    87
by (Blast_tac 1);
paulson@4648
    88
qed "UN_vimage";
paulson@4648
    89
Addsimps [UN_vimage];
paulson@4648
    90
paulson@4734
    91
(*NOT suitable for rewriting*)
wenzelm@5069
    92
Goal "f-``B = (UN y: B. f-``{y})";
paulson@4734
    93
by (Blast_tac 1);
paulson@4734
    94
qed "vimage_eq_UN";
paulson@4734
    95
paulson@4648
    96
paulson@4648
    97
(** monotonicity **)
paulson@4648
    98
paulson@5143
    99
Goal "A<=B ==> f-``A <= f-``B";
paulson@4648
   100
by (Blast_tac 1);
paulson@4648
   101
qed "vimage_mono";