# HG changeset patch
# User huffman
# Date 1288214154 25200
# Node ID 707eb30e8a53f5d2d84261954a0ffeef693629af
# Parent  d065b195ec8962de6ca875196f1624702ba8a61a
make syntax of continuous if-then-else consistent with HOL if-then-else

diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -150,12 +150,12 @@
 definition
   match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_TT = (\<Lambda> x k. If x then k else fail fi)"
+  "match_TT = (\<Lambda> x k. If x then k else fail)"
  
 definition
   match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_FF = (\<Lambda> x k. If x then fail else k fi)"
+  "match_FF = (\<Lambda> x k. If x then fail else k)"
 
 lemma match_UU_simps [simp]:
   "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -39,7 +39,7 @@
     | x##xs => (flift1
             (%p.(If Def ((fst p)~:actions sig)
                  then Def (s=(snd p))
-                 else TT fi)
+                 else TT)
                 andalso (h$xs) (snd p))
              $x)
    )))"
@@ -137,7 +137,7 @@
      | x##xs => (flift1
              (%p.(If Def ((fst p)~:actions sig)
                   then Def (s=(snd p))
-                  else TT fi)
+                  else TT)
                  andalso (stutter2 sig$xs) (snd p))
               $x)
             ))"
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -70,7 +70,7 @@
   sfilter_nil: "sfilter$P$nil=nil"
 | sfilter_cons:
     "x~=UU ==> sfilter$P$(x##xs)=
-              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
+              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
 
 lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
 by fixrec_simp
@@ -98,7 +98,7 @@
   stakewhile_nil: "stakewhile$P$nil=nil"
 | stakewhile_cons:
     "x~=UU ==> stakewhile$P$(x##xs) =
-              (If P$x then x##(stakewhile$P$xs) else nil fi)"
+              (If P$x then x##(stakewhile$P$xs) else nil)"
 
 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
 by fixrec_simp
@@ -111,7 +111,7 @@
   sdropwhile_nil: "sdropwhile$P$nil=nil"
 | sdropwhile_cons:
     "x~=UU ==> sdropwhile$P$(x##xs) =
-              (If P$x then sdropwhile$P$xs else x##xs fi)"
+              (If P$x then sdropwhile$P$xs else x##xs)"
 
 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
 by fixrec_simp
@@ -123,7 +123,7 @@
 where
   slast_nil: "slast$nil=UU"
 | slast_cons:
-    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
+    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
 
 lemma slast_UU [simp]: "slast$UU=UU"
 by fixrec_simp
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/Library/Stream.thy
--- a/src/HOLCF/Library/Stream.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/Library/Stream.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -17,7 +17,7 @@
 definition
   sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream" where
   "sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
-                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
+                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs)"
 
 definition
   slen :: "'a stream \<Rightarrow> inat"  ("#_" [1000] 1000) where
@@ -504,7 +504,7 @@
 
 lemma sfilter_unfold:
  "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
-  If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
+  If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs)"
 by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
@@ -518,7 +518,7 @@
 
 lemma sfilter_scons [simp]:
   "x ~= \<bottom> ==> sfilter\<cdot>f\<cdot>(x && xs) =
-                           If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs fi"
+                           If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs"
 by (subst sfilter_unfold, force)
 
 
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -160,7 +160,7 @@
 
 definition
   sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
-  "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s))"
+  "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
 
 translations
   "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
@@ -170,7 +170,7 @@
   "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
 
 lemma beta_sscase:
-  "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s)"
+  "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
 unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
 
 lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/Tr.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -67,18 +67,20 @@
 definition
   trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
   ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
+
 abbreviation
-  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
-  "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
+  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
+where
+  "If b then e1 else e2 == trifte\<cdot>e1\<cdot>e2\<cdot>b"
 
 translations
   "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
   "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
 
 lemma ifte_thms [simp]:
-  "If \<bottom> then e1 else e2 fi = \<bottom>"
-  "If FF then e1 else e2 fi = e2"
-  "If TT then e1 else e2 fi = e1"
+  "If \<bottom> then e1 else e2 = \<bottom>"
+  "If FF then e1 else e2 = e2"
+  "If TT then e1 else e2 = e1"
 by (simp_all add: ifte_def TT_def FF_def)
 
 
@@ -86,14 +88,14 @@
 
 definition
   trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
-  andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
+  andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
 abbreviation
   andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
   "x andalso y == trand\<cdot>x\<cdot>y"
 
 definition
   tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
-  orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
+  orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
 abbreviation
   orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
   "x orelse y == tror\<cdot>x\<cdot>y"
@@ -104,7 +106,7 @@
 
 definition
   If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
-  "If2 Q x y = (If Q then x else y fi)"
+  "If2 Q x y = (If Q then x else y)"
 
 text {* tactic for tr-thms with case split *}
 
@@ -182,7 +184,7 @@
 by (simp add: TT_def)
 
 lemma If_and_if:
-  "(If Def P then A else B fi) = (if P then A else B)"
+  "(If Def P then A else B) = (if P then A else B)"
 apply (rule_tac p = "Def P" in trE)
 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
 done
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/ex/Hoare.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -30,11 +30,11 @@
 
 definition
   p :: "'a -> 'a" where
-  "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)"
+  "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)"
 
 definition
   q :: "'a -> 'a" where
-  "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"
+  "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)"
 
 
 (* --------- pure HOLCF logic, some little lemmas ------ *)
@@ -102,13 +102,13 @@
 
 (* ----- access to definitions ----- *)
 
-lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
+lemma p_def3: "p$x = If b1$x then p$(g$x) else x"
 apply (rule trans)
 apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
 apply simp
 done
 
-lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
+lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x"
 apply (rule trans)
 apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
 apply simp
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/ex/Loop.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -10,23 +10,23 @@
 
 definition
   step  :: "('a -> tr)->('a -> 'a)->'a->'a" where
-  "step = (LAM b g x. If b$x then g$x else x fi)"
+  "step = (LAM b g x. If b$x then g$x else x)"
 
 definition
   while :: "('a -> tr)->('a -> 'a)->'a->'a" where
-  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
+  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))"
 
 (* ------------------------------------------------------------------------- *)
 (* access to definitions                                                     *)
 (* ------------------------------------------------------------------------- *)
 
 
-lemma step_def2: "step$b$g$x = If b$x then g$x else x fi"
+lemma step_def2: "step$b$g$x = If b$x then g$x else x"
 apply (unfold step_def)
 apply simp
 done
 
-lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"
+lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)"
 apply (unfold while_def)
 apply simp
 done
@@ -36,7 +36,7 @@
 (* rekursive properties of while                                             *)
 (* ------------------------------------------------------------------------- *)
 
-lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"
+lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x"
 apply (rule trans)
 apply (rule while_def2 [THEN fix_eq5])
 apply simp
diff -r d065b195ec89 -r 707eb30e8a53 src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -184,11 +184,11 @@
 
 definition
   TT_pat :: "(tr, unit) pat" where
-  "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail fi)"
+  "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail)"
 
 definition
   FF_pat :: "(tr, unit) pat" where
-  "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>() fi)"
+  "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>())"
 
 definition
   ONE_pat :: "(one, unit) pat" where