--- a/src/HOL/Arith.ML Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/Arith.ML Mon Mar 20 15:35:28 1995 +0100
@@ -241,7 +241,7 @@
by (ALLGOALS(asm_simp_tac arith_ss));
qed "Suc_diff_n";
-goal Arith.thy "Suc(m)-n = if (m<n) 0 (Suc m-n)";
+goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)";
by(simp_tac (nat_ss addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
setloop (split_tac [expand_if])) 1);
qed "if_Suc_diff_n";
--- a/src/HOL/Arith.thy Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/Arith.thy Mon Mar 20 15:35:28 1995 +0100
@@ -20,8 +20,8 @@
add_def "m+n == nat_rec m n (%u v. Suc(v))"
diff_def "m-n == nat_rec n m (%u v. pred(v))"
mult_def "m*n == nat_rec m 0 (%u v. n + v)"
- mod_def "m mod n == wfrec (trancl pred_nat) m (%j f.(if (j<n) j (f (j-n))))"
- div_def "m div n == wfrec (trancl pred_nat) m (%j f.(if (j<n) 0 (Suc (f (j-n)))))"
+ mod_def "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
+ div_def "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
end
(*"Difference" is subtraction of natural numbers.
--- a/src/HOL/HOL.thy Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/HOL.thy Mon Mar 20 15:35:28 1995 +0100
@@ -38,7 +38,7 @@
Trueprop :: "bool => prop" ("(_)" 5)
not :: "bool => bool" ("~ _" [40] 40)
True, False :: "bool"
- if :: "[bool, 'a, 'a] => 'a"
+ If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
Inv :: "('a => 'b) => ('b => 'a)"
(* Binders *)
@@ -139,7 +139,7 @@
Let_def "Let s f == f(s)"
Inv_def "Inv(f::'a=>'b) == (% y. @x. f(x)=y)"
o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
- if_def "if P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
+ if_def "if P then x else y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
end
--- a/src/HOL/IMP/Com.thy Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/IMP/Com.thy Mon Mar 20 15:35:28 1995 +0100
@@ -86,7 +86,7 @@
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
rules
- assign_def "s[m/x] == (%y. if (y=x) m (s y))"
+ assign_def "s[m/x] == (%y. if y=x then m else s y)"
inductive "evalc"
intrs
--- a/src/HOL/List.thy Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/List.thy Mon Mar 20 15:35:28 1995 +0100
@@ -56,7 +56,7 @@
ttl_Cons "ttl(x#xs) = xs"
primrec "op mem" list
mem_Nil "x mem [] = False"
- mem_Cons "x mem (y#ys) = if (y=x) True (x mem ys)"
+ mem_Cons "x mem (y#ys) = (if y=x then True else x mem ys)"
primrec list_all list
list_all_Nil "list_all P [] = True"
list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
@@ -68,7 +68,7 @@
append_Cons "(x#xs)@ys = x#(xs@ys)"
primrec filter list
filter_Nil "filter P [] = []"
- filter_Cons "filter P (x#xs) = if (P x) (x#filter P xs) (filter P xs)"
+ filter_Cons "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
primrec foldl list
foldl_Nil "foldl f a [] = a"
foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
--- a/src/HOL/Ord.thy Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/Ord.thy Mon Mar 20 15:35:28 1995 +0100
@@ -18,8 +18,8 @@
defs
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
- min_def "min a b == if (a <= b) a b"
- max_def "max a b == if (a <= b) b a"
+ min_def "min a b == (if a <= b then a else b)"
+ max_def "max a b == (if a <= b then b else a)"
end
--- a/src/HOL/WF.thy Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/WF.thy Mon Mar 20 15:35:28 1995 +0100
@@ -17,7 +17,7 @@
defs
wf_def "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
- cut_def "cut f r x == (%y. if (<y,x>:r) (f y) (@z.True))"
+ cut_def "cut f r x == (%y. if <y,x>:r then f y else @z.True)"
is_recfun_def "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
--- a/src/HOL/simpdata.ML Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/simpdata.ML Mon Mar 20 15:35:28 1995 +0100
@@ -71,27 +71,28 @@
val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
-val if_True = prove_goalw HOL.thy [if_def] "if True x y = x"
+val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x"
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
-val if_False = prove_goalw HOL.thy [if_def] "if False x y = y"
+val if_False = prove_goalw HOL.thy [if_def] "(if False then x else y) = y"
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
-val if_P = prove_goal HOL.thy "P ==> if P x y = x"
+val if_P = prove_goal HOL.thy "P ==> (if P then x else y) = x"
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
-val if_not_P = prove_goal HOL.thy "~P ==> if P x y = y"
+val if_not_P = prove_goal HOL.thy "~P ==> (if P then x else y) = y"
(fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
val expand_if = prove_goal HOL.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 _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
rtac (if_P RS ssubst) 2,
rtac (if_not_P RS ssubst) 1,
REPEAT(fast_tac HOL_cs 1) ]);
-val if_bool_eq = prove_goal HOL.thy "if P Q R = ((P-->Q) & (~P-->R))"
- (fn _ => [rtac expand_if 1]);
+val if_bool_eq = prove_goal HOL.thy
+ "(if P then Q else R) = ((P-->Q) & (~P-->R))"
+ (fn _ => [rtac expand_if 1]);
infix addcongs;
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
@@ -99,7 +100,7 @@
val mksimps_pairs =
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
("All", [spec]), ("True", []), ("False", []),
- ("if", [if_bool_eq RS iffD1])];
+ ("If", [if_bool_eq RS iffD1])];
fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
@@ -139,14 +140,15 @@
(*Simplifies x assuming c and y assuming ~c*)
val if_cong = prove_goal HOL.thy
- "[| b=c; c ==> x=u; ~c ==> y=v |] ==> if b x y = if c u v"
+ "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
+\ (if b then x else y) = (if c then u else v)"
(fn rew::prems =>
[stac rew 1, stac expand_if 1, stac expand_if 1,
fast_tac (HOL_cs addDs prems) 1]);
(*Prevents simplification of x and y: much faster*)
val if_weak_cong = prove_goal HOL.thy
- "b=c ==> if b x y = if c x y"
+ "b=c ==> (if b then x else y) = (if c then x else y)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
(*Prevents simplification of t: much faster*)