Added > and >= sugar
authornipkow
Wed Dec 01 18:11:13 2004 +0100 (2004-12-01)
changeset 153549234f5765d9c
parent 15353 b53b89d3bf03
child 15355 0de05d104060
Added > and >= sugar
src/HOL/HOL.thy
src/HOL/IMPP/EvenOdd.ML
src/HOL/IMPP/EvenOdd.thy
src/HOL/IMPP/Misc.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Dec 01 18:10:49 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 01 18:11:13 2004 +0100
     1.3 @@ -343,10 +343,10 @@
     1.4  
     1.5  lemma simp_thms:
     1.6    shows not_not: "(~ ~ P) = P"
     1.7 +  and Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
     1.8    and
     1.9      "(P ~= Q) = (P = (~Q))"
    1.10      "(P | ~P) = True"    "(~P | P) = True"
    1.11 -    "((~P) = (~Q)) = (P=Q)"
    1.12      "(x = x) = True"
    1.13      "(~True) = False"  "(~False) = True"
    1.14      "(~P) ~= P"  "P ~= (~P)"
    1.15 @@ -660,9 +660,21 @@
    1.16    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    1.17    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    1.18  
    1.19 +text{* Syntactic sugar: *}
    1.20  
    1.21 -lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
    1.22 -by blast
    1.23 +consts
    1.24 +  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    1.25 +  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    1.26 +translations
    1.27 +  "x > y"  => "y < x"
    1.28 +  "x >= y" => "y <= x"
    1.29 +
    1.30 +syntax (xsymbols)
    1.31 +  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
    1.32 +
    1.33 +syntax (HTML output)
    1.34 +  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
    1.35 +
    1.36  
    1.37  subsubsection {* Monotonicity *}
    1.38  
     2.1 --- a/src/HOL/IMPP/EvenOdd.ML	Wed Dec 01 18:10:49 2004 +0100
     2.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Wed Dec 01 18:11:13 2004 +0100
     2.3 @@ -77,7 +77,7 @@
     2.4  by  (force_tac Arg_Res_css 1);
     2.5  by (rtac export_s 1);
     2.6  by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
     2.7 -		  ("Q1","%Z s. even Z = (s<Arg>=0)")]
     2.8 +		  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
     2.9  		 (Call_invariant RS conseq12) 1);
    2.10  by (rtac (single_asm RS conseq2) 1);
    2.11  by  (clarsimp_tac Arg_Res_css 1);
     3.1 --- a/src/HOL/IMPP/EvenOdd.thy	Wed Dec 01 18:10:49 2004 +0100
     3.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Wed Dec 01 18:11:13 2004 +0100
     3.3 @@ -19,13 +19,13 @@
     3.4  
     3.5  constdefs
     3.6    evn :: com
     3.7 - "evn == IF (%s. s<Arg>=0)
     3.8 + "evn == IF (%s. s<Arg> = 0)
     3.9           THEN Loc Res:==(%s. 0)
    3.10           ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
    3.11                Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
    3.12                Loc Res:==(%s. s<Res> * s<Arg>))"
    3.13    odd :: com
    3.14 - "odd == IF (%s. s<Arg>=0)
    3.15 + "odd == IF (%s. s<Arg> = 0)
    3.16           THEN Loc Res:==(%s. 1)
    3.17           ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
    3.18  
    3.19 @@ -37,6 +37,6 @@
    3.20   "even_Z=(Res=0)" ::        nat assn ("Res'_ok")
    3.21  defs
    3.22    Z_eq_Arg_plus_def "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
    3.23 -  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res>=0)"
    3.24 +  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
    3.25  
    3.26  end
     4.1 --- a/src/HOL/IMPP/Misc.ML	Wed Dec 01 18:10:49 2004 +0100
     4.2 +++ b/src/HOL/IMPP/Misc.ML	Wed Dec 01 18:11:13 2004 +0100
     4.3 @@ -82,8 +82,8 @@
     4.4  *)
     4.5  qed "classic_Local";
     4.6  
     4.7 -Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
     4.8 -\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
     4.9 +Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
    4.10 +\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
    4.11  by (rtac classic_Local 1);
    4.12  by (ALLGOALS Clarsimp_tac);
    4.13  by (etac conseq12 1);
    4.14 @@ -92,15 +92,15 @@
    4.15  by (Asm_full_simp_tac 1);
    4.16  qed "classic_Local_indep";
    4.17  
    4.18 -Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
    4.19 -\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
    4.20 +Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
    4.21 +\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
    4.22  by (rtac export_s 1);
    4.23  by (rtac hoare_derivs.Local 1);
    4.24  by (Clarsimp_tac 1);
    4.25  qed "Local_indep";
    4.26  
    4.27 -Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
    4.28 -\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
    4.29 +Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
    4.30 +\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
    4.31  by (rtac weak_Local 1);
    4.32  by (ALLGOALS Clarsimp_tac);
    4.33  qed "weak_Local_indep";