author paulson Wed, 13 Jan 1999 11:56:28 +0100 changeset 6111 5347c9a22897 parent 6110 15c2b571225b child 6112 5e4871c5136b
better qed_spec_mp
 src/ZF/ZF.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/ZF.ML	Wed Jan 13 08:41:59 1999 +0100
+++ b/src/ZF/ZF.ML	Wed Jan 13 11:56:28 1999 +0100
@@ -6,8 +6,6 @@
Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory
*)

-open ZF;
-
(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
Goal "[| b:A;  a=b |] ==> a:A";
by (etac ssubst 1);
@@ -128,6 +126,9 @@
qed_goal "rev_subsetD" ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
(fn _=> [ Blast_tac 1 ]);

+(*Converts A<=B to x:A ==> x:B*)
+fun impOfSubs th = th RSN (2, rev_subsetD);
+
qed_goal "contra_subsetD" ZF.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
(fn _=> [ Blast_tac 1 ]);

@@ -475,3 +476,45 @@
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
(fn _ => [Blast_tac 1]);

+
+local
+val (bspecT, bspec') = make_new_spec bspec
+in
+
+fun RSbspec th =
+  (case concl_of th of
+     _ \$ (Const("Ball",_) \$ _ \$ Abs(a,_,_)) =>
+         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),bspecT))
+         in th RS forall_elim ca bspec' end
+  | _ => raise THM("RSbspec",0,[th]));
+
+
+fun qed_spec_mp name =
+  let val thm = normalize_thm_ZF (result())
+  in bind_thm(name, thm) end;
+
+fun qed_goal_spec_mp name thy s p =
+      bind_thm (name, normalize_thm_ZF (prove_goal thy s p));
+
+fun qed_goalw_spec_mp name thy defs s p =
+      bind_thm (name, normalize_thm_ZF (prove_goalw thy defs s p));
+
+end;
+
+
+(* attributes *)
+
+local
+
+fun gen_rulify x =
+    Attrib.no_args (Drule.rule_attribute (K (normalize_thm_ZF))) x;
+
+in
+
+val attrib_setup =