# HG changeset patch
# User clasohm
# Date 795710128 -3600
# Node ID 24eef3860714dd91e3e969fe2d2dbb64bc171e8f
# Parent  5f690b184f916937d47d39144a1921c411f54643
changed syntax of "if"

diff -r 5f690b184f91 -r 24eef3860714 src/HOL/Arith.ML
--- 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";
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/Arith.thy
--- 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.
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/HOL.thy
--- 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
 
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/IMP/Com.thy
--- 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
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/List.thy
--- 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"
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/Ord.thy
--- 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
 
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/WF.thy
--- 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)"
 
diff -r 5f690b184f91 -r 24eef3860714 src/HOL/simpdata.ML
--- 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*)