--- a/src/ZF/AC/WO1_WO6.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/AC/WO1_WO6.ML Thu Jan 07 10:56:05 1999 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/AC/WO1-WO6.ML
+(* Title: ZF/AC/WO1_WO6.ML
ID: $Id$
Author: Krzysztof Grabczewski
--- a/src/ZF/AC/WO2_AC16.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/AC/WO2_AC16.ML Thu Jan 07 10:56:05 1999 +0100
@@ -544,8 +544,7 @@
by (resolve_tac [bij_is_fun RS apply_type] 1 THEN (assume_tac 1));
by (eresolve_tac [Least_le RS lt_trans2 RS ltD] 1
THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1));
-(*SLOW! 5 secs?*)
-by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1));
+by (rtac (lt_Ord RSN (2, LeastI)) 1 THEN REPEAT (assume_tac 1));
qed "main_induct";
(* ********************************************************************** *)
@@ -581,7 +580,8 @@
by (rtac ex1I 1);
by (fast_tac (claset() addSIs [OUN_I]) 1);
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
-by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1));
+by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1
+ THEN assume_tac 1);
by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2));
(** LEVEL 20 **)
by (fast_tac FOL_cs 2);
--- a/src/ZF/AC/WO6_WO1.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Thu Jan 07 10:56:05 1999 +0100
@@ -31,19 +31,20 @@
domain(uu(f,b,g,d)) lepoll m));
d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
domain(uu(f,b,g,d)) lepoll m
- in if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
+ in if f`b ~= 0 then domain(uu(f,b,g,d)) else 0"
ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
- gg1_def "gg1(f,a,m) == lam b:a++a. if (b<a, vv1(f,m,b), ww1(f,m,b--a))"
+ gg1_def "gg1(f,a,m) == lam b:a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)"
(*Definitions for case 2*)
vv2_def "vv2(f,b,g,s) ==
- if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
+ if f`g ~= 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s} else 0"
ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
- gg2_def "gg2(f,a,b,s) == lam g:a++a. if (g<a, vv2(f,b,g,s), ww2(f,b,g--a,s))"
+ gg2_def "gg2(f,a,b,s) ==
+ lam g:a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
end
--- a/src/ZF/AC/recfunAC16.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/AC/recfunAC16.ML Thu Jan 07 10:56:05 1999 +0100
@@ -5,8 +5,6 @@
Properties of the recursive definition used in the proof of WO2 ==> AC16
*)
-open recfunAC16;
-
(* ********************************************************************** *)
(* Basic properties of recfunAC16 *)
(* ********************************************************************** *)
@@ -15,11 +13,13 @@
by (rtac transrec2_0 1);
qed "recfunAC16_0";
-Goalw [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \
-\ if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y, recfunAC16(f,fa,i,a), \
-\ recfunAC16(f,fa,i,a) Un {f ` (LEAST j. fa ` i <= f ` j & \
-\ (ALL b<a. (fa`b <= f`j \
-\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
+Goalw [recfunAC16_def]
+ "recfunAC16(f,fa,succ(i),a) = \
+\ (if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y) then recfunAC16(f,fa,i,a) \
+\ else recfunAC16(f,fa,i,a) Un \
+\ {f ` (LEAST j. fa ` i <= f ` j & \
+\ (ALL b<a. (fa`b <= f`j \
+\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
by (rtac transrec2_succ 1);
qed "recfunAC16_succ";
--- a/src/ZF/Arith.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Arith.ML Thu Jan 07 10:56:05 1999 +0100
@@ -396,10 +396,11 @@
div_termination RS ltD, add_diff_inverse]) 1);
qed "mod_div_equality";
-(*** Further facts about mod (mainly for mutilated checkerboard ***)
+
+(*** Further facts about mod (mainly for mutilated chess board) ***)
-Goal "[| 0<n; m:nat; n:nat |] ==> \
-\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))";
+Goal "[| 0<n; m:nat; n:nat |] \
+\ ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
by (etac complete_induct 1);
by (excluded_middle_tac "succ(x)<n" 1);
(* case succ(x) < n *)
@@ -427,7 +428,7 @@
qed "mod_less_divisor";
-Goal "[| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)";
+Goal "[| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
by (subgoal_tac "k mod 2: 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
by (dtac ltD 1);
--- a/src/ZF/Cardinal.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Cardinal.ML Thu Jan 07 10:56:05 1999 +0100
@@ -157,7 +157,7 @@
"[| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)";
by (safe_tac (claset_of ZF.thy));
by (swap_res_tac [exI] 1);
-by (res_inst_tac [("a", "lam z:A. if(f`z=m, y, f`z)")] CollectI 1);
+by (res_inst_tac [("a", "lam z:A. if f`z=m then y else f`z")] CollectI 1);
by (best_tac (claset() addSIs [if_type RS lam_type]
addEs [apply_funtype RS succE]) 1);
(*Proving it's injective*)
@@ -429,7 +429,7 @@
Goalw [lepoll_def, inj_def]
"[| cons(u,A) lepoll cons(v,B); u~:A; v~:B |] ==> A lepoll B";
by Safe_tac;
-by (res_inst_tac [("x", "lam x:A. if(f`x=v, f`u, f`x)")] exI 1);
+by (res_inst_tac [("x", "lam x:A. if f`x=v then f`u else f`x")] exI 1);
by (rtac CollectI 1);
(*Proving it's in the function space A->B*)
by (rtac (if_type RS lam_type) 1);
@@ -561,8 +561,8 @@
Goalw [lepoll_def]
"[| A lepoll B; b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
by Safe_tac;
-by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1);
-by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, a)")]
+by (res_inst_tac [("x", "lam y: cons(a,A). if y=a then b else f`y")] exI 1);
+by (res_inst_tac [("d","%z. if z:B then converse(f)`z else a")]
lam_injective 1);
by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, cons_iff]
setloop etac consE') 1);
@@ -614,8 +614,8 @@
Goalw [eqpoll_def]
"[| f: inj(A,B); A Int B = 0 |] ==> A Un (B - range(f)) eqpoll B";
by (rtac exI 1);
-by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"),
- ("d", "%y. if(y: range(f), converse(f)`y, y)")]
+by (res_inst_tac [("c", "%x. if x:A then f`x else x"),
+ ("d", "%y. if y: range(f) then converse(f)`y else y")]
lam_bijective 1);
by (blast_tac (claset() addSIs [if_type, inj_is_fun RS apply_type]) 1);
by (asm_simp_tac
@@ -662,11 +662,11 @@
qed "lepoll_1_is_sing";
Goalw [lepoll_def] "A Un B lepoll A+B";
-by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1);
+by (res_inst_tac [("x",
+ "lam x: A Un B. if x:A then Inl(x) else Inr(x)")] exI 1);
by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
-by (split_tac [split_if] 1);
-by (blast_tac (claset() addSIs [InlI, InrI]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Inl_def, Inr_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Inl_def, Inr_def]) 2);
+by Auto_tac;
qed "Un_lepoll_sum";
Goal "[| well_ord(X,R); well_ord(Y,S) |] ==> EX T. well_ord(X Un Y, T)";
@@ -676,7 +676,7 @@
(*Krzysztof Grabczewski*)
Goalw [eqpoll_def] "A Int B = 0 ==> A Un B eqpoll A + B";
-by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
+by (res_inst_tac [("x","lam a:A Un B. if a:A then Inl(a) else Inr(a)")] exI 1);
by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
by Auto_tac;
qed "disj_Un_eqpoll_sum";
--- a/src/ZF/CardinalArith.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/CardinalArith.ML Thu Jan 07 10:56:05 1999 +0100
@@ -102,8 +102,8 @@
Goalw [eqpoll_def] "succ(A)+B eqpoll succ(A+B)";
by (rtac exI 1);
-by (res_inst_tac [("c", "%z. if(z=Inl(A),A+B,z)"),
- ("d", "%z. if(z=A+B,Inl(A),z)")]
+by (res_inst_tac [("c", "%z. if z=Inl(A) then A+B else z"),
+ ("d", "%z. if z=A+B then Inl(A) else z")]
lam_bijective 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [succI2, mem_imp_not_eq]
@@ -268,7 +268,7 @@
Goalw [eqpoll_def] "succ(A)*B eqpoll B + A*B";
by (rtac exI 1);
-by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"),
+by (res_inst_tac [("c", "%<x,y>. if x=A then Inl(y) else Inr(<x,y>)"),
("d", "case(%y. <A,y>, %z. z)")]
lam_bijective 1);
by Safe_tac;
@@ -315,17 +315,18 @@
(*** Infinite Cardinals are Limit Ordinals ***)
(*This proof is modelled upon one assuming nat<=A, with injection
- lam z:cons(u,A). if(z=u, 0, if(z : nat, succ(z), z)) and inverse
- %y. if(y:nat, nat_case(u,%z.z,y), y). If f: inj(nat,A) then
- range(f) behaves like the natural numbers.*)
-Goalw [lepoll_def]
- "nat lepoll A ==> cons(u,A) lepoll A";
+ lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z
+ and inverse %y. if y:nat then nat_case(u, %z. z, y) else y. \
+ If f: inj(nat,A) then range(f) behaves like the natural numbers.*)
+Goalw [lepoll_def] "nat lepoll A ==> cons(u,A) lepoll A";
by (etac exE 1);
by (res_inst_tac [("x",
- "lam z:cons(u,A). if(z=u, f`0, \
-\ if(z: range(f), f`succ(converse(f)`z), z))")] exI 1);
-by (res_inst_tac [("d", "%y. if(y: range(f), \
-\ nat_case(u, %z. f`z, converse(f)`y), y)")]
+ "lam z:cons(u,A). if z=u then f`0 \
+\ else if z: range(f) then f`succ(converse(f)`z) \
+\ else z")] exI 1);
+by (res_inst_tac [("d", "%y. if y: range(f) \
+\ then nat_case(u, %z. f`z, converse(f)`y) \
+\ else y")]
lam_injective 1);
by (fast_tac (claset() addSIs [if_type, apply_type]
addIs [inj_is_fun, inj_converse_fun]) 1);
--- a/src/ZF/Cardinal_AC.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Cardinal_AC.ML Thu Jan 07 10:56:05 1999 +0100
@@ -162,9 +162,8 @@
qed "lt_subset_trans";
(*Work backwards along the injection from W into K, given that W~=0.*)
-goal Perm.thy
- "!!A. [| f: inj(A,B); a:A |] ==> \
-\ (UN x:A. C(x)) <= (UN y:B. C(if(y: range(f), converse(f)`y, a)))";
+Goal "[| f: inj(A,B); a:A |] ==> \
+\ (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))";
by (rtac UN_least 1);
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
--- a/src/ZF/Coind/Map.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Coind/Map.ML Thu Jan 07 10:56:05 1999 +0100
@@ -33,7 +33,7 @@
(* Lemmas *)
(* ############################################################ *)
-Goal "Sigma(A,B)``{a} = if (a:A, B(a), 0)";
+Goal "Sigma(A,B)``{a} = (if a:A then B(a) else 0)";
by Auto_tac;
qed "qbeta_if";
@@ -194,7 +194,7 @@
(** Application **)
Goalw [map_app_def,map_owr_def]
- "map_app(map_owr(f,a,b),c) = if (c=a, b, map_app(f,c))";
+ "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))";
by (asm_simp_tac (simpset() addsimps [qbeta_if]) 1);
by (Fast_tac 1);
qed "map_app_owr";
--- a/src/ZF/Coind/Map.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Coind/Map.thy Thu Jan 07 10:56:05 1999 +0100
@@ -21,7 +21,8 @@
map_app :: [i,i]=>i
defs
map_emp_def "map_emp == 0"
- map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
+ map_owr_def "map_owr(m,a,b) ==
+ SUM x:{a} Un domain(m). if x=a then b else m``{x}"
map_app_def "map_app(m,a) == m``{a}"
end
--- a/src/ZF/Coind/Types.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Coind/Types.thy Thu Jan 07 10:56:05 1999 +0100
@@ -33,7 +33,7 @@
primrec (*lookup up identifiers in the type environment*)
"te_app (te_emp,x) = 0"
- "te_app (te_owr(te,y,t),x) = if(x=y, t, te_app(te,x))"
+ "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
end
--- a/src/ZF/Coind/Values.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Coind/Values.ML Thu Jan 07 10:56:05 1999 +0100
@@ -92,7 +92,8 @@
by (rtac Un_commute 1);
qed "ve_dom_owr";
-Goal "ve:ValEnv ==> ve_app(ve_owr(ve,y,v),x) = if(x=y, v, ve_app(ve,x))";
+Goal "ve:ValEnv \
+\ ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))";
by (etac ValEnvE 1);
by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
qed "ve_app_owr";
--- a/src/ZF/OrderArith.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/OrderArith.ML Thu Jan 07 10:56:05 1999 +0100
@@ -132,7 +132,7 @@
ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
Goal "A Int B = 0 ==> \
\ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
-by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")]
+by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")]
lam_bijective 1);
by (blast_tac (claset() addSIs [if_type]) 2);
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
--- a/src/ZF/Perm.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Perm.ML Thu Jan 07 10:56:05 1999 +0100
@@ -463,8 +463,8 @@
(*Theorem by KG, proof by LCP*)
Goal "[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] \
-\ ==> (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
-by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
+\ ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)";
+by (res_inst_tac [("d","%z. if z:B then converse(f)`z else converse(g)`z")]
lam_injective 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
--- a/src/ZF/Resid/Substitution.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Resid/Substitution.ML Thu Jan 07 10:56:05 1999 +0100
@@ -10,25 +10,25 @@
(* ------------------------------------------------------------------------- *)
goal Arith.thy
- "!!m.[| p < n; n:nat|]==> n~=p";
+ "!!m.[| p < n; n:nat|] ==> n~=p";
by (Fast_tac 1);
qed "gt_not_eq";
val succ_pred = prove_goal Arith.thy
- "!!i.[|j:nat; i:nat|]==> i < j --> succ(j #- 1) = j"
+ "!!i.[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j"
(fn prems =>[(etac nat_induct 1),
(Fast_tac 1),
(Asm_simp_tac 1)]);
goal Arith.thy
- "!!i.[|succ(x)<n; n:nat; x:nat|]==> x < n #- 1 ";
+ "!!i.[|succ(x)<n; n:nat; x:nat|] ==> x < n #- 1 ";
by (rtac succ_leE 1);
by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
qed "lt_pred";
goal Arith.thy
- "!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|]==> n #- 1 < x ";
+ "!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|] ==> n #- 1 < x ";
by (rtac succ_leE 1);
by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
qed "gt_pred";
@@ -40,24 +40,25 @@
(* ------------------------------------------------------------------------- *)
(* lift_rec equality rules *)
(* ------------------------------------------------------------------------- *)
-Goal "[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
+Goal "[|n:nat; i:nat|] \
+\ ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_Var";
-Goal "[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
+Goal "[|n:nat; i:nat; k:nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_le";
-Goal "[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
+Goal "[|i:nat; k:nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_gt";
-Goal "[|n:nat; k:nat|]==> \
+Goal "[|n:nat; k:nat|] ==> \
\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_Fun";
-Goal "[|n:nat; k:nat|]==> \
+Goal "[|n:nat; k:nat|] ==> \
\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_App";
@@ -67,31 +68,32 @@
(* substitution quality rules *)
(* ------------------------------------------------------------------------- *)
-Goal "[|i:nat; k:nat; u:redexes|]==> \
-\ subst_rec(u,Var(i),k) = if(k<i,Var(i #- 1),if(k=i,u,Var(i)))";
+Goal "[|i:nat; k:nat; u:redexes|] \
+\ ==> subst_rec(u,Var(i),k) = \
+\ (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
qed "subst_Var";
-Goal "[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
+Goal "[|n:nat; u:redexes|] ==> subst_rec(u,Var(n),n) = u";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_eq";
-Goal "[|n:nat; u:redexes; p:nat; p<n|]==> \
+Goal "[|n:nat; u:redexes; p:nat; p<n|] ==> \
\ subst_rec(u,Var(n),p) = Var(n #- 1)";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_gt";
-Goal "[|n:nat; u:redexes; p:nat; n<p|]==> \
+Goal "[|n:nat; u:redexes; p:nat; n<p|] ==> \
\ subst_rec(u,Var(n),p) = Var(n)";
by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
qed "subst_lt";
-Goal "[|p:nat; u:redexes|]==> \
+Goal "[|p:nat; u:redexes|] ==> \
\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_Fun";
-Goal "[|p:nat; u:redexes|]==> \
+Goal "[|p:nat; u:redexes|] ==> \
\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_App";
@@ -133,7 +135,7 @@
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
qed "lift_lift_rec";
-Goal "[|u:redexes; n:nat|]==> \
+Goal "[|u:redexes; n:nat|] ==> \
\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
qed "lift_lift";
@@ -158,7 +160,7 @@
by (asm_simp_tac (simpset() addsimps [leI]) 1);
qed "lift_rec_subst_rec";
-Goal "[|v:redexes; u:redexes; n:nat|]==> \
+Goal "[|v:redexes; u:redexes; n:nat|] ==> \
\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
qed "lift_subst";
@@ -221,7 +223,7 @@
qed "subst_rec_subst_rec";
-Goal "[|v:redexes; u:redexes; w:redexes; n:nat|]==> \
+Goal "[|v:redexes; u:redexes; w:redexes; n:nat|] ==> \
\ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
qed "substitution";
@@ -232,7 +234,7 @@
(* ------------------------------------------------------------------------- *)
-Goal "[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)";
+Goal "[|n:nat; u ~ v|] ==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
qed "lift_rec_preserve_comp";
--- a/src/ZF/Resid/Substitution.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Resid/Substitution.thy Thu Jan 07 10:56:05 1999 +0100
@@ -17,7 +17,7 @@
lift_rec :: [i,i]=> i
"lift_rec(r,k) == lift_aux(r)`k"
- subst_rec :: [i,i,i]=> i
+ subst_rec :: [i,i,i]=> i (**NOTE THE ARGUMENT ORDER BELOW**)
"subst_rec(u,r,k) == subst_aux(r)`u`k"
translations
@@ -29,7 +29,7 @@
in the recursive calls ***)
primrec
- "lift_aux(Var(i)) = (lam k:nat. if(i<k, Var(i), Var(succ(i))))"
+ "lift_aux(Var(i)) = (lam k:nat. if i<k then Var(i) else Var(succ(i)))"
"lift_aux(Fun(t)) = (lam k:nat. Fun(lift_aux(t) ` succ(k)))"
@@ -38,17 +38,9 @@
primrec
-(* subst_aux(u,Var(i),k) = if k<i then Var(i-1)
- else if k=i then u
- else Var(i)
- subst_aux(u,Fun(t),k) = Fun(subst_aux(lift(u),t,succ(k)))
- subst_aux(u,App(b,f,a),k) = App(b,subst_aux(u,f,p),subst_aux(u,a,p))
-
-*)
-
"subst_aux(Var(i)) =
- (lam r:redexes. lam k:nat. if(k<i, Var(i #- 1),
- if(k=i, r, Var(i))))"
+ (lam r:redexes. lam k:nat. if k<i then Var(i #- 1)
+ else if k=i then r else Var(i))"
"subst_aux(Fun(t)) =
(lam r:redexes. lam k:nat. Fun(subst_rec(lift(r), t, succ(k))))"
--- a/src/ZF/Update.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/Update.ML Thu Jan 07 10:56:05 1999 +0100
@@ -8,7 +8,7 @@
open Update;
-Goal "f(x:=y) ` z = if(z=x, y, f`z)";
+Goal "f(x:=y) ` z = (if z=x then y else f`z)";
by (simp_tac (simpset() addsimps [update_def]) 1);
by (case_tac "z : domain(f)" 1);
by (Asm_simp_tac 1);
--- a/src/ZF/ZF.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/ZF.thy Thu Jan 07 10:56:05 1999 +0100
@@ -40,8 +40,16 @@
(* Descriptions *)
The :: (i => o) => i (binder "THE " 10)
- if :: [o, i, i] => i
+ If :: [o, i, i] => i ("(if (_)/ then (_)/ else (_))" [10] 10)
+
+syntax
+ old_if :: [o, i, i] => i ("if '(_,_,_')")
+translations
+ "if(P,a,b)" => "If(P,a,b)"
+
+
+consts
(* Finite Sets *)
Upair, cons :: [i, i] => i
--- a/src/ZF/equalities.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/equalities.ML Thu Jan 07 10:56:05 1999 +0100
@@ -602,7 +602,8 @@
by (Blast_tac 1);
qed "Collect_Diff";
-Goal "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
+Goal "{x:cons(a,B). P(x)} = \
+\ (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})";
by (simp_tac (simpset() addsplits [split_if]) 1);
by (Blast_tac 1);
qed "Collect_cons";
--- a/src/ZF/ex/Mutil.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/ex/Mutil.ML Thu Jan 07 10:56:05 1999 +0100
@@ -32,7 +32,7 @@
Goalw [evnodd_def]
"evnodd(cons(<i,j>,C), b) = \
-\ if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))";
+\ (if (i#+j) mod 2 = b then cons(<i,j>, evnodd(C,b)) else evnodd(C,b))";
by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1);
qed "evnodd_cons";
--- a/src/ZF/ex/PropLog.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/ex/PropLog.ML Thu Jan 07 10:56:05 1999 +0100
@@ -126,7 +126,7 @@
qed "Imp_Fls";
(*Typical example of strengthening the induction formula*)
-Goal "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
+Goal "p: prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)";
by (Simp_tac 1);
by (etac prop.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
--- a/src/ZF/ex/PropLog.thy Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/ex/PropLog.thy Thu Jan 07 10:56:05 1999 +0100
@@ -56,12 +56,13 @@
primrec (** A finite set of hypotheses from t and the Vars in p **)
"hyps(Fls, t) = 0"
- "hyps(Var(v), t) = if(v:t, {#v}, {#v=>Fls})"
+ "hyps(Var(v), t) = (if v:t then {#v} else {#v=>Fls})"
"hyps(p=>q, t) = hyps(p,t) Un hyps(q,t)"
primrec (** Semantics of propositional logic **)
"is_true_fun(Fls, t) = 0"
- "is_true_fun(Var(v), t) = if(v:t, 1, 0)"
- "is_true_fun(p=>q, t) = if(is_true_fun(p,t)=1, is_true_fun(q,t), 1)"
+ "is_true_fun(Var(v), t) = (if v:t then 1 else 0)"
+ "is_true_fun(p=>q, t) = (if is_true_fun(p,t)=1 then is_true_fun(q,t)
+ else 1)"
end
--- a/src/ZF/upair.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/upair.ML Thu Jan 07 10:56:05 1999 +0100
@@ -234,34 +234,35 @@
(*** if -- a conditional expression for formulae ***)
-Goalw [if_def] "if(True,a,b) = a";
+Goalw [if_def] "(if True then a else b) = a";
by (Blast_tac 1);
qed "if_true";
-Goalw [if_def] "if(False,a,b) = b";
+Goalw [if_def] "(if False then a else b) = b";
by (Blast_tac 1);
qed "if_false";
(*Never use with case splitting, or if P is known to be true or false*)
val prems = Goalw [if_def]
- "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
+ "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] \
+\ ==> (if P then a else b) = (if Q then c else d)";
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
qed "if_cong";
(*Not needed for rewriting, since P would rewrite to True anyway*)
-Goalw [if_def] "P ==> if(P,a,b) = a";
+Goalw [if_def] "P ==> (if P then a else b) = a";
by (Blast_tac 1);
qed "if_P";
(*Not needed for rewriting, since P would rewrite to False anyway*)
-Goalw [if_def] "~P ==> if(P,a,b) = b";
+Goalw [if_def] "~P ==> (if P then a else b) = b";
by (Blast_tac 1);
qed "if_not_P";
Addsimps [if_true, if_false];
qed_goal "split_if" thy
- "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
+ "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (case_tac "Q" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1) ]);
@@ -280,11 +281,11 @@
split_if_mem1, split_if_mem2];
(*Logically equivalent to split_if_mem2*)
-qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
+qed_goal "if_iff" thy "a: (if P then x else y) <-> P & a:x | ~P & a:y"
(fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
qed_goal "if_type" thy
- "[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A"
+ "[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A"
(fn prems=> [ (simp_tac
(simpset() addsimps prems addsplits [split_if]) 1) ]);