src/ZF/upair.ML
 changeset 6 8ce8c4d13d4d parent 0 a5a9c433f639 child 14 1c0926788772
```--- a/src/ZF/upair.ML	Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/upair.ML	Fri Sep 17 16:16:38 1993 +0200
@@ -167,10 +167,6 @@
(resolve_tac [major RS the_equality2 RS ssubst] 1),
(REPEAT (assume_tac 1)) ]);

-val the_cong = prove_goalw ZF.thy [the_def]
-    "[| !!y. P(y) <-> Q(y) |] ==> (THE x. P(x)) = (THE x. Q(x))"
- (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
-

(*** if -- a conditional expression for formulae ***)

@@ -182,38 +178,34 @@
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
val if_false = result();

+(*Never use with case splitting, or if P is known to be true or false*)
val prems = goalw ZF.thy [if_def]
-    "[| P<->Q;  a=c;  b=d |] ==> if(P,a,b) = if(Q,c,d)";
-by (REPEAT (resolve_tac (prems@[refl,the_cong]@FOL_congs) 1));
+    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
val if_cong = result();

(*Not needed for rewriting, since P would rewrite to True anyway*)
-val prems = goalw ZF.thy [if_def] "P ==> if(P,a,b) = a";
-by (cut_facts_tac prems 1);
+goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
val if_P = result();

(*Not needed for rewriting, since P would rewrite to False anyway*)
-val prems = goalw ZF.thy [if_def] "~P ==> if(P,a,b) = b";
-by (cut_facts_tac prems 1);
+goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
val if_not_P = result();

-val if_ss =
-    FOL_ss addcongs (if_cong :: mk_typed_congs ZF.thy [("P", "i=>o")]
-			      @ basic_ZF_congs)
+val if_ss = FOL_ss addsimps  [if_true,if_false];

val expand_if = prove_goal ZF.thy
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
-	   (ASM_SIMP_TAC if_ss 1),
-	   (ASM_SIMP_TAC if_ss 1) ]);
+	   (asm_simp_tac if_ss 1),
+	   (asm_simp_tac if_ss 1) ]);

val prems = goal ZF.thy
"[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);
-by (ALLGOALS (ASM_SIMP_TAC (if_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
val if_type = result();

```