# HG changeset patch # User paulson # Date 915702965 -3600 # Node ID 2d8f3e1f1151e87269f7682d573cb9cd06a39783 # Parent 0f8ab32093ae088c0e29a7b2bcb8d3660606f492 if-then-else syntax for ZF diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/AC/WO1_WO6.ML --- 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 diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/AC/WO2_AC16.ML --- 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); diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/AC/WO6_WO1.thy --- 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 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 (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 (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})"; by (rtac transrec2_succ 1); qed "recfunAC16_succ"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Arith.ML --- 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 \ -\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))"; +Goal "[| 0 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) 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); diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Cardinal.ML --- 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"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/CardinalArith.ML --- 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", "%. if(x=A, Inl(y), Inr())"), +by (res_inst_tac [("c", "%. if x=A then Inl(y) else Inr()"), ("d", "case(%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); diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Cardinal_AC.ML --- 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); diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Coind/Map.ML --- 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"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Coind/Map.thy --- 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 diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Coind/Types.thy --- 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 diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Coind/Values.ML --- 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"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/OrderArith.ML --- 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)); diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Perm.ML --- 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] diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Resid/Substitution.ML --- 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) x < n #- 1 "; + "!!i.[|succ(x) 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 #- 1 < x "; + "!!i.[|n < succ(x); p 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 lift_rec(Var(i),n) = (if 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 lift_rec(Var(i),k) = Var(i)"; +Goal "[|i:nat; k:nat; i 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 subst_rec(u,Var(i),k) = \ +\ (if k 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 \ +Goal "[|n:nat; u:redexes; p:nat; p \ \ 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 \ +Goal "[|n:nat; u:redexes; p:nat; n \ \ 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"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/Resid/Substitution.thy --- 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 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 diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/equalities.ML --- 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"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/ex/Mutil.ML --- 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(,C), b) = \ -\ if((i#+j) mod 2 = b, cons(, evnodd(C,b)), evnodd(C,b))"; +\ (if (i#+j) mod 2 = b then cons(, evnodd(C,b)) else evnodd(C,b))"; by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1); qed "evnodd_cons"; diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/ex/PropLog.ML --- 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]))); diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/ex/PropLog.thy --- 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 diff -r 0f8ab32093ae -r 2d8f3e1f1151 src/ZF/upair.ML --- 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) ]);