src/HOL/Subst/Setplus.ML
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1465 5d7a7e439cec
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
clasohm@1465
     1
(*  Title:      Substitutions/setplus.ML
clasohm@1465
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
For setplus.thy.
clasohm@968
     6
Properties of subsets and empty sets.
clasohm@968
     7
*)
clasohm@968
     8
clasohm@968
     9
open Setplus;
clasohm@968
    10
clasohm@968
    11
(*********)
clasohm@968
    12
clasohm@968
    13
(*** Rules for subsets ***)
clasohm@968
    14
clasohm@968
    15
goal Set.thy "A <= B =  (! t.t:A --> t:B)";
clasohm@968
    16
by (fast_tac set_cs 1);
clasohm@968
    17
qed "subset_iff";
clasohm@968
    18
clasohm@968
    19
goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))";
clasohm@968
    20
by (rtac refl 1);
clasohm@968
    21
qed "ssubset_iff";
clasohm@968
    22
clasohm@968
    23
goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))";
clasohm@1266
    24
by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1);
clasohm@968
    25
by (fast_tac set_cs 1);
clasohm@968
    26
qed "subseteq_iff_subset_eq";
clasohm@968
    27
clasohm@968
    28
(*Rule in Modus Ponens style*)
clasohm@968
    29
goal Setplus.thy "A < B --> c:A --> c:B";
clasohm@1266
    30
by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1);
clasohm@968
    31
by (fast_tac set_cs 1);
clasohm@968
    32
qed "ssubsetD";
clasohm@968
    33
clasohm@968
    34
(*********)
clasohm@968
    35
clasohm@968
    36
goalw Setplus.thy [empty_def] "~ a : {}";
clasohm@968
    37
by (fast_tac set_cs 1);
clasohm@968
    38
qed "not_in_empty";
clasohm@968
    39
clasohm@968
    40
goalw Setplus.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
clasohm@968
    41
by (fast_tac (set_cs addIs [set_ext]) 1);
clasohm@968
    42
qed "empty_iff";
clasohm@968
    43
clasohm@968
    44
clasohm@968
    45
(*********)
clasohm@968
    46
clasohm@968
    47
goal Set.thy "(~A=B)  = ((? x.x:A & ~x:B) | (? x.~x:A & x:B))";
clasohm@968
    48
by (fast_tac (set_cs addIs [set_ext]) 1);
clasohm@968
    49
qed "not_equal_iff";
clasohm@968
    50
clasohm@968
    51
(*********)
clasohm@968
    52
clasohm@968
    53
val setplus_rews = [ssubset_iff,not_in_empty,empty_iff];
clasohm@968
    54
clasohm@968
    55
(*********)
clasohm@968
    56
clasohm@968
    57
(*Case analysis for rewriting; P also gets rewritten*)
clasohm@968
    58
val [prem1,prem2] = goal HOL.thy "[| P-->Q;  ~P-->Q |] ==> Q";
clasohm@968
    59
by (rtac (excluded_middle RS disjE) 1);
clasohm@968
    60
by (etac (prem2 RS mp) 1);
clasohm@968
    61
by (etac (prem1 RS mp) 1);
clasohm@968
    62
qed "imp_excluded_middle";
clasohm@968
    63
clasohm@968
    64
fun imp_excluded_middle_tac s = res_inst_tac [("P",s)] imp_excluded_middle;