changed syntax of "if"
authorclasohm
Mon Mar 20 15:35:28 1995 +0100 (1995-03-20)
changeset 96524eef3860714
parent 964 5f690b184f91
child 966 3fd66f245ad7
changed syntax of "if"
src/HOL/Arith.ML
src/HOL/Arith.thy
src/HOL/HOL.thy
src/HOL/IMP/Com.thy
src/HOL/List.thy
src/HOL/Ord.thy
src/HOL/WF.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Mar 17 22:46:26 1995 +0100
     1.2 +++ b/src/HOL/Arith.ML	Mon Mar 20 15:35:28 1995 +0100
     1.3 @@ -241,7 +241,7 @@
     1.4  by (ALLGOALS(asm_simp_tac arith_ss));
     1.5  qed "Suc_diff_n";
     1.6  
     1.7 -goal Arith.thy "Suc(m)-n = if (m<n) 0 (Suc m-n)";
     1.8 +goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)";
     1.9  by(simp_tac (nat_ss addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
    1.10                      setloop (split_tac [expand_if])) 1);
    1.11  qed "if_Suc_diff_n";
     2.1 --- a/src/HOL/Arith.thy	Fri Mar 17 22:46:26 1995 +0100
     2.2 +++ b/src/HOL/Arith.thy	Mon Mar 20 15:35:28 1995 +0100
     2.3 @@ -20,8 +20,8 @@
     2.4    add_def   "m+n == nat_rec m n (%u v. Suc(v))"
     2.5    diff_def  "m-n == nat_rec n m (%u v. pred(v))"
     2.6    mult_def  "m*n == nat_rec m 0 (%u v. n + v)"
     2.7 -  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.(if (j<n) j (f (j-n))))"
     2.8 -  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.(if (j<n) 0 (Suc (f (j-n)))))"
     2.9 +  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
    2.10 +  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
    2.11  end
    2.12  
    2.13  (*"Difference" is subtraction of natural numbers.
     3.1 --- a/src/HOL/HOL.thy	Fri Mar 17 22:46:26 1995 +0100
     3.2 +++ b/src/HOL/HOL.thy	Mon Mar 20 15:35:28 1995 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4    Trueprop      :: "bool => prop"                     ("(_)" 5)
     3.5    not           :: "bool => bool"                     ("~ _" [40] 40)
     3.6    True, False   :: "bool"
     3.7 -  if            :: "[bool, 'a, 'a] => 'a"
     3.8 +  If            :: "[bool, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
     3.9    Inv           :: "('a => 'b) => ('b => 'a)"
    3.10  
    3.11    (* Binders *)
    3.12 @@ -139,7 +139,7 @@
    3.13    Let_def       "Let s f == f(s)"
    3.14    Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
    3.15    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    3.16 -  if_def        "if P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    3.17 +  if_def   "if P then x else y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    3.18  
    3.19  end
    3.20  
     4.1 --- a/src/HOL/IMP/Com.thy	Fri Mar 17 22:46:26 1995 +0100
     4.2 +++ b/src/HOL/IMP/Com.thy	Mon Mar 20 15:35:28 1995 +0100
     4.3 @@ -86,7 +86,7 @@
     4.4         "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
     4.5  
     4.6  rules 
     4.7 -	assign_def	"s[m/x] == (%y. if (y=x) m (s y))"
     4.8 +	assign_def	"s[m/x] == (%y. if y=x then m else s y)"
     4.9  
    4.10  inductive "evalc"
    4.11    intrs
     5.1 --- a/src/HOL/List.thy	Fri Mar 17 22:46:26 1995 +0100
     5.2 +++ b/src/HOL/List.thy	Mon Mar 20 15:35:28 1995 +0100
     5.3 @@ -56,7 +56,7 @@
     5.4    ttl_Cons "ttl(x#xs) = xs"
     5.5  primrec "op mem" list
     5.6    mem_Nil  "x mem [] = False"
     5.7 -  mem_Cons "x mem (y#ys) = if (y=x) True (x mem ys)"
     5.8 +  mem_Cons "x mem (y#ys) = (if y=x then True else x mem ys)"
     5.9  primrec list_all list
    5.10    list_all_Nil  "list_all P [] = True"
    5.11    list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
    5.12 @@ -68,7 +68,7 @@
    5.13    append_Cons "(x#xs)@ys = x#(xs@ys)"
    5.14  primrec filter list
    5.15    filter_Nil  "filter P [] = []"
    5.16 -  filter_Cons "filter P (x#xs) = if (P x) (x#filter P xs) (filter P xs)"
    5.17 +  filter_Cons "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
    5.18  primrec foldl list
    5.19    foldl_Nil  "foldl f a [] = a"
    5.20    foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
     6.1 --- a/src/HOL/Ord.thy	Fri Mar 17 22:46:26 1995 +0100
     6.2 +++ b/src/HOL/Ord.thy	Mon Mar 20 15:35:28 1995 +0100
     6.3 @@ -18,8 +18,8 @@
     6.4  
     6.5  defs
     6.6    mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
     6.7 -  min_def       "min a b == if (a <= b) a b"
     6.8 -  max_def       "max a b == if (a <= b) b a"
     6.9 +  min_def       "min a b == (if a <= b then a else b)"
    6.10 +  max_def       "max a b == (if a <= b then b else a)"
    6.11  
    6.12  end
    6.13  
     7.1 --- a/src/HOL/WF.thy	Fri Mar 17 22:46:26 1995 +0100
     7.2 +++ b/src/HOL/WF.thy	Mon Mar 20 15:35:28 1995 +0100
     7.3 @@ -17,7 +17,7 @@
     7.4  defs
     7.5    wf_def  "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
     7.6    
     7.7 -  cut_def 	 "cut f r x == (%y. if (<y,x>:r) (f y) (@z.True))"
     7.8 +  cut_def 	 "cut f r x == (%y. if <y,x>:r then f y else @z.True)"
     7.9  
    7.10    is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
    7.11  
     8.1 --- a/src/HOL/simpdata.ML	Fri Mar 17 22:46:26 1995 +0100
     8.2 +++ b/src/HOL/simpdata.ML	Mon Mar 20 15:35:28 1995 +0100
     8.3 @@ -71,27 +71,28 @@
     8.4  
     8.5  val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
     8.6  
     8.7 -val if_True = prove_goalw HOL.thy [if_def] "if True x y = x"
     8.8 +val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x"
     8.9   (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    8.10  
    8.11 -val if_False = prove_goalw HOL.thy [if_def] "if False x y = y"
    8.12 +val if_False = prove_goalw HOL.thy [if_def] "(if False then x else y) = y"
    8.13   (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    8.14  
    8.15 -val if_P = prove_goal HOL.thy "P ==> if P x y = x"
    8.16 +val if_P = prove_goal HOL.thy "P ==> (if P then x else y) = x"
    8.17   (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
    8.18  
    8.19 -val if_not_P = prove_goal HOL.thy "~P ==> if P x y = y"
    8.20 +val if_not_P = prove_goal HOL.thy "~P ==> (if P then x else y) = y"
    8.21   (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
    8.22  
    8.23  val expand_if = prove_goal HOL.thy
    8.24 -    "P(if Q x y) = ((Q --> P(x)) & (~Q --> P(y)))"
    8.25 +    "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
    8.26   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
    8.27  	 rtac (if_P RS ssubst) 2,
    8.28  	 rtac (if_not_P RS ssubst) 1,
    8.29  	 REPEAT(fast_tac HOL_cs 1) ]);
    8.30  
    8.31 -val if_bool_eq = prove_goal HOL.thy "if P Q R = ((P-->Q) & (~P-->R))"
    8.32 -  (fn _ => [rtac expand_if 1]);
    8.33 +val if_bool_eq = prove_goal HOL.thy
    8.34 +                   "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    8.35 +                   (fn _ => [rtac expand_if 1]);
    8.36  
    8.37  infix addcongs;
    8.38  fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    8.39 @@ -99,7 +100,7 @@
    8.40  val mksimps_pairs =
    8.41    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    8.42     ("All", [spec]), ("True", []), ("False", []),
    8.43 -   ("if", [if_bool_eq RS iffD1])];
    8.44 +   ("If", [if_bool_eq RS iffD1])];
    8.45  
    8.46  fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
    8.47  
    8.48 @@ -139,14 +140,15 @@
    8.49  
    8.50  (*Simplifies x assuming c and y assuming ~c*)
    8.51  val if_cong = prove_goal HOL.thy
    8.52 -  "[| b=c; c ==> x=u; ~c ==> y=v |] ==> if b x y = if c u v"
    8.53 +  "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
    8.54 +\  (if b then x else y) = (if c then u else v)"
    8.55    (fn rew::prems =>
    8.56     [stac rew 1, stac expand_if 1, stac expand_if 1,
    8.57      fast_tac (HOL_cs addDs prems) 1]);
    8.58  
    8.59  (*Prevents simplification of x and y: much faster*)
    8.60  val if_weak_cong = prove_goal HOL.thy
    8.61 -  "b=c ==> if b x y = if c x y"
    8.62 +  "b=c ==> (if b then x else y) = (if c then x else y)"
    8.63    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    8.64  
    8.65  (*Prevents simplification of t: much faster*)