Subst/setplus.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Subst/setplus.ML	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,64 @@
+(*  Title: 	Substitutions/setplus.ML
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+For setplus.thy.
+Properties of subsets and empty sets.
+*)
+
+open Setplus;
+
+(*********)
+
+(*** Rules for subsets ***)
+
+goal Set.thy "A <= B =  (! t.t:A --> t:B)";
+by (fast_tac set_cs 1);
+val subset_iff = result();
+
+goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))";
+by (rtac refl 1);
+val ssubset_iff = result();
+
+goal Setplus.thy "(A::'a set <= B) = ((A < B) | (A=B))";
+by (simp_tac (set_ss addsimps [ssubset_iff]) 1);
+by (fast_tac set_cs 1);
+val subseteq_iff_subset_eq = result();
+
+(*Rule in Modus Ponens style*)
+goal Setplus.thy "A < B --> c:A --> c:B";
+by (simp_tac (set_ss addsimps [ssubset_iff]) 1);
+by (fast_tac set_cs 1);
+val ssubsetD = result();
+
+(*********)
+
+goalw Setplus.thy [empty_def] "~ a : {}";
+by (fast_tac set_cs 1);
+val not_in_empty = result();
+
+goalw Setplus.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
+by (fast_tac (set_cs addIs [set_ext]) 1);
+val empty_iff = result();
+
+
+(*********)
+
+goal Set.thy "(~A=B)  = ((? x.x:A & ~x:B) | (? x.~x:A & x:B))";
+by (fast_tac (set_cs addIs [set_ext]) 1);
+val not_equal_iff = result();
+
+(*********)
+
+val setplus_rews = [ssubset_iff,not_in_empty,empty_iff];
+
+(*********)
+
+(*Case analysis for rewriting; P also gets rewritten*)
+val [prem1,prem2] = goal HOL.thy "[| P-->Q;  ~P-->Q |] ==> Q";
+by (rtac (excluded_middle RS disjE) 1);
+by (etac (prem2 RS mp) 1);
+by (etac (prem1 RS mp) 1);
+val imp_excluded_middle = result();
+
+fun imp_excluded_middle_tac s = res_inst_tac [("P",s)] imp_excluded_middle;