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