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