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