--- 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>"
--- 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)
))"
--- 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
--- 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)
--- 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>"
--- 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
--- 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
--- 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
--- 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